From 484ea488c39c8ff8a65a626ad0084d93d4c4d972 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 13 Jun 2012 21:16:33 +0200
Subject: [PATCH] Use bdd_implies() to speedup various algorithms.

* src/ltlvisit/simplify.cc, src/tgba/tgbaproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc: Here.
---
 src/ltlvisit/simplify.cc    | 10 ++--------
 src/tgba/tgbaproduct.cc     |  6 +++---
 src/tgba/tgbatba.cc         |  8 ++++----
 src/tgbaalgos/sccfilter.cc  |  7 +++----
 src/tgbaalgos/simulation.cc |  3 +--
 5 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 514e8f354..d5b911fc4 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -4140,15 +4140,9 @@ namespace spot
       bool result;
 
       if (f->is_boolean() && g->is_boolean())
-	{
-	  bdd l = as_bdd(f);
-	  bdd r = as_bdd(g);
-	  result = ((l & r) == l);
-	}
+	result = bdd_implies(as_bdd(f), as_bdd(g));
       else
-	{
-	  result = syntactic_implication_aux(f, g);
-	}
+	result = syntactic_implication_aux(f, g);
 
       // Cache result
       {
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index 8d1bad400..c0f791851 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -319,7 +319,7 @@ namespace spot
       {
 	assert(bdd_high(tmp) == bddfalse);
 	int var = bdd_var(tmp);
-	if ((bdd_nithvar(var) & rna) == rna)
+	if (bdd_implies(rna, bdd_nithvar(var)))
 	  {
 	    int varclone = dict_->register_clone_acc(var, this);
 	    bdd_setpair(right_common_acc_, var, varclone);
diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc
index f2ddc4e25..9f2bef2fe 100644
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@@ -241,11 +241,11 @@ namespace spot
 		    --prev;
 		    bdd common = aut->
 		      common_acceptance_conditions_of_original_state(rs);
-		    if ((common & *prev) == *prev)
+		    if (bdd_implies(*prev, common))
 		      {
 			bdd u = aut->
 			  union_acceptance_conditions_of_original_state(odest);
-			if ((u & *prev) != *prev)
+			if (!bdd_implies(*prev, u))
 			  acc -= *prev;
 		      }
 		  }
@@ -279,7 +279,7 @@ namespace spot
 		// acceptance sets common to the outgoing transition of
 		// the destination state.
 		acc |= otheracc;
-		while (next != cycle.end() && (acc & *next) == *next)
+		while (next != cycle.end() && bdd_implies(*next, acc))
 		  ++next;
 		if (next != cycle.end())
 		  {
@@ -291,7 +291,7 @@ namespace spot
 	    accepting = true;
 	    // Skip as much acceptance conditions as we can on our cycle.
 	    next = cycle.begin();
-	    while (next != expected && (acc & *next) == *next)
+	    while (next != expected && bdd_implies(*next, acc))
 	      ++next;
 	  next_is_set:
 	    state_tba_proxy* dest =
diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc
index 8b64aab99..53f670ce5 100644
--- a/src/tgbaalgos/sccfilter.cc
+++ b/src/tgbaalgos/sccfilter.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -142,8 +142,7 @@ namespace spot
     // and we want to find that 'a' and 'b' are useless because
     // they always occur with 'c'.
     // The way we check if 'a' is useless that is to look whether
-    // USEFUL & (x -> a) == USEFUL for some other acceptance
-    // condition x.
+    // USEFUL implies (x -> a) for some other acceptance condition x.
     bdd allconds = bdd_support(negall);
     bdd allcondscopy = allconds;
     bdd useless = bddtrue;
@@ -157,7 +156,7 @@ namespace spot
 	    bdd x = bdd_ithvar(bdd_var(others));
 	    if (x != a)
 	      {
-		if ((useful & (x >> a)) == useful)
+		if (bdd_implies(useful, x >> a))
 		  {
 		    // a is useless
 		    useful = bdd_exist(useful, a);
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index f67fb776f..e4aa36693 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -411,8 +411,7 @@ namespace spot
 		if (it1 == it2)
 		  continue;
 
-		// We detect that "a&b -> a" by testing "a&b = a".
-		if ((it1->first & it2->first) == (it1->first))
+		if (bdd_implies(it1->first, it2->first))
 		  {
 		    accu &= it2->second;
 		    ++po_size_;