smt-lang 0.7.5

Sat Modulo Theory Language
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

use super::*;
use crate::combine::Combine;
use crate::problem::*;
use crate::solve::Smt;

//-------------------------------------------------- Method Value --------------------------------------------------

pub struct MethodValue<T: Id> {
    id: MethodId<T>,
    calls: Vec<CallValue>,
}

pub trait NewMethod<T: Id> {
    fn new(smt: &Smt, model: &z3::Model, instance: InstanceId, method: &Method<T>) -> Self;
}

impl NewMethod<StructureId> for MethodValue<StructureId> {
    fn new(
        smt: &Smt,
        model: &z3::Model,
        instance: InstanceId,
        method: &Method<StructureId>,
    ) -> Self {
        let mut calls = Vec::new();
        //
        let params_all = method
            .parameters()
            .iter()
            .map(|p| p.typ().all(smt.problem()))
            .collect();
        let mut combine = Combine::new(params_all);
        //
        loop {
            let inst = Expr::Instance(instance, None);
            let values = combine.values();
            let call = Expr::StrucMetCall(Box::new(inst), method.id(), values.clone(), None);
            //
            let value = CallValue::new(smt, model, values, &call);
            calls.push(value);
            //
            if !combine.step() {
                break;
            }
        }

        Self {
            id: method.id(),
            calls,
        }
    }
}

//------------------------- To Lang -------------------------

impl ToLang for MethodValue<StructureId> {
    fn to_lang(&self, problem: &Problem) -> String {
        let mut meth = problem.get(self.id).unwrap().clone();
        meth.set_expr(None);
        let mut s = format!("{} {{\n", meth.to_lang(problem));
        for v in self.calls.iter() {
            s.push_str(&format!("        {}\n", v.to_lang(problem)));
        }
        s.push_str("        }");
        s
    }
}

impl NewMethod<ClassId> for MethodValue<ClassId> {
    fn new(smt: &Smt, model: &z3::Model, instance: InstanceId, method: &Method<ClassId>) -> Self {
        let mut calls = Vec::new();
        //
        let params_all = method
            .parameters()
            .iter()
            .map(|p| p.typ().all(smt.problem()))
            .collect();
        let mut combine = Combine::new(params_all);
        //
        loop {
            let inst = Expr::Instance(instance, None);
            let values = combine.values();
            let call = Expr::ClassMetCall(Box::new(inst), method.id(), values.clone(), None);
            //
            let value = CallValue::new(smt, model, values, &call);
            calls.push(value);
            //
            if !combine.step() {
                break;
            }
        }

        Self {
            id: method.id(),
            calls,
        }
    }
}

//------------------------- To Lang -------------------------

impl ToLang for MethodValue<ClassId> {
    fn to_lang(&self, problem: &Problem) -> String {
        let mut meth = problem.get(self.id).unwrap().clone();
        meth.set_expr(None);
        let mut s = format!("{} {{\n", meth.to_lang(problem));
        for v in self.calls.iter() {
            s.push_str(&format!("        {}\n", v.to_lang(problem)));
        }
        s.push_str("        }");
        s
    }
}