BDD.ite: skip the operator cache when we're building the BDD bottom-up
Many/most uses of ite are for constructing BDDs bottom up: the condition BDD is a single variable whose level is less than that of either branch BDD. These are inexpensive operations so don't cache them.
@@ -960,6 +960,14 @@ public final class JFactory extends BDDFactory {
return g;
} else if (ISZERO(f)) {
return h;
+ } else if (HIGH(f) == BDDONE
+ && LOW(f) == BDDZERO
+ && LEVEL(f) < LEVEL(g)
+ && LEVEL(f) < LEVEL(h)) {
+ // f is a single variable BDD, and its level is lower than g's and h's.
+ // this is a common case: we're building a BDD bottom-up
+ // skip the operator cache
+ return bdd_makenode(LEVEL(f), h /* low/else */, g /* high/then */);
} else if (g == h) {
return g;
} else if (ISZERO(g)) {
