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

acccompl: Speed up.

* src/misc/acccompl.cc: Simplify both directions of the conversion.
* src/misc/acccompl.hh: Pass bdds by reference.
parent ce21af63
...@@ -21,32 +21,18 @@ ...@@ -21,32 +21,18 @@
namespace spot namespace spot
{ {
// The algorithm of this method is simple. We explain this in // If ALL = a!b!c + !ab!c + !a!bc", the negation of ACC = a!b!c is
// bottom/up. // RES = bc. We do that by computing ALL-ACC and enumerating
// Internally, the bdd is represented like a tree. There is two // all positive variables in the remaining products.
// output: high(1) and low (0). An acceptance condition is like bdd acc_compl::complement(const bdd& acc)
// the following:
// if all has three acceptance conditions, all is equal to
// "a!b!c + !ab!c + !a!bc".
// So, to compute the negation of an acceptance condition, say "a!b!c"
// we need to know wich one is go to one when true. So we are looping
// through the conditions until bdd_high is true.
// Once found, we keep only it.
bdd acc_compl::complement(const bdd acc)
{ {
bdd_cache_t::const_iterator it = cache_.find(acc); bdd_cache_t::const_iterator it = cache_.find(acc);
if (it != cache_.end()) if (it != cache_.end())
return it->second; return it->second;
bdd res = bddtrue; bdd res = bddtrue;
bdd n = all_ - acc; bdd n = all_ - acc;
// This means, if acc == all, the opposite is bddfalse, and not
// bddtrue.
if (n == bddfalse)
res = bddtrue;
while (n != bddfalse) while (n != bddfalse)
{ {
bdd cond = bdd_satone(n); bdd cond = bdd_satone(n);
...@@ -67,41 +53,27 @@ namespace spot ...@@ -67,41 +53,27 @@ namespace spot
return res; return res;
} }
bdd acc_compl::reverse_complement(const bdd& acc)
bdd acc_compl::reverse_complement(const bdd acc)
{ {
// We are sure that if we have no acceptance condition // We are sure that if we have no acceptance condition the result
// the result is all_. // is all_.
if (acc == bddtrue) if (acc == bddtrue)
return all_; return all_;
// Since we never cache a unique positive bdd, we can reuse the // Since we never cache a unique positive bdd, we can reuse the
// same cache. // same cache. In fact the only kind of acc we will receive in
// In fact the only kind of acc we will received in this method, // this method, are a conjunction of positive acceptance
// are a conjunction of positive acceptance condition. // conditions. (i.e., "ab" and not "a!b + !ab")
// I mean: "ab" and not "a!b + !ab"
bdd_cache_t::const_iterator it = cache_.find(acc); bdd_cache_t::const_iterator it = cache_.find(acc);
if (it != cache_.end()) if (it != cache_.end())
return it->second; return it->second;
bdd res = all_; bdd res = all_;
bdd cond = acc; bdd cond = acc;
while (cond != bddtrue) while (cond != bddtrue)
{ {
bdd one; res &= bdd_nithvar(bdd_var(cond));
one = bdd_ithvar(bdd_var(cond));
// Because it is a conjunction of positive bdd, we just have to
// traverse through the high branch.
cond = bdd_high(cond); cond = bdd_high(cond);
// We remove the current `one' from the `neg_' and we associate
// `one'.
bdd n = bdd_exist(neg_, one) & one;
res -= n;
} }
cache_[acc] = res; cache_[acc] = res;
......
...@@ -35,19 +35,19 @@ namespace spot ...@@ -35,19 +35,19 @@ namespace spot
class acc_compl class acc_compl
{ {
public: public:
acc_compl(bdd all, bdd neg) acc_compl(const bdd& all, const bdd& neg)
: all_(all), : all_(all),
neg_(neg) neg_(neg)
{ {
} }
bdd complement(const bdd acc); bdd complement(const bdd& acc);
bdd reverse_complement(const bdd acc); bdd reverse_complement(const bdd& acc);
protected: protected:
bdd all_; const bdd all_;
bdd neg_; const bdd neg_;
typedef Sgi::hash_map<bdd, bdd, bdd_hash> bdd_cache_t; typedef Sgi::hash_map<bdd, bdd, bdd_hash> bdd_cache_t;
bdd_cache_t cache_; bdd_cache_t cache_;
}; };
......
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