smt_lang/solution/
method.rs

1use super::*;
2use crate::combine::Combine;
3use crate::problem::*;
4use crate::solve::Smt;
5
6//-------------------------------------------------- Method Value --------------------------------------------------
7
8pub struct MethodValue<T: Id> {
9    id: MethodId<T>,
10    calls: Vec<CallValue>,
11}
12
13pub trait NewMethod<T: Id> {
14    fn new(smt: &Smt, model: &z3::Model, instance: InstanceId, method: &Method<T>) -> Self;
15}
16
17impl NewMethod<StructureId> for MethodValue<StructureId> {
18    fn new(
19        smt: &Smt,
20        model: &z3::Model,
21        instance: InstanceId,
22        method: &Method<StructureId>,
23    ) -> Self {
24        let mut calls = Vec::new();
25        //
26        let params_all = method
27            .parameters()
28            .iter()
29            .map(|p| p.typ().all(smt.problem()))
30            .collect();
31        let mut combine = Combine::new(params_all);
32        //
33        loop {
34            let inst = Expr::Instance(instance, None);
35            let values = combine.values();
36            let call = Expr::StrucMetCall(Box::new(inst), method.id(), values.clone(), None);
37            //
38            let value = CallValue::new(smt, model, values, &call);
39            calls.push(value);
40            //
41            if !combine.step() {
42                break;
43            }
44        }
45
46        Self {
47            id: method.id(),
48            calls,
49        }
50    }
51}
52
53//------------------------- To Lang -------------------------
54
55impl ToLang for MethodValue<StructureId> {
56    fn to_lang(&self, problem: &Problem) -> String {
57        let mut meth = problem.get(self.id).unwrap().clone();
58        meth.set_expr(None);
59        let mut s = format!("{} {{\n", meth.to_lang(problem));
60        for v in self.calls.iter() {
61            s.push_str(&format!("        {}\n", v.to_lang(problem)));
62        }
63        s.push_str("        }");
64        s
65    }
66}
67
68impl NewMethod<ClassId> for MethodValue<ClassId> {
69    fn new(smt: &Smt, model: &z3::Model, instance: InstanceId, method: &Method<ClassId>) -> Self {
70        let mut calls = Vec::new();
71        //
72        let params_all = method
73            .parameters()
74            .iter()
75            .map(|p| p.typ().all(smt.problem()))
76            .collect();
77        let mut combine = Combine::new(params_all);
78        //
79        loop {
80            let inst = Expr::Instance(instance, None);
81            let values = combine.values();
82            let call = Expr::ClassMetCall(Box::new(inst), method.id(), values.clone(), None);
83            //
84            let value = CallValue::new(smt, model, values, &call);
85            calls.push(value);
86            //
87            if !combine.step() {
88                break;
89            }
90        }
91
92        Self {
93            id: method.id(),
94            calls,
95        }
96    }
97}
98
99//------------------------- To Lang -------------------------
100
101impl ToLang for MethodValue<ClassId> {
102    fn to_lang(&self, problem: &Problem) -> String {
103        let mut meth = problem.get(self.id).unwrap().clone();
104        meth.set_expr(None);
105        let mut s = format!("{} {{\n", meth.to_lang(problem));
106        for v in self.calls.iter() {
107            s.push_str(&format!("        {}\n", v.to_lang(problem)));
108        }
109        s.push_str("        }");
110        s
111    }
112}
smt_lang/solution/method.rs

smt_lang/solution/
method.rs
