[buddy] Improve bdd_have_common_assignment

* src/bddop.c: Improve here
* src/bddtest.cxx: Tests here

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 ================*/
+static int bdd_have_common_assignment_(BDD left, BDD right)
-
-/*
-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
+#ifndef NDEBUG
-  if (ISZERO(left) || ISZERO(right))
+  // arguments can't be constant
-    return 0;
+  if (ISCONST(left))
-  // If one of them is true and the other is not false
+    return bdd_error(BDD_ILLBDD);
-  // or if they are identical -> true
+  if (ISCONST(right))
-  if (ISONE(left) || ISONE(right) || left == right)
+    return bdd_error(BDD_ILLBDD);
-    return 1;
+#endif
-  // Now both of them are not constant
+
+  // 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)
+      // left has to "catch up"
-           || bdd_have_common_assignment(HIGH(left), right));
+      // 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))
+      // right has to "catch up"
-           || bdd_have_common_assignment(left, HIGH(right)));
+      // 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))
+      // They evolve jointly
-           || bdd_have_common_assignment(HIGH(left), HIGH(right)));
+      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 ================*/
 
 /*

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;