From 72f36c50a5cde988e0cc179baa14ec5b08f8387f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 21 May 2012 22:35:51 +0200
Subject: [PATCH] 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.
---
 src/ltlvisit/contain.cc  | 6 ++++++
 src/ltlvisit/contain.hh  | 3 +++
 src/ltlvisit/simplify.cc | 1 +
 src/ltlvisit/simplify.hh | 2 ++
 4 files changed, 12 insertions(+)

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.