From 317fed597b9852f14c7ed82de5b55d4b5398a08b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 10 Aug 2003 13:09:50 +0000
Subject: [PATCH] * src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc,
 src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !' between
 two BDDs.  That's one less call to BuDDy.

---
 ChangeLog                    | 4 ++++
 src/tgba/bdddict.cc          | 2 +-
 src/tgba/succiterconcrete.cc | 8 ++++----
 src/tgba/tgbaexplicit.cc     | 2 +-
 src/tgba/tgbatba.cc          | 4 ++--
 src/tgbaalgos/lbtt.cc        | 6 +++---
 6 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 79a8a1b7b..561901b6c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,9 @@
 2003-08-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc,
+	src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !'
+	between two BDDs.  That's one less call to BuDDy.
+
 	* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test:
 	Adjust expected output after 2003-08-07's change.
 
diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc
index 4b12092b0..38115ca80 100644
--- a/src/tgba/bdddict.cc
+++ b/src/tgba/bdddict.cc
@@ -28,7 +28,7 @@ namespace spot
     fv_map::iterator sii = var_map.find(f);
     if (sii != var_map.end())
       {
-	num =  sii->second;
+	num = sii->second;
       }
     else
       {
diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc
index 91c34a78c..09cf4a808 100644
--- a/src/tgba/succiterconcrete.cc
+++ b/src/tgba/succiterconcrete.cc
@@ -66,11 +66,11 @@ namespace spot
     do
       {
 	// FIXME: Iterating on the successors this way (calling
-	// bdd_satone{,set} and NANDing out the result from a
+	// bdd_satone{,set} and NANDing out (-=) the result from a
 	// set) requires several descent of the BDD.  Maybe it would be
 	// faster to compute all satisfying formula in one operation.
 
-	succ_set_left_ &= !current_;
+	succ_set_left_ -= current_;
 	if (succ_set_left_ == bddfalse) // No more successors?
 	  return;
 
@@ -113,7 +113,7 @@ namespace spot
 	    // So, first, filter out all transitions like p, which
 	    // are also in other accepting sets.
 	    bdd fout = bdd_relprod(as, !current_acc_, data_.acc_set);
-	    bdd as_fout = as & !fout;
+	    bdd as_fout = as - fout;
 	    // Then, pick the remaining term that are exactly in all
 	    // required accepting sets.
 	    bdd all = bddtrue;
@@ -121,7 +121,7 @@ namespace spot
 	    do
 	      {
 		bdd one_acc = bdd_satone(acc);
-		acc &= !one_acc;
+		acc -= one_acc;
 		all &= bdd_relprod(as_fout, one_acc, data_.acc_set);
 	      }
 	    while (acc != bddfalse);
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index f00c1e7b9..b490dabaf 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -151,7 +151,7 @@ namespace spot
   void
   tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
   {
-    t->condition &= ! get_condition(f);
+    t->condition -= get_condition(f);
   }
 
   void
diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc
index 92df1ffdd..9c7160af3 100644
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@@ -156,14 +156,14 @@ namespace spot
     // Now build the "cycle" of accepting conditions.
 
     bdd last = bdd_satone(all);
-    all &= !last;
+    all -= last;
 
     acc_cycle_[bddtrue] = last;
 
     while (all != bddfalse)
       {
 	bdd next = bdd_satone(all);
-	all &= !next;
+	all -= next;
 	acc_cycle_[last] = next;
 	last = next;
       }
diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc
index 3aae51295..73151095d 100644
--- a/src/tgbaalgos/lbtt.cc
+++ b/src/tgbaalgos/lbtt.cc
@@ -24,7 +24,7 @@ namespace spot
       while (all_acc != bddfalse)
 	{
 	  bdd acc = bdd_satone(all_acc);
-	  all_acc &= !acc;
+	  all_acc -= acc;
 	  sm[acc] = count++;
 	}
     }
@@ -35,7 +35,7 @@ namespace spot
       while (b != bddfalse)
 	{
 	  bdd acc = bdd_satone(b);
-	  b &= !acc;
+	  b -= acc;
 	  os << sm[acc] << " ";
 	}
       return os;
@@ -65,7 +65,7 @@ namespace spot
     else
       {
 	bdd cube = bdd_satone(b);
-	b &= !cube;
+	b -= cube;
 	if (b != bddfalse)
 	  {
 	    return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d);