From b0888257f8914d8c1274af5f21a00bc0c7325084 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 Nov 2009 11:41:46 +0100 Subject: [PATCH] Rename formula::ref and formula::unref as formula::clone and formula::destroy. * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc, src/ltlast/binop.cc, src/ltlast/formula.hh, src/ltlast/formula.cc, src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, src/ltlvisit/destroy.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc, src/ltlvisit/reduce.cc, src/tgbatest/randtgba.cc: Adjust. --- ChangeLog | 13 +++++++++++++ src/ltlast/atomic_prop.cc | 6 +++--- src/ltlast/automatop.cc | 8 ++++---- src/ltlast/binop.cc | 12 ++++++------ src/ltlast/formula.cc | 6 +++--- src/ltlast/formula.hh | 12 ++++-------- src/ltlast/multop.cc | 16 ++++++++-------- src/ltlast/unop.cc | 8 ++++---- src/ltlenv/declenv.cc | 5 ++--- src/ltlvisit/basicreduce.cc | 4 ++-- src/ltlvisit/clone.cc | 6 +++--- src/ltlvisit/destroy.cc | 2 +- src/ltlvisit/nenoform.cc | 4 ++-- src/ltlvisit/randomltl.cc | 4 ++-- src/ltlvisit/reduce.cc | 4 ++-- src/tgbatest/randtgba.cc | 7 ++++--- 16 files changed, 63 insertions(+), 54 deletions(-) diff --git a/ChangeLog b/ChangeLog index 9d72804e2..e5e44a709 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2009-11-08 Alexandre Duret-Lutz + + Rename formula::ref and formula::unref as formula::clone + and formula::destroy. + + * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc, + src/ltlast/binop.cc, src/ltlast/formula.hh, src/ltlast/formula.cc, + src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc, + src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, + src/ltlvisit/destroy.cc, src/ltlvisit/nenoform.cc, + src/ltlvisit/randomltl.cc, src/ltlvisit/reduce.cc, + src/tgbatest/randtgba.cc: Adjust. + 2009-11-07 Alexandre Duret-Lutz Change the way references are counted to speedup cloning. diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 8fd0d2384..29a91cfaa 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -78,11 +78,11 @@ namespace spot map::iterator i = instances.find(p); if (i != instances.end()) { - return static_cast(i->second->ref()); + return static_cast(i->second->clone()); } atomic_prop* ap = new atomic_prop(name, env); instances[p] = ap; - return static_cast(ap->ref()); + return static_cast(ap->clone()); } unsigned diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 0c222417b..fea815d30 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -50,7 +50,7 @@ namespace spot // Dereference children. for (unsigned n = 0; n < size(); ++n) - formula::unref(nth(n)); + formula::destroy(nth(n)); delete children_; } @@ -79,13 +79,13 @@ namespace spot { // The instance already exists. for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) - formula::unref(*vi); + formula::destroy(*vi); delete v; - return static_cast(i->second->ref()); + return static_cast(i->second->clone()); } automatop* res = new automatop(nfa, v, negated); instances[p] = res; - return static_cast(res->ref()); + return static_cast(res->clone()); } unsigned diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index af5758402..9018239a3 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -48,8 +48,8 @@ namespace spot instances.erase(i); // Dereference children. - formula::unref(first()); - formula::unref(second()); + formula::destroy(first()); + formula::destroy(second()); } void @@ -143,13 +143,13 @@ namespace spot if (i != instances.end()) { // This instance already exists. - formula::unref(first); - formula::unref(second); - return static_cast(i->second->ref()); + formula::destroy(first); + formula::destroy(second); + return static_cast(i->second->clone()); } binop* ap = new binop(op, first, second); instances[p] = ap; - return static_cast(ap->ref()); + return static_cast(ap->clone()); } unsigned diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index e194c2c72..c0c498e78 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2005, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -27,7 +27,7 @@ namespace spot namespace ltl { formula* - formula::ref() + formula::clone() { ref_(); return this; @@ -38,7 +38,7 @@ namespace spot } void - formula::unref(formula* f) + formula::destroy(formula* f) { if (f->unref_()) delete f; diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index dba656f7c..1667d7d1c 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -79,17 +79,13 @@ namespace spot /// \brief clone this node /// /// This increments the reference counter of this node (if one is - /// used). You should almost never use this method directly as - /// it doesn't touch the children. If you want to clone a - /// whole formula, use spot::ltl::clone() instead. - formula* ref(); + /// used). + formula* clone(); /// \brief release this node /// /// This decrements the reference counter of this node (if one is - /// used) and can free the object. You should almost never use - /// this method directly as it doesn't touch the children. If you - /// want to release a whole formula, use spot::ltl::destroy() instead. - static void unref(formula* f); + /// used) and can free the object. + static void destroy(formula* f); /// Return a canonic representation of the formula const std::string& dump() const; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 8317e6fcf..3b62d6ed2 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -55,7 +55,7 @@ namespace spot // Dereference children. for (unsigned n = 0; n < size(); ++n) - formula::unref(nth(n)); + formula::destroy(nth(n)); delete children_; } @@ -130,8 +130,8 @@ namespace spot { unsigned ps = p->size(); for (unsigned n = 0; n < ps; ++n) - inlined.push_back(p->nth(n)->ref()); - formula::unref(*i); + inlined.push_back(p->nth(n)->clone()); + formula::destroy(*i); i = v->erase(i); } else @@ -145,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 unref() any formula we drop. + // must destroy() any formula we drop. { formula* last = 0; vec::iterator i = v->begin(); @@ -153,7 +153,7 @@ namespace spot { if (*i == last) { - formula::unref(*i); + formula::destroy(*i); i = v->erase(i); } else @@ -193,9 +193,9 @@ namespace spot { // The instance already exists. for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) - formula::unref(*vi); + formula::destroy(*vi); delete v; - return static_cast(i->second->ref()); + return static_cast(i->second->clone()); } // This is the first instance of this formula. @@ -203,7 +203,7 @@ namespace spot // Record the instance in the map, multop* ap = new multop(op, v); instances[p] = ap; - return ap->ref(); + return ap->clone(); } formula* diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 963e8484c..63bed9cda 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -46,7 +46,7 @@ namespace spot instances.erase(i); // Dereference child. - formula::unref(child()); + formula::destroy(child()); } void @@ -110,12 +110,12 @@ namespace spot if (i != instances.end()) { // This instance already exists. - formula::unref(child); - return static_cast(i->second->ref()); + formula::destroy(child); + return static_cast(i->second->clone()); } unop* ap = new unop(op, child); instances[p] = ap; - return static_cast(ap->ref()); + return static_cast(ap->clone()); } unsigned diff --git a/src/ltlenv/declenv.cc b/src/ltlenv/declenv.cc index 9f3a5a55f..71c795166 100644 --- a/src/ltlenv/declenv.cc +++ b/src/ltlenv/declenv.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -51,8 +51,7 @@ namespace spot prop_map::iterator i = props_.find(prop_str); if (i == props_.end()) return 0; - // It's an atomic_prop, so we do not have to use the clone() visitor. - return i->second->ref(); + return i->second->clone(); } const std::string& diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 7c0a7dac3..0eaea337b 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2007, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2007, 2008, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -76,7 +76,7 @@ namespace spot void visit(atomic_prop* ap) { - formula* f = ap->ref(); + formula* f = ap->clone(); result_ = f; } diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index e08de2c0f..8c6339662 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -43,13 +43,13 @@ namespace spot void clone_visitor::visit(atomic_prop* ap) { - result_ = ap->ref(); + result_ = ap->clone(); } void clone_visitor::visit(constant* c) { - result_ = c->ref(); + result_ = c->clone(); } void @@ -93,7 +93,7 @@ namespace spot formula* clone(const formula* f) { - formula* res = const_cast(f)->ref(); + formula* res = const_cast(f)->clone(); return res; } } diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 9e6e01257..9f61cd808 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -28,7 +28,7 @@ namespace spot void destroy(const formula* f) { - formula::unref(const_cast(f)); + formula::destroy(const_cast(f)); } } } diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 9799996ce..1dfb233a5 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.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. // @@ -50,7 +50,7 @@ namespace spot void visit(atomic_prop* ap) { - formula* f = ap->ref(); + formula* f = ap->clone(); if (negated_) result_ = unop::instance(unop::Not, f); else diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 73cf99493..2816703e2 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2005, 2008 Laboratoire d'Informatique de Paris 6 +// Copyright (C) 2005, 2008, 2009 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // @@ -40,7 +40,7 @@ namespace spot (void) n; atomic_prop_set::const_iterator i = rl->ap()->begin(); std::advance(i, mrand(rl->ap()->size())); - return (*i)->ref(); + return (*i)->clone(); } formula* diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index ae5915a7e..ad364059c 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006, 2007, 2008 Laboratoire d'Informatique de +// Copyright (C) 2004, 2006, 2007, 2008, 2009 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -59,7 +59,7 @@ namespace spot void visit(atomic_prop* ap) { - formula* f = ap->ref(); + formula* f = ap->clone(); result_ = f; } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 5204484af..6080da701 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris +// Copyright (C) 2004, 2005, 2008, 2009 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -876,7 +876,8 @@ main(int argc, char** argv) spot::ltl::atomic_prop_collect(f); for (spot::ltl::atomic_prop_set::iterator i = tmp->begin(); i != tmp->end(); ++i) - apf->insert(dynamic_cast((*i)->ref())); + apf->insert(dynamic_cast + ((*i)->clone())); spot::ltl::destroy(f); delete tmp; } @@ -890,7 +891,7 @@ main(int argc, char** argv) for (spot::ltl::atomic_prop_set::iterator i = ap->begin(); i != ap->end(); ++i) - apf->insert(dynamic_cast((*i)->ref())); + apf->insert(dynamic_cast((*i)->clone())); if (!opt_S) {