• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
      • Ubdd-constructors
      • 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

• Ubdds

Ubdd-fix

(ubdd-fix x) constructs a valid ubddp that is treated identically to x under eval-bdd.

This fixes up the tips of x to be Booleans and handles any collapsing of (t . t) and (nil . nil) nodes. It is occasionally useful in theorems to avoid ubddp hypotheses.

Definitions and Theorems

Function: ubdd-fix

(defun ubdd-fix (x)
  (declare (xargs :guard t))
  (if (atom x)
      (if x t nil)
    (if (and (atom (car x))
             (atom (cdr x))
             (iff (car x) (cdr x)))
        (if (car x) t nil)
      (qcons (ubdd-fix (car x))
             (ubdd-fix (cdr x))))))

Function: ubdd-fix-memoize-condition

(defun ubdd-fix-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard 't))
  (consp x))

Theorem: ubddp-ubdd-fix

(defthm ubddp-ubdd-fix
  (ubddp (ubdd-fix x)))

Theorem: eval-bdd-ubdd-fix

(defthm eval-bdd-ubdd-fix
  (equal (eval-bdd (ubdd-fix x) env)
         (eval-bdd x env)))

Theorem: ubdd-fix-x-is-x

(defthm ubdd-fix-x-is-x
  (implies (ubddp x)
           (equal (ubdd-fix x) x)))