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

[buddy] fix bdd_has_common_assignement

Browse source 
* src/bddop.c, src/bddx.h (bdd_has_common_assignement): Rename as...
(bdd_have_common_assignment): ... this, and fix level comparisons.
Also add a cache.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-30 11:16:39 +02:00
parent af511707c0
commit dfd168b048
2 changed files with 43 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

56
buddy/src/bddop.c
View file

@ -1,5 +1,5 @@
/*======================================================================== /*========================================================================
Copyright (C) 1996-2004 by Jorn Lind-Nielsen Copyright (C) 1996-2004, 2021 by Jorn Lind-Nielsen
All rights reserved All rights reserved
Permission is hereby granted, without written agreement and without Permission is hereby granted, without written agreement and without
@ -60,6 +60,7 @@
#define CACHEID_SETXOR 0x5 #define CACHEID_SETXOR 0x5
#define CACHEID_SUPPORT 0x6 #define CACHEID_SUPPORT 0x6
#define CACHEID_IMPLIES 0x7 #define CACHEID_IMPLIES 0x7
#define CACHEID_COMMON 0x8
/* Hash value modifiers for replace/compose */ /* Hash value modifiers for replace/compose */
#define CACHEID_REPLACE 0x0 #define CACHEID_REPLACE 0x0
@ -170,6 +171,7 @@ static int varset2svartable(BDD);
#define ITEHASH(f,g,h) (TRIPLE(f,g,h)) #define ITEHASH(f,g,h) (TRIPLE(f,g,h))
#define SETXORHASH(l,r) (TRIPLE(l,r,CACHEID_SETXOR)) #define SETXORHASH(l,r) (TRIPLE(l,r,CACHEID_SETXOR))
#define IMPLIESHASH(l,r) (TRIPLE(l,r,CACHEID_IMPLIES)) #define IMPLIESHASH(l,r) (TRIPLE(l,r,CACHEID_IMPLIES))
#define COMMONHASH(l,r) (TRIPLE(l,r,CACHEID_COMMON))
#define RESTRHASH(r,var) (PAIR(r,var)) #define RESTRHASH(r,var) (PAIR(r,var))
#define CONSTRAINHASH(f,c) (PAIR(f,c)) #define CONSTRAINHASH(f,c) (PAIR(f,c))
#define QUANTHASH(r) (r) #define QUANTHASH(r) (r)
@ -3586,43 +3588,63 @@ static double bdd_pathcount_rec(BDD r)
return size; return size;
} }
/*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNEMENT ================*/ /*=== DECIDE IF TWO BDDS SHARE AT LEAST ONE ASSIGNMENT ================*/
/* /*
NAME {* bdd\_has\_common\_assignement *} NAME {* bdd\_have\_common\_assignment *}
SECTION {* info *} SECTION {* info *}
SHORT {* Decide if two bdds share an accepted assignement *} SHORT {* Decide if two bdds share an satisfying assignement *}
PROTO {* int bdd_has_common_assignement(BDD l, BDD r) *} PROTO {* int bdd_have_common_assignment(BDD l, BDD r) *}
DESCR {* Returns 1 iff l&r != bddfalse *} DESCR {* Returns 1 iff l&r != bddfalse *}
RETURN {* 0 or 1 *} RETURN {* 0 or 1 *}
*/ */
int bdd_has_common_assignement(BDD left, BDD right) int bdd_have_common_assignment(BDD left, BDD right)
{ {
// If one of them is false -> false // If one of them is false -> false
if (left == 0 || right == 0) if (ISZERO(left) || ISZERO(right))
return 0; return 0;
// If one of them is true and the other is not false // If one of them is true and the other is not false
// or if they are identical -> true // or if they are identical -> true
if (left == 1 || right == 1 || left == right) if (ISONE(left) || ISONE(right) || left == right)
return 1; return 1;
// Now both of them are not constant // Now both of them are not constant
// Do they share the top variable? BddCacheData *entry = BddCache_lookup(&misccache, COMMONHASH(left,right));
int vl = bddlevel2var[LEVEL(left)]; /* Check entry->b last, because not_rec() does not initialize it. */
int vr = bddlevel2var[LEVEL(right)]; if (entry->i.a == left && entry->i.c == CACHEID_COMMON && entry->i.b == right)
{
#ifdef CACHESTATS
bddcachestats.opHit++;
#endif
return entry->i.res;
}
#ifdef CACHESTATS
bddcachestats.opMiss++;
#endif
// Do they share the top variable?
int vl = LEVEL(left);
int vr = LEVEL(right);
int res;
if (vl < vr) if (vl < vr)
// left has to "catch up" // left has to "catch up"
return bdd_has_common_assignement(LOW(left), right) res = (bdd_have_common_assignment(LOW(left), right)
|| bdd_has_common_assignement(HIGH(left), right); || bdd_have_common_assignment(HIGH(left), right));
else if (vr < vl) else if (vr < vl)
// right has to "catch up" // right has to "catch up"
return bdd_has_common_assignement(left, LOW(right)) res = (bdd_have_common_assignment(left, LOW(right))
|| bdd_has_common_assignement(left, HIGH(right)); || bdd_have_common_assignment(left, HIGH(right)));
else else
// They evolve jointly // They evolve jointly
return bdd_has_common_assignement(LOW(left), LOW(right)) res = (bdd_have_common_assignment(LOW(left), LOW(right))
|| bdd_has_common_assignement(HIGH(left), HIGH(right)); || bdd_have_common_assignment(HIGH(left), HIGH(right)));
entry->i.a = left;
entry->i.c = CACHEID_COMMON;
entry->i.b = right;
entry->i.res = res;
return res;
} }
/************************************************************************* /*************************************************************************

8
buddy/src/bddx.h
View file

@ -389,7 +389,7 @@ BUDDY_API int bdd_nodecount(BDD);
BUDDY_API int bdd_anodecount(BDD *, int); BUDDY_API int bdd_anodecount(BDD *, int);
BUDDY_API int* bdd_varprofile(BDD); BUDDY_API int* bdd_varprofile(BDD);
BUDDY_API double bdd_pathcount(BDD); BUDDY_API double bdd_pathcount(BDD);
BUDDY_API int bdd_has_common_assignement(BDD, BDD); BUDDY_API int bdd_have_common_assignment(BDD, BDD);
/* In file "bddio.c" */ /* In file "bddio.c" */
@ -646,7 +646,7 @@ protected:
friend int bdd_anodecountpp(const bdd *, int); friend int bdd_anodecountpp(const bdd *, int);
friend int* bdd_varprofile(const bdd &); friend int* bdd_varprofile(const bdd &);
friend double bdd_pathcount(const bdd &); friend double bdd_pathcount(const bdd &);
friend int bdd_has_common_assignement(const bdd&, const bdd&); friend int bdd_have_common_assignment(const bdd&, const bdd&);
friend void bdd_fprinttable(FILE *, const bdd &); friend void bdd_fprinttable(FILE *, const bdd &);
friend void bdd_printtable(const bdd &); friend void bdd_printtable(const bdd &);
@ -898,8 +898,8 @@ inline int* bdd_varprofile(const bdd &r)
inline double bdd_pathcount(const bdd &r) inline double bdd_pathcount(const bdd &r)
{ return bdd_pathcount(r.root); } { return bdd_pathcount(r.root); }
inline int bdd_has_common_assignement(const bdd &l, const bdd &r) inline int bdd_have_common_assignment(const bdd &l, const bdd &r)
{ return bdd_has_common_assignement(l.root, r.root); } { return bdd_have_common_assignment(l.root, r.root); }
/* I/O extensions */ /* I/O extensions */