From 92239d8242edc106cfc5cb87cd45939ed83f70f8 Mon Sep 17 00:00:00 2001
From: philipp <philipp@lrde.epita.fr>
Date: Mon, 21 Jun 2021 14:31:11 +0200
Subject: [PATCH] [buddy] Adding bdd_has_common_assignement

bdd_has_common_assignement determines if two bdds a and b
have (at least) one common assignement.
That is it will return true iff bdd_and(a, b) != bddfalse.

* src/bddx.h: Here
* src/bddop.c: Here
---
 buddy/src/bddop.c | 38 ++++++++++++++++++++++++++++++++++++++
 buddy/src/bddx.h  |  6 +++++-
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c
index fd8a06104..44b3dc34b 100644
--- a/buddy/src/bddop.c
+++ b/buddy/src/bddop.c
@@ -3586,6 +3586,44 @@ static double bdd_pathcount_rec(BDD r)
    return size;
 }
 
+/*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNEMENT ================*/
+
+/*
+NAME    {* bdd\_has\_common\_assignement *}
+SECTION {* info *}
+SHORT   {* Decide if two bdds share an accepted assignement *}
+PROTO   {* int bdd_has_common_assignement(BDD l, BDD r) *}
+DESCR   {* Returns 1 iff l&r != bddfalse *}
+RETURN  {* 0 or 1 *}
+*/
+int bdd_has_common_assignement(BDD left, BDD right)
+{
+  // If one of them is false -> false
+  if (left == 0 || right == 0)
+    return 0;
+  // If one of them is true and the other is not false
+  // or if they are identical -> true
+  if (left == 1 || right == 1 || left == right)
+    return 1;
+  // Now both of them are not constant
+
+  // Do they share the top variable?
+  int vl = bddlevel2var[LEVEL(left)];
+  int vr = bddlevel2var[LEVEL(right)];
+
+  if (vl < vr)
+    // left has to "catch up"
+    return bdd_has_common_assignement(LOW(left), right)
+           || bdd_has_common_assignement(HIGH(left), right);
+  else if (vr < vl)
+    // right has to "catch up"
+    return bdd_has_common_assignement(left, LOW(right))
+           || bdd_has_common_assignement(left, HIGH(right));
+  else
+    // They evolve jointly
+    return bdd_has_common_assignement(LOW(left), LOW(right))
+           || bdd_has_common_assignement(HIGH(left), HIGH(right));
+}
 
 /*************************************************************************
   Other internal functions
diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 4deef3497..98b0d3237 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -389,7 +389,7 @@ BUDDY_API int      bdd_nodecount(BDD);
 BUDDY_API int      bdd_anodecount(BDD *, int);
 BUDDY_API int*     bdd_varprofile(BDD);
 BUDDY_API double   bdd_pathcount(BDD);
-
+BUDDY_API int      bdd_has_common_assignement(BDD, BDD);
 
 /* In file "bddio.c" */
 
@@ -646,6 +646,7 @@ protected:
    friend int      bdd_anodecountpp(const bdd *, int);
    friend int*     bdd_varprofile(const bdd &);
    friend double   bdd_pathcount(const bdd &);
+   friend int      bdd_has_common_assignement(const bdd&, const bdd&);
 
    friend void   bdd_fprinttable(FILE *, const bdd &);
    friend void   bdd_printtable(const bdd &);
@@ -897,6 +898,9 @@ inline int* bdd_varprofile(const bdd &r)
 inline double bdd_pathcount(const bdd &r)
 { return bdd_pathcount(r.root); }
 
+inline int bdd_has_common_assignement(const bdd &l, const bdd &r)
+{ return bdd_has_common_assignement(l.root, r.root); }
+
 
    /* I/O extensions */