diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index aa12fc8b2..9835945fb 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -48,6 +48,12 @@ namespace spot } language_containment_checker::~language_containment_checker() + { + clear(); + } + + void + language_containment_checker::clear() { while (!translated_.empty()) { diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index 78833e131..541f9be3e 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -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). diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 0f6948e3d..8172a9755 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -4294,6 +4294,7 @@ namespace spot ltl_simplifier::clear_as_bdd_cache() { cache_->clear_as_bdd_cache(); + cache_->lcc.clear(); } } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index c8a34c5ad..d55dc89a4 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -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.