BitVectors

BitVectors represent arrays of binary values. Because they model how data is represented in a computer, they can be used to prove properties of computer systems.

These two mini-examples are taken from Microsoft's Z3 documentation.

First, we want to prove the statement "a bitvector x is a power of two or zero if and only if x & (x - 1) is zero", where & represents bitwise and.

This is useful because it provides a fast way to check that fixed size numbers are powers of two. We'll check the property for 8 bits.

using Satisfiability

println("Example 1 (should be SAT)")
@satvariable(b, BitVector, 8)
is_power_of_two = b & (b - 0x01) == 0

# iff is_power_of_two holds, b must be one of 1, 2, 4, ... 128
expr = iff(is_power_of_two,
           or([b == 2^i for i=0:7]))
status = sat!(expr)
println(status) # if status is SAT we proved it.

Next, we can prove a bitwise version of de Morgan's law. We want to show there is NO possible value of x and y such that de Morgan's bitwise law doesn't hold.

println("Example 2 (should be UNSAT)")
@satvariable(x, BitVector, 64)
@satvariable(y, BitVector, 64)

expr = not((~x & ~y) == ~(x | y))

status = sat!(expr, solver=Z3())
println(status) # if status is UNSAT we proved it.