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

accconv: speed up acceptance_convertor::as_positive_product()

Browse source 
* src/misc/accconv.cc (as_positive_product): Use a small loop instead
of calling bdd_satone().
This commit is contained in:
Alexandre Duret-Lutz 2012-10-19 20:50:35 +02:00
parent 31fb3d9d15
commit c6030df936
1 changed files with 28 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

61
src/misc/accconv.cc
View file

@ -1,5 +1,6 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de // -*- coding: utf-8 -*-
// l'Epita (LRDE) // Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -23,43 +24,37 @@ namespace spot
{ {
bdd acceptance_convertor::as_positive_product(bdd acc) bdd acceptance_convertor::as_positive_product(bdd acc)
{ {
// Lookup in cache. // Cache lookup.
bdd_cache_t::const_iterator it = pos_prod_cache_.find(acc); bdd_cache_t::const_iterator it = pos_prod_cache_.find(acc);
if (it != pos_prod_cache_.end()) if (it != pos_prod_cache_.end())
return it->second; return it->second;
// Split the sum // This would be one way to construct the positive product,
// if we did not want to populate a cache.
//
// bdd res = bddtrue;
// BDD a = acc.id();
// while (a)
// {
// if (bdd_high(a))
// res &= bdd_ithvar(bdd_var(a));
// a = bdd_low(a);
// }
// Skip all negative variables.
bdd a = acc;
while (a != bddfalse && bdd_high(a) == bddfalse)
a = bdd_low(a);
bdd res = bddtrue; bdd res = bddtrue;
bdd all = acc; if (a != bddfalse)
while (all != bddfalse)
{ {
bdd one = bdd_satone(all); // Make a recursive call right below each positive variable,
all -= one; // in order to populate the cache.
// Lookup the subproduct in the cache. res = bdd_ithvar(bdd_var(a));
it = pos_prod_cache_.find(one); bdd low = bdd_low(a);
if (it != pos_prod_cache_.end()) if (low != bddfalse)
{ res &= as_positive_product(low);
res &= it->second;
continue;
}
// Otherwise, strip negative variables.
bdd pos = bddfalse;
bdd cur = one;
while (cur != bddfalse)
{
bdd low = bdd_low(cur);
if (low == bddfalse)
{
pos = bdd_ithvar(bdd_var(cur));
break;
}
cur = low;
}
assert(pos != bddfalse);
// Cache result for subproduct.
pos_prod_cache_[one] = pos;
// Augment final result.
res &= pos;
} }
// Cache final result. // Cache final result.