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

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):

Browse source 
Factorize.
This commit is contained in:
Alexandre Duret-Lutz 2004-06-22 22:48:34 +00:00
parent 47e9ac108f
commit 473af5bb1d
2 changed files with 10 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2004-06-23 Alexandre Duret-Lutz <adl@gnu.org> 2004-06-23 Alexandre Duret-Lutz <adl@gnu.org>
* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):
Factorize.
* src/ltlvisit/basicreduce.hh: New file, extracted from ... * src/ltlvisit/basicreduce.hh: New file, extracted from ...
* src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/reducform.hh: ... here.
* src/ltlvisit/basereduc.cc: Rename as ... * src/ltlvisit/basereduc.cc: Rename as ...

52
src/ltlvisit/basicreduce.cc
View file

@ -232,56 +232,18 @@ namespace spot
switch (bo->op()) switch (bo->op())
{ {
case binop::Xor: case binop::Xor:
result_ = binop::instance(binop::Xor,
basic_reduce(f1),
basic_reduce(f2));
return;
case binop::Equiv: case binop::Equiv:
result_ = binop::instance(binop::Equiv,
basic_reduce(f1),
basic_reduce(f2));
return;
case binop::Implies: case binop::Implies:
result_ = binop::instance(binop::Implies, result_ = binop::instance(bo->op(),
basic_reduce(f1), basic_reduce(f1),
basic_reduce(f2)); basic_reduce(f2));
return; return;
case binop::U: case binop::U:
case binop::R:
f2 = basic_reduce(f2); f2 = basic_reduce(f2);
// a U false = false // a U false = false
// a U true = true // a U true = true
if (dynamic_cast<constant*>(f2))
{
result_ = f2;
return;
}
f1 = basic_reduce(f1);
// X(a) U X(b) = X(a U b)
fu1 = dynamic_cast<unop*>(f1);
fu2 = dynamic_cast<unop*>(f2);
if ((fu1 && fu2) &&
(fu1->op() == unop::X) &&
(fu2->op() == unop::X))
{
formula* ftmp = binop::instance(binop::U,
basic_reduce(fu1->child()),
basic_reduce(fu2->child()));
result_ = unop::instance(unop::X, basic_reduce(ftmp));
destroy(f1);
destroy(f2);
destroy(ftmp);
return;
}
result_ = binop::instance(binop::U, f1, f2);
return;
case binop::R:
f2 = basic_reduce(f2);
// a R false = false // a R false = false
// a R true = true // a R true = true
if (dynamic_cast<constant*>(f2)) if (dynamic_cast<constant*>(f2))
@ -292,12 +254,13 @@ namespace spot
f1 = basic_reduce(f1); f1 = basic_reduce(f1);
// X(a) U X(b) = X(a U b)
// X(a) R X(b) = X(a R b) // X(a) R X(b) = X(a R b)
fu1 = dynamic_cast<unop*>(f1); fu1 = dynamic_cast<unop*>(f1);
fu2 = dynamic_cast<unop*>(f2); fu2 = dynamic_cast<unop*>(f2);
if ((fu1 && fu2) && if (fu1 && fu2
(fu1->op() == unop::X) && && fu1->op() == unop::X
(fu2->op() == unop::X)) && fu2->op() == unop::X)
{ {
formula* ftmp = binop::instance(bo->op(), formula* ftmp = binop::instance(bo->op(),
basic_reduce(fu1->child()), basic_reduce(fu1->child()),
@ -309,8 +272,7 @@ namespace spot
return; return;
} }
result_ = binop::instance(bo->op(), result_ = binop::instance(bo->op(), f1, f2);
f1, f2);
return; return;
} }
/* Unreachable code. */ /* Unreachable code. */