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

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

//-------------------------------------------------- Call Value --------------------------------------------------

pub struct CallValue {
    parameters: Vec<Value>,
    value: Value,
}

impl CallValue {
    pub fn new(smt: &Smt, model: &z3::Model, parameters: Vec<Expr>, value: &Expr) -> Self {
        let parameters = parameters
            .iter()
            .map(|p| Value::new(smt, model, p))
            .collect();
        let value = Value::new(smt, model, value);
        Self { parameters, value }
    }
}

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

impl ToLang for CallValue {
    fn to_lang(&self, problem: &Problem) -> String {
        let mut s = "    (".to_string();
        if let Some((first, others)) = self.parameters.split_first() {
            s.push_str(&format!("{}", first.to_lang(problem)));
            for p in others.iter() {
                s.push_str(&format!(", {}", p.to_lang(problem)));
            }
        }
        s.push_str(&format!(") -> {}", self.value.to_lang(problem)));
        s
    }
}