From 1628b188fee71dd6276ee05e6f8f484912848d6a Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Thu, 24 Sep 2015 14:19:48 +0200
Subject: [PATCH] Remove useless register_propositions method

* src/twa/bdddict.cc, src/twa/bdddict.hh,
src/twaalgos/ltl2tgba_fm.cc: here.
---
 src/twa/bdddict.cc          | 16 ----------------
 src/twa/bdddict.hh          | 17 -----------------
 src/twaalgos/ltl2tgba_fm.cc |  8 --------
 3 files changed, 41 deletions(-)

diff --git a/src/twa/bdddict.cc b/src/twa/bdddict.cc
index 6e4751738..b1c01ce90 100644
--- a/src/twa/bdddict.cc
+++ b/src/twa/bdddict.cc
@@ -131,22 +131,6 @@ namespace spot
     return num;
   }
 
-  void
-  bdd_dict::register_propositions(bdd f, const void* for_me)
-  {
-    if (f == bddtrue || f == bddfalse)
-      return;
-
-    int v = bdd_var(f);
-    assert(unsigned(v) < bdd_map.size());
-    bdd_info& i = bdd_map[v];
-    assert(i.type == var);
-    i.refs.insert(for_me);
-
-    register_propositions(bdd_high(f), for_me);
-    register_propositions(bdd_low(f), for_me);
-  }
-
   int
   bdd_dict::register_acceptance_variable(const ltl::formula* f,
 					const void* for_me)
diff --git a/src/twa/bdddict.hh b/src/twa/bdddict.hh
index 284891f09..9c15bacc1 100644
--- a/src/twa/bdddict.hh
+++ b/src/twa/bdddict.hh
@@ -109,23 +109,6 @@ namespace spot
     }
     /// @}
 
-    /// \brief Register BDD variables as atomic propositions.
-    ///
-    /// Register all variables occurring in \a f as atomic propositions
-    /// used by \a for_me.  This assumes that these atomic propositions
-    /// are already known from the dictionary (i.e., they have already
-    /// been registered by register_proposition() for another
-    /// automaton).
-    /// @{
-    void register_propositions(bdd f, const void* for_me);
-
-    template <typename T>
-    void register_propositions(bdd f, std::shared_ptr<T> for_me)
-    {
-      register_propositions(f, for_me.get());
-    }
-    /// @}
-
     /// \brief whether a proposition has already been registered
     ///
     /// If \a f has been registered for \a me, this returns
diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index fedd6950b..912f93010 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -1187,14 +1187,6 @@ namespace spot
 	    }
 	}
 
-      // Register all known propositions for a. This may contain
-      // proposition from other parts of the formula being translated,
-      // but this is not really important as this automaton will be
-      // short-lived.  (Maybe it would even work without this line.)
-      dict_.dict->register_propositions(dict_.var_set, a);
-
-      //print_dot(std::cerr, a);
-
       // The following code trims the automaton in a crude way by
       // eliminating SCCs that are not coaccessible.  It does not
       // actually remove the states, it simply marks the corresponding
-- 
GitLab