From 3aef5f31c09040e1c0b58e23a7f774310e953e85 Mon Sep 17 00:00:00 2001
From: philipp <philipp@lrde.epita.fr>
Date: Tue, 3 Aug 2021 11:37:48 +0200
Subject: [PATCH] [buddy] Adding bdd_is_cube

bdd_is_cube determines whether or not a given bdd
represents a cube.

* src/bddop.c: Here
* src/bddx.h: And here
---
 buddy/src/bddop.c | 37 +++++++++++++++++++++++++++++++++++++
 buddy/src/bddx.h  |  5 +++++
 2 files changed, 42 insertions(+)

diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c
index a05152c6d..fb2be011d 100644
--- a/buddy/src/bddop.c
+++ b/buddy/src/bddop.c
@@ -3798,6 +3798,43 @@ int bdd_have_common_assignment(BDD left, BDD right)
   return res;
 }
 
+/*=== DECIDE IF A BDD is a cube ================*/
+
+/*
+NAME    {* bdd\_is\_cube *}
+SECTION {* info *}
+SHORT   {* Decide if a bdd represents a cube *}
+PROTO   {* int bdd_is_cube(BDD b) *}
+DESCR   {* Returns 1 iff the given bdd is a conjunction of atomics and
+           negations of atomics. Returns 0 if input is false, 1
+           if input is true*}
+RETURN  {* 0 or 1 *}
+*/
+int bdd_is_cube(BDD b)
+{
+  if (ISZERO(b))
+    return 0;
+  if (ISONE(b))
+    return 0;
+
+  while (!ISONE(b))
+    {
+      BDD l = LOW(b);
+      BDD h = HIGH(b);
+
+      // Cube : high / low / do not care
+      if (!ISZERO(l) && !ISZERO(h))
+        return 0;
+
+      if (!ISZERO(l))
+        b = l;
+      else
+        b = h;
+    }
+
+  return 1;
+}
+
 /*************************************************************************
   Other internal functions
 *************************************************************************/
diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 174c5713b..0efd3a0a9 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -391,6 +391,7 @@ BUDDY_API int      bdd_anodecount(BDD *, int);
 BUDDY_API int*     bdd_varprofile(BDD);
 BUDDY_API double   bdd_pathcount(BDD);
 BUDDY_API int      bdd_have_common_assignment(BDD, BDD);
+BUDDY_API int      bdd_is_cube(BDD);
 
 /* In file "bddio.c" */
 
@@ -650,6 +651,7 @@ protected:
    friend int*     bdd_varprofile(const bdd &);
    friend double   bdd_pathcount(const bdd &);
    friend int      bdd_have_common_assignment(const bdd&, const bdd&);
+   friend int      bdd_is_cube(const bdd&);
 
    friend void   bdd_fprinttable(FILE *, const bdd &);
    friend void   bdd_printtable(const bdd &);
@@ -910,6 +912,9 @@ inline double bdd_pathcount(const bdd &r)
 inline int bdd_have_common_assignment(const bdd &l, const bdd &r)
 { return bdd_have_common_assignment(l.root, r.root); }
 
+inline int bdd_is_cube(const bdd &b)
+{ return bdd_is_cube(b.root); }
+
 
    /* I/O extensions */