3991a51a17
* src/ltlvisit/clone.hh (clone): Likewise. * src/ltlvisit/destroy.cc (destroy): New const version. * src/ltlvisit/destroy.hh (destroy): Likewise. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::create_state, tgba_bdd_concrete_factory::create_atomic_prop, tgba_bdd_concrete_factory::promise): Clone new formulae. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods that clone and destroy formulae. * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. (ltl2tgba_SOURCES): New variable. (TESTS): Add ltl2tgba.test.
44 lines
984 B
C++
44 lines
984 B
C++
#ifndef SPOT_LTLVISIT_CLONE_HH
|
|
# define SPOT_LTLVISIT_CLONE_HH
|
|
|
|
#include "ltlast/formula.hh"
|
|
#include "ltlast/visitor.hh"
|
|
|
|
namespace spot
|
|
{
|
|
namespace ltl
|
|
{
|
|
/// \brief Clone a formula.
|
|
///
|
|
/// This visitor is public, because it's convenient
|
|
/// 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 visitor
|
|
{
|
|
public:
|
|
clone_visitor();
|
|
virtual ~clone_visitor();
|
|
|
|
formula* result() const;
|
|
|
|
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(formula* f);
|
|
/// \brief Clone a formula.
|
|
formula* clone(const formula* f);
|
|
}
|
|
}
|
|
|
|
#endif // SPOT_LTLVISIT_LUNABBREV_HH
|