Change the way references are counted to speedup cloning.

Before this patch, every time you cloned a formula, the clone
visitor would recurse into the entire AST to increment the
reference count of all nodes.  When running ltl2tgba_fm on
the formula generated by "LTLcounterLinear.pl 8", approx 27% of
the time was spent in the clone visitor.

After this patch, cloning a formula is just an increment of the
reference count of the top node.  Children are decremented only
when the top node's ref count is decremented to zero.  With this
change, clone() and destroy() become constant time, the
ltl2tgba_fm spend only 0.01% of the time cloning formulae.

* src/ltlast/automatop.cc (~automatop): Decrement children.
(instance): Decrement children if the instance already exists.
* src/ltlast/binop.cc, src/ltlast/multop.cc, src/ltlast/unop.cc:
Likewise.
* src/ltlvisit/clone.cc (clone): Simplify, now we only need to
call ref().
* src/ltlvisit/destroy.cc (destroy): Simplify, now we only need
to call unref().
(destroy_visitor): Remove, no longer needed.

ChangeLog

@@ -1,3 +1,30 @@
+2009-11-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Change the way references are counted to speedup cloning.
+
+	Before this patch, every time you cloned a formula, the clone
+	visitor would recurse into the entire AST to increment the
+	reference count of all nodes.  When running ltl2tgba_fm on
+	the formula generated by "LTLcounterLinear.pl 8", approx 27% of
+	the time was spent in the clone visitor.
+
+	After this patch, cloning a formula is just an increment of the
+	reference count of the top node.  Children are decremented only
+	when the top node's ref count is decremented to zero.  With this
+	change, clone() and destroy() become constant time, the
+	ltl2tgba_fm spend only 0.01% of the time cloning formulae.
+
+
+	* src/ltlast/automatop.cc (~automatop): Decrement children.
+	(instance): Decrement children if the instance already exists.
+	* src/ltlast/binop.cc, src/ltlast/multop.cc, src/ltlast/unop.cc:
+	Likewise.
+	* src/ltlvisit/clone.cc (clone): Simplify, now we only need to
+	call ref().
+	* src/ltlvisit/destroy.cc (destroy): Simplify, now we only need
+	to call unref().
+	(destroy_visitor): Remove, no longer needed.
+
 2009-11-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Make it easier to debug reference counts in LTL nodes.

src/ltlast/automatop.cc

@@ -48,6 +48,10 @@ namespace spot
       assert (i != instances.end());
       instances.erase(i);
 
+      // Dereference children.
+      for (unsigned n = 0; n < size(); ++n)
+	formula::unref(nth(n));
+
       delete children_;
     }
 
@@ -73,6 +77,9 @@ namespace spot
       map::iterator i = instances.find(p);
       if (i != instances.end())
 	{
+	  // The instance already exists.
+	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
+	    formula::unref(*vi);
 	  delete v;
 	  return static_cast<automatop*>(i->second->ref());
 	}

src/ltlast/binop.cc

@@ -46,6 +46,10 @@ namespace spot
       map::iterator i = instances.find(p);
       assert (i != instances.end());
       instances.erase(i);
+
+      // Dereference children.
+      formula::unref(first());
+      formula::unref(second());
     }
 
     void
@@ -138,6 +142,9 @@ namespace spot
       map::iterator i = instances.find(p);
       if (i != instances.end())
 	{
+	  // This instance already exists.
+	  formula::unref(first);
+	  formula::unref(second);
 	  return static_cast<binop*>(i->second->ref());
 	}
       binop* ap = new binop(op, first, second);

src/ltlast/multop.cc

@@ -26,7 +26,6 @@
 #include "multop.hh"
 #include "constant.hh"
 #include "visitor.hh"
-#include "ltlvisit/destroy.hh"
 
 namespace spot
 {
@@ -54,6 +53,10 @@ namespace spot
       assert (i != instances.end());
       instances.erase(i);
 
+      // Dereference children.
+      for (unsigned n = 0; n < size(); ++n)
+	formula::unref(nth(n));
+
       delete children_;
     }
 
