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

Clean the as_bdd() cache after LTL simplification.

Syntactic implication checks may use as_bdd() to compare Boolean
formulae.  By doing so, they register Boolean variables in an order
that is usially detrimental to the LTL translator.  The new,
clear_as_bdd_cache() function offers a mean to unregister these
variables, so that the LTL translator will register them again in the
a more natural way.

* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(clear_as_bdd_cache): New function.
* src/tgbatest/ltl2tgba.cc, wrap/python/ajax/spot.in: Call it.
parent 9633dd6e
......@@ -131,6 +131,19 @@ namespace spot
<< "star normal form: " << snf_cache_.size() << " entries\n";
}
void
clear_as_bdd_cache()
{
f2b_map::iterator i = as_bdd_.begin();
f2b_map::iterator end = as_bdd_.end();
while (i != end)
{
f2b_map::iterator old = i++;
old->first->destroy();
}
as_bdd_.clear();
}
// Convert a Boolean formula into a BDD for easier comparison.
bdd
as_bdd(const formula* f)
......@@ -4277,6 +4290,11 @@ namespace spot
cache_->print_stats(os);
}
void
ltl_simplifier::clear_as_bdd_cache()
{
cache_->clear_as_bdd_cache();
}
}
}
......@@ -131,6 +131,15 @@ namespace spot
/// to the constructor.
bdd as_bdd(const formula* f);
/// \brief Clear the as_bdd() cache.
///
/// Calling this function is recommended before running other
/// algorithms that create BDD variables in a more natural
/// order. For instance ltl_to_tgba_fm() will usually be more
/// efficient if the BDD variables for atomic propositions have
/// not been ordered before hand.
void clear_as_bdd_cache();
/// Return the bdd_dict used.
bdd_dict* get_dict() const;
......
......@@ -849,6 +849,9 @@ main(int argc, char** argv)
else
std::cout << spot::ltl::to_string(f) << std::endl;
}
// This helps ltl_to_tgba_fm() to order BDD variables in
// a more natural way.
simp->clear_as_bdd_cache();
}
if (f->is_psl_formula()
......
......@@ -391,6 +391,8 @@ if dored:
f2 = simp.simplify(f)
f.destroy()
f = f2
# This also clears the as_bdd() cache.
simp = None
# Formula manipulation only.
if output_type == 'f':
......
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