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

Simplify {#e}[]->Exp and {#e}<>->Exp.

Browse source 
* src/ltlast/binop.cc: Add simplification rules.
This commit is contained in:
Alexandre Duret-Lutz 2010-02-08 18:00:24 +01:00
parent fc7c2943de
commit 76528ee2fb
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ltlast/binop.cc
View file

@ -258,13 +258,15 @@ namespace spot
case EConcat: case EConcat:
// - 0 <>-> Exp = 0 // - 0 <>-> Exp = 0
// - 1 <>-> Exp = Exp // - 1 <>-> Exp = Exp
// - #e <>-> Exp = 0
// - Exp <>-> 0 = 0 // - Exp <>-> 0 = 0
if (first == constant::true_instance()) if (first == constant::true_instance())
return second; return second;
if (first == constant::false_instance()) if (first == constant::false_instance()
|| first == constant::empty_word_instance())
{ {
second->destroy(); second->destroy();
return first; return constant::false_instance();
} }
if (second == constant::false_instance()) if (second == constant::false_instance())
{ {
@ -275,13 +277,15 @@ namespace spot
case UConcat: case UConcat:
// - 0 []-> Exp = 1 // - 0 []-> Exp = 1
// - 1 []-> Exp = Exp // - 1 []-> Exp = Exp
// - #e []-> Exp = 1
// - Exp []-> 1 = 1 // - Exp []-> 1 = 1
if (first == constant::false_instance())
return constant::true_instance();
if (first == constant::true_instance()) if (first == constant::true_instance())
return second;
if (first == constant::false_instance()
|| first == constant::empty_word_instance())
{ {
second->destroy(); second->destroy();
return first; return constant::true_instance();
} }
if (second == constant::true_instance()) if (second == constant::true_instance())
{ {