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

[buddy] avoid costly calls to setjmp() when BDD_REORDER_NONE

Browse source 
* src/reorder.c, src/kernel.h: Expose bddreordermethod.
* src/bddop.c: Test bddreordermethod before ever calling setjmp().
This commit is contained in:
Alexandre Duret-Lutz 2016-11-09 11:03:24 +01:00
parent 2e6297c26a
commit 0ac14e9ca2
3 changed files with 26 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

33
buddy/src/bddop.c
View file

@ -415,7 +415,8 @@ BDD bdd_not(BDD r)
CHECKa(r, bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
@ -534,7 +535,8 @@ BDD bdd_apply(BDD l, BDD r, int op)
#endif
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
applyop = op;
@ -1001,7 +1003,8 @@ BDD bdd_ite(BDD f, BDD g, BDD h)
CHECKa(h, bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
@ -1177,7 +1180,8 @@ BDD bdd_restrict(BDD r, BDD var)
return r;
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
if (varset2svartable(var) < 0)
return bddfalse;
@ -1274,7 +1278,8 @@ BDD bdd_constrain(BDD f, BDD c)
CHECKa(c,bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
miscid = CACHEID_CONSTRAIN;
@ -1399,7 +1404,8 @@ BDD bdd_replace(BDD r, bddPair *pair)
CHECKa(r, bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
replacepair = pair->result;
@ -1534,7 +1540,8 @@ BDD bdd_compose(BDD f, BDD g, int var)
#endif
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE) ||
setjmp(bddexception) == 0)
{
INITREF;
composelevel = bddvar2level[var];
@ -1651,7 +1658,8 @@ BDD bdd_veccompose(BDD f, bddPair *pair)
CHECKa(f, bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE) ||
setjmp(bddexception) == 0)
{
INITREF;
replacepair = pair->result;
@ -1739,7 +1747,8 @@ BDD bdd_simplify(BDD f, BDD d)
CHECKa(d, bddfalse);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
INITREF;
applyop = bddop_or;
@ -1848,7 +1857,8 @@ static BDD quantify(BDD r, BDD var, int op, int comp, int id)
return r;
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
if (varset2vartable(var, comp) < 0)
return bddfalse;
@ -2039,7 +2049,8 @@ static BDD appquantify(BDD l, BDD r, int opr, BDD var,
return bdd_apply(l,r,opr);
again:
if (__likely(setjmp(bddexception) == 0))
if (__likely(bddreordermethod == BDD_REORDER_NONE)
|| setjmp(bddexception) == 0)
{
if (varset2vartable(var, comp) < 0)
return bddfalse;

3
buddy/src/kernel.h
View file

@ -132,6 +132,9 @@ extern int bddreorderdisabled;
extern int bddresized;
extern bddCacheStat bddcachestats;
/* from reorder.c */
extern int bddreordermethod;
#ifdef CPLUSPLUS
}
#endif

2
buddy/src/reorder.c
View file

@ -63,7 +63,7 @@
#define __USERESIZE /* FIXME */
/* Current auto reord. method and number of automatic reorderings left */
static int bddreordermethod;
int bddreordermethod;
static int bddreordertimes;
/* Flag for disabling reordering temporarily */