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

use super::*;

//------------------------- TypeEntry Type -------------------------

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum TypeEntryType {
    Structure(StructureId),
    Class(ClassId),
}

//------------------------- TypeEntry -------------------------

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

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

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

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

impl FromId<StructureId> for TypeEntry {
    fn from_id(problem: &Problem, id: StructureId) -> Self {
        let name = problem.get(id).unwrap().name().into();
        let typ = TypeEntryType::Structure(id);
        Self { name, typ }
    }
}

impl FromId<ClassId> for TypeEntry {
    fn from_id(problem: &Problem, id: ClassId) -> Self {
        let name = problem.get(id).unwrap().name().into();
        let typ = TypeEntryType::Class(id);
        Self { name, typ }
    }
}

//------------------------- TypeEntries -------------------------

#[derive(Clone, Debug)]
pub struct TypeEntries(Vec<TypeEntry>);

impl TypeEntries {
    pub fn new(entries: Vec<TypeEntry>) -> Self {
        TypeEntries(entries)
    }

    fn entries(&self) -> &Vec<TypeEntry> {
        let TypeEntries(entries) = self;
        entries
    }

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

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