From 2052e73af881ad6c70843387ca771df4db73500b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 1 Dec 2015 00:12:45 +0100
Subject: [PATCH] word: store the bdd dict for easier printing

* src/twaalgos/word.hh, src/twaalgos/word.cc: Store the
bdd_dict, and replace the print() method by a << overload.
* NEWS: Mention it.
* src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust.
---
 NEWS                      |  1 +
 src/bin/common_aoutput.hh |  2 +-
 src/bin/ltlcross.cc       |  2 +-
 src/twaalgos/word.cc      | 13 ++++++++-----
 src/twaalgos/word.hh      | 18 ++++++++++++++++--
 5 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/NEWS b/NEWS
index cb241cbff..3fcb916c3 100644
--- a/NEWS
+++ b/NEWS
@@ -81,6 +81,7 @@ New in spot 1.99.5a (not yet released)
   * Renamings:
     is_guarantee_automaton() -> is_terminal_automaton()
     tgba_run -> twa_run
+    twa_word::print -> operator<<
     dtgba_sat_synthetize() -> dtwa_sat_synthetize()
     dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()
 
diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh
index a7247ec33..8afc53dfe 100644
--- a/src/bin/common_aoutput.hh
+++ b/src/bin/common_aoutput.hh
@@ -181,7 +181,7 @@ public:
 	      spot::twa_word w(run->reduce());
 	      w.simplify();
 	      std::ostringstream out;
-	      w.print(out, aut->get_dict());
+	      out << w;
 	      aut_word_ = out.str();
 	    }
 	  else
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 13b9e5885..7b208c3c2 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -695,7 +695,7 @@ namespace
 		      << "       ";
 	    spot::twa_word w(run->reduce());
 	    w.simplify();
-	    w.print(example(), prod->get_dict()) << '\n';
+	    example() << w << '\n';
 	  }
 	else
 	  {
diff --git a/src/twaalgos/word.cc b/src/twaalgos/word.cc
index f708c16b5..941775f8d 100644
--- a/src/twaalgos/word.cc
+++ b/src/twaalgos/word.cc
@@ -24,11 +24,13 @@
 namespace spot
 {
   twa_word::twa_word(const twa_run_ptr run)
+    : dict_(run->aut->get_dict())
   {
     for (auto& i: run->prefix)
       prefix.push_back(i.label);
     for (auto& i: run->cycle)
       cycle.push_back(i.label);
+    dict_->register_all_variables_of(run->aut, this);
   }
 
   void
@@ -81,18 +83,19 @@ namespace spot
   }
 
   std::ostream&
-  twa_word::print(std::ostream& os, const bdd_dict_ptr& d) const
+  operator<<(std::ostream& os, const twa_word& w)
   {
-    if (!prefix.empty())
-      for (auto& i: prefix)
+    auto d = w.get_dict();
+    if (!w.prefix.empty())
+      for (auto& i: w.prefix)
 	{
 	  bdd_print_formula(os, d, i);
 	  os << "; ";
 	}
-    assert(!cycle.empty());
+    assert(!w.cycle.empty());
     bool notfirst = false;
     os << "cycle{";
-    for (auto& i: cycle)
+    for (auto& i: w.cycle)
       {
 	if (notfirst)
 	  os << "; ";
diff --git a/src/twaalgos/word.hh b/src/twaalgos/word.hh
index 7b97fdc4a..72f9f72cb 100644
--- a/src/twaalgos/word.hh
+++ b/src/twaalgos/word.hh
@@ -26,15 +26,29 @@ namespace spot
   class bdd_dict;
 
   /// \brief An infinite word stored as a lasso.
-  struct SPOT_API twa_word
+  struct SPOT_API twa_word final
   {
     twa_word(const twa_run_ptr run);
+    ~twa_word()
+    {
+      dict_->unregister_all_my_variables(this);
+    }
+
     void simplify();
-    std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const;
 
     typedef std::list<bdd> seq_t;
     seq_t prefix;
     seq_t cycle;
+
+    bdd_dict_ptr get_dict() const
+    {
+      return dict_;
+    }
+
+    SPOT_API
+    friend std::ostream& operator<<(std::ostream& os, const twa_word& w);
+  private:
+    bdd_dict_ptr dict_;
   };
 
 }