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

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

//-------------------------------------------------- Function --------------------------------------------------

pub struct FunctionValue {
    calls: Vec<CallValue>,
}

impl FunctionValue {
    pub fn new(smt: &Smt, model: &z3::Model, function: &Function) -> Self {
        //
        let fun = smt.function(function.id());
        let i = z3::ast::Int::fresh_const(smt.ctx(), "i");
        let j = z3::ast::Int::fresh_const(smt.ctx(), "j");
        let app = fun.apply(&[&i, &j]);
        let e = model.eval(&app, false).unwrap();
        println!("{:?}", e);
        //
        let i = z3::ast::Int::from_i64(smt.ctx(), 1);
        let app = fun.apply(&[&i, &j]);
        let e = model.eval(&app, false).unwrap();
        println!("{:?}", e);
        //
        let mut calls = Vec::new();
        //
        let params_all = function
            .parameters()
            .iter()
            .map(|p| p.typ().all(smt.problem()))
            .collect();
        let mut combine = Combine::new(params_all);
        //
        loop {
            let values = combine.values();
            let call = Expr::FunctionCall(function.id(), values.clone(), None);
            //
            let value = CallValue::new(smt, model, values, &call);
            calls.push(value);
            //
            if !combine.step() {
                break;
            }
        }

        Self { calls }
    }
}

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

impl ToLang for FunctionValue {
    fn to_lang(&self, problem: &Problem) -> String {
        let mut s = "{\n".to_string();
        for v in self.calls.iter() {
            s.push_str(&format!("{}\n", v.to_lang(problem)));
        }
        s.push_str("}");
        s
    }
}