diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index 23a78f379..f54a39442 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -3739,26 +3739,23 @@ static double bdd_pathcount_rec(BDD r) return size; } -/*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNMENT ================*/ - -/* -NAME {* bdd\_have\_common\_assignment *} -SECTION {* info *} -SHORT {* Decide if two bdds share an satisfying assignement *} -PROTO {* int bdd_have_common_assignment(BDD l, BDD r) *} -DESCR {* Returns 1 iff l&r != bddfalse *} -RETURN {* 0 or 1 *} -*/ -int bdd_have_common_assignment(BDD left, BDD right) +static int bdd_have_common_assignment_(BDD left, BDD right) { - // If one of them is false -> false - if (ISZERO(left) || ISZERO(right)) - return 0; - // If one of them is true and the other is not false - // or if they are identical -> true - if (ISONE(left) || ISONE(right) || left == right) - return 1; - // Now both of them are not constant +#ifndef NDEBUG + // arguments can't be constant + if (ISCONST(left)) + return bdd_error(BDD_ILLBDD); + if (ISCONST(right)) + return bdd_error(BDD_ILLBDD); +#endif + + // Always make "left" the smaller one to improve cache usage + if (left > right) + { + BDD tmp = left; + left = right; + right = tmp; + } BddCacheData *entry = BddCache_lookup(&misccache, COMMONHASH(left,right)); /* Check entry->b last, because not_rec() does not initialize it. */ @@ -3777,19 +3774,47 @@ int bdd_have_common_assignment(BDD left, BDD right) int vl = LEVEL(left); int vr = LEVEL(right); + // Try avoiding as many recursive calls as possible int res; if (vl < vr) - // left has to "catch up" - res = (bdd_have_common_assignment(LOW(left), right) - || bdd_have_common_assignment(HIGH(left), right)); + { + // left has to "catch up" + // We know that right is not constant + BDD l_left = LOW(left); + BDD h_left = HIGH(left); + res = ISONE(l_left) || (l_left == right) + || ISONE(h_left) || (h_left == right) + || (!ISZERO(l_left) && bdd_have_common_assignment_(l_left, right)) + || (!ISZERO(h_left) && bdd_have_common_assignment_(h_left, right)); + } else if (vr < vl) - // right has to "catch up" - res = (bdd_have_common_assignment(left, LOW(right)) - || bdd_have_common_assignment(left, HIGH(right))); + { + // right has to "catch up" + // We know that left is not constant + BDD l_right = LOW(right); + BDD h_right = HIGH(right); + res = ISONE(l_right) || (l_right == left) + || ISONE(h_right) || (h_right == left) + || (!ISZERO(l_right) && bdd_have_common_assignment_(left, + l_right)) + || (!ISZERO(h_right) && bdd_have_common_assignment_(left, + h_right)); + } else - // They evolve jointly - res = (bdd_have_common_assignment(LOW(left), LOW(right)) - || bdd_have_common_assignment(HIGH(left), HIGH(right))); + { + // They evolve jointly + BDD l_left = LOW(left); + BDD h_left = HIGH(left); + BDD l_right = LOW(right); + BDD h_right = HIGH(right); + + res = ((!ISZERO(l_left) && !ISZERO(l_right)) + && (ISONE(l_left) || ISONE(l_right) || l_left == l_right + || bdd_have_common_assignment_(l_left, l_right))) + || ((!ISZERO(h_left) && !ISZERO(h_right)) + && (ISONE(h_left) || ISONE(h_right) || h_left == h_right + || bdd_have_common_assignment_(h_left, h_right))); + } entry->i.a = left; entry->i.c = CACHEID_COMMON; @@ -3798,6 +3823,31 @@ int bdd_have_common_assignment(BDD left, BDD right) return res; } +/*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNMENT ================*/ + +/* +NAME {* bdd\_have\_common\_assignment *} +SECTION {* info *} +SHORT {* Decide if two bdds share an satisfying assignement *} +PROTO {* int bdd_have_common_assignment(BDD l, BDD r) *} +DESCR {* Returns 1 iff l&r != bddfalse *} +RETURN {* 0 or 1 *} +*/ +int bdd_have_common_assignment(BDD left, BDD right) +{ + // If one of them is false -> false + if (ISZERO(left) || ISZERO(right)) + return 0; + + // If one of them is true and the other is not false + // or if they are identical -> true + if (ISONE(left) || ISONE(right) || left == right) + return 1; + // Now both of them are not constant + + return bdd_have_common_assignment_(left, right); +} + /*=== DECIDE IF A BDD is a cube ================*/ /* diff --git a/buddy/src/bddtest.cxx b/buddy/src/bddtest.cxx index c8eddc407..b77e3dc77 100644 --- a/buddy/src/bddtest.cxx +++ b/buddy/src/bddtest.cxx @@ -189,6 +189,57 @@ void testIsCube(){ ERROR("is_cube failed on b2"); } +void testHaveCommon() +{ + cout << "Testing have_common_assignment()\n"; + + if (bdd_have_common_assignment(bddtrue, bddtrue) != 1) + ERROR(" have_common_assignment on true, true"); + if (bdd_have_common_assignment(bddfalse, bddtrue) != 0) + ERROR(" have_common_assignment on false, true"); + if (bdd_have_common_assignment(bddtrue, bddfalse) != 0) + ERROR(" have_common_assignment on true, false"); + if (bdd_have_common_assignment(bddfalse, bddfalse) != 0) + ERROR(" have_common_assignment on false, false"); + + + // Some cubes + bdd a = bdd_ithvar(0); + bdd b = bdd_ithvar(1); + bdd c = bdd_ithvar(2); + bdd d = bdd_ithvar(3); + + bdd ca[5]; + ca[0] = a&c; + ca[1] = a&!c; + ca[2] = c&d; + ca[3] = a&b&c&!d; + ca[4] = !a&!d; + + // Some tests + for (unsigned i1 = 0; i1 < 5; i1++) + { + for (unsigned j1 = i1; j1 < 5; j1++) + { + if (bdd_have_common_assignment(ca[i1], ca[j1]) + != ((ca[i1] & ca[j1]) != bddfalse)) + ERROR("bdd_have_common_assignment(): failed on cube"); + for (unsigned i2 = 0; i2 < 5; i2++) + { + for (unsigned j2 = i2; j2 < 5; j2++) + { + bdd b1 = ca[i1]|ca[j1]; + bdd b2 = ca[i2]|ca[j2]; + if (bdd_have_common_assignment(b1, b2) + != ((b1 & b2) != bddfalse)) + ERROR("bdd_have_common_assignment(): failed on " + "disjunction of cubes"); + } + } + } + } +} + int main(int ac, char** av) { bdd_init(1000,1000); @@ -199,6 +250,7 @@ int main(int ac, char** av) testBvecIte(); testShortest(); testIsCube(); + testHaveCommon(); bdd_done(); return 0;