		Search-engine friendly clone of the ACL2 documentation.

Faig

Faig-partial-eval

(faig-partial-eval x env) evaluates x, an FAIG, under the partial environment env, producing a new FAIG as a result.

Signature
(faig-partial-eval x env) → *

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

Definitions and Theorems

Function: faig-partial-eval

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

Subtopics

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