		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.