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

Speed up syntactic_implication() for constants.

Browse source 
* src/ltlvisit/syntimpl.cc (syntactic_implication): Do not
create visitors if arguments are constant.
This commit is contained in:
Alexandre Duret-Lutz 2010-04-15 12:27:31 +02:00
parent 7021e45f70
commit 946f305f7c
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Speed up syntactic_implication() for constants.
* src/ltlvisit/syntimpl.cc (syntactic_implication): Do not
create visitors if arguments are constant.
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix simplification of "a M true" as Fa. Fix simplification of "a M true" as Fa.

6
src/ltlvisit/syntimpl.cc
View file

@ -616,13 +616,13 @@ namespace spot
{ {
if (f1 == f2) if (f1 == f2)
return true; return true;
inf_left_recurse_visitor v1(f2);
inf_right_recurse_visitor v2(f1);
if (f2 == constant::true_instance() if (f2 == constant::true_instance()
|| f1 == constant::false_instance()) || f1 == constant::false_instance())
return true; return true;
inf_left_recurse_visitor v1(f2);
inf_right_recurse_visitor v2(f1);
const_cast<formula*>(f1)->accept(v1); const_cast<formula*>(f1)->accept(v1);
if (v1.result()) if (v1.result())
return true; return true;