notes on `z3` `c++` bindings

notes on z3 c++ bindings

resilience

gauss research lab

gauss@cs.utah.edu

1. z3

1.1. about

z3 is a theorem prover.
For examples, we can ask z3 to prove the following:
your conjecture:

(1)

z3-interface:

(declare-fun y () Bool)
(declare-fun x () Bool)
(assert (not (= (not (and x y)) (or (not x) (not y)))))
(check-sat)

z3-output:

If this theorem is satisfyable      : sat
If this theorem is not satisfyable  : unsat
If this proving process times out   : unknown

1.2. building

clone from github, and build using gnu make

Steps:

git clone https://github.com/Z3Prover/z3.git
python scripts/mk_make.py
cd build
make
sudo make install
make examples

1.3. bindings

z3 has bindings for various programming languages.
c++ bindings is what we currently are interested in.
these bindings generate code in smt2 format.

1.4. z3 `c++` interface cheat-sheet

class expr

  F.app()
  F.decl()
  F.simplify()
  F.arg()

class expr_vector
```
   ev.size()
```

class context

  context c
  c.bool_const("x")
  c.int_constant("x")
  c.int_sort("x")
  c.real_const("x")
  c.real_val("-1/3")
  c.bv_const("x",32)
  c.int_sort()

class solver

  solver s(c)
  s.add()
  s.set(p)
  s.check()
  s.get_model()
  s.unsat_core()

class param
```
param p(c)
p.set("mul2concat", true)
```
class tactic
```
tactic t
```

misc Functions:

  function()
  implies()
  prove()
  distinct()

2. c++ examples

2.1. z3 hello world

Proove theorem with boolean variables:

(2)

create a solver
assert the negation of the conjecture
checks if the result is unsat.

    //~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    // STEP-0 init
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr conjecture = !(x && y) == (!x || !y);
    
    // STEP-1  create a solver
    solver s(c);
    
    // STEP-2 assert the negation of the conjecture
    s.add(!conjecture);
    
    std::cout << s << "\n";
    std::cout << s.to_smt2() << "\n";
     
    // STEP-3 checks if the result is unsat.
    switch (s.check()) {
    case unsat:   std::cout << "de-Morgan is valid\n"; break;
    case sat:     std::cout << "de-Morgan is not valid\n"; break;
    case unknown: std::cout << "unknown\n"; break;
    }
    
    //~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    
    Z3 OUTPUT:
    
    (declare-fun y () Bool)
    (declare-fun x () Bool)
    (assert (not (= (not (and x y)) (or (not x) (not y)))))
    (check-sat)
    de-Morgan is valid
    //~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Classes used:

context
expr
solver

2.2. Using `get_model()`

How to find values of expressions that satisfy the following:

(3)

(4)

    context c;
    expr x = c.int_const("x");
    expr y = c.int_const("y");
    solver s(c);

    s.add(x >= 1);
    s.add(y < x + 3);
    std::cout << s.check() << "\n";

    model m = s.get_model();
    std::cout << m << "\n";
    
    // traversing the model
    for (unsigned i = 0; i < m.size(); i++) {
        func_decl v = m[i];
        assert(v.arity() == 0);
         
        std::cout << v.name() << " = " << m.get_const_interp(v) << "\n";
    }
    
    // we can evaluate expressions in the model.
    std::cout << "x + y + 1 = " << m.eval(x + y + 1) << "\n";

OUTPUT:

sat
(define-fun x () Int  1)
(define-fun y () Int  3)
x = 1
y = 3
x + y + 1 = 5

2.3. Un-Interpreted Types and Functions

Prove that :

(5)

Disprove that

(6)

    context c;
    
    expr x      = c.int_const("x");
    expr y      = c.int_const("y");
    
    sort I      = c.int_sort();
    
    func_decl g = function("g", I, I);
    
    solver s(c);
    
    expr conjecture1 = implies(x == y, g(x) == g(y));
    
    std::cout << "conjecture 1\n" << conjecture1 << "\n";
    s.add(!conjecture1);
    
    if (s.check() == unsat) 
        std::cout << "proved" << "\n";
    else
        std::cout << "failed to prove" << "\n";

    s.reset(); // remove all assertions from solver s

    expr conjecture2 = implies(x == y, g(g(x)) == g(y));
    std::cout << "conjecture 2\n" << conjecture2 << "\n";
    s.add(!conjecture2);
    if (s.check() == unsat) {
        std::cout << "proved" << "\n";
    }
    else {
        std::cout << "failed to prove" << "\n";
        model m = s.get_model();
        std::cout << "counterexample:\n" << m << "\n";
        std::cout << "g(g(x)) = " << m.eval(g(g(x))) << "\n";
        std::cout << "g(y)    = " << m.eval(g(y)) << "\n";
    }
}

