Symbolic-objects
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.
Evaluators
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.
Environments
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.
Symbolic Object Representation
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.
Miscellaneous notes about symbolic objects and evaluation
- 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.
