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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

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

//-------------------------------------------------- Instance Value --------------------------------------------------

pub struct ClassInstanceValue {
    id: InstanceId,
    attributes: Vec<AttributeValue<ClassId>>,
    methods: Vec<MethodValue<ClassId>>,
}

impl ClassInstanceValue {
    pub fn new(smt: &Smt, model: &z3::Model, class: ClassId, instance: InstanceId) -> Self {
        let class = smt.problem().get(class).unwrap();
        // Attributes
        let mut attributes = Vec::new();
        for id in class.all_attributes(smt.problem()).iter() {
            let av = AttributeValue::new(smt, model, instance, *id);
            attributes.push(av);
        }
        // Methods
        let mut methods = Vec::new();
        for id in class.all_methods(smt.problem()).iter() {
            let method = smt.problem().get(*id).unwrap();
            let mv = MethodValue::new(smt, model, instance, method);
            methods.push(mv);
        }
        //
        Self {
            id: instance,
            attributes,
            methods,
        }
    }
}

impl ToLang for ClassInstanceValue {
    fn to_lang(&self, problem: &Problem) -> String {
        let instance = problem.get(self.id).unwrap();
        let mut s = format!("    inst {} {{\n", instance.name());
        // Attribute
        for attribute in self.attributes.iter() {
            s.push_str(&format!("        {}\n", attribute.to_lang(problem)));
        }
        // Method
        for method in self.methods.iter() {
            s.push_str(&format!("    {}\n", method.to_lang(problem)));
        }
        //
        s.push_str("    }\n");
        s
    }
}

//-------------------------------------------------- Class Value --------------------------------------------------

pub struct ClassValue {
    id: ClassId,
    instances: Vec<ClassInstanceValue>,
}

impl ClassValue {
    pub fn new(smt: &Smt, model: &z3::Model, class: ClassId) -> Self {
        let mut instances = Vec::new();
        for instance in smt.problem().get(class).unwrap().instances(smt.problem()) {
            instances.push(ClassInstanceValue::new(smt, model, class, instance));
        }
        Self {
            id: class,
            instances,
        }
    }
}

impl ToLang for ClassValue {
    fn to_lang(&self, problem: &Problem) -> String {
        let structure = problem.get(self.id).unwrap();
        let mut s = format!("class {} {{\n", structure.name());
        for instance in self.instances.iter() {
            s.push_str(&instance.to_lang(problem));
        }
        s.push_str("}\n");
        s
    }
}