# 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.