From 9633dd6e889340088c816224cd330e8bc654da49 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 19 May 2012 21:08:36 +0200
Subject: [PATCH] Speedup syntactic implication by not comparing literals using
 bdd.

* src/ltlvisit/simplify.cc
(ltl_simplifier_cache::syntactic_implication): If the lhs and rhs are
literals that are not equal, return false immediately.
---
 src/ltlvisit/simplify.cc | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index b5c91c85f..96185286d 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -4103,6 +4103,18 @@ namespace spot
       if (g == constant::true_instance()
 	  || f == constant::false_instance())
 	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
       {