• 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

Eval-bdd

Sematics of a UBDD.

(eval-bdd x values) evaluates the UBDD x with respect to a list of Boolean values, returning a Boolean value which we think of as the interpretation of x for this particular set of values.

Typically x should be a ubddp and values should be a boolean-listp, but we do not enforce this in our guard.

When x is t or nil, it represents a constant function and always evaluates to itself no matter what values are given for the variables.

When x is any other tree, we use (car values) to guide us down the car (the "true branch") or cdr (the "false branch") of x. In case we run out of values, we pretend that values contains an infinite list of nils at the end and just follow the false branches of x all the way down.

Definitions and Theorems

Function: eval-bdd

(defun eval-bdd (x values)
       (declare (xargs :guard t))
       (cond ((atom x) (if x t nil))
             ((atom values) (eval-bdd (cdr x) nil))
             ((car values)
              (eval-bdd (car x) (cdr values)))
             (t (eval-bdd (cdr x) (cdr values)))))

Theorem: eval-bdd-when-not-consp

(defthm eval-bdd-when-not-consp
        (implies (not (consp x))
                 (equal (eval-bdd x values)
                        (if x t nil))))

Theorem: eval-bdd-of-non-consp-cheap

(defthm eval-bdd-of-non-consp-cheap
        (implies (not (consp x))
                 (equal (eval-bdd x vals) (if x t nil)))
        :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: eval-bdd-of-nil

(defthm eval-bdd-of-nil
        (equal (eval-bdd nil values) nil))

Theorem: eval-bdd-of-t

(defthm eval-bdd-of-t
        (equal (eval-bdd t values) t))

Theorem: eval-bdd-when-non-consp-values

(defthm eval-bdd-when-non-consp-values
        (implies (and (syntaxp (not (equal vals *nil*)))
                      (atom vals))
                 (equal (eval-bdd x vals)
                        (eval-bdd x nil))))