Commit ae7fdeba authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* 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).
parent 0c7a2412
2003-04-17 Alexandre DURET-LUTZ <aduret@src.lip6.fr> 2003-04-17 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
* 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/nenoform.hh, src/ltlvisit/nenoform.cc: New files.
* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form. * src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
......
...@@ -3,6 +3,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) ...@@ -3,6 +3,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
lib_LIBRARIES = libltlvisit.a lib_LIBRARIES = libltlvisit.a
libltlvisit_a_SOURCES = \ libltlvisit_a_SOURCES = \
clone.cc \
clone.hh \
dotty.cc \ dotty.cc \
dotty.hh \ dotty.hh \
dump.cc \ dump.cc \
......
#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();
}
}
}
#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
...@@ -13,30 +13,6 @@ namespace spot ...@@ -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 void
unabbreviate_logic_visitor::visit(const binop* bo) unabbreviate_logic_visitor::visit(const binop* bo)
{ {
...@@ -74,20 +50,9 @@ namespace spot ...@@ -74,20 +50,9 @@ namespace spot
/* Unreachable code. */ /* Unreachable code. */
assert(0); 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); return unabbreviate_logic(f);
} }
......
#ifndef SPOT_LTLVISIT_LUNABBREV_HH #ifndef SPOT_LTLVISIT_LUNABBREV_HH
# define SPOT_LTLVISIT_LUNABBREV_HH # define SPOT_LTLVISIT_LUNABBREV_HH
#include "ltlast/formula.hh" #include "clone.hh"
#include "ltlast/visitor.hh"
namespace spot namespace spot
{ {
...@@ -10,24 +9,17 @@ namespace spot ...@@ -10,24 +9,17 @@ namespace spot
{ {
// This visitor is public, because it's convenient // This visitor is public, because it's convenient
// to derive from it and override part of its methods. // 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: public:
unabbreviate_logic_visitor(); unabbreviate_logic_visitor();
virtual ~unabbreviate_logic_visitor(); virtual ~unabbreviate_logic_visitor();
formula* result() const; using super::visit;
void visit(const atomic_prop* ap);
void visit(const unop* uo);
void visit(const binop* bo); void visit(const binop* bo);
void visit(const multop* mo);
void visit(const constant* c);
virtual formula* recurse(const formula* f); virtual formula* recurse(const formula* f);
protected:
formula* result_;
}; };
formula* unabbreviate_logic(const formula* f); formula* unabbreviate_logic(const formula* f);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment