Format of symbolic objects in gl.

Symbolic objects represent functions from the set of environments (described below) to the set of ACL2 objects. The value of an object at an environment is given by an evaluator function. Symbolic objects are recursively structured and have a number of constructors. We first briefly describe evaluators (and why there can be more than one), then the structure of environment objects, and then the symbolic object constructors.

A symbolic object evaluator is a function with the interface

(EV symbolic-object environment) => value.

There may be several evaluators defined. The differences between evaluators have to do with the G-APPLY symbolic object type, which represents a function applied to symbolic arguments. In order to evaluate such an object, the evaluator must be defined such that it recognizes the particular function symbol used in the G-APPLY object. An evaluator may not evaluate a symbolic object containing a G-APPLY construct with an unrecognized function symbol. One evaluator, named EVAL-G-BASE, is initially defined in the GL library, and recognizes function symbols of the predefined primitives included with the library.

The basic components of symbolic objects are data structures containing Boolean functions, represented either by BDDs or AIGs (see modes), and G-VAR constructs, which represent unconstrained variables. To evaluate a symbolic object, each of these needs to be evaluated to a constant. An environment contains the information necessary to evaluate either kind of expression:

- a truth assignment for the Boolean variables used in the Boolean function representation; in AIG mode, this is an alist mapping variable names to Booleans, and in BDD mode, an ordered list of Booleans corresponding to the decision levels of the BDDs.
- an alist mapping unconstrained variable names to their values.

There are eight basic constructions of symbolic objects, some of which may recursively contain other symbolic objects. We now describe each such construction and its evaluation.

- Representation: (:G-BOOLEAN . bfr)
- Constructor: (G-BOOLEAN bfr)
- Takes the values T and NIL. The evaluation of a G-BOOLEAN object is simply
the evaluation of
<bdd> using the list of Booleans in the environment. - Representation: (:G-INTEGER . list-of-bfrs)
- Constructor: (G-INTEGER list-of-bfrs)
- Evaluates to an integer.
<list-of-bfrs> gives the bits of the integer, least significant first. The representation is two's-complement, i.e. the last bit represents 0 if false or -1 if true. The enpty list represents 0. - Representation (:G-CONCRETE . object)
- Constructor: (G-CONCRETE object)
- Evaluates to
<object> . While most ACL2 objects evaluate to themselves anyway, this construct is useful for representing symbolic objects or objects structured similarly to symbolic objects. For example,(:G-CONCRETE . (:G-BOOLEAN . (T . NIL))) evaluates to (:G-BOOLEAN . (T . NIL)), whereas (:G-BOOLEAN . (T . NIL)) evaluates to either T or NIL.

- Representation: (:G-VAR . name)
- Constructor: (G-VAR . name)
<name> may be any object. Evaluates to the object bound to<name> in the environment.- Representation: (:G-ITE test then . else)
- Constructor: (G-ITE test then else)
- Each of
<test> ,<then> , and<else> must be symbolic objects. If<test> evaluates to a nonnil value, then this object evaluates to the evaluation of<then> ; otherwise this evaluates to the evaluation of<else> . - Representation: (:G-APPLY fn . arglist)
- Constructor: (G-APPLY fnsym arglist)
<fn> should be a symbol and<arglist> should be a symbolic object. If the evaluator recognizes<fn> and<arglist> evaluates to<args> , a true-list of length equal to the arity of the function<fn> , then this object evaluates to the application of<fn> to<args> . Otherwise, the evaluation is undefined.- Representation: atom
- Every atom evaluates to itself. However, the keyword symbols :G-BOOLEAN, :G-INTEGER, :G-CONCRETE, :G-VAR, :G-ITE, and :G-APPLY are not themselves well-formed symbolic objects.
- Representation:
(car . cdr) - A cons of two symbolic objects evaluates to the cons of their evaluations. Note that since the keyword symbols that distinguish symbolic object constructions are not themselves well-formed symbolic objects, this construction is unambiguous.

- Any function from finitely many Boolean values to the universe of ACL2 objects can be expressed using only the G-ITE, G-BOOLEAN, and G-CONCRETE forms.
- Most ACL2 objects are themselves well-formed symbolic objects which evaluate to themselves. The exceptions are ones which contain the special keyword symbolis :G-BOOLEAN, :G-INTEGER :G-CONCRETE, :G-VAR, :G-ITE, and :G-APPLY. These atoms (and out of all atoms, only these) are not well-formed symbolic objects. Since a cons of any two well-formed symbolic objects is itself a well-formed symbolic objects, only objects containing these atoms may be non-well-formed.
- The function that checks well-formedness of symbolic objects is GOBJECTP, and the initial evaluator function is GL::EVAL-G-BASE. It may be useful to read the definitions of these functions for reference in case the above symbolic object documentation is unclear.