From ae7fdeba59a08f1d11dd1baefd14fe6e34c7e238 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Apr 2003 13:59:15 +0000 Subject: [PATCH] * src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit from clone_visitor and remove all useless methods (now inherited). --- ChangeLog | 5 +++ src/ltlvisit/Makefile.am | 2 ++ src/ltlvisit/clone.cc | 74 +++++++++++++++++++++++++++++++++++++++ src/ltlvisit/clone.hh | 37 ++++++++++++++++++++ src/ltlvisit/lunabbrev.cc | 39 ++------------------- src/ltlvisit/lunabbrev.hh | 18 +++------- 6 files changed, 125 insertions(+), 50 deletions(-) create mode 100644 src/ltlvisit/clone.cc create mode 100644 src/ltlvisit/clone.hh diff --git a/ChangeLog b/ChangeLog index 7c7347013..46ef404e0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2003-04-17 Alexandre DURET-LUTZ + * src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files. + * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. + * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit + from clone_visitor and remove all useless methods (now inherited). + * src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form. diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 3aee2a75a..c3558c3ce 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -3,6 +3,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) lib_LIBRARIES = libltlvisit.a libltlvisit_a_SOURCES = \ + clone.cc \ + clone.hh \ dotty.cc \ dotty.hh \ dump.cc \ diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc new file mode 100644 index 000000000..4389029eb --- /dev/null +++ b/src/ltlvisit/clone.cc @@ -0,0 +1,74 @@ +#include "ltlast/allnodes.hh" +#include "clone.hh" + +namespace spot +{ + namespace ltl + { + clone_visitor::clone_visitor() + { + } + + clone_visitor::~clone_visitor() + { + } + + formula* + clone_visitor::result() const + { + return result_; + } + + void + clone_visitor::visit(const atomic_prop* ap) + { + result_ = new atomic_prop(ap->name()); + } + + void + clone_visitor::visit(const constant* c) + { + result_ = new constant(c->val()); + } + + void + clone_visitor::visit(const unop* uo) + { + result_ = new unop(uo->op(), recurse(uo->child())); + } + + void + clone_visitor::visit(const binop* bo) + { + result_ = new binop(bo->op(), + recurse(bo->first()), recurse(bo->second())); + } + + void + clone_visitor::visit(const multop* mo) + { + multop* res = new multop(mo->op()); + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + { + res->add(recurse(mo->nth(i))); + } + result_ = res; + } + + formula* + clone_visitor::recurse(const formula* f) + { + return clone(f); + } + + formula* + clone(const formula* f) + { + clone_visitor v; + f->accept(v); + return v.result(); + } + + } +} diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh new file mode 100644 index 000000000..5627a958d --- /dev/null +++ b/src/ltlvisit/clone.hh @@ -0,0 +1,37 @@ +#ifndef SPOT_LTLVISIT_CLONE_HH +# define SPOT_LTLVISIT_CLONE_HH + +#include "ltlast/formula.hh" +#include "ltlast/visitor.hh" + +namespace spot +{ + namespace ltl + { + // This visitor is public, because it's convenient + // to derive from it and override part of its methods. + class clone_visitor : public const_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); + + protected: + formula* result_; + }; + + formula* clone(const formula* f); + } +} + +#endif // SPOT_LTLVISIT_LUNABBREV_HH diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 9939fdb23..912e44cde 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -13,30 +13,6 @@ namespace spot { } - formula* - unabbreviate_logic_visitor::result() const - { - return result_; - } - - void - unabbreviate_logic_visitor::visit(const atomic_prop* ap) - { - result_ = new atomic_prop(ap->name()); - } - - void - unabbreviate_logic_visitor::visit(const constant* c) - { - result_ = new constant(c->val()); - } - - void - unabbreviate_logic_visitor::visit(const unop* uo) - { - result_ = new unop(uo->op(), recurse(uo->child())); - } - void unabbreviate_logic_visitor::visit(const binop* bo) { @@ -74,20 +50,9 @@ namespace spot /* Unreachable code. */ assert(0); } - - void - unabbreviate_logic_visitor::visit(const multop* mo) - { - multop* res = new multop(mo->op()); - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos; ++i) - { - res->add(recurse(mo->nth(i))); - } - result_ = res; - } - formula* unabbreviate_logic_visitor::recurse(const formula* f) + formula* + unabbreviate_logic_visitor::recurse(const formula* f) { return unabbreviate_logic(f); } diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 03082aadb..8d8b25d57 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -1,8 +1,7 @@ #ifndef SPOT_LTLVISIT_LUNABBREV_HH # define SPOT_LTLVISIT_LUNABBREV_HH -#include "ltlast/formula.hh" -#include "ltlast/visitor.hh" +#include "clone.hh" namespace spot { @@ -10,24 +9,17 @@ namespace spot { // This visitor is public, because it's convenient // to derive from it and override part of its methods. - class unabbreviate_logic_visitor : public const_visitor + class unabbreviate_logic_visitor : public clone_visitor { + typedef clone_visitor super; public: unabbreviate_logic_visitor(); virtual ~unabbreviate_logic_visitor(); - formula* result() const; - - void visit(const atomic_prop* ap); - void visit(const unop* uo); + using super::visit; void visit(const binop* bo); - void visit(const multop* mo); - void visit(const constant* c); - + virtual formula* recurse(const formula* f); - - protected: - formula* result_; }; formula* unabbreviate_logic(const formula* f);