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
For function calls, we set up a
When you add your own BDD producing functions, you may wish to use (add-bdd-fn fnname) to add them to the
(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)))))