Fgl-object-eval
Evaluator for FGL symbolic objects.
- Signature
(fgl-object-eval x env &optional (logicman 'logicman)) → val
- Arguments
- x — Guard (lgl-bfr-object-p x).
- env — Guard (fgl-env-p env).
Fgl-object-eval gives the semantics for FGL symbolic objects, in the
same way as a term evaluator gives the semantics for terms. In fact,
fgl-object-eval uses a term evaluator fgl-ev to interpret function
calls.
The inputs to fgl-object-eval are the object to be evaluated; an
env containing two parts: a Boolean formula environment binding Boolean
variables to values, and a term-level environment binding term variables to
objects; and the logic manager or logicman, a stobj containing (mainly)
the Boolean function mode and AIGNET relative to which Boolean formulas are
evaluated using bfr-eval.
- G-concrete objects return the quoted value.
- G-boolean objects return the evaluation using bfr-eval of
the Boolean formula under the Boolean environment.
- G-integer objects return the integer consisting of the bits
produced by evaluating the bits using bfr-eval.
- G-ite objects return the if-then-else of the recursive
fgl-object-eval of the three arguments.
- G-apply objects return the fgl-ev evaluation of the function
applied to the recursive fgl-object-eval evaluation of the arguments.
- G-var objects return the binding of the variable in the term-level
environment.
- G-map objects return the alist, with the bound values recursively
evaluated using fgl-object-eval.
- G-cons objects return the cons of the recursive
fgl-object-eval evaluations of the car and cdr.
Subtopics
- Fgl-env
- Type of environment objects for FGL object evaluation.
- Bools->int
- Convert a list of Booleans into an integer.
