		Search-engine friendly clone of the ACL2 documentation.

Basic-tutorial

2. Symbolic Objects

At its heart, GL works by manipulating Boolean expressions. There are many ways to represent Boolean expressions. GL currently supports a hons-based BDD package and also has support for using a hons-based aig representation.

For any particular proof, you can choose which representation to use by picking one of the available proof modes. Each representation has strengths and weaknesses, and the choice of representation can significantly impact performance. We give some advice about choosing these modes in modes.

The GL user does not need to know how BDDs and AIGs are represented; in this documentation we will just adopt a conventional syntax to describe Boolean expressions, e.g., true, false, A & B, ~C, etc.

GL groups Boolean expressions into symbolic objects. Much like a Boolean expression can be evaluated to obtain a Boolean value, a symbolic object can be evaluated to produce an ACL2 object. There are several kinds of symbolic objects, but numbers are a good start. GL represents symbolic, signed integers as

(:g-integer . <lsb-bits>)

Where lsb-bits is a list of Boolean expressions that represent the two's complement bits of the number. The bits are in lsb-first order, and the last, most significant bit is the sign bit. For instance, if p is the following :g-integer,

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

Then p represents a 4-bit, signed integer whose value is either 1 or 5, depending on the value of A & B.

GL uses another kind of symbolic object to represent ACL2 Booleans. In particular,

(:g-boolean . <val>)

represents t or nil, depending on the Boolean expression <val>. For example,

(:g-boolean . ~(A & B))

is a symbolic object whose value is t when p has value 1, and nil when p has value 5.

GL has a few other kinds of symbolic objects that are also tagged with keywords, such as :g-var and :g-apply. But an ACL2 object that does not have any of these special keywords within it is also considered to be a symbolic object, and just represents itself. Furthermore, a cons of two symbolic objects represents the cons of the two objects they represent. For instance,

(1 . (:g-boolean .  A & B))

represents either (1 . t) or (1 . nil). Together, these conventions allow GL to avoid lots of tagging as symbolic objects are manipulated.

One last kind of symbolic object we will mention represents an if-then-else among other symbolic objects. Its syntax is:

(:g-ite  <test>  <then>  .  <else>)

where <test>, <then>, and <else> are themselves symbolic objects. The value of a :g-ite is either the value of <then> or of <else>, depending on the value of <test>. For example,

(:g-ite  (:g-boolean . A)
         (:g-integer B  A  false)
         . #\C)

represents either 2, 3, or the character C.

GL doesn't have a special symbolic object format for ACL2 objects other than numbers and Booleans. But it is still possible to create symbolic objects that take any finite range of values among ACL2 objects, by using a nesting of :g-ites where the tests are :g-booleans.