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

[buddy] slight optimization of bdd_implies

Browse source 
* src/bddop.c: Avoid the first recursion when it is obvious that the
second will fail.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-20 20:59:28 +02:00
parent 41866b370c
commit a32ccd649d
1 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

21
buddy/src/bddop.c
View file

@ -931,15 +931,30 @@ int bdd_implies(BDD l, BDD r)
if (LEVEL(l) == LEVEL(r)) if (LEVEL(l) == LEVEL(r))
{ {
res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(HIGH(l), HIGH(r)); int hl = HIGH(l);
int hr = HIGH(r);
// Avoid the recursion if the second implication will trivially
// fail.
if ((ISONE(hl) || ISZERO(hr)) && (hl != hr))
res = 0;
else
res = bdd_implies(LOW(l), LOW(r)) && bdd_implies(hl, hr);
} }
else if (LEVEL(l) < LEVEL(r)) else if (LEVEL(l) < LEVEL(r))
{ {
res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r); int hl = HIGH(l);
if (ISONE(hl) && (hl != r))
res = 0;
else
res = bdd_implies(LOW(l), r) && bdd_implies(HIGH(l), r);
} }
else /* LEVEL(l) > LEVEL(r) */ else /* LEVEL(l) > LEVEL(r) */
{ {
res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r)); int hr = HIGH(r);
if (ISZERO(hr) && (hr != r))
res = 0;
else
res = bdd_implies(l, LOW(r)) && bdd_implies(l, HIGH(r));
} }
entry->i.a = l; entry->i.a = l;