		Search-engine friendly clone of the ACL2 documentation.

Faig

Faig-eval

(faig-eval x env) evaluates x, a faig, under the environment env, producing a pair of Boolean values.

Signature
(faig-eval x env) → *

See aig-eval; the env should be a fast alist and you will want to clear the memoize table for aig-eval when you are done using the env.

Definitions and Theorems

Function: faig-eval

(defun faig-eval (x env)
       (declare (xargs :guard t))
       (let ((__function__ 'faig-eval))
            (declare (ignorable __function__))
            (if (atom x)
                '(t . t)
                (cons (aig-eval (car x) env)
                      (aig-eval (cdr x) env)))))

Theorem: faig-eval-of-constants

(defthm faig-eval-of-constants
        (and (equal (faig-eval (faig-t) env)
                    (faig-t))
             (equal (faig-eval (faig-f) env)
                    (faig-f))
             (equal (faig-eval (faig-z) env)
                    (faig-z))
             (equal (faig-eval (faig-x) env)
                    (faig-x))
             (equal (faig-eval nil env) (faig-x))))

Subtopics

Faig-eval-alist: (faig-eval-list x env) evaluates an FAIG alist (an alist binding keys to FAIGs).
Faig-eval-list: (faig-eval-list x env) evaluates a list of FAIGs.
Faig-eval-thms: Basic theorems about faig-eval.