		Search-engine friendly clone of the ACL2 documentation.

Basic-tutorial

3. Computing with Symbolic Objects

Once we have a representation for symbolic objects, we can perform symbolic executions on those objects. For instance, recall the symbolic number p which can have value 1 or 5,

p = (:g-integer  true   false   A & B   false)

We might symbolically add 1 to p to obtain a new symbolic number, say q,

q = (:g-integer  false   true    A & B   false)

which represents either 2 or 6. Suppose r is another symbolic number,

r = (:g-integer  A   false   true   false)

which represents either 4 or 5. We might add q and r to obtain s,

s = (:g-integer  A    true    ~(A & B)    (A & B)    false)

whose value can be 6, 7, or 11.

Why can't s be 10 if q can be 6 and r can be 4? This combination isn't possible because q and r involve the same expression, A. The only way for r to be 4 is for A to be false, but then q must be 2.

The underlying algorithm GL uses for symbolic additions is just a ripple-carry addition on the Boolean expressions making up the bits of the two numbers. Performing a symbolic addition, then, means constructing new ubdds or aigs, depending on which mode is being used.

GL has built-in support for symbolically executing most ACL2 primitives. Generally, this is done by cases on the types of the symbolic objects being passed in as arguments. For instance, if we want to symbolically execute consp on s, then we are asking whether a :g-integer may ever represent a cons, so the answer is simply nil. Similarly, if we ever try to add a :g-boolean to a :g-integer, by the ACL2 axioms the :g-boolean is simply treated as 0.

Beyond these primitives, GL provides what is essentially a McCarthy-style interpreter for symbolically executing terms. By default, it expands function definitions until it reaches primitives, with some special handling for if. For better performance, its interpretation scheme can be customized with more efficient definitions and other optimizations.