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
87
88
89
90

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

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

pub struct StrucInstanceValue {
    id: InstanceId,
    attributes: Vec<AttributeValue<StructureId>>,
    methods: Vec<MethodValue<StructureId>>,
}

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

impl ToLang for StrucInstanceValue {
    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
    }
}

//-------------------------------------------------- Structure Value --------------------------------------------------

pub struct StructureValue {
    id: StructureId,
    instances: Vec<StrucInstanceValue>,
}

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

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