equivalence checking with Z3

Yes, it is possible. There are many ones to accomplish that using Z3. The simplest one uses the procedure prove in the Z3 Python API. For example, suppose we want to show that the formulas x >= 1 and x == 2*y and x - 2*y == 0, x >= 2 are equivalent. We can do that using the following Python program (you can try it online at rise4fun).

x, y = Ints('x y')
F = And(x >= 1, x == 2*y)
G = And(2*y - x == 0, x >= 2)
prove(F == G)

We can also show that two formulas are equivalent modulo some side-condition. For example, for bit-vectors (i.e., machine integers), x / 2 is equivalent to x >> 1 if x >= 0 (also available online).

x = BitVec('x', 32)
prove(Implies(x >= 0, x / 2 == x >> 1))

Note that, x / 2 is not equivalent to x >> 1. Z3 will produce a counterexample if we try to prove it.

x = BitVec('x', 32)
prove(x / 2 == x >> 1)
>> counterexample
>> [x = 4294967295]

The Z3 Python tutorial contains a more complicate example: it shows that x != 0 and x & (x - 1) == 0 is true if and only if x is a power of two.

In general, any satisfiability checker can be used to show that two formulas are equivalent. To show that two formulas F and G are equivalent using Z3, we show that F != G is unsatisfiable (i.e., there is no assignment/interpretation that will make F different from G). That is how the prove command is implemented in the Z3 Python API. Here is the script based on the Solver API:

s = Solver()
s.add(Not(F == G))
r = s.check()
if r == unsat:
    print("proved")
else:
    print("counterexample")
    print(s.model())

Recommended topics

Hot tags