diff --git a/ChangeLog b/ChangeLog index 561901b6c..cfb2dbfa8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,21 @@ 2003-08-10 Alexandre Duret-Lutz + Revamp the multop interface to allow some basic optimizations like + not constructing a single-child multop. + * src/ltlast/multop.hh (multop::instance(type)): Remove. + (multop::instance(type, formula*, formula*)): Return a formula*. + (multop::instance(type, vec*)): Make it public and return a formula*. + (multop::add_sorted, multop::add): + * src/ltlast/multop.cc (multop::instance(type, vec*)): Rewrite. + (multop::instance(type)): Delete. + (multop::instance(type, formula*, formula*)): Adjust. + (multop::add_sorted, multop::add): Remove. + * src/ltlvisit/clone.cc (clone_visitor::visit(multop*)) Adjust. + * src/ltlvisit/nenoform.cc + (negative_normal_form_visitor::::visit(multop*)) Adjust. + * src/ltltest/equals.test: Make sure `a & a' and `a' are equals. + * wrap/python/tests/ltlsimple.py: Adjust. + * src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !' between two BDDs. That's one less call to BuDDy. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index e49b72916..0c66360a9 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,6 +1,8 @@ #include #include +#include #include "multop.hh" +#include "constant.hh" #include "visitor.hh" #include "ltlvisit/destroy.hh" @@ -77,10 +79,78 @@ namespace spot multop::map multop::instances; - multop* + formula* multop::instance(type op, vec* v) { pair p(op, v); + + // Inline children of same kind. + { + vec inlined; + vec::iterator i = v->begin(); + while (i != v->end()) + { + multop* p = dynamic_cast(*i); + if (p && p->op() == op) + { + unsigned ps = p->size(); + for (unsigned n = 0; n < ps; ++n) + inlined.push_back(p->nth(n)); + // 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(*i); + i = v->erase(i); + } + else + { + ++i; + } + } + v->insert(v->end(), inlined.begin(), inlined.end()); + } + + std::sort(v->begin(), v->end()); + + // Remove duplicates. We can't use std::unique(), because we + // must destroy() any formula we drop. + { + formula* last = 0; + vec::iterator i = v->begin(); + while (i != v->end()) + { + if (*i == last) + { + destroy(*i); + i = v->erase(i); + } + else + { + last = *i++; + } + } + } + + if (v->size() == 0) + { + delete v; + switch (op) + { + case And: + return constant::true_instance(); + case Or: + return constant::false_instance(); + } + /* Unreachable code. */ + assert(0); + } + if (v->size() == 1) + { + formula* res = (*v)[0]; + delete v; + return res; + } + map::iterator i = instances.find(p); if (i != instances.end()) { @@ -93,75 +163,15 @@ namespace spot } - multop* - multop::instance(type op) - { - return instance(op, new vec); - } - - multop* + formula* multop::instance(type op, formula* first, formula* second) { vec* v = new vec; - multop::add(op, v, first); - multop::add(op, v, second); + v->push_back(first); + v->push_back(second); 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 identical 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 already a child. Drop it. - destroy(f); - return; - } - } - v->insert(i, f); - } - - multop::vec* - multop::add(type op, vec* v, formula* f) - { - // If the formula we add is itself a multop for the same operator, - // merge its children. - multop* p = dynamic_cast(f); - if (p && p->op() == op) - { - unsigned ps = p->size(); - for (unsigned i = 0; i < ps; ++i) - 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 - { - add_sorted(v, f); - } - return v; - } - - void - multop::add(multop** m, formula* f) - { - vec* v = new vec(*(*m)->children_); - type op = (*m)->op(); - multop::add(op, v, f); - formula::unref(*m); - *m = instance(op, v); - } - unsigned multop::instance_count() { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index e5ec1b3b7..67a46d76f 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -18,29 +18,36 @@ namespace spot public: enum type { Or, And }; - - /// \brief Build a spot::ltl::multop with no child. - /// - /// This has little value unless you call multop::add later. - static multop* instance(type op); + /// List of formulae. + typedef std::vector vec; /// \brief Build a spot::ltl::multop with two children. /// /// If one of the children itself is a spot::ltl::multop /// with the same type, it will be merged. I.e., children /// if that child will be added, and that child itself will - /// be destroyed. - static multop* instance(type op, formula* first, formula* second); + /// be destroyed. This allows incremental building of + /// n-ary ltl::multop. + /// + /// This functions can perform slight optimizations and + /// may not return an ltl::multop objects. For instance + /// if \c first and \c second are equal, that formula is + /// returned as-is. + static formula* instance(type op, formula* first, formula* second); - /// \brief Add another child to this operator. + /// \brief Build a spot::ltl::multop with many children. /// - /// If \a f itself is a spot::ltl::multop with the same type, it - /// will be merged. I.e., children of \a f will be added, and - /// that \a f will will be destroyed. + /// Same as the other instance() function, but take a vector of + /// formula in argument. This vector is acquired by the + /// spot::ltl::multop class, the caller should allocate it with + /// \c new, but not use it (especially not destroy it) after it + /// has been passed to spot::ltl::multop. /// - /// Note that this function overwrites the supplied ltl::multop pointer. - /// The old value is released and should not be used after this. - static void add(multop** m, formula* f); + /// This functions can perform slight optimizations and + /// may not return an ltl::multop objects. For instance + /// if the vector contain only one unique element, this + /// this formula will be returned as-is. + static formula* instance(type op, vec* v); virtual void accept(visitor& v); virtual void accept(const_visitor& v) const; @@ -65,10 +72,6 @@ namespace spot static unsigned instance_count(); protected: - // Sorted list of formulae. (Sorted by pointer comparison.) - typedef std::vector vec; - - typedef std::pair pair; /// Comparison functor used internally by ltl::multop. struct paircmp @@ -85,10 +88,6 @@ namespace spot static map instances; multop(type op, vec* v); - static multop* instance(type op, vec* v); - static vec* add(type op, vec* v, formula* f); - static void add_sorted(vec* v, formula* f); - virtual ~multop(); private: diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index d84cec858..6917b9a7f 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -25,6 +25,7 @@ check 0 'a && b & a' 'b & a & b' check 0 'a & b' 'b & a & b' check 0 'a & b' 'b & a & a' check 0 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b' +check 0 'a & a' 'a' # other formulae which are not check 1 'a' 'b' diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 3eed5e1d9..5b036b8af 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -47,13 +47,11 @@ namespace spot void clone_visitor::visit(multop* mo) { - multop* res = multop::instance(mo->op()); + multop::vec* res = new multop::vec; unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) - { - multop::add(&res, recurse(mo->nth(i))); - } - result_ = res; + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(mo->op(), res); } formula* diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 5965aec40..a923c39c4 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -143,11 +143,11 @@ namespace spot op = multop::And; break; } - multop* res = multop::instance(op); + multop::vec* res = new multop::vec; unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) - multop::add(&res, recurse(mo->nth(i))); - result_ = res; + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(op, res); } formula* diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 09cf4a808..647894e8b 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -67,8 +67,9 @@ namespace spot { // FIXME: Iterating on the successors this way (calling // bdd_satone{,set} and NANDing out (-=) the result from a - // set) requires several descent of the BDD. Maybe it would be - // faster to compute all satisfying formula in one operation. + // set) requires several descents of the BDD. Maybe it would + // be faster to compute all satisfying formulae in one + // operation. succ_set_left_ -= current_; if (succ_set_left_ == bddfalse) // No more successors? diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index b9c6c4e3f..92b8f4ff7 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -33,12 +33,12 @@ assert op2 == op3 op4 = spot.multop.instance(spot.multop.Or, op2, op3) print 'op4 =', op4 -assert op4.nth(0) == op2 +assert op4 == op2 del op2, op3 assert spot.atomic_prop.instance_count() == 3 -assert spot.multop.instance_count() == 2 +assert spot.multop.instance_count() == 1 spot.destroy(op4) del op4