From c9a659c8d452c740f3e290895cfcc1cd95a04807 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 12 Oct 2011 11:06:26 +0800
Subject: [PATCH] Compare Boolean LTL formulae using BDDs.

* src/ltlvisit/simplify.cc (syntactic_implication): Here.
---
 src/ltlvisit/simplify.cc | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 9afd20750..6d14df5be 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2754,18 +2754,27 @@ namespace spot
 
       bool result = false;
 
-      inf_left_recurse_visitor v1(f2, this);
-      const_cast<formula*>(f1)->accept(v1);
-      if (v1.result())
+      if (f1->is_boolean() && f2->is_boolean())
 	{
-	  result = true;
+	  bdd l = as_bdd(f1);
+	  bdd r = as_bdd(f2);
+	  result = ((l & r) == l);
 	}
       else
 	{
-	  inf_right_recurse_visitor v2(f1, this);
-	  const_cast<formula*>(f2)->accept(v2);
-	  if (v2.result())
-	    result = true;
+	  inf_left_recurse_visitor v1(f2, this);
+	  const_cast<formula*>(f1)->accept(v1);
+	  if (v1.result())
+	    {
+	      result = true;
+	    }
+	  else
+	    {
+	      inf_right_recurse_visitor v2(f1, this);
+	      const_cast<formula*>(f2)->accept(v2);
+	      if (v2.result())
+		result = true;
+	    }
 	}
 
       // Cache result