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
91
92
93
94
95
96
97
98

use super::*;

//------------------------- Entry Type -------------------------

#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum EntryType {
    Instance(InstanceId),
    Variable(VariableId),
    //
    Parameter(Parameter),
    //
    StrucSelf(StructureId),
    //
    ClassSelf(ClassId),
}

//------------------------- Entry -------------------------

#[derive(Clone, Debug)]
pub struct Entry {
    name: String,
    typ: EntryType,
}

impl Entry {
    pub fn new(name: String, typ: EntryType) -> Self {
        Self { name, typ }
    }

    pub fn new_parameter(parameter: &Parameter) -> Self {
        let name = parameter.name().to_string();
        let typ = EntryType::Parameter(parameter.clone());
        Self { name, typ }
    }

    pub fn name(&self) -> &str {
        &self.name
    }

    pub fn typ(&self) -> &EntryType {
        &self.typ
    }
}

impl FromId<InstanceId> for Entry {
    fn from_id(problem: &Problem, id: InstanceId) -> Self {
        let name = problem.get(id).unwrap().name().into();
        let typ = EntryType::Instance(id);
        Self { name, typ }
    }
}
impl FromId<VariableId> for Entry {
    fn from_id(problem: &Problem, id: VariableId) -> Self {
        let name = problem.get(id).unwrap().name().into();
        let typ = EntryType::Variable(id);
        Self { name, typ }
    }
}

//------------------------- Entries -------------------------

#[derive(Clone, Debug)]
pub struct Entries(Vec<Entry>);

impl Entries {
    pub fn new(entries: Vec<Entry>) -> Self {
        Entries(entries)
    }

    fn entries(&self) -> &Vec<Entry> {
        let Entries(entries) = self;
        entries
    }

    pub fn add(&self, entry: Entry) -> Entries {
        let mut v = self.entries().clone();
        v.push(entry);
        Entries(v)
    }

    pub fn add_all(&self, entries: Entries) -> Entries {
        let Entries(others) = entries;
        let mut v = self.entries().clone();
        for entry in others {
            v.push(entry);
        }
        Entries(v)
    }

    pub fn get(&self, name: &str) -> Option<Entry> {
        for e in self.entries().iter().rev() {
            if e.name() == name {
                return Some(e.clone());
            }
        }
        None
    }
}