From b4670f85f1c00f2d4ba816b7970127fbda026a2a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 12 May 2013 18:26:41 +0200
Subject: [PATCH] bdddict: add an unregister_all_typed_variables() method

* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(unregister_all_typed_variables): New method.
* src/tgbaalgos/degen.cc (degeneralize): Use it.
* NEWS: Mention it.
---
 NEWS                   |  4 ++++
 src/tgba/bdddict.cc    | 12 ++++++++++++
 src/tgba/bdddict.hh    |  4 ++++
 src/tgbaalgos/degen.cc |  7 +++++--
 4 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 0d6ef5072..3bf1b400b 100644
--- a/NEWS
+++ b/NEWS
@@ -42,6 +42,10 @@ New in spot 1.1a (not yet released):
     - ltlcross has a new option --seed, that makes it possible to
       change the seed used by the random graph generator.
 
+    - bdd_dict::unregister_all_typed_variables() is a new function,
+      making it easy to unregister all BDD variables of a given type
+      owned by some object.
+
   * Bug fixes:
 
     - genltl --gh-r generated the wrong formulas due to a typo.
diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc
index 94e4c2d9f..6d6440ee0 100644
--- a/src/tgba/bdddict.cc
+++ b/src/tgba/bdddict.cc
@@ -246,6 +246,7 @@ namespace spot
     assert(unsigned(v) < bdd_map.size());
 
     ref_set& s = bdd_map[v].refs;
+    // If the variable is not owned by me, ignore it.
     ref_set::iterator si = s.find(me);
     if (si == s.end())
       return;
@@ -314,6 +315,17 @@ namespace spot
     free_anonymous_list_of.erase(me);
   }
 
+  void
+  bdd_dict::unregister_all_typed_variables(var_type type, const void* me)
+  {
+    unsigned s = bdd_map.size();
+    for (unsigned i = 0; i < s; ++i)
+      if (bdd_map[i].type == type)
+	unregister_variable(i, me);
+    if (type == anon)
+      free_anonymous_list_of.erase(me);
+  }
+
   bool
   bdd_dict::is_registered_proposition(const ltl::formula* f, const void* by_me)
   {
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index 4198ab45c..276465bee 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -203,6 +203,10 @@ namespace spot
     /// Usually called in the destructor if \a me.
     void unregister_all_my_variables(const void* me);
 
+    /// \brief Release all variables of a given type, used by an
+    /// object.
+    void unregister_all_typed_variables(var_type type, const void* me);
+
     /// \brief Release a variable used by \a me.
     void unregister_variable(int var, const void* me);
 
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index 9b4189baf..26eff12b9 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -243,10 +243,13 @@ namespace spot
 
     bdd_dict* dict = a->get_dict();
 
-    // The result (degeneralized) automaton uses numbered state.
+    // The result (degeneralized) automaton uses numbered states.
     sba_explicit_number* res = new sba_explicit_number(dict);
+
+    // We use the same BDD variables as the input, except for the
+    // acceptance.
     dict->register_all_variables_of(a, res);
-    // FIXME: unregister acceptance conditions.
+    dict->unregister_all_typed_variables(bdd_dict::acc, res);
 
     // Invent a new acceptance set for the degeneralized automaton.
     int accvar =