Commit 253ee350 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

[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.
parent 81e0872b
2009-11-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.net> 2009-10-01 Alexandre Duret-Lutz <adl@lrde.epita.net>
Fix the previous patch in reorder.c: I missread the Fix the previous patch in reorder.c: I missread the
......
...@@ -308,6 +308,7 @@ extern BDD bdd_support(BDD); ...@@ -308,6 +308,7 @@ extern BDD bdd_support(BDD);
extern BDD bdd_satone(BDD); extern BDD bdd_satone(BDD);
extern BDD bdd_satoneset(BDD, BDD, BDD); extern BDD bdd_satoneset(BDD, BDD, BDD);
extern BDD bdd_fullsatone(BDD); extern BDD bdd_fullsatone(BDD);
extern BDD bdd_satprefix(BDD *);
extern void bdd_allsat(BDD r, bddallsathandler handler); extern void bdd_allsat(BDD r, bddallsathandler handler);
extern double bdd_satcount(BDD); extern double bdd_satcount(BDD);
extern double bdd_satcountset(BDD, BDD); extern double bdd_satcountset(BDD, BDD);
...@@ -513,6 +514,7 @@ private: ...@@ -513,6 +514,7 @@ private:
friend bdd bdd_satone(const bdd &); friend bdd bdd_satone(const bdd &);
friend bdd bdd_satoneset(const bdd &, const bdd &, const bdd &); friend bdd bdd_satoneset(const bdd &, const bdd &, const bdd &);
friend bdd bdd_fullsatone(const bdd &); friend bdd bdd_fullsatone(const bdd &);
friend bdd bdd_satprefix(bdd &);
friend void bdd_allsat(const bdd &r, bddallsathandler handler); friend void bdd_allsat(const bdd &r, bddallsathandler handler);
friend double bdd_satcount(const bdd &); friend double bdd_satcount(const bdd &);
friend double bdd_satcountset(const bdd &, 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) ...@@ -698,6 +700,9 @@ inline bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol)
inline bdd bdd_fullsatone(const bdd &r) inline bdd bdd_fullsatone(const bdd &r)
{ return bdd_fullsatone(r.root); } { 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) inline void bdd_allsat(const bdd &r, bddallsathandler handler)
{ bdd_allsat(r.root, handler); } { bdd_allsat(r.root, handler); }
......
...@@ -142,6 +142,7 @@ static void support_rec(int, int*); ...@@ -142,6 +142,7 @@ static void support_rec(int, int*);
static BDD satone_rec(BDD); static BDD satone_rec(BDD);
static BDD satoneset_rec(BDD, BDD); static BDD satoneset_rec(BDD, BDD);
static int fullsatone_rec(int); static int fullsatone_rec(int);
static BDD satprefix_rec(BDD*);
static void allsat_rec(BDD r); static void allsat_rec(BDD r);
static double satcount_rec(int); static double satcount_rec(int);
static double satcountln_rec(int); static double satcountln_rec(int);
...@@ -2124,7 +2125,7 @@ PROTO {* BDD bdd_satone(BDD r) *} ...@@ -2124,7 +2125,7 @@ PROTO {* BDD bdd_satone(BDD r) *}
DESCR {* Finds a BDD with at most one variable at each level. This BDD 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 implies {\tt r} and is not false unless {\tt r} is
false. *} 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. *} RETURN {* The result of the operation. *}
*/ */
BDD bdd_satone(BDD r) BDD bdd_satone(BDD r)
...@@ -2165,6 +2166,60 @@ static BDD satone_rec(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 *} NAME {* bdd\_satoneset *}
SECTION {* operator *} SECTION {* operator *}
...@@ -2177,7 +2232,7 @@ DESCR {* Finds a minterm in {\tt r}. The {\tt var} argument is a ...@@ -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 by the {\tt pol} parameter. If {\tt pol} is the false BDD then
the variables will be in negative form, and otherwise they will the variables will be in negative form, and otherwise they will
be in positive form. *} 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. *} RETURN {* The result of the operation. *}
*/ */
BDD bdd_satoneset(BDD r, BDD var, BDD pol) BDD bdd_satoneset(BDD r, BDD var, BDD pol)
...@@ -2259,7 +2314,7 @@ PROTO {* BDD bdd_fullsatone(BDD r) *} ...@@ -2259,7 +2314,7 @@ PROTO {* BDD bdd_fullsatone(BDD r) *}
DESCR {* Finds a BDD with exactly one variable at all levels. This BDD DESCR {* Finds a BDD with exactly one variable at all levels. This BDD
implies {\tt r} and is not false unless {\tt r} is implies {\tt r} and is not false unless {\tt r} is
false. *} 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. *} RETURN {* The result of the operation. *}
*/ */
BDD bdd_fullsatone(BDD r) BDD bdd_fullsatone(BDD r)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment