• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
        • Equal-by-eval-bdds-hint-heavy
        • Term-is-bdd
        • Equal-by-eval-bdds-hint
        • Max-depth
      • 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

Equal-by-eval-bdds

Reasoning strategy: reduce equality of ubdds to equality of an arbitrary evaluation.

Suppose we know that x and y are ubddp objects, and we are trying to prove they are equal. The equal-by-eval-bdds approach involves trying to establish this equality by proving the equivalent fact, roughly:

(forall values
        (equal (eval-bdd x values)
               (eval-bdd y values)))

Actually, we can even assume that values has a certain length and contains only Booleans, but usually these extra facts are not needed.

It is somewhat tricky to implement this sort of reduction in ACL2. Our approach is very similar to the "pick a point" strategy for proving that sets are equal, described in the following paper:

Jared Davis. Finite Set Theory based on Fully Ordered Lists. In ACL2 2004. November, 2004, Austin, TX, USA.

The computed hint equal-by-eval-bdds-hint automates the strategy. That is, when this hint is active, ACL2 will automatically try to use equal-by-eval-bdds to prove equalities when we can determine (with rewriting) that x and y are ubddps.

At any rate, if you want to prove that (foo ...) and (bar ...) are equal BDDs, you might start by proving the rules:

(equal (eval-bdd (foo ...) values)
       (... expression 1 ...))

(equal (eval-bdd (bar ...) values)
       (... expression 2 ...))

Then you will be able to prove (equal (foo ...) (bar ...)) by arguing that expression 1 and expression 2 are equal.

Definitions and Theorems

Theorem: bdd-equivalence-constraint

(defthm bdd-equivalence-constraint
        (implies (and (bdd-hyps)
                      (equal (len arbitrary-values)
                             (max (max-depth (bdd-lhs))
                                  (max-depth (bdd-rhs))))
                      (boolean-listp arbitrary-values)
                      (ubddp (bdd-lhs))
                      (ubddp (bdd-rhs)))
                 (equal (eval-bdd (bdd-lhs) arbitrary-values)
                        (eval-bdd (bdd-rhs) arbitrary-values))))

Theorem: equal-by-eval-bdds

(defthm equal-by-eval-bdds
        (implies (and (bdd-hyps)
                      (ubddp (bdd-lhs))
                      (ubddp (bdd-rhs)))
                 (equal (equal (bdd-lhs) (bdd-rhs)) t)))

Subtopics

Equal-by-eval-bdds-hint-heavy

Experimental "heavyweight" hint.

Term-is-bdd

Heuristic for deciding which terms are UBDDs.

Equal-by-eval-bdds-hint

Basic automation of equal-by-eval-bdds.

Max-depth

Depth of a cons tree.