Check trivial multop equality at build time. The makes the
equal visitor useless, since two equals formulae will now share the same address. * src/ltlast/multop.hh (add_sorted): New function. (paircmp): New comparison functor. (map): Use paircmp, we want to compare the vectors' contents, not their addresses. * src/ltlast/multop.cc (add_sorted): New function. (add): Use it. * src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare pointers instead of calling equal. * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove equals.cc and equals.hh. * wrap/spot.i: Do not include equals.hh.
This commit is contained in:
Alexandre Duret-Lutz
parent
9123e56ff9
commit
1cdfea31b0
10 changed files with 65 additions and 197 deletions
19
ChangeLog
19
ChangeLog
|
|
@ -1,3 +1,22 @@
|
|||
2003-05-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
Check trivial multop equality at build time. The makes the
|
||||
equal visitor useless, since two equals formulae will now
|
||||
share the same address.
|
||||
|
||||
* src/ltlast/multop.hh (add_sorted): New function.
|
||||
(paircmp): New comparison functor.
|
||||
(map): Use paircmp, we want to compare the vectors' contents,
|
||||
not their addresses.
|
||||
* src/ltlast/multop.cc (add_sorted): New function.
|
||||
(add): Use it.
|
||||
* src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare
|
||||
pointers instead of calling equal.
|
||||
* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete.
|
||||
* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove
|
||||
equals.cc and equals.hh.
|
||||
* wrap/spot.i: Do not include equals.hh.
|
||||
|
||||
2003-05-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
Implements spot::ltl::destroy() and exercise it.
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
#include <utility>
|
||||
#include "multop.hh"
|
||||
#include "visitor.hh"
|
||||
#include "ltlvisit/destroy.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -107,6 +108,27 @@ namespace spot
|
|||
return instance(op, v);
|
||||
}
|
||||
|
||||
void
|
||||
multop::add_sorted(vec* v, formula* f)
|
||||
{
|
||||
// Keep V sorted. When adding a new multop, iterate over all
|
||||
// element until we find either an identicalle element, or the
|
||||
// place where the new one should be inserted.
|
||||
vec::iterator i;
|
||||
for (i = v->begin(); i != v->end(); ++i)
|
||||
{
|
||||
if (*i > f)
|
||||
break;
|
||||
if (*i == f)
|
||||
{
|
||||
// F is arleady a child. Drop it.
|
||||
destroy(f);
|
||||
return;
|
||||
}
|
||||
}
|
||||
v->insert(i, f);
|
||||
}
|
||||
|
||||
multop::vec*
|
||||
multop::add(type op, vec* v, formula* f)
|
||||
{
|
||||
|
|
@ -117,13 +139,15 @@ namespace spot
|
|||
{
|
||||
unsigned ps = p->size();
|
||||
for (unsigned i = 0; i < ps; ++i)
|
||||
v->push_back(p->nth(i));
|
||||
// that sub-formula is now useless
|
||||
add_sorted(v, p->nth(i));
|
||||
// That sub-formula is now useless, drop it.
|
||||
// Note that we use unref(), not destroy(), because we've
|
||||
// adopted its children and don't want to destroy these.
|
||||
formula::unref(f);
|
||||
}
|
||||
else
|
||||
{
|
||||
v->push_back(f);
|
||||
add_sorted(v, f);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -65,14 +65,28 @@ namespace spot
|
|||
static unsigned instance_count();
|
||||
|
||||
protected:
|
||||
// Sorted list of formulae. (Sorted by pointer comparison.)
|
||||
typedef std::vector<formula*> vec;
|
||||
|
||||
|
||||
typedef std::pair<type, vec*> pair;
|
||||
typedef std::map<pair, formula*> map;
|
||||
struct paircmp
|
||||
{
|
||||
bool
|
||||
operator () (const pair& p1, const pair& p2) const
|
||||
{
|
||||
if (p1.first != p2.first)
|
||||
return p1.first < p2.first;
|
||||
return *p1.second < *p2.second;
|
||||
}
|
||||
};
|
||||
typedef std::map<pair, formula*, paircmp> 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);
|
||||
static void multop::add_sorted(vec* v, formula* f);
|
||||
|
||||
virtual ~multop();
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
#include <iostream>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/equals.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
#include "ltlvisit/tunabbrev.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
|
|
@ -62,12 +61,10 @@ main(int argc, char** argv)
|
|||
std::cout << std::endl;
|
||||
#endif
|
||||
|
||||
int exit_code = !equals(f1, f2);
|
||||
int exit_code = 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);
|
||||
|
|
|
|||
|
|
@ -41,6 +41,7 @@ for f in \
|
|||
'()b' \
|
||||
'long_atomic_proposition_1 U long_atomic_proposition_2' \
|
||||
' ab & ac | ad ^ af' \
|
||||
'((b * a) + a) & d' \
|
||||
'(ab & ac | ad ) <=> af ' \
|
||||
'a U b U c U d U e U f U g U h U i U j U k U l U m' \
|
||||
'(ab * !Xad + ad U ab) & FG p12 & GF p13' \
|
||||
|
|
@ -55,7 +56,7 @@ do
|
|||
fi
|
||||
|
||||
if test -n "$DOT"; then
|
||||
./ltl2dot "$f" > parse.dot
|
||||
./ltl2dot "$f" > parse.dot
|
||||
if $DOT -o /dev/null parse.dot; then
|
||||
rm -f parse.dot
|
||||
else
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
#include <iostream>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "ltlvisit/equals.hh"
|
||||
#include "ltlvisit/destroy.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
|
|
@ -37,7 +36,7 @@ main(int argc, char **argv)
|
|||
|
||||
// This second abstract tree should be equal to the first.
|
||||
|
||||
if (! equals(f1, f2))
|
||||
if (f1 != f2)
|
||||
return 1;
|
||||
|
||||
// It should also map to the same string.
|
||||
|
|
|
|||
|
|
@ -13,8 +13,6 @@ libltlvisit_la_SOURCES = \
|
|||
dump.hh \
|
||||
tostring.cc \
|
||||
tostring.hh \
|
||||
equals.cc \
|
||||
equals.hh \
|
||||
lunabbrev.hh \
|
||||
lunabbrev.cc \
|
||||
nenoform.hh \
|
||||
|
|
|
|||
|
|
@ -1,136 +0,0 @@
|
|||
#include <vector>
|
||||
#include "equals.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace ltl
|
||||
{
|
||||
equals_visitor::equals_visitor(const formula* f)
|
||||
: f_(f), result_(false)
|
||||
{
|
||||
}
|
||||
|
||||
equals_visitor::~equals_visitor()
|
||||
{
|
||||
}
|
||||
|
||||
bool
|
||||
equals_visitor::result() const
|
||||
{
|
||||
return result_;
|
||||
}
|
||||
|
||||
void
|
||||
equals_visitor::visit(const atomic_prop* ap)
|
||||
{
|
||||
result_ = f_ == ap;
|
||||
}
|
||||
|
||||
void
|
||||
equals_visitor::visit(const constant* c)
|
||||
{
|
||||
result_ = f_ == c;
|
||||
}
|
||||
|
||||
void
|
||||
equals_visitor::visit(const unop* uo)
|
||||
{
|
||||
const unop* p = dynamic_cast<const unop*>(f_);
|
||||
if (!p || p->op() != uo->op())
|
||||
return;
|
||||
f_ = p->child();
|
||||
uo->child()->accept(*this);
|
||||
}
|
||||
|
||||
void
|
||||
equals_visitor::visit(const binop* bo)
|
||||
{
|
||||
const binop* p = dynamic_cast<const binop*>(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<const multop*>(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<bool> p_seen(p_size, false);
|
||||
|
||||
for (unsigned nf = 0; nf < m_size; ++nf)
|
||||
{
|
||||
unsigned np;
|
||||
const formula* mnth = m->nth(nf);
|
||||
for (np = 0; np < p_size; ++np)
|
||||
{
|
||||
if (equals(p->nth(np), mnth))
|
||||
{
|
||||
p_seen[np] = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
// We we haven't found mnth in any child of p, then
|
||||
// the two formulas aren't equal.
|
||||
if (np == p_size)
|
||||
return;
|
||||
}
|
||||
// At this point, we have found all children of m' in children
|
||||
// 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
|
||||
// contain duplicate children, its faster to test that
|
||||
// unmarked children of `p' have a counterpart in marked children
|
||||
// of `p'.
|
||||
for (unsigned np = 0; np < p_size; ++np)
|
||||
{
|
||||
// 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)
|
||||
return;
|
||||
}
|
||||
|
||||
// The two formulas match.
|
||||
result_ = true;
|
||||
}
|
||||
|
||||
|
||||
bool
|
||||
equals(const formula* f1, const formula* f2)
|
||||
{
|
||||
equals_visitor v(f1);
|
||||
f2->accept(v);
|
||||
return v.result();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
#include "ltlast/formula.hh"
|
||||
#include "ltlast/visitor.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace ltl
|
||||
{
|
||||
/// \brief Check for equality between two formulae.
|
||||
///
|
||||
/// This visitor is public, because it's convenient
|
||||
/// to derive from it and override some of its methods.
|
||||
/// But if you just want the functionality, consider using
|
||||
/// spot::ltl::equals instead.
|
||||
class equals_visitor : public const_visitor
|
||||
{
|
||||
public:
|
||||
equals_visitor(const formula* f);
|
||||
virtual ~equals_visitor();
|
||||
|
||||
// Return true iff the visitor has visited a
|
||||
// formula which is equal to `f'.
|
||||
bool result() const;
|
||||
|
||||
void visit(const atomic_prop* ap);
|
||||
void visit(const unop* uo);
|
||||
void visit(const binop* bo);
|
||||
void visit(const multop* bo);
|
||||
void visit(const constant* c);
|
||||
|
||||
private:
|
||||
const formula* f_;
|
||||
bool result_;
|
||||
|
||||
};
|
||||
|
||||
/// \brief Check whether two formulae are syntaxically equal.
|
||||
/// \return \c true iff \a f1 equals \a f2.
|
||||
///
|
||||
/// This tests for syntaxic equality rather than semantic equality.
|
||||
/// Two formulae are equals of their abstract syntax tree are equals.
|
||||
/// ltl::multop children can be permuted or repeated without
|
||||
/// impact on the result of this comparison.
|
||||
bool equals(const formula* f1, const formula* f2);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -13,7 +13,6 @@
|
|||
#include "ltlvisit/clone.hh"
|
||||
#include "ltlvisit/dotty.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/equals.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
#include "ltlvisit/tunabbrev.hh"
|
||||
#include "ltlvisit/nenoform.hh"
|
||||
|
|
@ -31,7 +30,6 @@ using namespace spot::ltl;
|
|||
%include "ltlvisit/clone.hh"
|
||||
%include "ltlvisit/dotty.hh"
|
||||
%include "ltlvisit/dump.hh"
|
||||
%include "ltlvisit/equals.hh"
|
||||
%include "ltlvisit/lunabbrev.hh"
|
||||
%include "ltlvisit/tunabbrev.hh"
|
||||
%include "ltlvisit/nenoform.hh"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue