To see how symbolic execution can be used to prove theorems, let's return to the bit-counting example, where our goal was to prove

(implies (unsigned-byte-p 32 x) (equal (fast-logcount-32 x) (logcount x)))

The basic idea is to first symbolically execute the above formula, and then
check whether it can ever evaluate to

We want our symbolic execution to cover all the cases necessary for proving
the theorem, namely all

Many symbolic objects cover this range. As notation, let

Xinit = (:g-integer b0 b1 ... b31 b32).

Why does this have 33 variables? The final bit,

Xbest = (:g-integer b0 b1 ... b31 false).

since it covers exactly the desired range using the simplest possible Boolean expressions.

Suppose we choose

What does this involve? First,

Next, the

Finally, we symbolically execute equal on these two results. This compares the Boolean expressions for their bits to determine if they are equivalent, and produces a symbolic object representing the answer.

So far we have basically ignored the differences between using ubdds or aigs as our Boolean expression representation. But here, the two approaches produce very different answers:

- Since UBDDs are canonical, the expressions for the bits of the two numbers
are syntactically equal, and the result from equal is simply
t . - With AIGs, the expressions for the bits are semantically equivalent but not
syntactically equal. The result is therefore
(:g-boolean . phi) , wherephi is a large Boolean expression in the variablesb0, ..., b31 . The fact thatphi always evaluates tot is not obvious just from its syntax.

At this point we have completed the symbolic execution of our goal formula,
obtaining either

GL automates this proof strategy, taking care of many of the details
relating to creating symbolic objects, ensuring that they cover all the
possible cases, and ensuring that