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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138

pub mod error;
pub mod parser;
pub mod problem;
pub mod solution;
pub mod solve;

pub mod combine;
pub use combine::*;

#[macro_use]
extern crate lalrpop_util;

pub fn ok_entry<S: Into<String>>(title: S) -> d_stuff::Entry {
    let title = d_stuff::Text::new(
        title,
        termion::style::Bold.to_string(),
        termion::color::Blue.fg_str(),
    );
    let message = d_stuff::Text::new(
        "OK",
        termion::style::Reset.to_string(),
        termion::color::Green.fg_str(),
    );
    d_stuff::Entry::new(d_stuff::Status::Success, title, Some(message), vec![])
}

pub fn load_file(
    pretty: &mut d_stuff::Pretty,
    problem: &mut problem::Problem,
    filename: &str,
    verbose: u8,
) -> Result<(), error::Error> {
    // Parsing
    match parser::parse_file(problem, filename) {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Parse    "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Resolve Type
    match problem.resolve_type() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Resolve T"));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Check Cycle
    match problem.check_cycle() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Cycle    "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Duplicate
    match problem.duplicate() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Unicity  "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Check Interval
    match problem.check_interval() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Interval "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Check Bounded
    match problem.check_bounded() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Bounded  "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // ------------------------- Preprocess ? -------------------------

    // Check Empty
    match problem.check_empty() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Empty    "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }

    // resolve Expr
    match problem.resolve_expr() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Resolve E"));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Check Parameter Size
    match problem.check_parameter_size() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Parameter"));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }
    // Check Type
    match problem.check_type() {
        Ok(_) => {
            if verbose >= 2 {
                pretty.add(ok_entry("Type     "));
                pretty.print();
            }
        }
        Err(e) => return Err(e),
    }

    Ok(())
}