# Term-is-bdd

Heuristic for deciding which terms are UBDDs.

The computed hint equal-by-eval-bdds-hint is supposed to
automatically apply equal-by-eval-bdds when we are trying to prove that
two ubdds are equal. But a basic prerequisite to being able to
do this is to determine whether the terms on either side of an equality are
actually UBDDs or not.

We use the function term-is-bdd to decide if a particular term is a
BDD. For variables, we ask the rewriter if the variable is known to be a
ubddp. For quoted constants, we just run ubddp to see if it's a
UBDD.

For function calls, we set up a bdd-fns table that lists functions that
produce BDDs, and we just check whether the function being called is mentioned
in this table. This is a pretty dumb heuristic, and we may eventually want a
more flexible notion here that allows us to pattern match against mv-nths and so on.

When you add your own BDD producing functions, you may wish to use `(add-bdd-fn fnname)` to add them to the bdd-fns table.

### Definitions and Theorems

**Function: **term-is-bdd

(defun
term-is-bdd
(term hyps whole hist pspv world ctx state)
(declare (xargs :stobjs state))
(cond
((atom term)
(let
((term-and-ttree
(computed-hint-rewrite (cons 'ubddp (cons term 'nil))
hyps
t whole hist pspv world ctx state)))
(equal (car term-and-ttree) *t*)))
((eq (car term) 'quote)
(ubddp (cadr term)))
(t (member-eq (car term) (bdd-fns)))))