diff --git a/buddy/ChangeLog b/buddy/ChangeLog index 8833b44f5..19934f202 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,13 @@ +2009-12-09 Alexandre Duret-Lutz + + Inline bdd_addref() and bdd_delref() to speedup BDD operations. + + * src/kernel.c, src/kernel.h (bdd_addref, bdd_delref): Move these + functions and there associated global variables... + * src/bdd.c (bdd_error): ... and this function ... + * src/bdd.h (bdd_addref, bdd_delref, bdd_error): ...here so that + they can be inlined. + 2009-11-23 Alexandre Duret-Lutz Introduce bdd_satprefix, to speedup spot::minato(). diff --git a/buddy/src/bdd.h b/buddy/src/bdd.h index 53dc3a6e1..4ee6bb675 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -80,6 +80,158 @@ typedef struct s_bddPair struct s_bddPair *next; } bddPair; +/*=== Reordering algorithms ============================================*/ + +#define BDD_REORDER_NONE 0 +#define BDD_REORDER_WIN2 1 +#define BDD_REORDER_WIN2ITE 2 +#define BDD_REORDER_SIFT 3 +#define BDD_REORDER_SIFTITE 4 +#define BDD_REORDER_WIN3 5 +#define BDD_REORDER_WIN3ITE 6 +#define BDD_REORDER_RANDOM 7 + +#define BDD_REORDER_FREE 0 +#define BDD_REORDER_FIXED 1 + + +/*=== Error codes ======================================================*/ + +#define BDD_MEMORY (-1) /* Out of memory */ +#define BDD_VAR (-2) /* Unknown variable */ +#define BDD_RANGE (-3) /* Variable value out of range (not in domain) */ +#define BDD_DEREF (-4) /* Removing external reference to unknown node */ +#define BDD_RUNNING (-5) /* Called bdd_init() twice whithout bdd_done() */ +#define BDD_FILE (-6) /* Some file operation failed */ +#define BDD_FORMAT (-7) /* Incorrect file format */ +#define BDD_ORDER (-8) /* Vars. not in order for vector based functions */ +#define BDD_BREAK (-9) /* User called break */ +#define BDD_VARNUM (-10) /* Different number of vars. for vector pair */ +#define BDD_NODES (-11) /* Tried to set max. number of nodes to be fewer */ + /* than there already has been allocated */ +#define BDD_OP (-12) /* Unknown operator */ +#define BDD_VARSET (-13) /* Illegal variable set */ +#define BDD_VARBLK (-14) /* Bad variable block operation */ +#define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */ +#define BDD_REPLACE (-16) /* Replacing to already existing variables */ +#define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */ +#define BDD_ILLBDD (-18) /* Illegal bdd argument */ +#define BDD_SIZE (-19) /* Illegal size argument */ + +#define BVEC_SIZE (-20) /* Mismatch in bitvector size */ +#define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */ +#define BVEC_DIVZERO (-22) /* Division by zero */ + +#define BDD_INVMERGE (-23) /* Merging clashing rewriting rules */ + +#define BDD_ERRNUM 25 + +#ifdef CPLUSPLUS +extern "C" { +#endif + +/* In kernel.c */ +extern int bdd_error(int); + + +/*=== SEMI-INTERNAL TYPES ==============================================*/ + +typedef struct s_BddNode /* Node table entry */ +{ + unsigned int refcou : 10; + unsigned int level : 22; + int low; + int high; + int hash; + int next; +} BddNode; + +#define MAXVAR 0x1FFFFF +#define MAXREF 0x3FF + + /* Reference counting */ +#define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou-- +#define INCREF(n) if (bddnodes[n].refcourefcou!=MAXREF && n->refcou>0) n->refcou-- +#define INCREFp(n) if (n->refcourefcou++ +#define HASREF(n) (bddnodes[n].refcou > 0) + +extern int bddrunning; /* Flag - package initialized */ +extern int bddnodesize; /* Number of allocated nodes */ +extern BddNode* bddnodes; /* All of the bdd nodes */ + + /* Inspection of BDD nodes */ +#define ISCONST(a) ((a) < 2) +#define ISNONCONST(a) ((a) >= 2) +#define ISONE(a) ((a) == 1) +#define ISZERO(a) ((a) == 0) +#define LEVEL(a) (bddnodes[a].level) +#define LOW(a) (bddnodes[a].low) +#define HIGH(a) (bddnodes[a].high) +#define LEVELp(p) ((p)->level) +#define LOWp(p) ((p)->low) +#define HIGHp(p) ((p)->high) + +/* +NAME {* bdd\_addref *} +SECTION {* kernel *} +SHORT {* increases the reference count on a node *} +PROTO {* BDD bdd_addref(BDD r) *} +DESCR {* Reference counting is done on externaly referenced nodes only + and the count for a specific node {\tt r} can and must be + increased using this function to avoid loosing the node in the next + garbage collection. *} +ALSO {* bdd\_delref *} +RETURN {* The BDD node {\tt r}. *} +*/ +static inline +BDD bdd_addref(BDD root) +{ + if (root < 2 || !bddrunning) + return root; + if (root >= bddnodesize) + return bdd_error(BDD_ILLBDD); + if (LOW(root) == -1) + return bdd_error(BDD_ILLBDD); + + INCREF(root); + return root; +} + + +/* +NAME {* bdd\_delref *} +SECTION {* kernel *} +SHORT {* decreases the reference count on a node *} +PROTO {* BDD bdd_delref(BDD r) *} +DESCR {* Reference counting is done on externaly referenced nodes only + and the count for a specific node {\tt r} can and must be + decreased using this function to make it possible to reclaim the + node in the next garbage collection. *} +ALSO {* bdd\_addref *} +RETURN {* The BDD node {\tt r}. *} +*/ +static inline +BDD bdd_delref(BDD root) +{ + if (root < 2 || !bddrunning) + return root; + if (root >= bddnodesize) + return bdd_error(BDD_ILLBDD); + if (LOW(root) == -1) + return bdd_error(BDD_ILLBDD); + + /* if the following line is present, fails there much earlier */ + if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */ + + DECREF(root); + return root; +} + +#ifdef CPLUSPLUS +} +#endif + /*=== Status information ===============================================*/ @@ -258,8 +410,6 @@ extern int bdd_var(BDD); extern BDD bdd_low(BDD); extern BDD bdd_high(BDD); extern int bdd_varlevel(int); -extern BDD bdd_addref(BDD); -extern BDD bdd_delref(BDD); extern void bdd_gbc(void); extern int bdd_scanset(BDD, int**, int*); extern BDD bdd_makeset(int *, int); @@ -376,52 +526,6 @@ extern const BDD bddtrue; #endif /* CPLUSPLUS */ -/*=== Reordering algorithms ============================================*/ - -#define BDD_REORDER_NONE 0 -#define BDD_REORDER_WIN2 1 -#define BDD_REORDER_WIN2ITE 2 -#define BDD_REORDER_SIFT 3 -#define BDD_REORDER_SIFTITE 4 -#define BDD_REORDER_WIN3 5 -#define BDD_REORDER_WIN3ITE 6 -#define BDD_REORDER_RANDOM 7 - -#define BDD_REORDER_FREE 0 -#define BDD_REORDER_FIXED 1 - - -/*=== Error codes ======================================================*/ - -#define BDD_MEMORY (-1) /* Out of memory */ -#define BDD_VAR (-2) /* Unknown variable */ -#define BDD_RANGE (-3) /* Variable value out of range (not in domain) */ -#define BDD_DEREF (-4) /* Removing external reference to unknown node */ -#define BDD_RUNNING (-5) /* Called bdd_init() twice whithout bdd_done() */ -#define BDD_FILE (-6) /* Some file operation failed */ -#define BDD_FORMAT (-7) /* Incorrect file format */ -#define BDD_ORDER (-8) /* Vars. not in order for vector based functions */ -#define BDD_BREAK (-9) /* User called break */ -#define BDD_VARNUM (-10) /* Different number of vars. for vector pair */ -#define BDD_NODES (-11) /* Tried to set max. number of nodes to be fewer */ - /* than there already has been allocated */ -#define BDD_OP (-12) /* Unknown operator */ -#define BDD_VARSET (-13) /* Illegal variable set */ -#define BDD_VARBLK (-14) /* Bad variable block operation */ -#define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */ -#define BDD_REPLACE (-16) /* Replacing to already existing variables */ -#define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */ -#define BDD_ILLBDD (-18) /* Illegal bdd argument */ -#define BDD_SIZE (-19) /* Illegal size argument */ - -#define BVEC_SIZE (-20) /* Mismatch in bitvector size */ -#define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */ -#define BVEC_DIVZERO (-22) /* Division by zero */ - -#define BDD_INVMERGE (-23) /* Merging clashing rewriting rules */ - -#define BDD_ERRNUM 25 - /************************************************************************* If this file is included from a C++ compiler then the following classes, wrappers and hacks are supplied. diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c index d4b45afb3..c1b9b0ad7 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -1100,60 +1100,6 @@ void bdd_gbc(void) } -/* -NAME {* bdd\_addref *} -SECTION {* kernel *} -SHORT {* increases the reference count on a node *} -PROTO {* BDD bdd_addref(BDD r) *} -DESCR {* Reference counting is done on externaly referenced nodes only - and the count for a specific node {\tt r} can and must be - increased using this function to avoid loosing the node in the next - garbage collection. *} -ALSO {* bdd\_delref *} -RETURN {* The BDD node {\tt r}. *} -*/ -BDD bdd_addref(BDD root) -{ - if (root < 2 || !bddrunning) - return root; - if (root >= bddnodesize) - return bdd_error(BDD_ILLBDD); - if (LOW(root) == -1) - return bdd_error(BDD_ILLBDD); - - INCREF(root); - return root; -} - - -/* -NAME {* bdd\_delref *} -SECTION {* kernel *} -SHORT {* decreases the reference count on a node *} -PROTO {* BDD bdd_delref(BDD r) *} -DESCR {* Reference counting is done on externaly referenced nodes only - and the count for a specific node {\tt r} can and must be - decreased using this function to make it possible to reclaim the - node in the next garbage collection. *} -ALSO {* bdd\_addref *} -RETURN {* The BDD node {\tt r}. *} -*/ -BDD bdd_delref(BDD root) -{ - if (root < 2 || !bddrunning) - return root; - if (root >= bddnodesize) - return bdd_error(BDD_ILLBDD); - if (LOW(root) == -1) - return bdd_error(BDD_ILLBDD); - - /* if the following line is present, fails there much earlier */ - if (!HASREF(root)) bdd_error(BDD_BREAK); /* distinctive */ - - DECREF(root); - return root; -} - /*=== RECURSIVE MARK / UNMARK ==========================================*/ diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h index 580311724..e33ed8c29 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -1,5 +1,5 @@ /*======================================================================== - Copyright (C) 1996-2002 by Jorn Lind-Nielsen + Copyright (C) 1996-2002, 2009 by Jorn Lind-Nielsen All rights reserved Permission is hereby granted, without written agreement and without @@ -77,31 +77,15 @@ { bdd_error(BDD_ILLBDD); return; } -/*=== SEMI-INTERNAL TYPES ==============================================*/ - -typedef struct s_BddNode /* Node table entry */ -{ - unsigned int refcou : 10; - unsigned int level : 22; - int low; - int high; - int hash; - int next; -} BddNode; - - /*=== KERNEL VARIABLES =================================================*/ #ifdef CPLUSPLUS extern "C" { #endif -extern int bddrunning; /* Flag - package initialized */ extern int bdderrorcond; /* Some error condition was met */ -extern int bddnodesize; /* Number of allocated nodes */ extern int bddmaxnodesize; /* Maximum allowed number of nodes */ extern int bddmaxnodeincrease; /* Max. # of nodes used to inc. table */ -extern BddNode* bddnodes; /* All of the bdd nodes */ extern int bddvarnum; /* Number of defined BDD variables */ extern int* bddrefstack; /* Internal node reference stack */ extern int* bddrefstacktop; /* Internal node reference stack top */ @@ -119,16 +103,6 @@ extern bddCacheStat bddcachestats; /*=== KERNEL DEFINITIONS ===============================================*/ -#define MAXVAR 0x1FFFFF -#define MAXREF 0x3FF - - /* Reference counting */ -#define DECREF(n) if (bddnodes[n].refcou!=MAXREF && bddnodes[n].refcou>0) bddnodes[n].refcou-- -#define INCREF(n) if (bddnodes[n].refcourefcou!=MAXREF && n->refcou>0) n->refcou-- -#define INCREFp(n) if (n->refcourefcou++ -#define HASREF(n) (bddnodes[n].refcou > 0) - /* Marking BDD nodes */ #define MARKON 0x200000 /* Bit used to mark a node (1) */ #define MARKOFF 0x1FFFFF /* - unmark */ @@ -146,18 +120,6 @@ extern bddCacheStat bddcachestats; #define TRIPLE(a,b,c) ((unsigned int)(PAIR((unsigned int)c,PAIR(a,b)))) - /* Inspection of BDD nodes */ -#define ISCONST(a) ((a) < 2) -#define ISNONCONST(a) ((a) >= 2) -#define ISONE(a) ((a) == 1) -#define ISZERO(a) ((a) == 0) -#define LEVEL(a) (bddnodes[a].level) -#define LOW(a) (bddnodes[a].low) -#define HIGH(a) (bddnodes[a].high) -#define LEVELp(p) ((p)->level) -#define LOWp(p) ((p)->low) -#define HIGHp(p) ((p)->high) - /* Stacking for garbage collector */ #define INITREF bddrefstacktop = bddrefstack #define PUSHREF(a) *(bddrefstacktop++) = (a) @@ -189,7 +151,6 @@ extern bddCacheStat bddcachestats; extern "C" { #endif -extern int bdd_error(int); extern int bdd_makenode(unsigned int, int, int); extern int bdd_noderesize(int); extern void bdd_checkreorder(void);