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

Simplify some simplification code using but_all().

Browse source 
* src/ltlvisit/simplify.cc: Use but_all() to simplify code.
This commit is contained in:
Alexandre Duret-Lutz 2012-02-15 13:49:59 +01:00
parent 955fc041ca
commit aa4b68fcfc
1 changed files with 22 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/ltlvisit/simplify.cc
View file

@ -1774,27 +1774,17 @@ namespace spot
int s = fm2->size(); int s = fm2->size();
for (int i = 0; i < s; ++i) for (int i = 0; i < s; ++i)
{ {
if (fm2->nth(i)->kind() != formula::UnOp) unop* c = is_G(fm2->nth(i));
if (!c || c->child() != a)
continue; continue;
unop* c = static_cast<unop*>(fm2->nth(i)); result_ =
if (c->op() == unop::G && c->child() == a) recurse_destroy(binop::instance
{
multop::vec* v = new multop::vec;
v->reserve(s - 1);
int j;
for (j = 0; j < i; ++j)
v->push_back(fm2->nth(j)->clone());
// skip j=i
for (++j; j < s; ++j)
v->push_back(fm2->nth(j)->clone());
b->destroy();
result_ = recurse_destroy(binop::instance
(binop::W, a, (binop::W, a,
multop::instance(multop::Or, v))); fm2->all_but(i)));
b->destroy();
return; return;
} }
} }
}
// a U (b & a & c) == (b & c) M a // a U (b & a & c) == (b & c) M a
// a W (b & a & c) == (b & c) R a // a W (b & a & c) == (b & c) R a
if (bt == multop::And) if (bt == multop::And)
@ -1804,18 +1794,10 @@ namespace spot
{ {
if (fm2->nth(i) != a) if (fm2->nth(i) != a)
continue; continue;
multop::vec* v = new multop::vec;
v->reserve(s - 1);
int j;
for (j = 0; j < i; ++j)
v->push_back(fm2->nth(j)->clone());
// skip j=i
for (++j; j < s; ++j)
v->push_back(fm2->nth(j)->clone());
b->destroy();
result_ = recurse_destroy(binop::instance result_ = recurse_destroy(binop::instance
(op == binop::U ? binop::M : binop::R, (op == binop::U ? binop::M : binop::R,
multop::instance(multop::And, v), a)); fm2->all_but(i), a));
b->destroy();
return; return;
} }
} }
@ -1826,7 +1808,7 @@ namespace spot
if (!opt_.reduce_size_strictly if (!opt_.reduce_size_strictly
&& fu1 && fu1->op() == unop::X && b->is_boolean()) && fu1 && fu1->op() == unop::X && b->is_boolean())
{ {
formula* c = fu1->child()->clone();; formula* c = fu1->child()->clone();
fu1->destroy(); fu1->destroy();
formula* x = formula* x =
unop::instance(unop::X, unop::instance(unop::X,
@ -1850,8 +1832,8 @@ namespace spot
return; return;
} }
// a R (b & c & F(a)) = a M b // a R (b & c & F(a)) = a M (b & c)
// a M (b & c & F(a)) = a M b // a M (b & c & F(a)) = a M (b & c)
if (b->kind() == formula::MultOp) if (b->kind() == formula::MultOp)
{ {
multop* fm2 = static_cast<multop*>(b); multop* fm2 = static_cast<multop*>(b);
@ -1860,28 +1842,18 @@ namespace spot
int s = fm2->size(); int s = fm2->size();
for (int i = 0; i < s; ++i) for (int i = 0; i < s; ++i)
{ {
if (fm2->nth(i)->kind() != formula::UnOp) unop* c = is_F(fm2->nth(i));
if (!c || c->child() != a)
continue; continue;
unop* c = static_cast<unop*>(fm2->nth(i)); result_ =
if (c->op() == unop::F && c->child() == a) recurse_destroy(binop::instance
{
multop::vec* v = new multop::vec;
v->reserve(s - 1);
int j;
for (j = 0; j < i; ++j)
v->push_back(fm2->nth(j)->clone());
// skip j=i
for (++j; j < s; ++j)
v->push_back(fm2->nth(j)->clone());
b->destroy();
result_ = recurse_destroy(binop::instance
(binop::M, a, (binop::M, a,
multop::instance(multop::And, v))); fm2->all_but(i)));
b->destroy();
return; return;
} }
} }
} }
}
// If b is Boolean: // If b is Boolean:
// (Xc) R b = b & X(b W c) // (Xc) R b = b & X(b W c)
@ -1889,7 +1861,7 @@ namespace spot
if (!opt_.reduce_size_strictly if (!opt_.reduce_size_strictly
&& fu1 && fu1->op() == unop::X && b->is_boolean()) && fu1 && fu1->op() == unop::X && b->is_boolean())
{ {
formula* c = fu1->child()->clone();; formula* c = fu1->child()->clone();
fu1->destroy(); fu1->destroy();
formula* x = formula* x =
unop::instance(unop::X, unop::instance(unop::X,