alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] Adding bdd_is_cube

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

* src/bddop.c: Here
* src/bddx.h: And here
This commit is contained in:
philipp 2021-08-03 11:37:48 +02:00 • committed by Florian Renkin
parent 5a0fbf6cb9
commit 3aef5f31c0
2 changed files with 42 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

37
buddy/src/bddop.c
View file

@ -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
*************************************************************************/

5
buddy/src/bddx.h
View file

@ -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 */