OUTPUT:
conjecture 1
 (=> (= x y) (= (g x) (g y)))
 proved

conjecture 2
 (=> (= x y) (= (g (g x)) (g y)))
 failed to prove

counterexample:
 (define-fun y () Int 0)
 (define-fun x () Int 0)
 (define-fun g ((x!1 Int)) Int
  (ite (= x!1 0) 1 (ite (= x!1 1) 2 1)))
  
 g(g(x)) = 2
 g(y)    = 1

2.4. Combine Un-Interpreted Functions and Airthmetic

Prove :

(7)

(8)

    context c;

    expr x      = c.int_const("x");
    expr y      = c.int_const("y");
    expr z      = c.int_const("z");
    sort I      = c.int_sort();

    func_decl g = function("g", I, I);
    
    expr conjecture1 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
                               z < 0);

    solver s(c);
    s.add(!conjecture1);
    std::cout << "conjecture 1:\n" << conjecture1 << "\n";
    if (s.check() == unsat) 
        std::cout << "proved" << "\n";
    else
        std::cout << "failed to prove" << "\n";

    expr conjecture2 = implies(g(g(x) - g(y)) != g(z) && x + z <= y && y <= x,
                               z < -1);
    s.reset();
    s.add(!conjecture2);
    std::cout << "conjecture 2:\n" << conjecture2 << "\n";
    if (s.check() == unsat) {
        std::cout << "proved" << "\n";
    }
    else {
        std::cout << "failed to prove" << "\n";
        std::cout << "counterexample:\n" << s.get_model() << "\n";
    }
}

OUTPUT:

conjecture 1:
(let ((a!1 (distinct (g (- (g x) (g y))) (g z)))) (=> (and a!1 (<= (+ x z) y) (<= y x)) (< z 0)))
proved

conjecture 2:
(let ((a!1 (distinct (g (- (g x) (g y))) (g z)))) (=> (and a!1 (<= (+ x z) y) (<= y x)) (< z (- 1))))
failed to prove
counterexample:
(define-fun z () Int (- 1))
(define-fun y () Int 0)
(define-fun x () Int 0)
(define-fun g ((x!1 Int)) Int (ite (= x!1 0) 0 (ite (= x!1 (- 1)) 1 0)))

2.5. Non linear arithmetic

    config cfg;
    cfg.set("auto_config", true);
    context c(cfg);

    expr x = c.real_const("x");
    expr y = c.real_const("y");
    expr z = c.real_const("z");
                     
    solver s(c);

    s.add(x*x + y*y == 1);                     // x^2 + y^2 == 1
    s.add(x*x*x + z*z*z < c.real_val("1/2"));  // x^3 + z^3 < 1/2
    s.add(z != 0);
    
    std::cout << s.check() << "\n";
    
    model m = s.get_model();
    
    std::cout << m << "\n";
    set_param("pp.decimal", true); // set decimal notation
    std::cout << "model in decimal notation\n";
    std::cout << m << "\n";
    set_param("pp.decimal-precision", 50); // increase number of decimal places to 50.
    std::cout << "model using 50 decimal places\n";
    std::cout << m << "\n";
    set_param("pp.decimal", false); // disable decimal notation
}

OUTPUT:

sat
(define-fun x () Real (/ 1.0 8.0))
(define-fun y () Real (root-obj (+ (* 64 (^ x 2)) (- 63)) 1))
(define-fun z () Real (/ 1.0 2.0))

model in decimal notation
(define-fun x () Real 0.125)
(define-fun y () Real (- 0.9921567416?))
(define-fun z () Real 0.5)

