• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
  • Testing-utilities
  • Math

• 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)))