		Search-engine friendly clone of the ACL2 documentation.

Bfr-set-var

Set the nth BFR variable to some value in an AIG/BDD environment.

Signature
(bfr-set-var n val env &optional (logicman 'logicman)) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: bfr-set-var-fn

(defun bfr-set-var-fn (n val env logicman)
 (declare (xargs :stobjs (logicman)))
 (declare (xargs :guard (natp n)))
 (let ((__function__ 'bfr-set-var))
  (declare (ignorable __function__))
  (lbfr-case
      :bdd
      (with-guard-checking nil
                           (ec-call (update-nth n (and val t) env)))
      :aig (hons-acons (lnfix n) (and val t) env)
      :aignet (hons-acons (lnfix n)
                          (and val t)
                          env))))

Theorem: bfr-lookup-bfr-set-var

(defthm bfr-lookup-bfr-set-var
  (equal (bfr-lookup n (bfr-set-var m val env))
         (if (equal (nfix n) (nfix m))
             (and val t)
           (bfr-lookup n env))))

Theorem: bfr-set-var-of-logicman-extension

(defthm bfr-set-var-of-logicman-extension
  (implies (bind-logicman-extension new old)
           (equal (bfr-set-var n val env new)
                  (bfr-set-var n val env old))))

Theorem: bfr-set-var-fn-of-nfix-n

(defthm bfr-set-var-fn-of-nfix-n
  (equal (bfr-set-var-fn (nfix n)
                         val env logicman)
         (bfr-set-var-fn n val env logicman)))

Theorem: bfr-set-var-fn-nat-equiv-congruence-on-n

(defthm bfr-set-var-fn-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (bfr-set-var-fn n val env logicman)
                  (bfr-set-var-fn n-equiv val env logicman)))
  :rule-classes :congruence)