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

Clear the contaiment cache after -r7.

Doing so will release all BDD variables used by automata created for
syntactic implication.  This way the main translation will create
acceptance variables again in a more natural order, which will help
the degeneralization (until we get a better degeneralization).

* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
(language_containment_checker::clear): New method to clear the
containment cache.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(clear_as_bdd_cache): Also call language_containment_checker::clear.
parent 1c1c95f6
......@@ -48,6 +48,12 @@ namespace spot
}
language_containment_checker::~language_containment_checker()
{
clear();
}
void
language_containment_checker::clear()
{
while (!translated_.empty())
{
......
......@@ -54,6 +54,9 @@ namespace spot
~language_containment_checker();
/// Clear the cache.
void clear();
/// Check whether L(l) is a subset of L(g).
bool contained(const formula* l, const formula* g);
/// Check whether L(!l) is a subset of L(g).
......
......@@ -4294,6 +4294,7 @@ namespace spot
ltl_simplifier::clear_as_bdd_cache()
{
cache_->clear_as_bdd_cache();
cache_->lcc.clear();
}
}
......
......@@ -138,6 +138,8 @@ namespace spot
/// 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.
///
/// This also clears the language containment cache.
void clear_as_bdd_cache();
/// Return the bdd_dict used.
......
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