smt_lang/solution/
call.rs

1use super::*;
2use crate::problem::*;
3use crate::solve::Smt;
4
5//-------------------------------------------------- Call Value --------------------------------------------------
6
7pub struct CallValue {
8    parameters: Vec<Value>,
9    value: Value,
10}
11
12impl CallValue {
13    pub fn new(smt: &Smt, model: &z3::Model, parameters: Vec<Expr>, value: &Expr) -> Self {
14        let parameters = parameters
15            .iter()
16            .map(|p| Value::new(smt, model, p))
17            .collect();
18        let value = Value::new(smt, model, value);
19        Self { parameters, value }
20    }
21}
22
23//------------------------- To Lang -------------------------
24
25impl ToLang for CallValue {
26    fn to_lang(&self, problem: &Problem) -> String {
27        let mut s = "    (".to_string();
28        if let Some((first, others)) = self.parameters.split_first() {
29            s.push_str(&format!("{}", first.to_lang(problem)));
30            for p in others.iter() {
31                s.push_str(&format!(", {}", p.to_lang(problem)));
32            }
33        }
34        s.push_str(&format!(") -> {}", self.value.to_lang(problem)));
35        s
36    }
37}
smt_lang/solution/call.rs

smt_lang/solution/
call.rs
