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

Speedup syntactic implication by not comparing literals using bdd.

Browse source 
* src/ltlvisit/simplify.cc
(ltl_simplifier_cache::syntactic_implication): If the lhs and rhs are
literals that are not equal, return false immediately.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-19 21:08:36 +02:00
parent a80a5137fd
commit 9633dd6e88
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ltlvisit/simplify.cc
View file

@ -4103,6 +4103,18 @@ namespace spot
if (g == constant::true_instance() if (g == constant::true_instance()
|| f == constant::false_instance()) || f == constant::false_instance())
return true; return true;
if (g == constant::false_instance()
|| f == constant::true_instance())
return false;
// Often we compare a literals (an atomic_prop or its negation)
// to another literal. The result is necessarily false. To be
// true, the two literals would have to be equal, be we have
// already checked that.
if (f->is_in_nenoform() && g->is_in_nenoform()
&& (is_atomic_prop(f) || is_unop(f, unop::Not))
&& (is_atomic_prop(g) || is_unop(g, unop::Not)))
return false;
// Cache lookup // Cache lookup
{ {