alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Halve the number of application of eventual_universal_visitor in

Browse source 
reduce_visitor::visit(binop).

* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_):
Move this method...
(recurse_eu): ... outside as a separate function.  Likewise for
the universal/eventual result struct.
(reduce_visitor::visit(binop)): Call recurse_eu() once to replace
two calls to is_eventual and is_universal, thus replacing two
recursions by one.
This commit is contained in:
Alexandre Duret-Lutz 2010-12-01 08:06:49 +01:00
parent dabb7ecc97
commit c735249873
2 changed files with 51 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

13
ChangeLog
View file

@ -1,3 +1,16 @@
2010-12-01 Alexandre Duret-Lutz <adl@gnu.org>
Halve the number of application of eventual_universal_visitor in
reduce_visitor::visit(binop).
* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_):
Move this method...
(recurse_eu): ... outside as a separate function. Likewise for
the universal/eventual result struct.
(reduce_visitor::visit(binop)): Call recurse_eu() once to replace
two calls to is_eventual and is_universal, thus replacing two
recursions by one.
2010-12-01 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-12-01 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Move the eventual-universal functions where the belong. Move the eventual-universal functions where the belong.

48
src/ltlvisit/reduce.cc
View file

@ -38,9 +38,7 @@ namespace spot
{ {
namespace namespace
{ {
class eventual_universal_visitor: public const_visitor typedef union
{
union
{ {
unsigned v; unsigned v;
struct is_struct struct is_struct
@ -48,8 +46,12 @@ namespace spot
bool eventual:1; bool eventual:1;
bool universal:1; bool universal:1;
} is; } is;
} ret_; } eu_info;
static unsigned recurse_eu(const formula* f);
class eventual_universal_visitor: public const_visitor
{
public: public:
eventual_universal_visitor() eventual_universal_visitor()
@ -73,6 +75,12 @@ namespace spot
return ret_.is.universal; return ret_.is.universal;
} }
unsigned
eu() const
{
return ret_.v;
}
void void
visit(const atomic_prop*) visit(const atomic_prop*)
{ {
@ -91,13 +99,13 @@ namespace spot
const formula* f1 = uo->child(); const formula* f1 = uo->child();
if (uo->op() == unop::F) if (uo->op() == unop::F)
{ {
ret_.v = recurse_(f1); ret_.v = recurse_eu(f1);
ret_.is.eventual = true; ret_.is.eventual = true;
return; return;
} }
if (uo->op() == unop::G) if (uo->op() == unop::G)
{ {
ret_.v = recurse_(f1); ret_.v = recurse_eu(f1);
ret_.is.universal = true; ret_.is.universal = true;
return; return;
} }
@ -122,7 +130,7 @@ namespace spot
// This means that we can use the following case to handle // This means that we can use the following case to handle
// all cases of (f U g), (f R g), (f W g), (f M g) for // all cases of (f U g), (f R g), (f W g), (f M g) for
// universality and eventuality. // universality and eventuality.
ret_.v = recurse_(f1) & recurse_(f2); ret_.v = recurse_eu(f1) & recurse_eu(f2);
// we are left with the case where U, R, W, or M are actually // we are left with the case where U, R, W, or M are actually
// used to represent F or G. // used to represent F or G.
@ -164,20 +172,22 @@ namespace spot
{ {
unsigned mos = mo->size(); unsigned mos = mo->size();
assert(mos != 0); assert(mos != 0);
ret_.v = recurse_(mo->nth(0)); ret_.v = recurse_eu(mo->nth(0));
for (unsigned i = 1; i < mos && ret_.v != 0; ++i) for (unsigned i = 1; i < mos && ret_.v != 0; ++i)
ret_.v &= recurse_(mo->nth(i)); ret_.v &= recurse_eu(mo->nth(i));
} }
private: private:
unsigned eu_info ret_;
recurse_(const formula* f) };
static unsigned
recurse_eu(const formula* f)
{ {
eventual_universal_visitor v; eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v); const_cast<formula*>(f)->accept(v);
return v.ret_.v; return v.eu();
} }
};
///////////////////////////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////////
@ -257,15 +267,14 @@ namespace spot
binop::type op = bo->op(); binop::type op = bo->op();
formula* f2 = recurse(bo->second()); formula* f2 = recurse(bo->second());
bool f2_eventual = false; eu_info f2i = { recurse_eu(f2) };
if (opt_ & Reduce_Eventuality_And_Universality) if (opt_ & Reduce_Eventuality_And_Universality)
{ {
f2_eventual = is_eventual(f2);
/* If b is a pure eventuality formula then a U b = b. /* If b is a pure eventuality formula then a U b = b.
If b is a pure universality formula a R b = b. */ If b is a pure universality formula a R b = b. */
if ((f2_eventual && (op == binop::U)) if ((f2i.is.eventual && (op == binop::U))
|| (is_universal(f2) && (op == binop::R))) || (f2i.is.universal && (op == binop::R)))
{ {
result_ = f2; result_ = f2;
return; return;
@ -273,16 +282,17 @@ namespace spot
} }
formula* f1 = recurse(bo->first()); formula* f1 = recurse(bo->first());
eu_info f1i = { recurse_eu(f1) };
if (opt_ & Reduce_Eventuality_And_Universality) if (opt_ & Reduce_Eventuality_And_Universality)
{ {
/* If a&b is a pure eventuality formula then a M b = a & b. /* If a&b is a pure eventuality formula then a M b = a & b.
If a is a pure universality formula a W b = a|b. */ If a is a pure universality formula a W b = a|b. */
if (is_eventual(f1) && f2_eventual && (op == binop::M)) if (f1i.is.eventual && f2i.is.eventual && (op == binop::M))
{ {
result_ = multop::instance(multop::And, f1, f2); result_ = multop::instance(multop::And, f1, f2);
return; return;
} }
if (is_universal(f1) && (op == binop::W)) if (f1i.is.universal && (op == binop::W))
{ {
result_ = multop::instance(multop::Or, f1, f2); result_ = multop::instance(multop::Or, f1, f2);
return; return;