From 10e5c623866b8a7c36761ced9135369252b33b2a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 13 Aug 2014 14:21:16 +0200
Subject: [PATCH] Simplify copying of atomic propositions in new tgba_digraph.

* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(register_all_propositions_of): New method.
* src/tgba/tgbagraph.hh (copy_ap_of): New method.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/dstarparse/nsa2tgba.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stripacc.cc: Simplify using copy_ap_of.
---
 src/dstarparse/dra2ba.cc    |  6 +++---
 src/dstarparse/nra2nba.cc   |  5 +----
 src/dstarparse/nsa2tgba.cc  |  8 +++-----
 src/tgba/bdddict.cc         | 27 ++++++++++++++++++++-------
 src/tgba/bdddict.hh         | 18 ++++++++++++++----
 src/tgba/tgbagraph.hh       |  5 +++++
 src/tgbaalgos/degen.cc      |  5 +----
 src/tgbaalgos/dtbasat.cc    |  2 +-
 src/tgbaalgos/dtgbasat.cc   |  3 +--
 src/tgbaalgos/dupexp.cc     |  2 +-
 src/tgbaalgos/emptiness.cc  |  3 ++-
 src/tgbaalgos/minimize.cc   | 20 +++++---------------
 src/tgbaalgos/powerset.cc   |  6 ++----
 src/tgbaalgos/sccfilter.cc  |  5 ++---
 src/tgbaalgos/simulation.cc | 10 ++++------
 src/tgbaalgos/stripacc.cc   |  1 -
 16 files changed, 65 insertions(+), 61 deletions(-)

diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc
index 22ae56e32..c06ebbc8e 100644
--- a/src/dstarparse/dra2ba.cc
+++ b/src/dstarparse/dra2ba.cc
@@ -235,8 +235,7 @@ namespace spot
 	sm_(sm),
 	realizable_(realizable)
       {
-	bdd_dict* bd = a->aut->get_dict();
-	bd->register_all_variables_of(a->aut, out_);
+	out_->copy_ap_of(a->aut);
 	out_->set_bprop(tgba_digraph::StateBasedAcc);
 	acc_ = out_->set_single_acceptance_set();
 	out_->new_states(num_states_ * (a->accpair_count + 1));
@@ -292,7 +291,8 @@ namespace spot
 		    // accepting cycle.
 		    out_->new_transition(in, out + shift, cond);
 
-		    // Acceptance transitions are those in the Li set. (Löding's Fi set.)
+		    // Acceptance transitions are those in the Li
+		    // set. (Löding's Fi set.)
 		    out_->new_acc_transition(in + shift, out + shift, cond,
 					     l.get(i));
 		  }
diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc
index 513b4c64e..935d2ab40 100644
--- a/src/dstarparse/nra2nba.cc
+++ b/src/dstarparse/nra2nba.cc
@@ -44,10 +44,7 @@ namespace spot
 	d_(a),
 	num_states_(a->aut->num_states())
       {
-	bdd_dict* bd = out_->get_dict();
-	bd->register_all_variables_of(aut, out_);
-
-	// Invent a new acceptance set for the degeneralized automaton.
+	out_->copy_ap_of(aut);
 	out_->set_single_acceptance_set();
 	out_->set_bprop(tgba_digraph::StateBasedAcc);
 	out_->new_states(num_states_ * (d_->accpair_count + 1));
diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc
index 332e17046..89e9ad29d 100644
--- a/src/dstarparse/nsa2tgba.cc
+++ b/src/dstarparse/nsa2tgba.cc
@@ -102,11 +102,9 @@ namespace spot
   tgba_digraph* nsa_to_tgba(const dstar_aut* nsa)
   {
     assert(nsa->type == Streett);
-    tgba_digraph* a = nsa->aut;
-    bdd_dict* dict = a->get_dict();
-
-    tgba_digraph* res = new tgba_digraph(dict);
-    dict->register_all_variables_of(a, res);
+    auto a = nsa->aut;
+    auto res = new tgba_digraph(a->get_dict());
+    res->copy_ap_of(a);
 
     // Create accpair_count acceptance sets for the output.
     unsigned npairs = nsa->accpair_count;
diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc
index a31f1337d..31296137a 100644
--- a/src/tgba/bdddict.cc
+++ b/src/tgba/bdddict.cc
@@ -245,18 +245,31 @@ namespace spot
   bdd_dict::register_all_variables_of(const void* from_other,
 				      const void* for_me)
   {
-    bdd_info_map::iterator i;
-    for (i = bdd_map.begin(); i != bdd_map.end(); ++i)
+    auto j = priv_->free_anonymous_list_of.find(from_other);
+    if (j != priv_->free_anonymous_list_of.end())
+      priv_->free_anonymous_list_of[for_me] = j->second;
+
+    for (auto& i: bdd_map)
       {
-	ref_set& s = i->refs;
+	ref_set& s = i.refs;
 	if (s.find(from_other) != s.end())
 	  s.insert(for_me);
       }
 
-    bdd_dict_priv::free_anonymous_list_of_type::const_iterator j =
-      priv_->free_anonymous_list_of.find(from_other);
-    if (j != priv_->free_anonymous_list_of.end())
-      priv_->free_anonymous_list_of[for_me] = j->second;
+  }
+
+  void
+  bdd_dict::register_all_propositions_of(const void* from_other,
+					 const void* for_me)
+  {
+    for (auto& i: bdd_map)
+      {
+	if (i.type != var_type::var)
+	  continue;
+	ref_set& s = i.refs;
+	if (s.find(from_other) != s.end())
+	  s.insert(for_me);
+      }
   }
 
   void
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index e37588436..4c79f33a7 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -169,12 +169,22 @@ namespace spot
 
     /// \brief Duplicate the variable usage of another object.
     ///
-    /// This tells this dictionary that the \a for_me object
-    /// will be using the same BDD variables as the \a from_other objects.
-    /// This ensure that the variables won't be freed when \a from_other
-    /// is deleted if \a from_other is still alive.
+    /// This tells this dictionary that the \a for_me object will be
+    /// using the same BDD variables as the \a from_other objects.
+    /// This ensures that the variables won't be freed when \a
+    /// from_other is deleted if \a from_other is still alive.
     void register_all_variables_of(const void* from_other, const void* for_me);
 
+    /// \brief Register the same propositions as another object.
+    ///
+    /// This tells this dictionary that the \a for_me object will be
+    /// using the same BDD variable used for atomic propositions by
+    /// the \a from_other object.  This ensures that the variables
+    /// won't be freed when \a from_other is deleted if \a from_other
+    /// is still alive.
+    void register_all_propositions_of(const void* from_other,
+				      const void* for_me);
+
     /// \brief Release all variables used by an object.
     ///
     /// Usually called in the destructor if \a me.
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index 01c153095..c8e87a168 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -351,6 +351,11 @@ namespace spot
       set_acceptance_conditions(a->neg_acceptance_conditions());
     }
 
+    void copy_ap_of(const tgba* a)
+    {
+      dict_->register_all_propositions_of(a, this);
+    }
+
     virtual bdd all_acceptance_conditions() const
     {
       return all_acceptance_conditions_;
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index f6a3c78a6..ae65282a4 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -260,14 +260,11 @@ namespace spot
 
       // The result automaton is an SBA.
       auto res = new tgba_digraph(dict);
+      res->copy_ap_of(a);
       res->set_single_acceptance_set();
       if (want_sba)
 	res->set_bprop(tgba_digraph::StateBasedAcc);
 
-      // We use the same BDD variables as the input, except for the
-      // acceptance.
-      dict->register_all_variables_of(a, res);
-
       // Create an order of acceptance conditions.  Each entry in this
       // vector correspond to an acceptance set.  Each index can
       // be used as a level in degen_state to indicate the next expected
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index bd9fedb75..14e0cde5b 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -671,7 +671,7 @@ namespace spot
     {
       auto autdict = aut->get_dict();
       auto a = new tgba_digraph(autdict);
-      autdict->register_all_variables_of(aut, a);
+      a->copy_ap_of(aut);
       bdd acc = a->set_single_acceptance_set();
       a->new_states(satdict.cand_size);
 
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index a13b305a7..b8ed4c9ab 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -843,8 +843,7 @@ namespace spot
     {
       auto autdict = aut->get_dict();
       auto a = new tgba_digraph(autdict);
-      autdict->register_all_variables_of(aut, a);
-      autdict->unregister_all_typed_variables(bdd_dict::acc, aut);
+      a->copy_ap_of(aut);
       a->set_acceptance_conditions(satdict.all_cand_acc.back());
 
       a->new_states(satdict.cand_size);
diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc
index 261d0bb76..5ad9bee17 100644
--- a/src/tgbaalgos/dupexp.cc
+++ b/src/tgbaalgos/dupexp.cc
@@ -38,7 +38,7 @@ namespace spot
 	: T(a), out_(new tgba_digraph(a->get_dict()))
       {
 	out_->copy_acceptance_conditions_of(a);
-	a->get_dict()->register_all_variables_of(a, out_);
+	out_->copy_ap_of(a);
       }
 
       tgba_digraph*
diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc
index cde8e9533..e4f93cb95 100644
--- a/src/tgbaalgos/emptiness.cc
+++ b/src/tgbaalgos/emptiness.cc
@@ -287,7 +287,8 @@ namespace spot
   {
     auto d = a->get_dict();
     auto res = new tgba_digraph(d);
-    d->register_all_variables_of(a, res);
+    res->copy_ap_of(a);
+    res->copy_acceptance_conditions_of(a);
 
     const state* s = a->get_init_state();
     unsigned src;
diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index 80ab3e066..ec6e17547 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -119,8 +119,7 @@ namespace spot
   {
     auto dict = a->get_dict();
     auto res = new tgba_digraph(dict);
-    dict->register_all_variables_of(a, res);
-    dict->unregister_all_typed_variables(bdd_dict::acc, res);
+    res->copy_ap_of(a);
     res->set_bprop(tgba_digraph::StateBasedAcc);
 
     // For each set, create a state in the resulting automaton.
@@ -139,15 +138,9 @@ namespace spot
 
     // For each transition in the initial automaton, add the corresponding
     // transition in res.
-    bdd allacc = bddfalse;
+
     if (!final->empty())
-      {
-	int accvar =
-	  dict->register_acceptance_variable(ltl::constant::true_instance(),
-					     res);
-	allacc = bdd_ithvar(accvar);
-	res->set_acceptance_conditions(allacc);
-      }
+      res->set_single_acceptance_set();
 
     for (sit = sets.begin(); sit != sets.end(); ++sit)
       {
@@ -167,11 +160,8 @@ namespace spot
 	    dst->destroy();
 	    if (i == state_num.end()) // Ignore useless destinations.
 	      continue;
-	    bdd acc = bddfalse;
-	    if (accepting)
-	      acc = allacc;
-	    res->new_transition(src_num, i->second,
-				succit->current_condition(), acc);
+	    res->new_acc_transition(src_num, i->second,
+				    succit->current_condition(), accepting);
 	  }
       }
     res->merge_transitions();
diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc
index 9254b4af1..a2003b28b 100644
--- a/src/tgbaalgos/powerset.cc
+++ b/src/tgbaalgos/powerset.cc
@@ -51,10 +51,8 @@ namespace spot
 
     power_set seen;
     todo_list todo;
-    auto d = aut->get_dict();
-    auto res = new tgba_digraph(d);
-    d->register_all_variables_of(aut, res);
-    d->unregister_all_typed_variables(bdd_dict::acc, res);
+    auto res = new tgba_digraph(aut->get_dict());
+    res->copy_ap_of(aut);
 
     {
       power_state ps;
diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc
index 5aed42152..ec49d19f9 100644
--- a/src/tgbaalgos/sccfilter.cc
+++ b/src/tgbaalgos/sccfilter.cc
@@ -434,11 +434,11 @@ namespace spot
     tgba_digraph* scc_filter_apply(const tgba_digraph* aut,
 				   scc_info* given_si, Args&&... args)
     {
-      bdd_dict* bd = aut->get_dict();
-      tgba_digraph* filtered = new tgba_digraph(bd);
+      tgba_digraph* filtered = new tgba_digraph(aut->get_dict());
       unsigned in_n = aut->num_states(); // Number of input states.
       if (in_n == 0)			 // Nothing to filter.
 	return filtered;
+      filtered->copy_ap_of(aut);
 
       // Compute scc_info if not supplied.
       scc_info* si = given_si;
@@ -457,7 +457,6 @@ namespace spot
 	else
 	  inout.push_back(-1U);
 
-      bd->register_all_variables_of(aut, filtered);
       {
 	bdd all = aut->all_acceptance_conditions();
 	bdd neg = aut->neg_acceptance_conditions();
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 2d8418717..84b198cec 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -230,9 +230,8 @@ namespace spot
 	{
 	  if (Cosimulation)
 	    {
-	      bdd_dict* bd = a_->get_dict();
-	      a_ = new tgba_digraph(bd);
-	      bd->register_all_variables_of(old_a_, a_);
+	      a_ = new tgba_digraph(a_->get_dict());
+	      a_->copy_ap_of(old_a_);
 	      a_->copy_acceptance_conditions_of(old_a_);
 	    }
 	  unsigned ns = old_a_->num_states();
@@ -546,9 +545,8 @@ namespace spot
 	acc_compl reverser(all_acceptance_conditions_,
 			   a_->neg_acceptance_conditions());
 
-	bdd_dict* d = a_->get_dict();
-	tgba_digraph* res = new tgba_digraph(d);
-	d->register_all_variables_of(a_, res);
+	tgba_digraph* res = new tgba_digraph(a_->get_dict());
+	res->copy_ap_of(a_);
 	res->set_acceptance_conditions(all_acceptance_conditions_);
 	if (Sba)
 	  res->set_bprop(tgba_digraph::StateBasedAcc);
diff --git a/src/tgbaalgos/stripacc.cc b/src/tgbaalgos/stripacc.cc
index aced5b2cf..5a366f086 100644
--- a/src/tgbaalgos/stripacc.cc
+++ b/src/tgbaalgos/stripacc.cc
@@ -29,6 +29,5 @@ namespace spot
       for (auto& t: a->out(s))
 	t.acc = bddfalse;
     a->set_acceptance_conditions(bddfalse);
-    a->get_dict()->unregister_all_typed_variables(bdd_dict::acc, a);
   }
 }