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

use crate::problem::{Expr, GetFromId, InstanceId, Named, ToLang};
use crate::solve::Smt;
use fraction::Fraction;

pub enum Value {
    Instance(InstanceId),
    Bool(bool),
    Integer(isize),
    Real(Fraction),
}

impl Value {
    pub fn new(smt: &Smt, model: &z3::Model, expr: &Expr) -> Self {
        let t = &expr.typ(smt.problem());
        let expr = &expr.type_inference(smt.problem());
        if t.is_bool() {
            // TODO
            // let e = smt.to_bool(expr);
            // let x = model.eval(&e, false).unwrap();
            // println!(
            //     "{}: {:?} = {:?} {}",
            //     expr.to_lang(smt.problem()),
            //     e,
            //     x,
            //     x == e
            // );
            let value = model
                .eval(&smt.to_bool(expr), true)
                .unwrap()
                .as_bool()
                .unwrap();
            Value::Bool(value)
        } else if t.is_integer() {
            let value = model
                .eval(&smt.to_int(expr), true)
                .unwrap()
                .as_i64()
                .unwrap();

            Value::Integer(value as isize)
        } else if t.is_real() {
            let (num, den) = model
                .eval(&smt.to_real(expr), true)
                .unwrap()
                .as_real()
                .unwrap();
            let value = if num >= 0 {
                Fraction::new_generic(fraction::Sign::Plus, num, den).unwrap()
            } else {
                Fraction::new_generic(fraction::Sign::Minus, -num, den).unwrap()
            };
            Value::Real(value)
        } else if t.is_structure() {
            let value = model
                .eval(&smt.to_datatype(expr), true)
                .unwrap()
                .to_string();
            let instance = smt.problem().find_instance(&value).unwrap();
            Value::Instance(instance.id())
        } else if t.is_class() {
            let value = model
                .eval(&smt.to_datatype(expr), true)
                .unwrap()
                .to_string();
            let value = value.split(' ').last().unwrap().replace(")", "");
            let instance = smt.problem().find_instance(&value).unwrap();
            Value::Instance(instance.id())
        } else {
            panic!()
        }
    }
}

//------------------------- To Lang -------------------------

impl ToLang for Value {
    fn to_lang(&self, problem: &crate::problem::Problem) -> String {
        match self {
            Value::Instance(id) => problem.get(*id).unwrap().name().to_string(),
            Value::Bool(value) => value.to_string(),
            Value::Integer(value) => value.to_string(),
            Value::Real(value) => value.to_string(),
        }
    }
}