Q-ite
Optimized way to construct a new if-then-else UBDD.
(q-ite x y z) is a macro that is logically equal to (q-ite-fn x y z). But in the execution, special measures are taken so that we can
sometimes avoid evaluating y or z.
At a first approximation, (q-ite x y z) expands into
(let ((<x> x))
(cond ((null <x>) z)
((atom <x>) y)
(t
(let* ((<y> y)
(<z> z))
(q-ite-fn <x> <y> <z>)))))
The advantage of this over a raw call of q-ite-fn is that when the
expression for x evaluates to an atom, then we can avoid evaluating y
or z. Hence, when y or z is expensive to evaluate (e.g.,
perhaps they are terms involving calls to UBDD-building operations like q-not), we can save some time.
Of course, if neither y nor z is expensive to evaluate, then the
above just adds some minor overhead to each call of q-ite-fn. Sometimes
we can avoid this overhead by recognizing that they are cheap to evaluate. In
particular, we claim that constants and variable symbols are always cheap to
evaluate, and so, if both y and z are either constants or variables,
then we do not bother to introduce the let statement above and instead
we just lay down a raw call of q-ite-fn.
Theorem: ubddp-of-q-ite
(defthm ubddp-of-q-ite
(implies (and (force (ubddp x))
(force (ubddp y))
(force (ubddp z)))
(equal (ubddp (q-ite x y z)) t)))
Theorem: eval-bdd-of-q-ite
(defthm eval-bdd-of-q-ite
(equal (eval-bdd (q-ite x y z) values)
(if (eval-bdd x values)
(eval-bdd y values)
(eval-bdd z values))))
Subtopics
- Q-ite-reductions
- Basic rewriting of q-ite expressions.
- Canonicalize-to-q-ite
- Reasoning strategy: rewrite all BDD-building functions into calls of
q-ite.
