Replace the hash key construction of LTL formulae by a simple

counter updated each time we create a new (unique) formula.

Doing so saves a lot of memory during the translation of the
ltlcounter formulae, because the formulae are quite big and
storing a string representation of each formula on its node was a
bad idea.  For instance with n=12, the translation now uses 40MB
where it used 290MB.  (Note: in both cases, 20MB is being used by
the BDD cache.)

* src/ltlast/formula.hh (hash_key_): Rename as ...
(count_): ... this.
(hash): Adjust.
(max_count): New static variable to count the number of
formulae created.
(formula): Update max_count and set count_.
(dump): Make it a virtual pure method.
(set_key_): Remove.
(formula_ptr_less_than): Speed up and return false when
the two formula pointer are equal.
* src/ltlast/formula.cc (set_key_, dump): Remove.
* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
Empty the constructor (do not precompute the dump_ anymore),
and add a dump() implementation.

ChangeLog

@@ -1,3 +1,34 @@
+2009-11-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Replace the hash key construction of LTL formulae by a simple
+	counter updated each time we create a new (unique) formula.
+
+	Doing so saves a lot of memory during the translation of the
+	ltlcounter formulae, because the formulae are quite big and
+	storing a string representation of each formula on its node was a
+	bad idea.  For instance with n=12, the translation now uses 40MB
+	where it used 290MB.  (Note: in both cases, 20MB is being used by
+	the BDD cache.)
+
+	* src/ltlast/formula.hh (hash_key_): Rename as ...
+	(count_): ... this.
+	(hash): Adjust.
+	(max_count): New static variable to count the number of
+	formulae created.
+	(formula): Update max_count and set count_.
+	(dump): Make it a virtual pure method.
+	(set_key_): Remove.
+	(formula_ptr_less_than): Speed up and return false when
+	the two formula pointer are equal.
+	* src/ltlast/formula.cc (set_key_, dump): Remove.
+	* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
+	src/ltlast/automatop.cc, src/ltlast/automatop.hh,
+	src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
+	src/ltlast/constant.hh, src/ltlast/multop.cc,
+	src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
+	Empty the constructor (do not precompute the dump_ anymore),
+	and add a dump() implementation.
+
 2009-11-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Use -l wherever we where expecting ltl2tgba to default to LaCIM.

src/ltlast/atomic_prop.cc

@@ -32,8 +32,6 @@ namespace spot
     atomic_prop::atomic_prop(const std::string& name, environment& env)
       : name_(name), env_(&env)
     {
-      dump_ = "AP(" + name + ")";
-      set_key_();
     }
 
     atomic_prop::~atomic_prop()
@@ -45,6 +43,12 @@ namespace spot
       instances.erase(i);
     }
 
+    std::string
+    atomic_prop::dump() const
+    {
+      return "AP(" + name() + ")";
+    }
+
     void
     atomic_prop::accept(visitor& v)
     {

src/ltlast/atomic_prop.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -52,6 +52,9 @@ namespace spot
       /// Get the environment of the atomic proposition.
       environment& env() const;
 
+      /// Return a canonic representation of the atomic proposition
+      virtual std::string dump() const;
+
       /// Number of instantiated atomic propositions.  For debugging.
       static unsigned instance_count();
       /// List all instances of atomic propositions.  For debugging.

src/ltlast/automatop.cc

@@ -30,14 +30,6 @@ namespace spot
     automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
       : nfa_(nfa), children_(v), negated_(negated)
     {
-      dump_ = negated ? "!" : "";
-      dump_ += nfa->get_name();
-      dump_ += "(";
-      dump_ += (*v)[0]->dump();
-      for (unsigned n = 1; n < v->size(); ++n)
-	dump_ += ", " + (*v)[n]->dump();
-      dump_ += ")";
-      set_key_();
     }
 
     automatop::~automatop()
@@ -55,6 +47,19 @@ namespace spot
       delete children_;
     }
 
