		Search-engine friendly clone of the ACL2 documentation.

Bfr-eval

Evaluate a BFR under an appropriate BDD/AIG environment.

Signature
(bfr-eval x env &optional (logicman 'logicman)) → bool
Arguments: x — A Boolean function object.
Guard (lbfr-p x).; env — The (Boolean) evaluation environment.; logicman — The logic manager.

Bfr-eval is the evaluator for Boolean function objects in FGL.

Boolean function objects in FGL may be UBDDs, hons-AIGs, or aignet literals (represented as natural numbers). The bfr-mode of the logic manager (accessed as (logicman->mode logicman)) determines how the objects are interpreted. Furthermore, in the aignet mode, literals must be evaluated relative to an aignet, which is also stored in the logic manager as a nested stobj, accessed using (logicman->aignet logicman).

The env input determines the values of Boolean variables, but its form also depends on the BFR mode. In UBDD mode, it is an ordered list of Boolean values, where (nth n env) is the value of Boolean variable n. Otherwise, it is a fast alist mapping natural numbers to Boolean values, and the value of the nth Boolean variable is (cdr (hons-get n env)). In aignet mode, the Boolean variable numbers map to primary inputs of the AIG -- registers are not used.

Definitions and Theorems

Function: bfr-eval-fn

(defun bfr-eval-fn (x env logicman)
 (declare (xargs :stobjs (logicman)))
 (declare (xargs :guard (lbfr-p x)))
 (let ((__function__ 'bfr-eval))
  (declare (ignorable __function__))
  (b* ((bfrstate (logicman->bfrstate)))
   (bfrstate-case
    :bdd (acl2::eval-bdd (bfr-fix x) env)
    :aig (acl2::aig-eval (bfr-fix x) env)
    :aignet
    (mbe
     :logic
     (non-exec
        (bit->bool
             (aignet::lit-eval
                  (bfr->aignet-lit x)
                  (alist-to-bitarr
                       (aignet::num-ins (logicman->aignet logicman))
                       env nil)
                  nil (logicman->aignet logicman))))
     :exec
     (b* ((x (bfr->aignet-lit x))
          ((acl2::local-stobjs aignet::invals aignet::regvals)
           (mv ans aignet::invals aignet::regvals)))
      (stobj-let
       ((aignet (logicman->aignet logicman)))
       (ans aignet::invals aignet::regvals)
       (b*
        ((aignet::invals (alist-to-bitarr (aignet::num-ins aignet)
                                          env aignet::invals))
         (aignet::regvals (alist-to-bitarr (aignet::num-regs aignet)
                                           nil aignet::regvals)))
        (mv
         (bit->bool
           (aignet::lit-eval x
                             aignet::invals aignet::regvals aignet))
         aignet::invals aignet::regvals))
       (mv ans
           aignet::invals aignet::regvals))))))))

Theorem: bfr-eval-consts

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

Theorem: bfr-eval-of-bfr-fix

(defthm bfr-eval-of-bfr-fix
  (b* ((bfrstate (logicman->bfrstate logicman)))
    (equal (bfr-eval (bfr-fix x) env)
           (bfr-eval x env))))

Theorem: bfr-eval-of-logicman-extension

(defthm bfr-eval-of-logicman-extension
  (implies (and (bind-logicman-extension new old)
                (lbfr-p x old))
           (equal (bfr-eval x env new)
                  (bfr-eval x env old))))