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

Take trivial identities into account to simplify basicreduce.

Browse source 
* src/ltlvisit/basicreduce.cc: Do not test
for things like X(true), F(false), or `a U 1`.
These are all trivial identities.
This commit is contained in:
Alexandre Duret-Lutz 2011-05-28 15:01:22 +02:00
parent bd720488b4
commit aa5c2f606b
1 changed files with 13 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/ltlvisit/basicreduce.cc
View file

@ -137,17 +137,18 @@ namespace spot
return; return;
case unop::X: case unop::X:
// X(true) = true // X(constant) = constant is a trivial identity.
// X(false) = false assert(result_->kind() != formula::Constant);
if (result_->kind() == formula::Constant)
return;
// XGF(f) = GF(f) // XGF(f) = GF(f)
// FIXME: isn't that true also for FG ?
if (is_GF(result_)) if (is_GF(result_))
return; return;
// X(f1 & GF(f2)) = X(f1) & GF(F2) // X(f1 & GF(f2)) = X(f1) & GF(f2)
// X(f1 | GF(f2)) = X(f1) | GF(F2) // X(f1 | GF(f2)) = X(f1) | GF(f2)
// FIXME: isn't that true also for FG ?
if (result_->kind() == formula::MultOp) if (result_->kind() == formula::MultOp)
{ {
mo = static_cast<multop*>(result_); mo = static_cast<multop*>(result_);
@ -159,10 +160,8 @@ namespace spot
return; return;
case unop::F: case unop::F:
// F(true) = true // F(constant) = constant is a trivial identity.
// F(false) = false assert(result_->kind() != formula::Constant);
if (result_->kind() == formula::Constant)
return;
// FX(a) = XF(a) // FX(a) = XF(a)
if (result_->kind() == formula::UnOp) if (result_->kind() == formula::UnOp)
@ -211,10 +210,8 @@ namespace spot
return; return;
case unop::G: case unop::G:
// G(true) = true // G(constant) = constant is a trivial identity
// G(false) = false assert(result_->kind() != formula::Constant);
if (result_->kind() == formula::Constant)
return;
// G(a R b) = G(b) // G(a R b) = G(b)
if (result_->kind() == formula::BinOp) if (result_->kind() == formula::BinOp)
@ -309,18 +306,14 @@ namespace spot
result_ = unop::instance(unop::F, f1); result_ = unop::instance(unop::F, f1);
return; return;
} }
// These are trivial identities:
// a U false = false // a U false = false
// a U true = true // a U true = true
// a R false = false // a R false = false
// a R true = true // a R true = true
// a W true = true // a W true = true
// a M false = false // a M false = false
if (f2->kind() == formula::Constant) assert(f2->kind() != formula::Constant);
{
result_ = f2;
f1->destroy();
return;
}
// Same effect as dynamic_cast<unop*>, only faster. // Same effect as dynamic_cast<unop*>, only faster.
unop* fu1 = unop* fu1 =