From 1d1872ab90a511b9f3fed780299ec752a0fd14a2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 30 Apr 2011 13:37:53 +0200 Subject: [PATCH] [buddy] Inline the "is bdd constant" check performed in copies/constructors. This avoids a library call to bdd_addref or bdd_delref. * src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function, that work only on BDD that are not constant. * src/cpext.cxx (bdd::operator=): Move... * src/bdd.hh (bdd::operator=): ... here. (bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant" check and call bdd_delref_nc/bdd_addref_nc only otherwise. --- buddy/ChangeLog | 13 +++++++ buddy/src/bdd.h | 34 ++++++++++++++++-- buddy/src/cppext.cxx | 85 +++++++++++++++----------------------------- buddy/src/kernel.c | 31 ++++++++++++++++ 4 files changed, 104 insertions(+), 59 deletions(-) diff --git a/buddy/ChangeLog b/buddy/ChangeLog index a943c378c..b76203606 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,16 @@ +2011-04-30 Alexandre Duret-Lutz + + Inline the "is bdd constant" check performed in copies/constructors. + + This avoids a library call to bdd_addref or bdd_delref. + + * src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function, + that work only on BDD that are not constant. + * src/cpext.cxx (bdd::operator=): Move... + * src/bdd.hh (bdd::operator=): ... here. + (bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant" + check and call bdd_delref_nc/bdd_addref_nc only otherwise. + 2011-04-30 Alexandre Duret-Lutz Hint gcc about likely/unlikely branches. diff --git a/buddy/src/bdd.h b/buddy/src/bdd.h index ef7154f04..af5fb30cf 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -272,7 +272,9 @@ extern int bdd_var(BDD) __purefn; extern BDD bdd_low(BDD) __purefn; extern BDD bdd_high(BDD) __purefn; extern int bdd_varlevel(int) __purefn; +extern BDD bdd_addref_nc(BDD); extern BDD bdd_addref(BDD); +extern BDD bdd_delref_nc(BDD); extern BDD bdd_delref(BDD); extern void bdd_gbc(void); extern int bdd_scanset(BDD, int**, int*); @@ -453,8 +455,8 @@ class bdd public: bdd(void) { root=0; } - bdd(const bdd &r) { bdd_addref(root=r.root); } - ~bdd(void) { bdd_delref(root); } + bdd(const bdd &r) { root=r.root; if (root > 1) bdd_addref_nc(root); } + ~bdd(void) { if (root > 1) bdd_delref_nc(root); } int id(void) const; @@ -481,7 +483,7 @@ class bdd private: BDD root; - bdd(BDD r) { bdd_addref(root=r); } + bdd(BDD r) { root=r; if (root > 1) bdd_addref_nc(root); } bdd operator=(BDD r); friend int bdd_init(int, int); @@ -849,6 +851,32 @@ inline int bdd::operator==(const bdd &r) const inline int bdd::operator!=(const bdd &r) const { return r.root!=root; } +inline bdd bdd::operator=(const bdd &r) +{ + if (__likely(root != r.root)) + { + if (root > 1) + bdd_delref_nc(root); + root = r.root; + if (root > 1) + bdd_addref_nc(root); + } + return *this; +} + +inline bdd bdd::operator=(int r) +{ + if (__likely(root != r)) + { + if (root > 1) + bdd_delref_nc(root); + root = r; + if (root > 1) + bdd_addref_nc(root); + } + return *this; +} + inline bdd bdd_true(void) { return 1; } diff --git a/buddy/src/cppext.cxx b/buddy/src/cppext.cxx index a3110fb4f..e0d2102ce 100644 --- a/buddy/src/cppext.cxx +++ b/buddy/src/cppext.cxx @@ -81,7 +81,7 @@ static bddstrmhandler strmhandler_fdd; int bdd_cpp_init(int n, int c) { int ok = bdd_init(n,c); - + strmhandler_bdd = NULL; strmhandler_fdd = NULL; @@ -115,11 +115,11 @@ int bdd_setbddpairs(bddPair *pair, int *oldvar, const bdd *newvar, int size) { if (pair == NULL) return 0; - + for (int n=0,e=0 ; n 0) @@ -386,10 +359,10 @@ static void bdd_printset_rec(ostream& o, int r, int* set) { set[LEVEL(r)] = 1; bdd_printset_rec(o, LOW(r), set); - + set[LEVEL(r)] = 2; bdd_printset_rec(o, HIGH(r), set); - + set[LEVEL(r)] = 0; } } @@ -410,7 +383,7 @@ static void bdd_printdot_rec(ostream& o, int r) o << r << " -> " << HIGH(r) << "[style=filled];\n"; SETMARK(r); - + bdd_printdot_rec(o, LOW(r)); bdd_printdot_rec(o, HIGH(r)); } @@ -422,7 +395,7 @@ static void fdd_printset_rec(ostream &o, int r, int *set) int used = 0; int *binval; int ok, first; - + if (r == 0) return; else @@ -431,18 +404,18 @@ static void fdd_printset_rec(ostream &o, int r, int *set) o << "<"; first=1; int fdvarnum = fdd_domainnum(); - + for (n=0 ; n= bddnodesize) + return bdd_error(BDD_ILLBDD); + if (LOW(root) == -1) + return bdd_error(BDD_ILLBDD); +#endif + INCREF(root); + return root; +} + /* NAME {* bdd\_addref *} SECTION {* kernel *} @@ -1131,6 +1145,23 @@ BDD bdd_addref(BDD root) return root; } +// Non constant version +BDD bdd_delref_nc(BDD root) +{ +#ifndef NDEBUG + 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 */ +#endif + DECREF(root); + return root; +} /* NAME {* bdd\_delref *}