model using 50 decimal places
(define-fun x () Real 0.125)
(define-fun y () Real (- 0.99215674164922147143810590761472265964134719365591?))
(define-fun z () Real 0.5)

2.6. Another hello z3:

create a solver
assert the negation of the conjecture
checks if the result is unsat.

void prove(expr conjecture) {
    context & c = conjecture.ctx();
    solver s(c);
    s.add(!conjecture);
    std::cout << "conjecture:\n" << conjecture << "\n";
    if (s.check() == unsat) {
        std::cout << "proved" << "\n";
    }
    else {
        std::cout << "failed to prove" << "\n";
        std::cout << "counterexample:\n" << s.get_model() << "\n";
    }
}

2.7. Using bit-vectors

Simple bit-vector example.
This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers

void bitvector_example1() {
    std::cout << "bitvector example 1\n";
    context c;
    expr x = c.bv_const("x", 32);
    
    // using signed <=
    prove((x - 10 <= 0) == (x <= 10));

    // using unsigned <=
    prove(ule(x - 10, 0) == ule(x, 10));

    expr y = c.bv_const("y", 32);
    prove(implies(concat(x, y) == concat(y, x), x == y));
}

OUTPUT:
bitvector example 1

conjecture:
(= (bvsle (bvsub x #x0000000a) #x00000000) (bvsle x #x0000000a))
failed to prove
counterexample:
(define-fun x () (_ BitVec 32) #x80000000)

conjecture:
(= (bvule (bvsub x #x0000000a) #x00000000) (bvule x #x0000000a))
failed to prove
counterexample:
(define-fun x () (_ BitVec 32) #x00000000)

conjecture:
(=> (= (concat x y) (concat y x)) (= x y))
proved

2.8. Another get_model()

Find x and y such that: x ^ y - 103 == x * y

void bitvector_example2() {
    std::cout << "bitvector example 2\n";
    context c;
    expr x = c.bv_const("x", 32);
    expr y = c.bv_const("y", 32);
    solver s(c);
    // In C++, the operator == has higher precedence than ^.
    s.add((x ^ y) - 103 == x * y);
    std::cout << s << "\n";
    std::cout << s.check() << "\n";
    std::cout << s.get_model() << "\n";
}

2.9. Mixing C and C++ APIs.

void capi_example() {
    std::cout << "capi example\n";
    context c;
    expr x = c.bv_const("x", 32);
    expr y = c.bv_const("y", 32);
    // Invoking a C API function, and wrapping the result using an expr object.
    expr r = to_expr(c, Z3_mk_bvsrem(c, x, y));
    std::cout << "r: " << r << "\n";
}

2.10. How to evaluate expressions in a model.

void eval_example1() {
    std::cout << "eval example 1\n";
    context c;
    expr x = c.int_const("x");
    expr y = c.int_const("y");
    solver s(c);

    /* assert x < y */
    s.add(x < y);
    /* assert x > 2 */
    s.add(x > 2);
    
    std::cout << s.check() << "\n";
    
    model m = s.get_model();
    std::cout << "Model:\n" << m << "\n";
    std::cout << "x+y = " << m.eval(x+y) << "\n";
}

2.11. Several contexts can be used simultaneously.

void two_contexts_example1() {
    std::cout << "two contexts example 1\n";
    context c1, c2;
    
    expr x = c1.int_const("x");
    expr n = x + 1;
    // We cannot mix expressions from different contexts, but we can copy
    // an expression from one context to another.
    // The following statement copies the expression n from c1 to c2.
    expr n1 = to_expr(c2, Z3_translate(c1, n, c2));
    std::cout << n1 << "\n";
}

2.12. Dealing with Rational numbers

Demonstrate different ways of creating rational numbers: decimal and fractional representations.

void numeral_example() {
    std::cout << "numeral example\n";
    context c;
    
    expr n1 = c.real_val("1/2");
    expr n2 = c.real_val("0.5");
    expr n3 = c.real_val(1, 2);
    std::cout << n1 << " " << n2 << " " << n3 << "\n";
    prove(n1 == n2 && n1 == n3);
    
    n1 = c.real_val("-1/3");
    n2 = c.real_val("-0.3333333333333333333333333333333333");
    std::cout << n1 << " " << n2 << "\n";
    prove(n1 != n2);
}