From 9123e56ff98c05dc7e4be47f5b08c33a1a5d1965 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 May 2003 18:06:54 +0000 Subject: [PATCH] Implements spot::ltl::destroy() and exercise it. * src/ltlast/atomic_prop.hh: Declare instance_count(). * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh: Likewise. Also, really inherit for ref_formula this time. * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress the instance from the instance map. Implement instance_count(). * src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual destructors. * src/ltlparse/ltlparse.yy: Recover from binary operators with missing right hand operand (the point is just to destroy the the left hand operand). * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/ltltest/tostring.cc: Destroy used formulae. Make sure instance_count()s are null are the end. * src/ltltest/parseerr.test: Adjust expected result, now that the parser lnows about missing right hand operands. * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc, src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them. * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae occurring twice in the rewritten expression. --- ChangeLog | 25 +++++++++++ src/ltlast/atomic_prop.cc | 11 +++++ src/ltlast/atomic_prop.hh | 4 ++ src/ltlast/binop.cc | 11 +++++ src/ltlast/binop.hh | 7 ++- src/ltlast/formula.cc | 4 ++ src/ltlast/formula.hh | 2 + src/ltlast/multop.cc | 11 +++++ src/ltlast/multop.hh | 7 ++- src/ltlast/refformula.cc | 4 ++ src/ltlast/refformula.hh | 1 + src/ltlast/unop.cc | 10 +++++ src/ltlast/unop.hh | 7 ++- src/ltlparse/ltlparse.yy | 53 +++++++++++++++++++++++ src/ltltest/equals.cc | 32 +++++++++++--- src/ltltest/parseerr.test | 8 ++-- src/ltltest/readltl.cc | 17 +++++--- src/ltltest/tostring.cc | 11 ++++- src/ltlvisit/Makefile.am | 6 ++- src/ltlvisit/destroy.cc | 25 +++++++++++ src/ltlvisit/destroy.hh | 15 +++++++ src/ltlvisit/lunabbrev.cc | 8 ++-- src/ltlvisit/postfix.cc | 89 +++++++++++++++++++++++++++++++++++++++ src/ltlvisit/postfix.hh | 38 +++++++++++++++++ 24 files changed, 382 insertions(+), 24 deletions(-) create mode 100644 src/ltlvisit/destroy.cc create mode 100644 src/ltlvisit/destroy.hh create mode 100644 src/ltlvisit/postfix.cc create mode 100644 src/ltlvisit/postfix.hh diff --git a/ChangeLog b/ChangeLog index af56c9a61..8644ee98d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,30 @@ 2003-05-15 Alexandre Duret-Lutz + Implements spot::ltl::destroy() and exercise it. + + * src/ltlast/atomic_prop.hh: Declare instance_count(). + * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh: + Likewise. Also, really inherit for ref_formula this time. + * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, + src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress + the instance from the instance map. Implement instance_count(). + * src/ltlast/formula.cc, src/ltlast/formula.hh, + src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual + destructors. + * src/ltlparse/ltlparse.yy: Recover from binary operators with + missing right hand operand (the point is just to destroy the + the left hand operand). + * src/ltltest/equals.cc, src/ltltest/readltl.cc, + src/ltltest/tostring.cc: Destroy used formulae. Make sure + instance_count()s are null are the end. + * src/ltltest/parseerr.test: Adjust expected result, now + that the parser lnows about missing right hand operands. + * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc, + src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files. + * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them. + * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae + occurring twice in the rewritten expression. + 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() diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 51d900743..eb9518aa4 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -13,6 +13,11 @@ namespace spot atomic_prop::~atomic_prop() { + // Get this instance out of the instance map. + pair p(name(), &env()); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); } void @@ -55,5 +60,11 @@ namespace spot return static_cast(ap->ref()); } + unsigned + atomic_prop::instance_count() + { + return instances.size(); + } + } } diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index a55984d3a..de167814b 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -26,6 +26,10 @@ namespace spot const std::string& name() const; /// Get the environment of the atomic proposition. environment& env() const; + + /// Number of instantiated atomic propositions. For debugging. + static unsigned instance_count(); + protected: atomic_prop(const std::string& name, environment& env); virtual ~atomic_prop(); diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 566264dba..6129556ad 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -13,6 +13,12 @@ namespace spot binop::~binop() { + // Get this instance out of the instance map. + pairf pf(first(), second()); + pair p(op(), pf); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); } void @@ -95,5 +101,10 @@ namespace spot return static_cast(ap->ref()); } + unsigned + binop::instance_count() + { + return instances.size(); + } } } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 9ad27d72a..8acfa29ef 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -2,7 +2,7 @@ # define SPOT_LTLAST_BINOP_HH #include -#include "formula.hh" +#include "refformula.hh" namespace spot { @@ -10,7 +10,7 @@ namespace spot { /// Binary operator. - class binop : public formula + class binop : public ref_formula { public: /// Different kinds of binary opertaors @@ -40,6 +40,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Number of instantiated binary operators. For debugging. + static unsigned instance_count(); + protected: typedef std::pair pairf; typedef std::pair pair; diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 02fca0f30..1e7e4c9f8 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -11,6 +11,10 @@ namespace spot return this; } + formula::~formula() + { + } + void formula::unref(formula* f) { diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 2fc674a77..eb8992e22 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -15,6 +15,8 @@ namespace spot class formula { public: + virtual ~formula(); + virtual void accept(visitor& v) = 0; virtual void accept(const_visitor& v) const = 0; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index a2295828d..f55a394f1 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -14,6 +14,12 @@ namespace spot multop::~multop() { + // Get this instance out of the instance map. + pair p(op(), children_); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); + delete children_; } @@ -132,5 +138,10 @@ namespace spot *m = instance(op, v); } + unsigned + multop::instance_count() + { + return instances.size(); + } } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 8ff548718..da412bf33 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -3,7 +3,7 @@ #include #include -#include "formula.hh" +#include "refformula.hh" namespace spot { @@ -13,7 +13,7 @@ namespace spot /// \brief Multi-operand operators. /// /// These operators are considered commutative and associative. - class multop : public formula + class multop : public ref_formula { public: enum type { Or, And }; @@ -61,6 +61,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Number of instantiated multi-operand operators. For debugging. + static unsigned instance_count(); + protected: typedef std::vector vec; typedef std::pair pair; diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc index 0286d20fe..b57cb4c40 100644 --- a/src/ltlast/refformula.cc +++ b/src/ltlast/refformula.cc @@ -10,6 +10,10 @@ namespace spot { } + ref_formula::~ref_formula() + { + } + void ref_formula::ref_() { diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index 36572cbec..7c67b9171 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -12,6 +12,7 @@ namespace spot class ref_formula : public formula { protected: + virtual ~ref_formula(); ref_formula(); void ref_(); bool unref_(); diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index e15597c51..1c8891c45 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -13,6 +13,11 @@ namespace spot unop::~unop() { + // Get this instance out of the instance map. + pair p(op(), child()); + map::iterator i = instances.find(p); + assert (i != instances.end()); + instances.erase(i); } void @@ -80,5 +85,10 @@ namespace spot return static_cast(ap->ref()); } + unsigned + unop::instance_count() + { + return instances.size(); + } } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 54510e489..5ebfb6969 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -2,7 +2,7 @@ # define SPOT_LTLAST_UNOP_HH #include -#include "formula.hh" +#include "refformula.hh" namespace spot { @@ -10,7 +10,7 @@ namespace spot { /// Unary operator. - class unop : public formula + class unop : public ref_formula { public: enum type { Not, X, F, G }; @@ -32,6 +32,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Number of instantiated unary operators. For debugging. + static unsigned instance_count(); + protected: typedef std::pair pair; typedef std::map map; diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 47251589c..d2bc47795 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -2,6 +2,7 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" +#include "ltlvisit/destroy.hh" extern spot::ltl::formula* result; @@ -83,6 +84,9 @@ ltl_formula: subformula many_errors: error | many_errors error +/* The reason we use `constant::false_instance()' for error recovery + is that it isn't reference counted. (Hence it can't leak references.) */ + subformula: ATOMIC_PROP { $$ = parse_environment.require(*$1); @@ -120,18 +124,67 @@ subformula: ATOMIC_PROP { $$ = unop::instance(unop::Not, $2); } | subformula OP_AND subformula { $$ = multop::instance(multop::And, $1, $3); } + | subformula OP_AND error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_AND")); + $$ = constant::false_instance(); + } | subformula OP_OR subformula { $$ = multop::instance(multop::Or, $1, $3); } + | subformula OP_OR error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_OR")); + $$ = constant::false_instance(); + } | subformula OP_XOR subformula { $$ = binop::instance(binop::Xor, $1, $3); } + | subformula OP_XOR error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_XOR")); + $$ = constant::false_instance(); + } | subformula OP_IMPLIES subformula { $$ = binop::instance(binop::Implies, $1, $3); } + | subformula OP_IMPLIES error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_IMPLIES")); + $$ = constant::false_instance(); + } | subformula OP_EQUIV subformula { $$ = binop::instance(binop::Equiv, $1, $3); } + | subformula OP_EQUIV error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_EQUIV")); + $$ = constant::false_instance(); + } | subformula OP_U subformula { $$ = binop::instance(binop::U, $1, $3); } + | subformula OP_U error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_U")); + $$ = constant::false_instance(); + } | subformula OP_R subformula { $$ = binop::instance(binop::R, $1, $3); } + | subformula OP_R error + { + destroy($1); + error_list.push_back(parse_error(@2, + "missing right operand for OP_R")); + $$ = constant::false_instance(); + } | OP_F subformula { $$ = unop::instance(unop::F, $2); } | OP_G subformula diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 47feda478..6bb958a08 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -5,6 +5,8 @@ #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/nenoform.hh" +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) @@ -19,7 +21,7 @@ main(int argc, char** argv) if (argc != 3) syntax(argv[0]); - + spot::ltl::parse_error_list p1; spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); @@ -28,28 +30,48 @@ main(int argc, char** argv) spot::ltl::parse_error_list p2; spot::ltl::formula* f2 = spot::ltl::parse(argv[2], p2); - + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; +#if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM) + spot::ltl::formula* tmp; +#endif #ifdef LUNABBREV + tmp = f1; + std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; f1 = spot::ltl::unabbreviate_logic(f1); + std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; + spot::ltl::destroy(tmp); + std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; spot::ltl::dump(*f1, std::cout); std::cout << std::endl; #endif #ifdef TUNABBREV + tmp = f1; f1 = spot::ltl::unabbreviate_ltl(f1); + spot::ltl::destroy(tmp); spot::ltl::dump(*f1, std::cout); std::cout << std::endl; #endif #ifdef NENOFORM + tmp = f1; f1 = spot::ltl::negative_normal_form(f1); + spot::ltl::destroy(tmp); spot::ltl::dump(*f1, std::cout); std::cout << std::endl; #endif - if (equals(f1, f2)) - return 0; - return 1; + int exit_code = !equals(f1, f2); + spot::ltl::destroy(f1); + std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; + spot::ltl::destroy(f2); + std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + + return exit_code; } diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test index ed7e7a5f6..a00618ac8 100755 --- a/src/ltltest/parseerr.test +++ b/src/ltltest/parseerr.test @@ -33,17 +33,19 @@ check() # Empty or unparsable strings check '' '' check '+' '' -check 'a U' '' -check 'a U b V c R' '' # leading and trailing garbage are skipped check '/2/3/4/5 a + b /6/7/8/' 'multop(Or, AP(a), AP(b))' check 'a U b c' 'binop(U, AP(a), AP(b))' -check 'a &&& b' 'AP(b)' +check 'a &&& b' 'multop(And, constant(0), AP(b))' # (check multop merging while we are at it) check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))' check 'a & (b | c) & d should work' 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))' +# Binop recovery +check 'a U' 'constant(0)' +check 'a U b V c R' 'constant(0)' + # Recovery inside parentheses check 'a U (b c) U e R (f g <=> h)' \ 'binop(R, binop(U, binop(U, AP(a), AP(b)), AP(e)), AP(f))' diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index 261c4d4f6..f403dacf4 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -2,6 +2,8 @@ #include "ltlparse/public.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/dotty.hh" +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) @@ -27,15 +29,15 @@ main(int argc, char** argv) if (argc < 3) syntax(argv[0]); formula_index = 2; - } - + } + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], + spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], pel, env, debug); spot::ltl::parse_error_list::iterator it; - exit_code = + exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); if (f) @@ -46,11 +48,16 @@ main(int argc, char** argv) spot::ltl::dump(*f, std::cout); std::cout << std::endl; #endif + spot::ltl::destroy(f); } else { exit_code = 1; } - + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); return exit_code; } diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 50ff4fc98..e049e7614 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -2,6 +2,8 @@ #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/equals.hh" +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" void syntax(char *prog) @@ -45,5 +47,12 @@ main(int argc, char **argv) if (f2s != f1s) return 1; + + spot::ltl::destroy(f1); + spot::ltl::destroy(f2); + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return 0; } - diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index cf1f119bb..85eb4eaa5 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -5,6 +5,8 @@ noinst_LTLIBRARIES = libltlvisit.la libltlvisit_la_SOURCES = \ clone.cc \ clone.hh \ + destroy.cc \ + destroy.hh \ dotty.cc \ dotty.hh \ dump.cc \ @@ -17,5 +19,7 @@ libltlvisit_la_SOURCES = \ lunabbrev.cc \ nenoform.hh \ nenoform.cc \ + postfix.hh \ + postfix.cc \ tunabbrev.hh \ - tunabbrev.cc \ No newline at end of file + tunabbrev.cc diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc new file mode 100644 index 000000000..5ab24ef6e --- /dev/null +++ b/src/ltlvisit/destroy.cc @@ -0,0 +1,25 @@ +#include "ltlvisit/destroy.hh" + +namespace spot +{ + namespace ltl + { + + class destroy_visitor : public postfix_visitor + { + public: + virtual void + doit_default(formula* c) + { + formula::unref(c); + } + }; + + void + destroy(formula *f) + { + destroy_visitor v; + f->accept(v); + } + } +} diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh new file mode 100644 index 000000000..375c4f57d --- /dev/null +++ b/src/ltlvisit/destroy.hh @@ -0,0 +1,15 @@ +#ifndef SPOT_LTLVISIT_DESTROY_HH +# define SPOT_LTLVISIT_DESTROY_HH + +#include "ltlvisit/postfix.hh" + +namespace spot +{ + namespace ltl + { + /// \brief Destroys a formula + void destroy(formula *f); + } +} + +#endif // SPOT_LTLVISIT_DESTROY_HH diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index e48ffa823..a6f599385 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,4 +1,5 @@ #include "ltlast/allnodes.hh" +#include "ltlvisit/clone.hh" #include "lunabbrev.hh" namespace spot @@ -23,10 +24,10 @@ namespace spot /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: result_ = multop::instance(multop::Or, - multop::instance(multop::And, f1, + multop::instance(multop::And, clone(f1), unop::instance(unop::Not, f2)), - multop::instance(multop::And, f2, + multop::instance(multop::And, clone(f2), unop::instance(unop::Not, f1))); return; @@ -38,7 +39,8 @@ namespace spot /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ case binop::Equiv: result_ = multop::instance(multop::Or, - multop::instance(multop::And, f1, f2), + multop::instance(multop::And, + clone(f1), clone(f2)), multop::instance(multop::And, unop::instance(unop::Not, f1), diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc new file mode 100644 index 000000000..aee85ad15 --- /dev/null +++ b/src/ltlvisit/postfix.cc @@ -0,0 +1,89 @@ +#include "ltlvisit/postfix.hh" +#include "ltlast/allnodes.hh" + +namespace spot +{ + namespace ltl + { + postfix_visitor::postfix_visitor() + { + } + + postfix_visitor::~postfix_visitor() + { + } + + void + postfix_visitor::visit(atomic_prop* ap) + { + doit(ap); + } + + void + postfix_visitor::visit(unop* uo) + { + uo->child()->accept(*this); + doit(uo); + } + + void + postfix_visitor::visit(binop* bo) + { + bo->first()->accept(*this); + bo->second()->accept(*this); + doit(bo); + } + + void + postfix_visitor::visit(multop* mo) + { + unsigned s = mo->size(); + for (unsigned i = 0; i < s; ++i) + mo->nth(i)->accept(*this); + doit(mo); + } + + void + postfix_visitor::visit(constant* c) + { + doit(c); + } + + void + postfix_visitor::doit(atomic_prop* ap) + { + doit_default(ap); + } + + void + postfix_visitor::doit(unop* uo) + { + doit_default(uo); + } + + void + postfix_visitor::doit(binop* bo) + { + doit_default(bo); + } + + void + postfix_visitor::doit(multop* mo) + { + doit_default(mo); + } + + void + postfix_visitor::doit(constant* c) + { + doit_default(c); + } + + void + postfix_visitor::doit_default(formula* f) + { + (void)f; + // Dummy implementation that does nothing. + } + } +} diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh new file mode 100644 index 000000000..821a973dc --- /dev/null +++ b/src/ltlvisit/postfix.hh @@ -0,0 +1,38 @@ +#ifndef SPOT_LTLVISIT_POSTFIX_HH +# define SPOT_LTLVISIT_POSTFIX_HH + +#include "ltlast/formula.hh" +#include "ltlast/visitor.hh" + +namespace spot +{ + namespace ltl + { + /// \brief Apply a algorithm on each node of an AST, + /// during a postfix traversal. + /// + /// Override one or more of the postifix_visitor::doit methods + /// with the algorithm to apply. + class postfix_visitor : public visitor + { + public: + postfix_visitor(); + virtual ~postfix_visitor(); + + void visit(atomic_prop* ap); + void visit(unop* uo); + void visit(binop* bo); + void visit(multop* mo); + void visit(constant* c); + + virtual void doit(atomic_prop* ap); + virtual void doit(unop* uo); + virtual void doit(binop* bo); + virtual void doit(multop* mo); + virtual void doit(constant* c); + virtual void doit_default(formula* f); + }; + } +} + +#endif // SPOT_LTLVISIT_POSTFIX_HH