ltl: get rid of ltl::ref_formula

Instead, manage all reference counting from ltl::formula.
It ridance of virtual calls to clone() and destroy() easily compensate
the extra test in destroy() to not delete constant nodes.

* src/ltlast/refformula.cc, src/ltlast/refformula.hh: Delete.
* src/ltlast/Makefile.am, wrap/python/spot.i: Adjust.
* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/bunop.cc,
src/ltlast/bunop.hh, src/ltlast/formula.cc, src/ltlast/formula.hh,
src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc,
src/ltlast/unop.hh: Ajust the reference counting code.

src/ltlast/Makefile.am

@@ -35,7 +35,6 @@ ltlast_HEADERS = \
   formula.hh \
   multop.hh \
   predecl.hh \
-  refformula.hh \
   unop.hh \
   visitor.hh
 
@@ -47,5 +46,4 @@ libltlast_la_SOURCES = \
   constant.cc \
   formula.cc \
   multop.cc \
-  refformula.cc \
   unop.cc

src/ltlast/atomic_prop.cc

@@ -33,7 +33,7 @@ namespace spot
   {
 
     atomic_prop::atomic_prop(const std::string& name, environment& env)
-      : ref_formula(AtomicProp), name_(name), env_(&env)
+      : formula(AtomicProp), name_(name), env_(&env)
     {
       is.boolean = true;
       is.sugar_free_boolean = true;
@@ -93,10 +93,14 @@ namespace spot
       const atomic_prop* ap;
       auto ires = instances.emplace(key(name, &env), nullptr);
       if (!ires.second)
+	{
 	  ap = ires.first->second;
-      else
-	ap = ires.first->second = new atomic_prop(name, env);
 	  ap->clone();
+	}
+      else
+	{
+	  ap = ires.first->second = new atomic_prop(name, env);
+	}
       return ap;
     }
 
@@ -110,9 +114,9 @@ namespace spot
     atomic_prop::dump_instances(std::ostream& os)
     {
       for (const auto& i: instances)
-	os << i.second << " = " << i.second->ref_count_()
+	os << i.second << " = " << 1 + i.second->refs_
 	   << " * atomic_prop(" << i.first.first << ", "
-	   << i.first.second->name() << ')' << std::endl;
+	   << i.first.second->name() << ")\n";
       return os;
     }
 

src/ltlast/atomic_prop.hh

@@ -25,7 +25,7 @@
 #ifndef SPOT_LTLAST_ATOMIC_PROP_HH
 # define SPOT_LTLAST_ATOMIC_PROP_HH
 
-#include "refformula.hh"
+#include "formula.hh"
 #include <string>
 #include <iosfwd>
 #include <map>
@@ -38,7 +38,7 @@ namespace spot
 
     /// \ingroup ltl_ast
     /// \brief Atomic propositions.
-    class SPOT_API atomic_prop : public ref_formula
+    class SPOT_API atomic_prop : public formula
     {
     public:
       /// Build an atomic proposition with name \a name in

src/ltlast/binop.cc

@@ -36,7 +36,7 @@ namespace spot
   namespace ltl
   {
     binop::binop(type op, const formula* first, const formula* second)
-      : ref_formula(BinOp), op_(op), first_(first), second_(second)
+      : formula(BinOp), op_(op), first_(first), second_(second)
     {
       // Beware: (f U g) is a pure eventuality if both operands
       // are pure eventualities, unlike in the proceedings of
@@ -503,20 +503,19 @@ namespace spot
 	  break;
 	}
 
-      const binop* res;
+      const formula* res;
       auto ires = instances.emplace(key(op, first, second), nullptr);
       if (!ires.second)
 	{
 	  // This instance already exists.
 	  first->destroy();
 	  second->destroy();
-	  res = ires.first->second;
+	  res = ires.first->second->clone();
 	}
       else
 	{
 	  res = ires.first->second = new binop(op, first, second);
 	}
-      res->clone();
       return res;
     }
 
@@ -531,9 +530,8 @@ namespace spot
     {
       for (const auto& i: instances)
 	os << i.second << " = "
-	   << i.second->ref_count_() << " * "
+	   << 1 + i.second->refs_ << " * "
-	   << i.second->dump()
+	   << i.second->dump() << '\n';
-	   << std::endl;
       return os;
     }
 

src/ltlast/binop.hh

@@ -28,7 +28,7 @@
 #ifndef SPOT_LTLAST_BINOP_HH
 # define SPOT_LTLAST_BINOP_HH
 
-#include "refformula.hh"
+#include "formula.hh"
 #include <map>
 #include <iosfwd>
 #include <tuple>
@@ -40,7 +40,7 @@ namespace spot
 
     /// \ingroup ltl_ast
     /// \brief Binary operator.
-    class SPOT_API binop : public ref_formula
+    class SPOT_API binop : public formula
     {
     public:
       /// Different kinds of binary opertaors

src/ltlast/bunop.cc

@@ -36,7 +36,7 @@ namespace spot
     const formula* bunop::one_star_ = 0;
 
     bunop::bunop(type op, const formula* child, unsigned min, unsigned max)
-      : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max)
+      : formula(BUnOp), op_(op), child_(child), min_(min), max_(max)
     {
       props = child->get_props();
 
@@ -242,13 +242,12 @@ namespace spot
 	{
 	  // This instance already exists.
 	  child->destroy();
-	  res = ires.first->second;
+	  res = ires.first->second->clone();
 	}
       else
 	{
 	  res = ires.first->second = new bunop(op, child, min, max);
 	}
-      res->clone();
       return res;
     }
 
@@ -299,9 +298,9 @@ namespace spot
     {
       for (const auto& i: instances)
 	os << i.second << " = "
-	   << i.second->ref_count_() << " * "
+	   << 1 + i.second->refs_ << " * "
 	   << i.second->dump()
-	   << std::endl;
+	   << '\n';
       return os;
     }
 

src/ltlast/bunop.hh

@@ -22,7 +22,7 @@
 #ifndef SPOT_LTLAST_BUNOP_HH
 # define SPOT_LTLAST_BUNOP_HH
 
-#include "refformula.hh"
+#include "formula.hh"
 #include <map>
 #include <iosfwd>
 #include <tuple>
@@ -35,7 +35,7 @@ namespace spot
 
     /// \ingroup ltl_ast
     /// \brief Bounded unary operator.
-    class SPOT_API bunop : public ref_formula
+    class SPOT_API bunop : public formula
     {
     public:
       enum type { Star };

src/ltlast/formula.cc

@@ -35,38 +35,6 @@ namespace spot
   {
     size_t formula::max_serial = 0;
 
-    const formula*
-    formula::clone() const
-    {
-      this->ref_();
-      return this;
-    }
-
-    formula::~formula()
-    {
-    }
-
-    void
-    formula::destroy() const
-    {
-      if (this->unref_())
-	delete this;
-    }
-
-    void
-    formula::ref_() const
-    {
-      // Not reference counted by default.
-    }
-
-    bool
-    formula::unref_() const
-    {
-      // Not reference counted by default.
-      return false;
-    }
-
-
 #define printprops							\
       proprint(is_boolean, "B", "Boolean formula");			\
       proprint(is_sugar_free_boolean, "&", "without Boolean sugar");	\

src/ltlast/formula.hh

@@ -97,14 +97,27 @@ namespace spot
 
       /// \brief clone this node
       ///
-      /// This increments the reference counter of this node (if one is
+      /// This increments the reference counter of the node.
-      /// used).
+      const formula* clone() const
-      const formula* clone() const;
+      {
-      /// \brief release this node
+	++refs_;
-      ///
+	return this;
-      /// This decrements the reference counter of this node (if one is
+      }
-      /// used) and can free the object.
+
-      void destroy() const;
+      /// \brief Release this node
+      void destroy() const
+      {
+	// Delete if this is the last node, and it is not a constant.
+	if (!refs_)
+	  {
+	    if (kind() != Constant)
+	      delete this;
+	  }
+	else
+	  {
+	    --refs_;
+	  }
+      }
 
       /// Return a canonic representation of the formula
       virtual std::string dump() const = 0;
@@ -293,17 +306,19 @@ namespace spot
 	return serial_;
       }
     protected:
-      virtual ~formula();
+      virtual ~formula()
-
+      {
-      /// \brief increment reference counter if any
+      }
-      virtual void ref_() const;
-      /// \brief decrement reference counter if any, return true when
-      /// the instance must be deleted (usually when the counter hits 0).
-      virtual bool unref_() const;
 
       /// \brief The hash key of this formula.
       size_t serial_;
 
+      // The number of actual references is refs_ + 1.
+      mutable unsigned refs_ = 0;
+      /// \brief Number of formulae created so far.
+      static size_t max_serial;
+      opkind kind_;
+
       struct ltl_prop
       {
 	// All properties here should be expressed in such a a way
@@ -346,11 +361,6 @@ namespace spot
 	unsigned props;
 	ltl_prop is;
       };
-
-    private:
-      /// \brief Number of formulae created so far.
-      static size_t max_serial;
-      opkind kind_;
     };
 
 

src/ltlast/multop.cc

@@ -36,7 +36,7 @@ namespace spot
   namespace ltl
   {
     multop::multop(type op, vec* v)
-      : ref_formula(MultOp), op_(op), children_(v)
+      : formula(MultOp), op_(op), children_(v)
     {
       unsigned s = v->size();
       assert(s > 1);
@@ -592,7 +592,7 @@ namespace spot
 	  v->insert(v->begin(), constant::true_instance());
 	}
 
-      const multop* res;
+      const formula* res;
       // Insert the key with the dummy nullptr just
       // to check if p already exists.
       auto ires = instances.emplace(key(op, v), nullptr);
@@ -602,14 +602,13 @@ namespace spot
 	  for (auto f: *v)
 	    f->destroy();
 	  delete v;
-	  res = ires.first->second;
+	  res = ires.first->second->clone();
 	}
       else
 	{
 	  // The instance did not already exist.
 	  res = ires.first->second = new multop(op, v);
 	}
-      res->clone();
       return res;
     }
 
@@ -633,9 +632,9 @@ namespace spot
     {
       for (const auto& i: instances)
 	os << i.second << " = "
-	   << i.second->ref_count_() << " * "
+	   << 1 + i.second->refs_ << " * "
 	   << i.second->dump()
-	   << std::endl;
+	   << '\n';
       return os;
     }
 

src/ltlast/multop.hh

@@ -25,7 +25,7 @@
 #ifndef SPOT_LTLAST_MULTOP_HH
 # define SPOT_LTLAST_MULTOP_HH
 
-#include "refformula.hh"
+#include "formula.hh"
 #include <vector>
 #include <map>
 #include <iosfwd>
@@ -37,7 +37,7 @@ namespace spot
 
     /// \ingroup ltl_ast
     /// \brief Multi-operand operators.
-    class SPOT_API multop : public ref_formula
+    class SPOT_API multop : public formula
     {
     public:
       enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion };

src/ltlast/refformula.cc

@@ -1,60 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de
-// Developpement de l'EPITA (LRDE).
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include "config.h"
-#include "refformula.hh"
-#include <cassert>
-
-namespace spot
-{
-  namespace ltl
-  {
-    ref_formula::ref_formula(opkind k)
-      : formula(k), ref_counter_(0)
-    {
-    }
-
-    ref_formula::~ref_formula()
-    {
-    }
-
-    void
-    ref_formula::ref_() const
-    {
-      ++ref_counter_;
-    }
-
-    bool
-    ref_formula::unref_() const
-    {
-      assert(ref_counter_ > 0);
-      return !--ref_counter_;
-    }
-
-    unsigned
-    ref_formula::ref_count_() const
-    {
-      return ref_counter_;
-    }
-
-  }
-}

src/ltlast/refformula.hh

@@ -1,53 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de
-// Développement de l'EPITA (LRDE).
-// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-/// \file ltlast/refformula.hh
-/// \brief Reference-counted LTL formulae
-#ifndef SPOT_LTLAST_REFFORMULA_HH
-# define SPOT_LTLAST_REFFORMULA_HH
-
-#include "formula.hh"
-
-namespace spot
-{
-  namespace ltl
-  {
-
-    /// \ingroup ltl_ast
-    /// \brief A reference-counted LTL formula.
-    class SPOT_API ref_formula : public formula
-    {
-    protected:
-      virtual ~ref_formula();
-      ref_formula(opkind k);
-      void ref_() const;
-      bool unref_() const;
-      /// Number of references to this formula.
-      unsigned ref_count_() const;
-    private:
-      mutable unsigned ref_counter_;
-    };
-
-  }
-}
-
-#endif // SPOT_LTLAST_REFFORMULA_HH

src/ltlast/unop.cc

@@ -28,13 +28,14 @@
 #include <iostream>
 #include "constant.hh"
 #include "atomic_prop.hh"
+#include "bunop.hh"
 
 namespace spot
 {
   namespace ltl
   {
     unop::unop(type op, const formula* child)
-      : ref_formula(UnOp), op_(op), child_(child)
+      : formula(UnOp), op_(op), child_(child)
     {
       props = child->get_props();
       switch (op)
@@ -299,19 +300,18 @@ namespace spot
 	  break;
 	}
 
-      const unop* res;
+      const formula* res;
       auto ires = instances.emplace(key(op, child), nullptr);
       if (!ires.second)
 	{
 	  // This instance already exists.
 	  child->destroy();
-	  res = ires.first->second;
+	  res = ires.first->second->clone();
 	}
       else
 	{
 	  res = ires.first->second = new unop(op, child);
 	}
-      res->clone();
       return res;
     }
 
@@ -326,9 +326,9 @@ namespace spot
     {
       for (const auto& i: instances)
 	os << i.second << " = "
-	   << i.second->ref_count_() << " * "
+	   << 1 + i.second->refs_ << " * "
 	   << i.second->dump()
-	   << std::endl;
+	   << '\n';
       return os;
     }
 

src/ltlast/unop.hh

@@ -27,8 +27,7 @@
 
 #include <map>
 #include <iosfwd>
-#include "refformula.hh"
+#include "formula.hh"
-#include "bunop.hh"
 
 namespace spot
 {
@@ -37,7 +36,7 @@ namespace spot
 
     /// \ingroup ltl_ast
     /// \brief Unary operators.
-    class SPOT_API unop : public ref_formula
+    class SPOT_API unop : public formula
     {
     public:
       enum type {

wrap/python/spot.i

@@ -79,7 +79,6 @@ namespace std {
 #include "misc/random.hh"
 
 #include "ltlast/formula.hh"
-#include "ltlast/refformula.hh"
 #include "ltlast/atomic_prop.hh"
 #include "ltlast/binop.hh"
 #include "ltlast/constant.hh"
@@ -198,7 +197,6 @@ using namespace spot;
 %include "misc/random.hh"
 
 %include "ltlast/formula.hh"
-%include "ltlast/refformula.hh"
 %include "ltlast/atomic_prop.hh"
 %include "ltlast/binop.hh"
 %include "ltlast/constant.hh"