From e5a86290cf8b560baea66dcde4b5edb5913ff8a5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 19 May 2012 22:51:18 +0200
Subject: [PATCH] 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.
---
 src/ltlvisit/simplify.cc | 18 ++++++++++++++++++
 src/ltlvisit/simplify.hh |  9 +++++++++
 src/tgbatest/ltl2tgba.cc |  3 +++
 wrap/python/ajax/spot.in |  2 ++
 4 files changed, 32 insertions(+)

diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 96185286d..0f6948e3d 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -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();
+    }
 
   }
 }
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index 142c88c7f..c8a34c5ad 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -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;
 
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index cd59dd569..44f229705 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -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()
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 03084a16b..722c2fe92 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -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':