smt_lang/solution/
structure.rs

1use super::*;
2use crate::problem::*;
3use crate::solve::Smt;
4
5//-------------------------------------------------- Instance Value --------------------------------------------------
6
7pub struct StrucInstanceValue {
8    id: InstanceId,
9    attributes: Vec<AttributeValue<StructureId>>,
10    methods: Vec<MethodValue<StructureId>>,
11}
12
13impl StrucInstanceValue {
14    pub fn new(smt: &Smt, model: &z3::Model, structure: StructureId, instance: InstanceId) -> Self {
15        let structure = smt.problem().get(structure).unwrap();
16        // Attributes
17        let mut attributes = Vec::new();
18        for attribute in structure.attributes().iter() {
19            let av = AttributeValue::new(smt, model, instance, attribute.id());
20            attributes.push(av);
21        }
22        // Methods
23        let mut methods = Vec::new();
24        for method in structure.methods().iter() {
25            let mv = MethodValue::new(smt, model, instance, method);
26            methods.push(mv);
27        }
28        //
29        Self {
30            id: instance,
31            attributes,
32            methods,
33        }
34    }
35}
36
37impl ToLang for StrucInstanceValue {
38    fn to_lang(&self, problem: &Problem) -> String {
39        let instance = problem.get(self.id).unwrap();
40        let mut s = format!("    inst {} {{\n", instance.name());
41        // Attribute
42        for attribute in self.attributes.iter() {
43            s.push_str(&format!("        {}\n", attribute.to_lang(problem)));
44        }
45        // Method
46        for method in self.methods.iter() {
47            s.push_str(&format!("    {}\n", method.to_lang(problem)));
48        }
49        //
50        s.push_str("    }\n");
51        s
52    }
53}
54
55//-------------------------------------------------- Structure Value --------------------------------------------------
56
57pub struct StructureValue {
58    id: StructureId,
59    instances: Vec<StrucInstanceValue>,
60}
61
62impl StructureValue {
63    pub fn new(smt: &Smt, model: &z3::Model, structure: StructureId) -> Self {
64        let mut instances = Vec::new();
65        for instance in smt
66            .problem()
67            .get(structure)
68            .unwrap()
69            .instances(smt.problem())
70        {
71            instances.push(StrucInstanceValue::new(smt, model, structure, instance));
72        }
73        Self {
74            id: structure,
75            instances,
76        }
77    }
78}
79
80impl ToLang for StructureValue {
81    fn to_lang(&self, problem: &Problem) -> String {
82        let structure = problem.get(self.id).unwrap();
83        let mut s = format!("struct {} {{\n", structure.name());
84        for instance in self.instances.iter() {
85            s.push_str(&instance.to_lang(problem));
86        }
87        s.push_str("}\n");
88        s
89    }
90}
smt_lang/solution/structure.rs

smt_lang/solution/
structure.rs
