		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) → *
Arguments: n — Guard (bfr-varname-p n).

Definitions and Theorems

Function: bfr-set-var

(defun bfr-set-var (n val env)
 (declare (xargs :guard (bfr-varname-p n)))
 (let ((__function__ 'bfr-set-var))
  (declare (ignorable __function__))
  (let ((n (bfr-varname-fix n)))
   (bfr-case
      :bdd
      (with-guard-checking nil
                           (ec-call (update-nth n (and val t) env)))
      :aig (hons-acons 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 (bfr-varname-fix n)
                    (bfr-varname-fix m))
             (and val t)
           (bfr-lookup n env))))

Theorem: bfr-varname-equiv-implies-equal-bfr-set-var-1

(defthm bfr-varname-equiv-implies-equal-bfr-set-var-1
  (implies (bfr-varname-equiv n n-equiv)
           (equal (bfr-set-var n val env)
                  (bfr-set-var n-equiv val env)))
  :rule-classes (:congruence))