smtlib 0.4.0

A high-level API for interacting with SMT solvers
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

use terms::StaticSorted;

use super::*;
use crate::terms::{forall, Sorted};

#[test]
fn int_math() {
    let st = Storage::new();
    let x = Int::new_const(&st, "x");
    let y = Int::new_const(&st, "hello");
    // let x_named = x.labeled();
    let mut z = 12 + y * 4;
    z += 3;
    let w = x * x + z;
    println!("{w}");
}

#[test]
fn quantifiers() {
    let st = Storage::new();
    let x = Int::new_const(&st, "x");
    let y = Int::new_const(&st, "y");

    let res = forall(&st, (x, y), (x + 2)._eq(y));
    println!("{}", res.sterm());
}

#[test]
fn negative_numbers() {
    let st = Storage::new();
    let mut solver =
        Solver::new(&st, crate::backend::z3_binary::Z3Binary::new("z3").unwrap()).unwrap();
    let x = Int::new_const(&st, "x");
    solver.assert(x.lt(-1)).unwrap();
    let model = solver.check_sat_with_model().unwrap().expect_sat().unwrap();
    match model.eval(x) {
        Some(x) => println!("This is the value of x: {x}"),
        None => panic!("Oh no! This should never happen, as x was part of an assert"),
    }
}

#[test]
fn big_numbers() {
    let st = Storage::new();
    let mut solver =
        Solver::new(&st, crate::backend::z3_binary::Z3Binary::new("z3").unwrap()).unwrap();
    let x = Int::new_const(&st, "x");

    macro_rules! check {
        ($t:ty) => {
            solver
                .scope(|solver| {
                    solver.assert(x._eq(<$t>::MIN)).unwrap();
                    let model = solver.check_sat_with_model().unwrap().expect_sat().unwrap();
                    assert_eq!(<$t>::try_from(model.eval(x).unwrap()), Ok(<$t>::MIN));
                    Ok(())
                })
                .unwrap();
            solver
                .scope(|solver| {
                    solver.assert(x._eq(<$t>::MAX)).unwrap();
                    let model = solver.check_sat_with_model().unwrap().expect_sat().unwrap();
                    assert_eq!(<$t>::try_from(model.eval(x).unwrap()), Ok(<$t>::MAX));
                    Ok(())
                })
                .unwrap();
        };
    }
    check!(i8);
    check!(i16);
    check!(i32);
    check!(i64);
    check!(i128);
    check!(isize);
    check!(u8);
    check!(u16);
    check!(u32);
    check!(u64);
    check!(u128);
    check!(usize);
}

#[test]
fn check_sat_assuming() {
    let st = Storage::new();
    let mut solver =
        Solver::new(&st, crate::backend::z3_binary::Z3Binary::new("z3").unwrap()).unwrap();

    let x = Int::new_const(&st, "x");
    let prop_1 = Bool::new_const(&st, "prop_1");
    let prop_2 = Bool::new_const(&st, "prop_2");
    solver.assert(prop_1.implies(x._eq(42))).unwrap();
    solver.assert(prop_2.implies(x._neq(42))).unwrap();
    solver.assert(*prop_1).unwrap();

    assert_eq!(solver.check_sat().unwrap(), SatResult::Sat);
    assert_eq!(
        solver.check_sat_assuming(&[(prop_2, true)]).unwrap(),
        SatResult::Unsat
    );
    assert_eq!(solver.check_sat().unwrap(), SatResult::Sat);
    assert_eq!(
        solver.check_sat_assuming(&[(prop_2, false)]).unwrap(),
        SatResult::Sat
    );
}

#[test]
fn check_maximize() {
    let st = Storage::new();
    let mut solver =
        Solver::new(&st, crate::backend::z3_binary::Z3Binary::new("z3").unwrap()).unwrap();

    let x = Int::new_const(&st, "x");
    let b = Bool::new_const(&st, "b");
    solver.assert(x.le(100)).unwrap();
    solver.assert(b.implies(x._eq(42))).unwrap();
    solver.maximize(x).unwrap();

    let sat_res = solver.check_sat_with_model().unwrap();
    let model = sat_res.expect_sat().unwrap();
    assert_eq!(model.eval(x).unwrap().to_string(), "100".to_string());
    assert_eq!(model.eval(b).unwrap().to_string(), "false".to_string());
}