diff --git a/ChangeLog b/ChangeLog index 8644ee98d..72cd909d5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,22 @@ +2003-05-16 Alexandre Duret-Lutz + + 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 Implements spot::ltl::destroy() and exercise it. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index f55a394f1..6bd6af5c0 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -2,6 +2,7 @@ #include #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; } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index da412bf33..77a91fcf4 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -65,14 +65,28 @@ namespace spot static unsigned instance_count(); protected: + // Sorted list of formulae. (Sorted by pointer comparison.) typedef std::vector vec; + + typedef std::pair pair; - typedef std::map 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 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(); diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 6bb958a08..b3c163be1 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,6 +1,5 @@ #include #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); diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test index cd2f7f26b..01a8845f3 100755 --- a/src/ltltest/parse.test +++ b/src/ltltest/parse.test @@ -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 diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index e049e7614..8b4299068 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -1,7 +1,6 @@ #include #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. diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 85eb4eaa5..fd6761db0 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -13,8 +13,6 @@ libltlvisit_la_SOURCES = \ dump.hh \ tostring.cc \ tostring.hh \ - equals.cc \ - equals.hh \ lunabbrev.hh \ lunabbrev.cc \ nenoform.hh \ diff --git a/src/ltlvisit/equals.cc b/src/ltlvisit/equals.cc deleted file mode 100644 index 6e0cf49b5..000000000 --- a/src/ltlvisit/equals.cc +++ /dev/null @@ -1,136 +0,0 @@ -#include -#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(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(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(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 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(); - } - } -} diff --git a/src/ltlvisit/equals.hh b/src/ltlvisit/equals.hh deleted file mode 100644 index b5e56c817..000000000 --- a/src/ltlvisit/equals.hh +++ /dev/null @@ -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); - } -} - diff --git a/wrap/spot.i b/wrap/spot.i index 364591501..d465beede 100644 --- a/wrap/spot.i +++ b/wrap/spot.i @@ -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"