@@ -113,9 +116,10 @@ namespace spot
     formula*
     multop::instance(type op, vec* v)
     {
-      pair p(op, v);
-
       // Inline children of same kind.
+      //
+      // When we construct a formula such as Multop(Op,X,Multop(Op,Y,Z))
+      // we will want to inline it as Multop(Op,X,Y,Z).
       {
 	vec inlined;
 	vec::iterator i = v->begin();
@@ -126,10 +130,7 @@ namespace spot
 	      {
 		unsigned ps = p->size();
 		for (unsigned n = 0; n < ps; ++n)
-		  inlined.push_back(p->nth(n));
-		// That sub-formula is now useless, drop it.
-		// Note that we use unref(), not destroy(), because we've
-		// adopted its children and don't want to destroy these.
+		  inlined.push_back(p->nth(n)->ref());
 		formula::unref(*i);
 		i = v->erase(i);
 	      }
@@ -144,7 +145,7 @@ namespace spot
       std::sort(v->begin(), v->end(), formula_ptr_less_than());
 
       // Remove duplicates.  We can't use std::unique(), because we
-      // must destroy() any formula we drop.
+      // must unref() any formula we drop.
       {
 	formula* last = 0;
 	vec::iterator i = v->begin();
@@ -152,7 +153,7 @@ namespace spot
 	  {
 	    if (*i == last)
 	      {
-		destroy(*i);
+		formula::unref(*i);
 		i = v->erase(i);
 	      }
 	    else
@@ -160,7 +161,7 @@ namespace spot
 		last = *i++;
 	      }
 	  }
-	}
+      }
 
       vec::size_type s = v->size();
       if (s == 0)
@@ -178,21 +179,31 @@ namespace spot
 	}
       else if (s == 1)
 	{
+	  // Simply replace Multop(Op,X) by X.
 	  formula* res = (*v)[0];
 	  delete v;
 	  return res;
 	}
 
+      // The hash key.
+      pair p(op, v);
+
       map::iterator i = instances.find(p);
       if (i != instances.end())
 	{
+	  // The instance already exists.
+	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
+	    formula::unref(*vi);
 	  delete v;
 	  return static_cast<multop*>(i->second->ref());
 	}
+
+      // This is the first instance of this formula.
+
+      // Record the instance in the map,
       multop* ap = new multop(op, v);
       instances[p] = ap;
-      return static_cast<multop*>(ap->ref());
-
+      return ap->ref();
     }
 
     formula*

src/ltlast/unop.cc

@@ -44,6 +44,9 @@ namespace spot
       map::iterator i = instances.find(p);
       assert (i != instances.end());
       instances.erase(i);
+
+      // Dereference child.
+      formula::unref(child());
     }
 
     void
@@ -106,6 +109,8 @@ namespace spot
       map::iterator i = instances.find(p);
       if (i != instances.end())
 	{
+	  // This instance already exists.
+	  formula::unref(child);
 	  return static_cast<unop*>(i->second->ref());
 	}
       unop* ap = new unop(op, child);

src/ltlvisit/clone.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -93,9 +93,8 @@ namespace spot
     formula*
     clone(const formula* f)
     {
-      clone_visitor v;
-      const_cast<formula*>(f)->accept(v);
-      return v.result();
+      formula* res = const_cast<formula*>(f)->ref();
+      return res;
     }
   }
 }

src/ltlvisit/destroy.cc

@@ -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.
 //
@@ -25,24 +25,10 @@ namespace spot
 {
   namespace ltl
   {
-    namespace
-    {
-      class destroy_visitor: public postfix_visitor
-      {
-      public:
-	virtual void
-	doit_default(formula* c)
-	{
-	  formula::unref(c);
-	}
-      };
-    }
-
     void
     destroy(const formula* f)
     {
-      destroy_visitor v;
-      const_cast<formula*>(f)->accept(v);
+      formula::unref(const_cast<formula*>(f));
     }
   }
 }