From 5f6d8b62349b9cc07bbcd29b37f43e998b350a1d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 May 2003 13:39:39 +0000 Subject: [PATCH] Massage the AST so that identical sub-formula share the same reference-counted formula*. One can't call constructors for AST items anymore, everything need to be acquired through instance() class methods. * src/ltlast/formula.cc, src/ltlast/refformula.cc, src/ltlast/refformula.hh: New files. * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them. * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor and destructor protected. Define a static function `instance()' to get an instance with specific argument. Use a map called `instances' to store all known instances. Inherit from ref_formula. * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect the constructor and destructor. Provide the false_instance() and true_instance() functions instead. * src/formula.hh (ref, unref, ref_, unref_): New methods. * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect the constructor, destructor, as well as the add() method. Provides the instance(), and add() class methods instead. Store children_ as a pointer. * src/ltlenv/defaultenv.cc (require): Adjust to call atomic_prop::instance. * src/ltlparse/ltlparse.yy: Adjust to call instance() functions instead of constructors. * src/ltltest/Makefile.am (LDADD): Tweak library ordering. * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor, not const_visitor, and adjust all prototypes appropriately. * src/ltlvisit/clone.cc (clone_visitor): Likewise. Call ref() or instance() methods instead of copy constructors. * src/ltlvisit/equals.cc: Simplify atomic_prop and constant cases. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc, src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance() methods instead of constructor. Make these children of visitor, not const_visitor. * src/ltltest/readltl.c (main): Do not delete the formula. --- ChangeLog | 41 ++++++++++++++ src/ltlast/Makefile.am | 4 +- src/ltlast/atomic_prop.cc | 28 +++++++--- src/ltlast/atomic_prop.hh | 18 +++++-- src/ltlast/binop.cc | 25 +++++++-- src/ltlast/binop.hh | 15 +++++- src/ltlast/constant.cc | 19 +++++-- src/ltlast/constant.hh | 13 +++-- src/ltlast/formula.cc | 34 ++++++++++++ src/ltlast/formula.hh | 22 ++++++-- src/ltlast/multop.cc | 111 +++++++++++++++++++++++++------------- src/ltlast/multop.hh | 33 +++++++++--- src/ltlast/refformula.cc | 27 ++++++++++ src/ltlast/refformula.hh | 25 +++++++++ src/ltlast/unop.cc | 22 ++++++-- src/ltlast/unop.hh | 16 ++++-- src/ltlenv/defaultenv.cc | 4 +- src/ltlparse/ltlparse.yy | 28 +++++----- src/ltltest/Makefile.am | 4 +- src/ltltest/readltl.cc | 1 - src/ltlvisit/clone.cc | 50 ++++++++--------- src/ltlvisit/clone.hh | 24 ++++----- src/ltlvisit/equals.cc | 40 +++++++------- src/ltlvisit/lunabbrev.cc | 43 ++++++++------- src/ltlvisit/lunabbrev.hh | 12 ++--- src/ltlvisit/nenoform.cc | 94 ++++++++++++++++---------------- src/ltlvisit/nenoform.hh | 8 +-- src/ltlvisit/tunabbrev.cc | 28 +++++----- src/ltlvisit/tunabbrev.hh | 12 ++--- 29 files changed, 548 insertions(+), 253 deletions(-) create mode 100644 src/ltlast/formula.cc create mode 100644 src/ltlast/refformula.cc create mode 100644 src/ltlast/refformula.hh diff --git a/ChangeLog b/ChangeLog index 5e55e353e..af56c9a61 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,46 @@ 2003-05-15 Alexandre Duret-Lutz + Massage the AST so that identical sub-formula share the same + reference-counted formula*. One can't call constructors for AST + items anymore, everything need to be acquired through instance() + class methods. + + * src/ltlast/formula.cc, src/ltlast/refformula.cc, + src/ltlast/refformula.hh: New files. + * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them. + * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, + src/ltlast/unop.cc, src/ltlast/unop.hh, + src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor + and destructor protected. Define a static function `instance()' + to get an instance with specific argument. Use a map called + `instances' to store all known instances. Inherit from + ref_formula. + * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect + the constructor and destructor. Provide the false_instance() + and true_instance() functions instead. + * src/formula.hh (ref, unref, ref_, unref_): New methods. + * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect + the constructor, destructor, as well as the add() method. + Provides the instance(), and add() class methods instead. + Store children_ as a pointer. + * src/ltlenv/defaultenv.cc (require): Adjust to + call atomic_prop::instance. + * src/ltlparse/ltlparse.yy: Adjust to call instance() functions + instead of constructors. + * src/ltltest/Makefile.am (LDADD): Tweak library ordering. + * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor, + not const_visitor, and adjust all prototypes appropriately. + * src/ltlvisit/clone.cc (clone_visitor): Likewise. + Call ref() or instance() methods instead of copy constructors. + * src/ltlvisit/equals.cc: Simplify atomic_prop and constant + cases. + * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc, + src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc, + src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance() + methods instead of constructor. Make these children of visitor, not + const_visitor. + * src/ltltest/readltl.c (main): Do not delete the formula. + * src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to remove a warning with newer versions of Flex. diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 57251bf3e..114e257a7 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -11,10 +11,12 @@ libltlast_la_SOURCES = \ constant.cc \ constant.hh \ formula.hh \ + formula.cc \ multop.cc \ multop.hh \ predecl.hh \ + refformula.cc \ + refformula.hh \ unop.cc \ unop.hh \ visitor.hh - diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 70bd1cccf..51d900743 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -5,7 +5,7 @@ namespace spot { namespace ltl { - + atomic_prop::atomic_prop(const std::string& name, environment& env) : name_(name), env_(&env) { @@ -15,29 +15,45 @@ namespace spot { } - void + void atomic_prop::accept(visitor& v) { v.visit(this); } - + void atomic_prop::accept(const_visitor& v) const { v.visit(this); - } + } const std::string& atomic_prop::name() const { return name_; } - - environment& + + environment& atomic_prop::env() const { return *env_; } + atomic_prop::map atomic_prop::instances; + + atomic_prop* + atomic_prop::instance(const std::string& name, environment& env) + { + pair p(name, &env); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast(i->second->ref()); + } + atomic_prop* ap = new atomic_prop(name, env); + instances[p] = ap; + return static_cast(ap->ref()); + } + } } diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index f293f10d6..a55984d3a 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -2,7 +2,8 @@ # define SPOT_LTLAST_ATOMIC_PROP_HH #include -#include "formula.hh" +#include +#include "refformula.hh" #include "ltlenv/environment.hh" namespace spot @@ -11,13 +12,12 @@ namespace spot { /// Atomic propositions. - class atomic_prop : public formula + class atomic_prop : public ref_formula { public: - /// Build an atomic proposition with name \a name in + /// Build an atomic proposition with name \a name in /// environment \a env. - atomic_prop(const std::string& name, environment& env); - virtual ~atomic_prop(); + static atomic_prop* instance(const std::string& name, environment& env); virtual void accept(visitor& visitor); virtual void accept(const_visitor& visitor) const; @@ -26,6 +26,14 @@ namespace spot const std::string& name() const; /// Get the environment of the atomic proposition. environment& env() const; + protected: + atomic_prop(const std::string& name, environment& env); + virtual ~atomic_prop(); + + typedef std::pair pair; + typedef std::map map; + static map instances; + private: std::string name_; environment* env_; diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 7aac72fbb..566264dba 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -5,7 +5,7 @@ namespace spot { namespace ltl - { + { binop::binop(type op, formula* first, formula* second) : op_(op), first_(first), second_(second) { @@ -45,19 +45,19 @@ namespace spot return second_; } - formula* + formula* binop::second() { return second_; } - binop::type + binop::type binop::op() const { return op_; } - const char* + const char* binop::op_name() const { switch (op_) @@ -78,5 +78,22 @@ namespace spot return 0; } + binop::map binop::instances; + + binop* + binop::instance(type op, formula* first, formula* second) + { + pairf pf(first, second); + pair p(op, pf); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast(i->second->ref()); + } + binop* ap = new binop(op, first, second); + instances[p] = ap; + return static_cast(ap->ref()); + } + } } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 8ebd996fb..9ad27d72a 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,6 +1,7 @@ #ifndef SPOT_LTLAST_BINOP_HH # define SPOT_LTLAST_BINOP_HH +#include #include "formula.hh" namespace spot @@ -18,8 +19,9 @@ namespace spot /// are often nested we represent them as multops. enum type { Xor, Implies, Equiv, U, R }; - binop(type op, formula* first, formula* second); - virtual ~binop(); + /// Build an unary operator with operation \a op and + /// children \a first and \a second. + static binop* instance(type op, formula* first, formula* second); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -38,6 +40,15 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + protected: + typedef std::pair pairf; + typedef std::pair pair; + typedef std::map map; + static map instances; + + binop(type op, formula* first, formula* second); + virtual ~binop(); + private: type op_; formula* first_; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index d7e52792c..73ecde98c 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -5,7 +5,7 @@ namespace spot { namespace ltl - { + { constant::constant(type val) : val_(val) { @@ -27,13 +27,13 @@ namespace spot v.visit(this); } - constant::type + constant::type constant::val() const { return val_; } - const char* + const char* constant::val_name() const { switch (val_) @@ -48,5 +48,18 @@ namespace spot return 0; } + constant* + constant::false_instance() + { + static constant f(constant::False); + return &f; + } + + constant* + constant::true_instance() + { + static constant t(constant::True); + return &t; + } } } diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 731dcf14f..09410bc7b 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -13,10 +13,6 @@ namespace spot { public: enum type { False, True }; - - constant(type val); - virtual ~constant(); - virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -25,6 +21,15 @@ namespace spot /// Return the value of the constant as a string. const char* val_name() 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). + static constant* false_instance(); + + protected: + constant(type val); + virtual ~constant(); + private: type val_; }; diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc new file mode 100644 index 000000000..02fca0f30 --- /dev/null +++ b/src/ltlast/formula.cc @@ -0,0 +1,34 @@ +#include "formula.hh" + +namespace spot +{ + namespace ltl + { + formula* + formula::ref() + { + ref_(); + return this; + } + + void + formula::unref(formula* f) + { + if (f->unref_()) + delete f; + } + + void + formula::ref_() + { + // Not reference counted by default. + } + + bool + formula::unref_() + { + // Not reference counted by default. + return false; + } + } +} diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 5784d3575..2fc674a77 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -3,20 +3,32 @@ #include "predecl.hh" -namespace spot +namespace spot { - namespace ltl + namespace ltl { /// \brief An LTL formula. - /// - /// The only way you can work with a formula is to + /// + /// The only way you can work with a formula is to /// build a spot::ltl::visitor or spot::ltl::const_visitor. - class formula + class formula { public: virtual void accept(visitor& v) = 0; virtual void accept(const_visitor& v) const = 0; + + /// \brief clone this formula + formula* ref(); + /// \brief release formula + static void unref(formula* f); + + protected: + /// \brief increment reference counter if any + virtual void ref_(); + /// \brief decrement reference counter if any, return true when + /// the instance must be delete (usually when the counter hits 0). + virtual bool unref_(); }; } diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 1da9f5595..a2295828d 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -6,42 +6,15 @@ namespace spot { namespace ltl - { - multop::multop(type op) - : op_(op) + { + multop::multop(type op, vec* v) + : op_(op), children_(v) { } - multop::multop(type op, formula* first, formula* second) - : op_(op) - { - children_.reserve(2); - add(first); - add(second); - } - - void - multop::add(formula* f) - { - // If the formula we add is itself a multop for the same operator, - // merge its children with ours. - multop* p = dynamic_cast(f); - if (p && p->op() == op()) - { - unsigned ps = p->size(); - for (unsigned i = 0; i < ps; ++i) - children_.push_back(p->nth(i)); - // that sub-formula is now useless - delete f; - } - else - { - children_.push_back(f); - } - } - multop::~multop() { + delete children_; } void @@ -59,28 +32,28 @@ namespace spot unsigned multop::size() const { - return children_.size(); + return children_->size(); } const formula* multop::nth(unsigned n) const { - return children_[n]; + return (*children_)[n]; } - formula* + formula* multop::nth(unsigned n) { - return children_[n]; + return (*children_)[n]; } - multop::type + multop::type multop::op() const { return op_; } - const char* + const char* multop::op_name() const { switch (op_) @@ -95,5 +68,69 @@ namespace spot return 0; } + multop::map multop::instances; + + multop* + multop::instance(type op, vec* v) + { + pair p(op, v); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + delete v; + return static_cast(i->second->ref()); + } + multop* ap = new multop(op, v); + instances[p] = ap; + return static_cast(ap->ref()); + + } + + multop* + multop::instance(type op) + { + return instance(op, new vec); + } + + multop* + multop::instance(type op, formula* first, formula* second) + { + vec* v = new vec; + multop::add(op, v, first); + multop::add(op, v, second); + return instance(op, v); + } + + multop::vec* + multop::add(type op, vec* v, formula* f) + { + // If the formula we add is itself a multop for the same operator, + // merge its children. + multop* p = dynamic_cast(f); + if (p && p->op() == op) + { + unsigned ps = p->size(); + for (unsigned i = 0; i < ps; ++i) + v->push_back(p->nth(i)); + // that sub-formula is now useless + formula::unref(f); + } + else + { + v->push_back(f); + } + return v; + } + + void + multop::add(multop** m, formula* f) + { + vec* v = new vec(*(*m)->children_); + type op = (*m)->op(); + multop::add(op, v, f); + formula::unref(*m); + *m = instance(op, v); + } + } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index a849c9230..8ff548718 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -2,13 +2,14 @@ # define SPOT_LTLAST_MULTOP_HH #include +#include #include "formula.hh" namespace spot { namespace ltl { - + /// \brief Multi-operand operators. /// /// These operators are considered commutative and associative. @@ -17,25 +18,29 @@ namespace spot public: enum type { Or, And }; + /// \brief Build a spot::ltl::multop with no child. /// /// This has little value unless you call multop::add later. - multop(type op); + static multop* instance(type op); + /// \brief Build a spot::ltl::multop with two children. - /// + /// /// If one of the children itself is a spot::ltl::multop /// with the same type, it will be merged. I.e., children /// if that child will be added, and that child itself will /// be destroyed. - multop(type op, formula* first, formula* second); + static multop* instance(type op, formula* first, formula* second); + /// \brief Add another child to this operator. /// /// If \a f itself is a spot::ltl::multop with the same type, it /// will be merged. I.e., children of \a f will be added, and /// that \a f will will be destroyed. - void add(formula* f); - - virtual ~multop(); + /// + /// Note that this function overwrites the supplied ltl::multop pointer. + /// The old value is released and should not be used after this. + static void add(multop** m, formula* f); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -56,9 +61,21 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + protected: + typedef std::vector vec; + typedef std::pair pair; + typedef std::map map; + static map instances; + + multop(type op, vec* v); + static multop* instance(type op, vec* v); + static vec* multop::add(type op, vec* v, formula* f); + + virtual ~multop(); + private: type op_; - std::vector children_; + vec* children_; }; } diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc new file mode 100644 index 000000000..0286d20fe --- /dev/null +++ b/src/ltlast/refformula.cc @@ -0,0 +1,27 @@ +#include "refformula.hh" +#include + +namespace spot +{ + namespace ltl + { + ref_formula::ref_formula() + : ref_count_(0) + { + } + + void + ref_formula::ref_() + { + ++ref_count_; + } + + bool + ref_formula::unref_() + { + assert(ref_count_ > 0); + return !--ref_count_; + } + + } +} diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh new file mode 100644 index 000000000..36572cbec --- /dev/null +++ b/src/ltlast/refformula.hh @@ -0,0 +1,25 @@ +#ifndef SPOT_LTLAST_REFFORMULAE_HH +# define SPOT_LTLAST_REFFORMULAE_HH + +#include "formula.hh" + +namespace spot +{ + namespace ltl + { + + /// \brief A reference-counted LTL formula. + class ref_formula : public formula + { + protected: + ref_formula(); + void ref_(); + bool unref_(); + private: + unsigned ref_count_; + }; + + } +} + +#endif // SPOT_LTLAST_REFFORMULAE_HH diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index f4f205b1e..e15597c51 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -5,7 +5,7 @@ namespace spot { namespace ltl - { + { unop::unop(type op, formula* child) : op_(op), child_(child) { @@ -39,13 +39,13 @@ namespace spot return child_; } - unop::type + unop::type unop::op() const { return op_; } - const char* + const char* unop::op_name() const { switch (op_) @@ -64,5 +64,21 @@ namespace spot return 0; } + unop::map unop::instances; + + unop* + unop::instance(type op, formula* child) + { + pair p(op, child); + map::iterator i = instances.find(p); + if (i != instances.end()) + { + return static_cast(i->second->ref()); + } + unop* ap = new unop(op, child); + instances[p] = ap; + return static_cast(ap->ref()); + } + } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 659f45b44..54510e489 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,21 +1,23 @@ #ifndef SPOT_LTLAST_UNOP_HH # define SPOT_LTLAST_UNOP_HH +#include #include "formula.hh" namespace spot { namespace ltl { - + /// Unary operator. class unop : public formula { public: enum type { Not, X, F, G }; - unop(type op, formula* child); - virtual ~unop(); + /// Build an unary operator with operation \a op and + /// child \a child. + static unop* instance(type op, formula* child); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -30,6 +32,14 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + protected: + typedef std::pair pair; + typedef std::map map; + static map instances; + + unop(type op, formula* child); + virtual ~unop(); + private: type op_; formula* child_; diff --git a/src/ltlenv/defaultenv.cc b/src/ltlenv/defaultenv.cc index 0f9cc2e17..c7a495108 100644 --- a/src/ltlenv/defaultenv.cc +++ b/src/ltlenv/defaultenv.cc @@ -9,7 +9,7 @@ namespace spot formula* default_environment::require(const std::string& s) { - return new atomic_prop(s, *this); + return atomic_prop::instance(s, *this); } const std::string& @@ -23,7 +23,7 @@ namespace spot { } - default_environment& + default_environment& default_environment::instance() { static default_environment* singleton = new default_environment(); diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index d3d807375..47251589c 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -101,15 +101,15 @@ subformula: ATOMIC_PROP delete $1; } | CONST_TRUE - { $$ = new constant(constant::True); } + { $$ = constant::true_instance(); } | CONST_FALSE - { $$ = new constant(constant::False); } + { $$ = constant::false_instance(); } | PAR_OPEN subformula PAR_CLOSE { $$ = $2; } | PAR_OPEN error PAR_CLOSE { error_list.push_back(parse_error(@$, "treating this parenthetical block as false")); - $$ = new constant(constant::False); + $$ = constant::false_instance(); } | PAR_OPEN subformula many_errors PAR_CLOSE { error_list.push_back(parse_error(@3, @@ -117,27 +117,27 @@ subformula: ATOMIC_PROP $$ = $2; } | OP_NOT subformula - { $$ = new unop(unop::Not, $2); } + { $$ = unop::instance(unop::Not, $2); } | subformula OP_AND subformula - { $$ = new multop(multop::And, $1, $3); } + { $$ = multop::instance(multop::And, $1, $3); } | subformula OP_OR subformula - { $$ = new multop(multop::Or, $1, $3); } + { $$ = multop::instance(multop::Or, $1, $3); } | subformula OP_XOR subformula - { $$ = new binop(binop::Xor, $1, $3); } + { $$ = binop::instance(binop::Xor, $1, $3); } | subformula OP_IMPLIES subformula - { $$ = new binop(binop::Implies, $1, $3); } + { $$ = binop::instance(binop::Implies, $1, $3); } | subformula OP_EQUIV subformula - { $$ = new binop(binop::Equiv, $1, $3); } + { $$ = binop::instance(binop::Equiv, $1, $3); } | subformula OP_U subformula - { $$ = new binop(binop::U, $1, $3); } + { $$ = binop::instance(binop::U, $1, $3); } | subformula OP_R subformula - { $$ = new binop(binop::R, $1, $3); } + { $$ = binop::instance(binop::R, $1, $3); } | OP_F subformula - { $$ = new unop(unop::F, $2); } + { $$ = unop::instance(unop::F, $2); } | OP_G subformula - { $$ = new unop(unop::G, $2); } + { $$ = unop::instance(unop::G, $2); } | OP_X subformula - { $$ = new unop(unop::X, $2); } + { $$ = unop::instance(unop::X, $2); } // | subformula many_errors // { error_list->push_back(parse_error(@2, // "ignoring these unexpected trailing tokens")); diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 37154e47a..066fc7341 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -1,8 +1,8 @@ AM_CPPFLAGS = -I$(srcdir)/.. LDADD = ../ltlparse/libltlparse.la \ ../ltlvisit/libltlvisit.la \ - ../ltlast/libltlast.la \ - ../ltlenv/libltlenv.la + ../ltlenv/libltlenv.la \ + ../ltlast/libltlast.la check_SCRIPTS = defs # Keep this sorted alphabetically. diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index bfcbd5b80..261c4d4f6 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -46,7 +46,6 @@ main(int argc, char** argv) spot::ltl::dump(*f, std::cout); std::cout << std::endl; #endif - delete f; } else { diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index ff27625d5..f9a976f87 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,7 +1,7 @@ #include "ltlast/allnodes.hh" #include "clone.hh" -namespace spot +namespace spot { namespace ltl { @@ -18,52 +18,52 @@ namespace spot { return result_; } - - void - clone_visitor::visit(const atomic_prop* ap) + + void + clone_visitor::visit(atomic_prop* ap) { - result_ = new atomic_prop(ap->name(), ap->env()); + result_ = ap->ref(); } - void - clone_visitor::visit(const constant* c) + void + clone_visitor::visit(constant* c) { - result_ = new constant(c->val()); + result_ = c->ref(); } - void - clone_visitor::visit(const unop* uo) + void + clone_visitor::visit(unop* uo) { - result_ = new unop(uo->op(), recurse(uo->child())); + result_ = unop::instance(uo->op(), recurse(uo->child())); } - - void - clone_visitor::visit(const binop* bo) + + void + clone_visitor::visit(binop* bo) { - result_ = new binop(bo->op(), - recurse(bo->first()), recurse(bo->second())); + result_ = binop::instance(bo->op(), + recurse(bo->first()), recurse(bo->second())); } - - void - clone_visitor::visit(const multop* mo) + + void + clone_visitor::visit(multop* mo) { - multop* res = new multop(mo->op()); + multop* res = multop::instance(mo->op()); unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) { - res->add(recurse(mo->nth(i))); + multop::add(&res, recurse(mo->nth(i))); } result_ = res; } - formula* - clone_visitor::recurse(const formula* f) + formula* + clone_visitor::recurse(formula* f) { return clone(f); } - formula* - clone(const formula* f) + formula* + clone(formula* f) { clone_visitor v; f->accept(v); diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index c9c2d6fca..6a4dcf97b 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -4,7 +4,7 @@ #include "ltlast/formula.hh" #include "ltlast/visitor.hh" -namespace spot +namespace spot { namespace ltl { @@ -14,28 +14,28 @@ namespace spot /// to derive from it and override part of its methods. /// But if you just want the functionality, consider using /// spot::ltl::clone instead. - class clone_visitor : public const_visitor + class clone_visitor : public visitor { public: clone_visitor(); virtual ~clone_visitor(); formula* result() const; - - void visit(const atomic_prop* ap); - void visit(const unop* uo); - void visit(const binop* bo); - void visit(const multop* mo); - void visit(const constant* c); - - virtual formula* recurse(const formula* f); - + + void visit(atomic_prop* ap); + void visit(unop* uo); + void visit(binop* bo); + void visit(multop* mo); + void visit(constant* c); + + virtual formula* recurse(formula* f); + protected: formula* result_; }; /// \brief Clone a formula. - formula* clone(const formula* f); + formula* clone(formula* f); } } diff --git a/src/ltlvisit/equals.cc b/src/ltlvisit/equals.cc index 915f606f9..6e0cf49b5 100644 --- a/src/ltlvisit/equals.cc +++ b/src/ltlvisit/equals.cc @@ -2,7 +2,7 @@ #include "equals.hh" #include "ltlast/allnodes.hh" -namespace spot +namespace spot { namespace ltl { @@ -15,26 +15,22 @@ namespace spot { } - bool + bool equals_visitor::result() const { return result_; } - + void equals_visitor::visit(const atomic_prop* ap) { - const atomic_prop* p = dynamic_cast(f_); - if (p && p->name() == ap->name()) - result_ = true; + result_ = f_ == ap; } void equals_visitor::visit(const constant* c) { - const constant* p = dynamic_cast(f_); - if (p && p->val() == c->val()) - result_ = true; + result_ = f_ == c; } void @@ -53,34 +49,34 @@ namespace spot const binop* p = dynamic_cast(f_); if (!p || p->op() != bo->op()) return; - + // The current visitor will descend the left branch. // Build a second visitor for the right branch. equals_visitor v2(p->second()); f_ = p->first(); - + bo->first()->accept(*this); if (result_ == false) return; - + bo->second()->accept(v2); result_ = v2.result(); } - + void equals_visitor::visit(const multop* m) { const multop* p = dynamic_cast(f_); if (!p || p->op() != m->op()) return; - + // This check is a bit more complicated than other checks // because And(a, b, c) is equal to And(c, a, b, a). - + unsigned m_size = m->size(); unsigned p_size = p->size(); std::vector p_seen(p_size, false); - + for (unsigned nf = 0; nf < m_size; ++nf) { unsigned np; @@ -102,7 +98,7 @@ namespace spot // of `p'. That doesn't means that both formula are equal. // Condider m = And(a, b, c) against p = And(c, d, a, b). // We should now check if any unmarked (accodring to p_seen) - // child of `p' has an counterpart in `m'. Because `m' might + // child of `p' has an counterpart in `m'. Because `m' might // contain duplicate children, its faster to test that // unmarked children of `p' have a counterpart in marked children // of `p'. @@ -111,25 +107,25 @@ namespace spot // Consider only unmarked children. if (p_seen[np]) continue; - + // Compare with marked children. unsigned np2; const formula *pnth = p->nth(np); for (np2 = 0; np2 < p_size; ++np2) if (p_seen[np2] && equals(p->nth(np2), pnth)) break; - + // No match? Too bad. - if (np2 == p_size) + if (np2 == p_size) return; } - + // The two formulas match. result_ = true; } - bool + bool equals(const formula* f1, const formula* f2) { equals_visitor v(f1); diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 912e44cde..e48ffa823 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,7 +1,7 @@ #include "ltlast/allnodes.hh" #include "lunabbrev.hh" -namespace spot +namespace spot { namespace ltl { @@ -13,8 +13,8 @@ namespace spot { } - void - unabbreviate_logic_visitor::visit(const binop* bo) + void + unabbreviate_logic_visitor::visit(binop* bo) { formula* f1 = recurse(bo->first()); formula* f2 = recurse(bo->second()); @@ -22,43 +22,48 @@ namespace spot { /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: - result_ = new multop(multop::Or, - new multop(multop::And, f1, - new unop(unop::Not, f2)), - new multop(multop::And, f2, - new unop(unop::Not, f1))); + result_ = multop::instance(multop::Or, + multop::instance(multop::And, f1, + unop::instance(unop::Not, + f2)), + multop::instance(multop::And, f2, + unop::instance(unop::Not, + f1))); return; /* f1 => f2 == !f1 | f2 */ case binop::Implies: - result_ = new multop(multop::Or, new unop(unop::Not, f1), f2); + result_ = multop::instance(multop::Or, + unop::instance(unop::Not, f1), f2); return; /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ case binop::Equiv: - result_ = new multop(multop::Or, - new multop(multop::And, f1, f2), - new multop(multop::And, - new unop(unop::Not, f1), - new unop(unop::Not, f2))); + result_ = multop::instance(multop::Or, + multop::instance(multop::And, f1, f2), + multop::instance(multop::And, + unop::instance(unop::Not, + f1), + unop::instance(unop::Not, + f2))); return; /* f1 U f2 == f1 U f2 */ /* f1 R f2 == f1 R f2 */ case binop::U: case binop::R: - result_ = new binop(bo->op(), f1, f2); + result_ = binop::instance(bo->op(), f1, f2); return; } /* Unreachable code. */ assert(0); } - formula* - unabbreviate_logic_visitor::recurse(const formula* f) + formula* + unabbreviate_logic_visitor::recurse(formula* f) { return unabbreviate_logic(f); } - formula* - unabbreviate_logic(const formula* f) + formula* + unabbreviate_logic(formula* f) { unabbreviate_logic_visitor v; f->accept(v); diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 711f13ec3..e24286e0b 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -3,11 +3,11 @@ #include "clone.hh" -namespace spot +namespace spot { namespace ltl { - /// \brief Clone and rewrite a formula to remove most of the + /// \brief Clone and rewrite a formula to remove most of the /// abbreviated logical operators. /// /// This will rewrite binary operators such as binop::Implies, @@ -26,18 +26,18 @@ namespace spot virtual ~unabbreviate_logic_visitor(); using super::visit; - void visit(const binop* bo); + void visit(binop* bo); - virtual formula* recurse(const formula* f); + virtual formula* recurse(formula* f); }; - /// \brief Clone rewrite a formula to remove most of the abbreviated + /// \brief Clone rewrite a formula to remove most of the abbreviated /// logical operators. /// /// This will rewrite binary operators such as binop::Implies, /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, /// and multop::And. - formula* unabbreviate_logic(const formula* f); + formula* unabbreviate_logic(formula* f); } } diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 153c505a8..131d21791 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -6,7 +6,7 @@ namespace spot namespace ltl { - class negative_normal_form_visitor : public const_visitor + class negative_normal_form_visitor : public visitor { public: negative_normal_form_visitor(bool negated) @@ -14,7 +14,7 @@ namespace spot { } - virtual + virtual ~negative_normal_form_visitor() { } @@ -23,43 +23,43 @@ namespace spot { return result_; } - - void - visit(const atomic_prop* ap) + + void + visit(atomic_prop* ap) { - formula* f = new atomic_prop(ap->name(), ap->env()); + formula* f = ap->ref(); if (negated_) - result_ = new unop(unop::Not, f); + result_ = unop::instance(unop::Not, f); else result_ = f; } - void - visit(const constant* c) + void + visit(constant* c) { if (! negated_) { - result_ = new constant(c->val()); + result_ = c; return; } switch (c->val()) { case constant::True: - result_ = new constant(constant::False); + result_ = constant::false_instance(); return; case constant::False: - result_ = new constant(constant::True); + result_ = constant::true_instance(); return; } /* Unreachable code. */ assert(0); } - void - visit(const unop* uo) + void + visit(unop* uo) { - const formula* f = uo->child(); + formula* f = uo->child(); switch (uo->op()) { case unop::Not: @@ -67,63 +67,67 @@ namespace spot return; case unop::X: /* !Xa == X!a */ - result_ = new unop(unop::X, recurse(f)); + result_ = unop::instance(unop::X, recurse(f)); return; case unop::F: /* !Fa == G!a */ - result_ = new unop(negated_ ? unop::G : unop::F, recurse(f)); + result_ = unop::instance(negated_ ? unop::G : unop::F, recurse(f)); return; case unop::G: /* !Ga == F!a */ - result_ = new unop(negated_ ? unop::F : unop::G, recurse(f)); + result_ = unop::instance(negated_ ? unop::F : unop::G, recurse(f)); return; } /* Unreachable code. */ assert(0); } - void - visit(const binop* bo) + void + visit(binop* bo) { - const formula* f1 = bo->first(); - const formula* f2 = bo->second(); + formula* f1 = bo->first(); + formula* f2 = bo->second(); switch (bo->op()) { case binop::Xor: /* !(a ^ b) == a <=> b */ - result_ = new binop(negated_ ? binop::Equiv : binop::Xor, - recurse_(f1, false), recurse_(f2, false)); + result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor, + recurse_(f1, false), + recurse_(f2, false)); return; case binop::Equiv: /* !(a <=> b) == a ^ b */ - result_ = new binop(negated_ ? binop::Xor : binop::Equiv, - recurse_(f1, false), recurse_(f2, false)); + result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv, + recurse_(f1, false), + recurse_(f2, false)); return; case binop::Implies: if (negated_) /* !(a => b) == a & !b */ - result_ = new multop(multop::And, - recurse_(f1, false), recurse_(f2, true)); + result_ = multop::instance(multop::And, + recurse_(f1, false), + recurse_(f2, true)); else - result_ = new binop(binop::Implies, recurse(f1), recurse(f2)); + result_ = binop::instance(binop::Implies, + recurse(f1), recurse(f2)); return; case binop::U: /* !(a U b) == !a R !b */ - result_ = new binop(negated_ ? binop::R : binop::U, - recurse(f1), recurse(f2)); + result_ = binop::instance(negated_ ? binop::R : binop::U, + recurse(f1), recurse(f2)); return; case binop::R: /* !(a R b) == !a U !b */ - result_ = new binop(negated_ ? binop::U : binop::R, - recurse(f1), recurse(f2)); + result_ = binop::instance(negated_ ? binop::U : binop::R, + recurse(f1), recurse(f2)); return; } /* Unreachable code. */ assert(0); } - void - visit(const multop* mo) + void + visit(multop* mo) { /* !(a & b & c) == !a | !b | !c */ /* !(a | b | c) == !a & !b & !c */ @@ -138,32 +142,32 @@ namespace spot op = multop::And; break; } - multop* res = new multop(op); + multop* res = multop::instance(op); unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) - res->add(recurse(mo->nth(i))); + multop::add(&res, recurse(mo->nth(i))); result_ = res; } - - formula* - recurse_(const formula* f, bool negated) + + formula* + recurse_(formula* f, bool negated) { return negative_normal_form(f, negated); } - formula* - recurse(const formula* f) + formula* + recurse(formula* f) { return recurse_(f, negated_); } - + protected: formula* result_; bool negated_; }; - formula* - negative_normal_form(const formula* f, bool negated) + formula* + negative_normal_form(formula* f, bool negated) { negative_normal_form_visitor v(negated); f->accept(v); diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index 443a836c9..2290fc30e 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -4,13 +4,13 @@ #include "ltlast/formula.hh" #include "ltlast/visitor.hh" -namespace spot +namespace spot { namespace ltl { /// \brief Build the negative normal form of \a f. - /// - /// All negations of the formula are pushed in front of the + /// + /// All negations of the formula are pushed in front of the /// atomic propositions. /// /// \param f The formula to normalize. @@ -22,7 +22,7 @@ namespace spot /// or spot::ltl::unabbreviate_ltl first. (Calling these functions /// after spot::ltl::negative_normal_form would likely produce a /// formula which is not in negative normal form.) - formula* negative_normal_form(const formula* f, bool negated = false); + formula* negative_normal_form(formula* f, bool negated = false); } } diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 6e0f415b5..eb1c23a98 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,7 +1,7 @@ #include "ltlast/allnodes.hh" #include "tunabbrev.hh" -namespace spot +namespace spot { namespace ltl { @@ -13,8 +13,8 @@ namespace spot { } - void - unabbreviate_ltl_visitor::visit(const unop* uo) + void + unabbreviate_ltl_visitor::visit(unop* uo) { switch (uo->op()) { @@ -23,26 +23,26 @@ namespace spot this->super::visit(uo); return; case unop::F: - result_ = new binop(binop::U, - new constant(constant::True), - recurse(uo->child())); + result_ = binop::instance(binop::U, + constant::true_instance(), + recurse(uo->child())); return; case unop::G: - result_ = new binop(binop::R, - new constant(constant::False), - recurse(uo->child())); + result_ = binop::instance(binop::R, + constant::false_instance(), + recurse(uo->child())); return; } } - - formula* - unabbreviate_ltl_visitor::recurse(const formula* f) + + formula* + unabbreviate_ltl_visitor::recurse(formula* f) { return unabbreviate_ltl(f); } - formula* - unabbreviate_ltl(const formula* f) + formula* + unabbreviate_ltl(formula* f) { unabbreviate_ltl_visitor v; f->accept(v); diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh index 347ca0994..6854d81cc 100644 --- a/src/ltlvisit/tunabbrev.hh +++ b/src/ltlvisit/tunabbrev.hh @@ -4,11 +4,11 @@ #include "ltlast/formula.hh" #include "ltlvisit/lunabbrev.hh" -namespace spot +namespace spot { namespace ltl { - /// \brief Clone and rewrite a formula to remove most of the + /// \brief Clone and rewrite a formula to remove most of the /// abbreviated LTL and logical operators. /// /// The rewriting performed on logical operator is @@ -28,12 +28,12 @@ namespace spot unabbreviate_ltl_visitor(); virtual ~unabbreviate_ltl_visitor(); - void visit(const unop* uo); + void visit(unop* uo); - formula* recurse(const formula* f); + formula* recurse(formula* f); }; - /// \brief Clone and rewrite a formula to remove most of the + /// \brief Clone and rewrite a formula to remove most of the /// abbreviated LTL and logical operators. /// /// The rewriting performed on logical operator is @@ -41,7 +41,7 @@ namespace spot /// /// This will also rewrite unary operators such as unop::F, /// and unop::G, using only binop::U, and binop::R. - formula* unabbreviate_ltl(const formula* f); + formula* unabbreviate_ltl(formula* f); } }