		Search-engine friendly clone of the ACL2 documentation.

Equal-by-eval-bdds

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)))))