[buddy] Add a function bdd_implies to decide implications between BDDs.

* src/bdd.h (bdd_implies): New function.
* src/bddop.c (bdd_implies): Implement it.
(CACHEID_IMPLIES, IMPLIES_HASH): New helper macros.

buddy/ChangeLog

+2012-06-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Add a function bdd_implies to decide implications between BDDs.
+
+	* src/bdd.h (bdd_implies): New function.
+	* src/bddop.c (bdd_implies): Implement it.
+	(CACHEID_IMPLIES, IMPLIES_HASH): New helper macros.
+
 2012-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Reduce the size of bddNode to improve cache efficiency.

buddy/src/bdd.h

@@ -302,6 +302,7 @@ extern BDD      bdd_xor(BDD, BDD);
 extern BDD      bdd_imp(BDD, BDD);
 extern BDD      bdd_biimp(BDD, BDD);
 extern BDD      bdd_setxor(BDD, BDD);
+extern int      bdd_implies(BDD, BDD);
 extern BDD      bdd_ite(BDD, BDD, BDD);
 extern BDD      bdd_restrict(BDD, BDD);
 extern BDD      bdd_constrain(BDD, BDD);
@@ -510,6 +511,7 @@ private:
    friend bdd      bdd_imp(const bdd &, const bdd &);
    friend bdd      bdd_biimp(const bdd &, const bdd &);
    friend bdd      bdd_setxor(const bdd &, const bdd &);
+   friend int      bdd_implies(const bdd &, const bdd &);
    friend bdd      bdd_ite(const bdd &, const bdd &, const bdd &);
    friend bdd      bdd_restrict(const bdd &, const bdd &);
    friend bdd      bdd_constrain(const bdd &, const bdd &);
@@ -670,6 +672,9 @@ inline bdd bdd_biimp(const bdd &l, const bdd &r)
 inline bdd bdd_setxor(const bdd &l, const bdd &r)
 { return bdd_setxor(l.root, r.root); }
 
+inline int bdd_implies(const bdd &l, const bdd &r)
+{ return bdd_implies(l.root, r.root); }
+
 inline bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h)
 { return bdd_ite(f.root, g.root, h.root); }
 

buddy/src/bddop.c

@@ -51,6 +51,7 @@
 #define CACHEID_PATHCOU     0x4
 #define CACHEID_SETXOR      0x5
 #define CACHEID_SUPPORT     0x6
+#define CACHEID_IMPLIES     0x7
 
    /* Hash value modifiers for replace/compose */
 #define CACHEID_REPLACE      0x0
@@ -159,6 +160,7 @@ static int    varset2svartable(BDD);
 #define APPLYHASH(l,r,op)    (TRIPLE(l,r,op))
 #define ITEHASH(f,g,h)       (TRIPLE(f,g,h))
 #define SETXORHASH(l,r)      (TRIPLE(l,r,CACHEID_SETXOR))
+#define IMPLIESHASH(l,r)     (TRIPLE(l,r,CACHEID_IMPLIES))
 #define RESTRHASH(r,var)     (PAIR(r,var))
 #define CONSTRAINHASH(f,c)   (PAIR(f,c))
 #define QUANTHASH(r)         (r)
@@ -894,6 +896,60 @@ BDD bdd_setxor(BDD l, BDD r)
 }
 
 
+/*=== bdd_implies =========================================================*/
+
+/*
+NAME    {* bdd\_implies *}
+SECTION {* operator *}
+SHORT   {* check whether one BDD implies another *}
+PROTO   {* int bdd_setxor(BDD l, BDD r) *}
+DESCR   {* Check wether $l$ implies $r$, or whether $r$ contains $l$. *}
+RETURN  {* 1 if $l$ implies $r$, 0 otherwise *}
+*/
+int bdd_implies(BDD l, BDD r)
+{
+  BddCacheData *entry;
+  int res;
+
+  if ((l == r) || ISZERO(l) || ISONE(r))
+    return 1;
+  if (ISONE(l) || ISZERO(r))
+    return 0;
+
+  entry = BddCache_lookup(&misccache, IMPLIESHASH(l,r));
+  if (entry->a == l &&  entry->b == r  && entry->c == CACHEID_IMPLIES)
+   {
+#ifdef CACHESTATS
+      bddcachestats.opHit++;
+#endif
+      return entry->r.res;
+   }
+#ifdef CACHESTATS
+   bddcachestats.opMiss++;
+#endif
+
+  if (LEVEL(l) == LEVEL(r))
+    {
+      res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(HIGH(l), HIGH(r));
+    }
+  else if (LEVEL(l) < LEVEL(r))
+    {
+      res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r);
+    }
+  else /* LEVEL(l) > LEVEL(r) */
+    {
+      res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r));
+    }
+
+  entry->a = l;
+  entry->b = r;
+  entry->c = CACHEID_IMPLIES;
+  entry->r.res = res;
+
+  return res;
+}
+
+
 
 /*=== ITE ==============================================================*/