Search code examples
z3bitvector

how to eliminate bitvector arithmetic in Z3

I am trying to use the z3 to eliminate the expression

not ((not x) add y)

which equals to

x sub y

by this code:

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (= (bvnot (bvadd (bvnot x) y)) (bvsub x y)))
(check-sat)
(simplify (bvnot (bvadd (bvnot x) y)))

I want to get the result like:

sat
(bvsub x y)

However, the result is:

sat
(bvnot (bvadd (bvnot x) y))

Would some one help me out?

Solution

  • We can prove that (bvnot (bvadd (bvnot x) y)) is equivalent to (bvsub x y) using the following script. 

    (declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))))
(check-sat)

    In this script, we used Z3 to show that (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))) is unsatisfiable. That is, it is not possible to find values for x and y such that the value of (bvnot (bvadd (bvnot x) y)) is different from the value of (bvsub x y).

    In Z3, the simplify command just applies rewriting rules, and it ignores the set of asserted expressions. The simplify command is much faster than checking satisfiability using check-sat. Moreover, given two equivalent expressions F and G, there is not guarantee that the result of (simplify F) will be equal to (simplify G). For example, in Z3 v4.3.1, the simplify command produces different results for (= (bvnot (bvadd (bvnot x) y) and (bvsub x y), although they are equivalent expressions. On the other hand, it produces the same result for (= (bvneg (bvadd (bvneg x) y) and (bvsub x y).

    (simplify (bvnot (bvadd (bvnot x) y)))
(simplify (bvneg (bvadd (bvneg x) y)))
(simplify (bvsub x y))

    Here is the full script for the examples above.

    BTW, these examples are much more readable if we use the Z3 Python interface. 

    x, y = BitVecs('x y', 32)
prove(~(~x + y) == x - y)
print simplify(x - y)
print simplify(~(~x + y))
print simplify(-(-x + y))

    Finally, Z3 has more complex simplification procedures. They are available as Tactics. The tutorials in Python and SMT 2.0 format provide additional information.

    Another possibility is to modify the Z3 simplier/rewriter. As you pointed out, not x is equivalent to -x -1. We can easily add this rewrite rule: not x --> -x - 1 to the Z3 rewriter. As an example, in this commit, I added a new option called "bvnot2arith" that enables this rule. The actual implementation is very small (5 lines of code).