+    std::string
+    automatop::dump() const
+    {
+      std::string r = is_negated() ? "!" : "";
+      r += nfa()->get_name();
+      r += "(";
+      r += nth(0)->dump();
+      for (unsigned n = 1; n < size(); ++n)
+	r += ", " + nth(n)->dump();
+      r += ")";
+      return r;
+    }
+
     void
     automatop::accept(visitor& v)
     {

src/ltlast/automatop.hh

@@ -68,8 +68,12 @@ namespace spot
       /// Get the NFA of this operator.
       const spot::ltl::nfa::ptr nfa() const;
 
+      /// Whether the automaton is negated.
       bool is_negated() const;
 
+      /// Return a canonic representation of the atomic proposition
+      std::string dump() const;
+
       /// Number of instantiated multop operators.  For debugging.
       static unsigned instance_count();
 

src/ltlast/binop.cc

@@ -32,10 +32,6 @@ namespace spot
     binop::binop(type op, formula* first, formula* second)
       : op_(op), first_(first), second_(second)
     {
-      dump_ = "binop(";
-      dump_ += op_name();
-      dump_ += ", " + first->dump() + ", " + second->dump() + ")";
-      set_key_();
     }
 
     binop::~binop()
@@ -52,6 +48,14 @@ namespace spot
       second()->destroy();
     }
 
+    std::string
+    binop::dump() const
+    {
+      return (std::string("binop(") + op_name()
+	      + ", " + first()->dump()
+	      + ", " + second()->dump() + ")");
+    }
+
     void
     binop::accept(visitor& v)
     {

src/ltlast/binop.hh

@@ -68,6 +68,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Return a canonic representation of the atomic proposition
+      virtual std::string dump() const;
+
       /// Number of instantiated binary operators.  For debugging.
       static unsigned instance_count();
 

src/ltlast/constant.cc

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2005, 2009 Laboratoire d'Informatique de Paris
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -30,25 +30,27 @@ namespace spot
     constant::constant(type val)
       : val_(val)
     {
-      switch (val)
-	{
-	case True:
-	  dump_ = "constant(1)";
-	  set_key_();
-	  return;
-	case False:
-	  dump_ = "constant(0)";
-	  set_key_();
-	  return;
-	}
-      // Unreachable code.
-      assert(0);
     }
 
     constant::~constant()
     {
     }
 
+    std::string
+    constant::dump() const
+    {
+      switch (val())
+	{
+	case True:
+	  return "constant(1)";
+	case False:
+	  return "constant(0)";
+	}
+      // Unreachable code.
+      assert(0);
+      return "BUG";
+    }
+
     void
     constant::accept(visitor& v)
     {

src/ltlast/constant.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -45,6 +45,8 @@ namespace spot
       /// Return the value of the constant as a string.
       const char* val_name() const;
 
+      virtual std::string dump() const;
+
       /// Get the sole instance of spot::ltl::constant::constant(True).
       static constant* true_instance();
       /// Get the sole instance of spot::ltl::constant::constant(False).

src/ltlast/formula.cc

@@ -26,6 +26,8 @@ namespace spot
 {
   namespace ltl
   {
+    size_t formula::max_count = 0;
+
     formula*
     formula::clone() const
     {
@@ -56,19 +58,5 @@ namespace spot
       // Not reference counted by default.
       return false;
     }
-
-    const std::string&
-    formula::dump() const
-    {
-      return dump_;
-    }
-
-    void
-    formula::set_key_()
-    {
-      string_hash sh;
-      hash_key_ = sh(dump_);
-    }
-
   }
 }

src/ltlast/formula.hh

@@ -71,6 +71,8 @@ namespace spot
     class formula
     {
     public:
+      formula() : count_(++max_count) {}
+
       /// Entry point for vspot::ltl::visitor instances.
       virtual void accept(visitor& v) = 0;
       /// Entry point for vspot::ltl::const_visitor instances.
@@ -88,13 +90,13 @@ namespace spot
       void destroy() const;
 
       /// Return a canonic representation of the formula
-      const std::string& dump() const;
+      virtual std::string dump() const = 0;
 
-      /// Return a hash_key for the formula.
+      /// Return a hash key for the formula.
       size_t
       hash() const
       {
-	return hash_key_;
+	return count_;
       }
     protected:
       virtual ~formula();
@@ -105,16 +107,12 @@ namespace spot
       /// the instance must be deleted (usually when the counter hits 0).
       virtual bool unref_();
 
-      /// \brief Compute key_ from dump_.
-      ///
-      /// Should be called once in each object, after dump_ has been set.
-      void set_key_();
-      /// The canonic representation of the formula
-      std::string dump_;
       /// \brief The hash key of this formula.
-      ///
+      size_t count_;
-      /// Initialized by set_key_().
+
-      size_t hash_key_;
+    private:
+      /// \brief Number of formulae created so far.
+      static size_t max_count;
     };
 
     /// \brief Strict Weak Ordering for <code>const formula*</code>.
@@ -138,10 +136,22 @@ namespace spot
       {
 	assert(left);
 	assert(right);
+	if (left == right)
+	  return false;
 	size_t l = left->hash();
 	size_t r = right->hash();
 	if (l != r)
 	  return l < r;
+	// Because the hash code assigned to each formula is the
+	// number of formulae constructed so far, it is very unlikely
+	// that we will ever reach a case were two different formulae
+	// have the same hash.  This will happen only ever with have
+	// produced 256**sizeof(size_t) formulae (i.e. max_count has
+	// looped back to 0 and started over).  In that case we can
+	// order two formulae by looking at their text representation.
+	// We could be more efficient and look at their AST, but it's
+	// not worth the burden.  (Also ordering pointers is ruled out
+	// because it breaks the determinism of the implementation.)
 	return left->dump() < right->dump();
       }
     };

src/ltlast/multop.cc

@@ -34,15 +34,6 @@ namespace spot
     multop::multop(type op, vec* v)
       : op_(op), children_(v)
     {
-      dump_ = "multop(";
-      dump_ += op_name();
-      unsigned max = v->size();
-      for (unsigned n = 0; n < max; ++n)
-	{
-	  dump_ += ", " + (*v)[n]->dump();
-	}
-      dump_ += ")";
-      set_key_();
     }
 
     multop::~multop()
@@ -60,6 +51,18 @@ namespace spot
       delete children_;
     }
 
+    std::string
+    multop::dump() const
+    {
+      std::string r = "multop(";
+      r += op_name();
+      unsigned max = size();
+      for (unsigned n = 0; n < max; ++n)
+	r += ", " + nth(n)->dump();
+      r += ")";
+      return r;
+    }
+
     void
     multop::accept(visitor& v)
     {

src/ltlast/multop.hh

@@ -93,6 +93,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Return a canonic representation of the atomic proposition
+      virtual std::string dump() const;
+
       /// Number of instantiated multi-operand operators.  For debugging.
       static unsigned instance_count();
 

src/ltlast/unop.cc

@@ -31,10 +31,6 @@ namespace spot
     unop::unop(type op, formula* child)
       : op_(op), child_(child)
     {
-      dump_ = "unop(";
-      dump_ += op_name();
-      dump_ += ", " + child->dump() + ")";
-      set_key_();
     }
 
     unop::~unop()
@@ -49,6 +45,12 @@ namespace spot
       child()->destroy();
     }
 
+    std::string
+    unop::dump() const
+    {
+      return std::string("unop(") + op_name() + ", " + child()->dump() + ")";
+    }
+
     void
     unop::accept(visitor& v)
     {

src/ltlast/unop.hh

@@ -57,6 +57,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Return a canonic representation of the atomic proposition
+      virtual std::string dump() const;
+
       /// Number of instantiated unary operators.  For debugging.
       static unsigned instance_count();