smt_lang/solution/
value.rs

1use crate::problem::{Expr, GetFromId, InstanceId, Named, ToLang};
2use crate::solve::Smt;
3use fraction::Fraction;
4
5pub enum Value {
6    Instance(InstanceId),
7    Bool(bool),
8    Integer(isize),
9    Real(Fraction),
10}
11
12impl Value {
13    pub fn new(smt: &Smt, model: &z3::Model, expr: &Expr) -> Self {
14        let t = &expr.typ(smt.problem());
15        let expr = &expr.type_inference(smt.problem());
16        if t.is_bool() {
17            // TODO
18            // let e = smt.to_bool(expr);
19            // let x = model.eval(&e, false).unwrap();
20            // println!(
21            //     "{}: {:?} = {:?} {}",
22            //     expr.to_lang(smt.problem()),
23            //     e,
24            //     x,
25            //     x == e
26            // );
27            let value = model
28                .eval(&smt.to_bool(expr), true)
29                .unwrap()
30                .as_bool()
31                .unwrap();
32            Value::Bool(value)
33        } else if t.is_integer() {
34            let value = model
35                .eval(&smt.to_int(expr), true)
36                .unwrap()
37                .as_i64()
38                .unwrap();
39
40            Value::Integer(value as isize)
41        } else if t.is_real() {
42            let (num, den) = model
43                .eval(&smt.to_real(expr), true)
44                .unwrap()
45                .as_real()
46                .unwrap();
47            let value = if num >= 0 {
48                Fraction::new_generic(fraction::Sign::Plus, num, den).unwrap()
49            } else {
50                Fraction::new_generic(fraction::Sign::Minus, -num, den).unwrap()
51            };
52            Value::Real(value)
53        } else if t.is_structure() {
54            let value = model
55                .eval(&smt.to_datatype(expr), true)
56                .unwrap()
57                .to_string();
58            let instance = smt.problem().find_instance(&value).unwrap();
59            Value::Instance(instance.id())
60        } else if t.is_class() {
61            let value = model
62                .eval(&smt.to_datatype(expr), true)
63                .unwrap()
64                .to_string();
65            let value = value.split(' ').last().unwrap().replace(")", "");
66            let instance = smt.problem().find_instance(&value).unwrap();
67            Value::Instance(instance.id())
68        } else {
69            panic!()
70        }
71    }
72}
73
74//------------------------- To Lang -------------------------
75
76impl ToLang for Value {
77    fn to_lang(&self, problem: &crate::problem::Problem) -> String {
78        match self {
79            Value::Instance(id) => problem.get(*id).unwrap().name().to_string(),
80            Value::Bool(value) => value.to_string(),
81            Value::Integer(value) => value.to_string(),
82            Value::Real(value) => value.to_string(),
83        }
84    }
85}
smt_lang/solution/value.rs

smt_lang/solution/
value.rs
