smt_lang/solution/
class.rs

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

smt_lang/solution/
class.rs
