From 0fe54039561fcd48f6ce34a5c383b4ae1c425a14 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Jan 2010 15:55:08 +0100 Subject: [PATCH] Revert inlining of bdd_addref() and bdd_delref(). This reverts commit d462f50b5965d6deb7e611f2ead160a984e522b4. Conflicts: buddy/ChangeLog --- buddy/ChangeLog | 10 --- buddy/src/bdd.h | 200 +++++++++++---------------------------------- buddy/src/kernel.c | 54 ++++++++++++ buddy/src/kernel.h | 41 +++++++++- 4 files changed, 142 insertions(+), 163 deletions(-) diff --git a/buddy/ChangeLog b/buddy/ChangeLog index b13467e9d..0985d52bb 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -12,16 +12,6 @@ * src/bddio.c (bdd_load): Check the return value of fscanf() to kill a warning. -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 4ee6bb675..53dc3a6e1 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -80,158 +80,6 @@ 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 ===============================================*/ @@ -410,6 +258,8 @@ 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); @@ -526,6 +376,52 @@ 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 c1b9b0ad7..d4b45afb3 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -1100,6 +1100,60 @@ 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 e33ed8c29..580311724 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -1,5 +1,5 @@ /*======================================================================== - Copyright (C) 1996-2002, 2009 by Jorn Lind-Nielsen + Copyright (C) 1996-2002 by Jorn Lind-Nielsen All rights reserved Permission is hereby granted, without written agreement and without @@ -77,15 +77,31 @@ { 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 */ @@ -103,6 +119,16 @@ 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 */ @@ -120,6 +146,18 @@ 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) @@ -151,6 +189,7 @@ 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);