easy-smt 0.3.2

Easily interact with an smt solver as a subprocess
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

// In this example, we assert quantified formulas over uninterpreted
// sorts and functions.

fn main() -> std::io::Result<()> {
    env_logger::init();
    let mut ctx = easy_smt::ContextBuilder::new().with_z3_defaults().build()?;

    // Declare an uninterpreted representation for sets.
    ctx.declare_sort("MySet", 0)?;
    // Declare representation for elements of those sets.
    ctx.declare_sort("MyElement", 0)?;

    // Our sets have a simple interface of predicates: empty(s),
    // member(x,s), and subset(s1,s2).
    ctx.declare_fun("empty", vec![ctx.atom("MySet")], ctx.bool_sort())?;
    ctx.declare_fun(
        "member",
        vec![ctx.atom("MyElement"), ctx.atom("MySet")],
        ctx.bool_sort(),
    )?;
    ctx.declare_fun(
        "subset",
        vec![ctx.atom("MySet"), ctx.atom("MySet")],
        ctx.bool_sort(),
    )?;

    // We assert some simple axioms on this interface.

    // First, a set s1 is either a subset of s2, or a member of s1
    // exists which is not a member of s2.
    ctx.assert(
        // For any pair of sets,
        ctx.forall(
            [("s1", ctx.atom("MySet")), ("s2", ctx.atom("MySet"))],
            // One of the following is true:
            ctx.or(
                // (1) s1 is a subset of s2, or
                ctx.list(vec![ctx.atom("subset"), ctx.atom("s1"), ctx.atom("s2")]),
                // (2) an element exists which is a member of s1, and
                // not a member of s2.
                ctx.exists(
                    [("x", ctx.atom("MyElement"))],
                    ctx.and(
                        ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s1")]),
                        ctx.not(ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s2")])),
                    ),
                ),
            ),
        ),
    )?;

    // Second, a set is empty iff no member exists.
    ctx.assert(
        // For any set,
        ctx.forall(
            [("s1", ctx.atom("MySet"))],
            // The following formulas are equivalent:
            ctx.eq(
                // (1) the set is not empty, and
                ctx.not(ctx.list(vec![ctx.atom("empty"), ctx.atom("s1")])),
                // (2) an element exists that is a member of the set.
                ctx.exists(
                    [("x", ctx.atom("MyElement"))],
                    ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s1")]),
                ),
            ),
        ),
    )?;

    // Now, let's check whether a relationship between two sets is
    // possible.
    ctx.declare_const("s1", ctx.atom("MySet"))?;
    ctx.declare_const("s2", ctx.atom("MySet"))?;

    // Is it possible for s1 to be empty,
    ctx.assert(ctx.list(vec![ctx.atom("empty"), ctx.atom("s1")]))?;
    // while also s1 is not a subset of s2?
    ctx.assert(ctx.not(ctx.list(vec![ctx.atom("subset"), ctx.atom("s1"), ctx.atom("s2")])))?;

    // We expect the answer to be no (UNSAT).
    match ctx.check()? {
        easy_smt::Response::Sat => {
            println!("Solver returned SAT. This is unexpected!");
        }
        easy_smt::Response::Unsat => {
            println!("Solver returned UNSAT. This is expected.");
        }
        easy_smt::Response::Unknown => {
            println!("Solver returned UNKNOWN. This is unexpected!");
        }
    }
    Ok(())
}