		Search-engine friendly clone of the ACL2 documentation.

Bfr-negate

Signature
(bfr-negate x &optional (bfrstate 'bfrstate)) → new-x
Arguments: x — Guard (bfr-p x).; bfrstate — Guard (bfrstate-p bfrstate).
Returns: new-x — Type (bfr-p new-x).

Definitions and Theorems

Function: bfr-negate-fn

(defun bfr-negate-fn (x bfrstate)
 (declare (xargs :guard (and (bfrstate-p bfrstate) (bfr-p x))))
 (let ((__function__ 'bfr-negate))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* ((x (bfr-fix x)))
    (bfrstate-case
       :aig (acl2::aig-not x)
       :bdd (acl2::q-not x)
       :aignet
       (aignet-lit->bfr (satlink::lit-negate (bfr->aignet-lit x)))))
   :exec
   (if (booleanp x)
       (not x)
     (bfrstate-case :aig (acl2::aig-not x)
                    :bdd (acl2::q-not x)
                    :aignet (satlink::lit-negate x))))))

Theorem: bfr-p-of-bfr-negate

(defthm bfr-p-of-bfr-negate
  (b* ((new-x (bfr-negate-fn x bfrstate)))
    (bfr-p new-x))
  :rule-classes :rewrite)

Theorem: bfr-negate-of-bfr-fix

(defthm bfr-negate-of-bfr-fix
  (equal (bfr-negate (bfr-fix x))
         (bfr-negate x)))

Theorem: bfr-negate-fn-of-bfrstate-fix-bfrstate

(defthm bfr-negate-fn-of-bfrstate-fix-bfrstate
  (equal (bfr-negate-fn x (bfrstate-fix bfrstate))
         (bfr-negate-fn x bfrstate)))

Theorem: bfr-negate-fn-bfrstate-equiv-congruence-on-bfrstate

(defthm bfr-negate-fn-bfrstate-equiv-congruence-on-bfrstate
  (implies (bfrstate-equiv bfrstate bfrstate-equiv)
           (equal (bfr-negate-fn x bfrstate)
                  (bfr-negate-fn x bfrstate-equiv)))
  :rule-classes :congruence)