From 946f305f7c88a919e1feb95062b3ce273b9cc40b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Apr 2010 12:27:31 +0200 Subject: [PATCH] Speed up syntactic_implication() for constants. * src/ltlvisit/syntimpl.cc (syntactic_implication): Do not create visitors if arguments are constant. --- ChangeLog | 7 +++++++ src/ltlvisit/syntimpl.cc | 6 +++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/ChangeLog b/ChangeLog index 39afdb2c5..b0744d86f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2010-04-15 Alexandre Duret-Lutz + + 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 Fix simplification of "a M true" as Fa. diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 576c92642..e3eefd498 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -616,13 +616,13 @@ namespace spot { if (f1 == f2) return true; - inf_left_recurse_visitor v1(f2); - inf_right_recurse_visitor v2(f1); - if (f2 == constant::true_instance() || f1 == constant::false_instance()) return true; + inf_left_recurse_visitor v1(f2); + inf_right_recurse_visitor v2(f1); + const_cast(f1)->accept(v1); if (v1.result()) return true;