		Search-engine friendly clone of the ACL2 documentation.

Bfr-p

Recognizer for valid Boolean Function Representation (bfr) objects.

Signature
(bfr-p x &optional (bfrstate 'bfrstate)) → *
Arguments: bfrstate — Guard (bfrstate-p bfrstate).

Definitions and Theorems

Function: bfr-p-fn

(defun bfr-p-fn (x bfrstate)
  (declare (xargs :guard (bfrstate-p bfrstate)))
  (let ((__function__ 'bfr-p))
    (declare (ignorable __function__))
    (bfrstate-case
         :aig (aig-p x (bfrstate->bound bfrstate))
         :bdd (ubddp x (bfrstate->bound bfrstate))
         :aignet (or (booleanp x)
                     (and (satlink::litp x)
                          (not (eql x 0))
                          (not (eql x 1))
                          (<= (satlink::lit->var x)
                              (bfrstate->bound bfrstate)))))))

Theorem: bfr-p-of-constants

(defthm bfr-p-of-constants
  (and (bfr-p t) (bfr-p nil)))

Theorem: bfr-p-when-bfrstate>=

(defthm bfr-p-when-bfrstate>=
  (implies (and (bfrstate>= new old) (bfr-p x old))
           (bfr-p x new)))

Theorem: bfr-p-in-terms-of-aig-p

(defthm bfr-p-in-terms-of-aig-p
  (equal (bfr-p x (bfrstate (bfrmode :aig) bound))
         (aig-p x bound)))

Theorem: bfr-p-in-terms-of-ubddp

(defthm bfr-p-in-terms-of-ubddp
  (equal (bfr-p x (bfrstate (bfrmode :bdd) bound))
         (ubddp x bound)))

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

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

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

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