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

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.
parent 317fed59
2003-08-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
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.
......
#include <cassert>
#include <utility>
#include <algorithm>
#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<multop*>(*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<multop*>(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()
{
......
......@@ -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<formula*> 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<formula*> vec;
typedef std::pair<type, vec*> 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:
......
......@@ -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'
......
......@@ -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*
......
......@@ -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*
......
......@@ -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?
......
......@@ -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
......
Supports Markdown
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