smt_lang/solution/
function.rs

1use super::*;
2use crate::combine::Combine;
3use crate::problem::*;
4use crate::solve::Smt;
5
6//-------------------------------------------------- Function --------------------------------------------------
7
8pub struct FunctionValue {
9    calls: Vec<CallValue>,
10}
11
12impl FunctionValue {
13    pub fn new(smt: &Smt, model: &z3::Model, function: &Function) -> Self {
14        //
15        let fun = smt.function(function.id());
16        let i = z3::ast::Int::fresh_const(smt.ctx(), "i");
17        let j = z3::ast::Int::fresh_const(smt.ctx(), "j");
18        let app = fun.apply(&[&i, &j]);
19        let e = model.eval(&app, false).unwrap();
20        println!("{:?}", e);
21        //
22        let i = z3::ast::Int::from_i64(smt.ctx(), 1);
23        let app = fun.apply(&[&i, &j]);
24        let e = model.eval(&app, false).unwrap();
25        println!("{:?}", e);
26        //
27        let mut calls = Vec::new();
28        //
29        let params_all = function
30            .parameters()
31            .iter()
32            .map(|p| p.typ().all(smt.problem()))
33            .collect();
34        let mut combine = Combine::new(params_all);
35        //
36        loop {
37            let values = combine.values();
38            let call = Expr::FunctionCall(function.id(), values.clone(), None);
39            //
40            let value = CallValue::new(smt, model, values, &call);
41            calls.push(value);
42            //
43            if !combine.step() {
44                break;
45            }
46        }
47
48        Self { calls }
49    }
50}
51
52//------------------------- To Lang -------------------------
53
54impl ToLang for FunctionValue {
55    fn to_lang(&self, problem: &Problem) -> String {
56        let mut s = "{\n".to_string();
57        for v in self.calls.iter() {
58            s.push_str(&format!("{}\n", v.to_lang(problem)));
59        }
60        s.push_str("}");
61        s
62    }
63}
smt_lang/solution/function.rs

smt_lang/solution/
function.rs
