• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
      • Ubdd-constructors
        • Q-and
        • Q-ite
        • Q-or
        • Q-implies
        • Q-iff
        • Q-and-c2
        • Q-and-c1
        • Q-or-c2
        • Q-not
        • Q-ite-fn
        • Q-xor
        • Cheap-and-expensive-arguments
        • Q-and-is-nil
        • Q-compose-list
        • Qv
        • Q-compose
        • Q-and-is-nilc2
        • Q-nor
        • Q-nand
      • Eval-bdd
      • Ubddp
      • Ubdd-fix
      • Q-sat
      • Bdd-sat-dfs
      • Eval-bdd-list
      • Qcdr
      • Qcar
      • Q-sat-any
      • Canonicalize-to-q-ite
      • Ubdd-listp
      • Qcons
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Ubdd-constructors

Q-not

Negate a UBDD.

(q-not x) builds a new UBDD representing (not x). That is, the the following is a theorem:

(equal (eval-bdd (q-not x) values)
       (not (eval-bdd x values)))

Note: memoized for efficiency.

Definitions and Theorems

Function: q-not

(defun q-not (x)
  (declare (xargs :guard t))
  (if (atom x)
      (if x nil t)
    (hons (q-not (car x)) (q-not (cdr x)))))

Function: q-not-memoize-condition

(defun q-not-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard 't))
  (and (consp x)
       (or (consp (car x)) (consp (cdr x)))))

Theorem: consp-of-q-not

(defthm consp-of-q-not
  (equal (consp (q-not x)) (consp x)))

Theorem: equal-t-and-q-not

(defthm equal-t-and-q-not
  (equal (equal t (q-not x)) (not x)))

Theorem: equal-nil-and-q-not

(defthm equal-nil-and-q-not
  (equal (equal nil (q-not x))
         (and (atom x) (if x t nil))))

Theorem: q-not-under-iff

(defthm q-not-under-iff
  (iff (q-not x)
       (if (consp x) t (if x nil t))))

Theorem: ubddp-of-q-not

(defthm ubddp-of-q-not
  (implies (force (ubddp x))
           (equal (ubddp (q-not x)) t)))

Theorem: eval-bdd-of-q-not

(defthm eval-bdd-of-q-not
  (equal (eval-bdd (q-not x) values)
         (not (eval-bdd x values))))

Theorem: canonicalize-q-not

(defthm canonicalize-q-not
  (implies (force (ubddp x))
           (equal (q-not x) (q-ite x nil t)))
  :rule-classes :definition)