		Search-engine friendly clone of the ACL2 documentation.

Bfr-eval

Evaluate a BFR under an appropriate BDD/AIG environment.

Signature
(bfr-eval x env) → bool

Definitions and Theorems

Function: bfr-eval

(defun bfr-eval (x env)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-eval))
    (declare (ignorable __function__))
    (mbe :logic
         (bfr-case :bdd (acl2::eval-bdd x env)
                   :aig (acl2::aig-eval x env))
         :exec
         (if (booleanp x)
             x
           (bfr-case :bdd (acl2::eval-bdd x env)
                     :aig (acl2::aig-eval x env))))))

Theorem: bfr-eval-consts

(defthm bfr-eval-consts
  (and (equal (bfr-eval t env) t)
       (equal (bfr-eval nil env) nil)))

Subtopics

Bfr-eval-alist: Evaluate an alist that maps names to BFRs, returning an alist mapping the same names to their (Boolean) results.