From 253ee35030efc09ee230971bcacb642c2fe46e61 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Nov 2009 21:32:13 +0100 Subject: [PATCH] [buddy] Introduce bdd_satprefix, to speedup spot::minato(). * src/bdd.h (bdd_satprefix): New function. * src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions. --- buddy/ChangeLog | 7 ++++++ buddy/src/bdd.h | 5 ++++ buddy/src/bddop.c | 61 ++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 70 insertions(+), 3 deletions(-) diff --git a/buddy/ChangeLog b/buddy/ChangeLog index a40dc3e20..8833b44f5 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,10 @@ +2009-11-23 Alexandre Duret-Lutz + + Introduce bdd_satprefix, to speedup spot::minato(). + + * src/bdd.h (bdd_satprefix): New function. + * src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions. + 2009-10-01 Alexandre Duret-Lutz Fix the previous patch in reorder.c: I missread the diff --git a/buddy/src/bdd.h b/buddy/src/bdd.h index 26cf1f5ef..53dc3a6e1 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -308,6 +308,7 @@ extern BDD bdd_support(BDD); extern BDD bdd_satone(BDD); extern BDD bdd_satoneset(BDD, BDD, BDD); extern BDD bdd_fullsatone(BDD); +extern BDD bdd_satprefix(BDD *); extern void bdd_allsat(BDD r, bddallsathandler handler); extern double bdd_satcount(BDD); extern double bdd_satcountset(BDD, BDD); @@ -513,6 +514,7 @@ private: friend bdd bdd_satone(const bdd &); friend bdd bdd_satoneset(const bdd &, const bdd &, const bdd &); friend bdd bdd_fullsatone(const bdd &); + friend bdd bdd_satprefix(bdd &); friend void bdd_allsat(const bdd &r, bddallsathandler handler); friend double bdd_satcount(const bdd &); friend double bdd_satcountset(const bdd &, const bdd &); @@ -698,6 +700,9 @@ inline bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol) inline bdd bdd_fullsatone(const bdd &r) { return bdd_fullsatone(r.root); } +inline bdd bdd_satprefix(bdd &r) +{ int ro = r.root; bdd res = bdd_satprefix(&ro); r = bdd(ro); return res; } + inline void bdd_allsat(const bdd &r, bddallsathandler handler) { bdd_allsat(r.root, handler); } diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index cd54dc05f..420579295 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -142,6 +142,7 @@ static void support_rec(int, int*); static BDD satone_rec(BDD); static BDD satoneset_rec(BDD, BDD); static int fullsatone_rec(int); +static BDD satprefix_rec(BDD*); static void allsat_rec(BDD r); static double satcount_rec(int); static double satcountln_rec(int); @@ -2124,7 +2125,7 @@ PROTO {* BDD bdd_satone(BDD r) *} DESCR {* Finds a BDD with at most one variable at each level. This BDD implies {\tt r} and is not false unless {\tt r} is false. *} -ALSO {* bdd\_allsat bdd\_satoneset, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} +ALSO {* bdd\_allsat, bdd\_satoneset, bdd\_satprefix, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} RETURN {* The result of the operation. *} */ BDD bdd_satone(BDD r) @@ -2165,6 +2166,60 @@ static BDD satone_rec(BDD r) } +/* +NAME {* bdd\_satprefix *} +SECTION {* operator *} +SHORT {* quickly remove a conjunction common to all satisfying assignments *} +PROTO {* BDD bdd_satprefix(BDD* r) *} +DESCR {* Recursively descend into the top of the BDD and return the + prefix common to all satisfying paths. Adjust r to point to + the rest of the BDD. *} +ALSO {* bdd\_allsat, bdd\_satone, bdd\_satoneset, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} +RETURN {* The result of the operation. *} +*/ +BDD bdd_satprefix(BDD* r) +{ + BDD res; + + CHECKa(*r, bddfalse); + if (*r < 2) + return *r; + + bdd_disable_reorder(); + + INITREF; + res = satprefix_rec(r); + + bdd_enable_reorder(); + + checkresize(); + return res; + +} + +static BDD satprefix_rec(BDD* r) +{ + if (ISCONST(*r)) + return *r; + + if (ISZERO(LOW(*r))) + { + int lr = LEVEL(*r); + *r = HIGH(*r); + return PUSHREF(bdd_makenode(lr, BDDZERO, satprefix_rec(r))); + } + else if (ISZERO(HIGH(*r))) + { + int lr = LEVEL(*r); + *r = LOW(*r); + return PUSHREF(bdd_makenode(lr, satprefix_rec(r), BDDZERO)); + } + else + { + return BDDONE; + } +} + /* NAME {* bdd\_satoneset *} SECTION {* operator *} @@ -2177,7 +2232,7 @@ DESCR {* Finds a minterm in {\tt r}. The {\tt var} argument is a by the {\tt pol} parameter. If {\tt pol} is the false BDD then the variables will be in negative form, and otherwise they will be in positive form. *} -ALSO {* bdd\_allsat bdd\_satone, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} +ALSO {* bdd\_allsat, bdd\_satone, bdd\_satprefix, bdd\_fullsatone, bdd\_satcount, bdd\_satcountln *} RETURN {* The result of the operation. *} */ BDD bdd_satoneset(BDD r, BDD var, BDD pol) @@ -2259,7 +2314,7 @@ PROTO {* BDD bdd_fullsatone(BDD r) *} DESCR {* Finds a BDD with exactly one variable at all levels. This BDD implies {\tt r} and is not false unless {\tt r} is false. *} -ALSO {* bdd\_allsat bdd\_satone, bdd\_satoneset, bdd\_satcount, bdd\_satcountln *} +ALSO {* bdd\_allsat, bdd\_satone, bdd\_satprefix, bdd\_satoneset, bdd\_satcount, bdd\_satcountln *} RETURN {* The result of the operation. *} */ BDD bdd_fullsatone(BDD r)