smt_lang/solution/
solution.rs

1use super::Value;
2use super::*;
3use crate::problem::*;
4use crate::solve::Smt;
5use std::collections::HashMap;
6
7pub struct Solution {
8    // Structure
9    structures: HashMap<StructureId, StructureValue>,
10    // Structure
11    classes: HashMap<ClassId, ClassValue>,
12    // Variable
13    variables: HashMap<VariableId, Value>,
14    // Function
15    functions: HashMap<FunctionId, FunctionValue>,
16    // Objective
17    objective: Option<Value>,
18}
19
20impl Solution {
21    pub fn new(smt: &Smt, model: &z3::Model) -> Self {
22        // Structures
23        let mut structures = HashMap::new();
24        for structure in smt.problem().structures().iter() {
25            if !structure.attributes().is_empty() || !structure.methods().is_empty() {
26                let value = StructureValue::new(smt, model, structure.id());
27                structures.insert(structure.id(), value);
28            }
29        }
30        // Classes
31        let mut classes = HashMap::new();
32        for class in smt.problem().classes().iter() {
33            if !class.all_attributes(smt.problem()).is_empty()
34                || !class.all_methods(smt.problem()).is_empty()
35            {
36                let value = ClassValue::new(smt, model, class.id());
37                classes.insert(class.id(), value);
38            }
39        }
40        // Variables
41        let mut variables = HashMap::new();
42        for variable in smt.problem().variables().iter() {
43            let value = Value::new(smt, model, &Expr::Variable(variable.id(), None));
44            variables.insert(variable.id(), value);
45        }
46        // Functions
47        let mut functions = HashMap::new();
48        for function in smt.problem().functions().iter() {
49            let value = FunctionValue::new(smt, model, function);
50            functions.insert(function.id(), value);
51        }
52        // Objective
53        let objective = match smt.problem().search() {
54            Search::Solve => None,
55            Search::Optimize(e, _, _) => {
56                let value = Value::new(smt, model, e);
57                Some(value)
58            }
59        };
60        //
61        Self {
62            structures,
63            classes,
64            variables,
65            functions,
66            objective,
67        }
68    }
69}
70
71//------------------------- To Lang -------------------------
72
73impl ToLang for Solution {
74    fn to_lang(&self, problem: &Problem) -> String {
75        let mut s = "".to_string();
76        // Structures
77        for structure in self.structures.values() {
78            s.push_str(&structure.to_lang(problem));
79        }
80        // Classes
81        for class in self.classes.values() {
82            s.push_str(&class.to_lang(problem));
83        }
84        // Variables
85        for variable in problem.variables().iter() {
86            let mut v = variable.clone();
87            v.set_expr(None);
88            let value = self.variables.get(&v.id()).unwrap();
89            s.push_str(&format!(
90                "{} = {}\n",
91                v.to_lang(problem),
92                value.to_lang(problem)
93            ));
94        }
95        // Functions
96        for function in problem.functions().iter() {
97            let mut f = function.clone();
98            f.set_expr(None);
99            let value = self.functions.get(&f.id()).unwrap();
100            s.push_str(&format!(
101                "{} = {}\n",
102                f.to_lang(problem),
103                value.to_lang(problem)
104            ));
105        }
106        // Objective
107        if let Some(value) = &self.objective {
108            s.push_str(&format!("objective = {}\n", value.to_lang(problem)))
109        }
110        //
111        s
112    }
113}
smt_lang/solution/solution.rs

smt_lang/solution/
solution.rs
