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

pub enum Z3Solver<'a> {
    Solve(z3::Solver<'a>),
    Optimize(z3::Optimize<'a>),
}

impl<'a> Z3Solver<'a> {
    pub fn assert(&self, ast: &z3::ast::Bool<'a>) {
        match self {
            Z3Solver::Solve(solver) => solver.assert(ast),
            Z3Solver::Optimize(solver) => solver.assert(ast),
        }
    }

    pub fn set_threads(&self, ctx: &'a z3::Context, threads: u32) {
        match self {
            Z3Solver::Solve(solver) => {
                let mut params = z3::Params::new(ctx);
                params.set_u32("threads", threads);
                solver.set_params(&params);
            }
            Z3Solver::Optimize(_) => {}
        }
    }

    pub fn check(&self) -> z3::SatResult {
        match self {
            Z3Solver::Solve(solver) => solver.check(),
            Z3Solver::Optimize(solver) => solver.check(&[]),
        }
    }

    pub fn get_model(&self) -> Option<z3::Model> {
        match self {
            Z3Solver::Solve(solver) => solver.get_model(),
            Z3Solver::Optimize(solver) => solver.get_model(),
        }
    }

    pub fn minimize_int(&self, expr: &z3::ast::Int) {
        match self {
            Z3Solver::Solve(_) => {}
            Z3Solver::Optimize(solver) => solver.minimize(expr),
        }
    }
    pub fn maximize_int(&self, expr: &z3::ast::Int) {
        match self {
            Z3Solver::Solve(_) => {}
            Z3Solver::Optimize(solver) => solver.maximize(expr),
        }
    }

    pub fn minimize_real(&self, expr: &z3::ast::Real) {
        match self {
            Z3Solver::Solve(_) => {}
            Z3Solver::Optimize(solver) => solver.minimize(expr),
        }
    }
    pub fn maximize_real(&self, expr: &z3::ast::Real) {
        match self {
            Z3Solver::Solve(_) => {}
            Z3Solver::Optimize(solver) => solver.maximize(expr),
        }
    }
}

impl<'a> std::fmt::Display for Z3Solver<'a> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Z3Solver::Solve(solver) => write!(f, "{}", solver),
            Z3Solver::Optimize(solver) => write!(f, "{}", solver),
        }
    }
}