From 9a14d28a068c21f736e0c8c90cd3abb7b4aecf5b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 23 Nov 2009 21:47:25 +0100
Subject: [PATCH] Use bdd_satprefix() to speedup minato on BDDs that are almost
 cubes.

* src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix.
(minato_isop::next): Avoid useless intermediate variables.
* src/misc/minato.hh: Typo in comments.
---
 ChangeLog          |  8 ++++++++
 src/misc/minato.cc | 22 +++++++++++++---------
 src/misc/minato.hh | 10 +++++-----
 3 files changed, 26 insertions(+), 14 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 461add2ab..9cc362f56 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2009-11-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Use bdd_satprefix() to speedup minato on BDDs that are almost cubes.
+
+	* src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix.
+	(minato_isop::next): Avoid useless intermediate variables.
+	* src/misc/minato.hh: Typo in comments.
+
 2009-11-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Specialize scc_filter when handling tgba_explicit_formula automata.
diff --git a/src/misc/minato.cc b/src/misc/minato.cc
index 1d2364990..c1b6aa220 100644
--- a/src/misc/minato.cc
+++ b/src/misc/minato.cc
@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
+// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,7 +20,6 @@
 // 02111-1307, USA.
 
 #include "minato.hh"
-#include <utility>
 #include <cassert>
 
 namespace spot
@@ -30,15 +29,22 @@ namespace spot
     : ret_(bddfalse)
 
   {
+    // If INPUT has the form a&b&c&(binary function) we want to
+    // compute the ISOP of the only binary and prepend a&b&c latter.
+    //
+    // Calling bdd_satprefix (it returns a&b&c and modify input to
+    // point to function) this way is an optimization to the
+    // original algorithm, because in many cases we are trying to
+    // build ISOPs out of formulae that are already cubes.
+    cube_.push(bdd_satprefix(input));
     todo_.push(local_vars(input, input, bdd_support(input)));
-    cube_.push(bddtrue);
   }
 
   minato_isop::minato_isop(bdd input, bdd vars)
     : ret_(bddfalse)
   {
+    cube_.push(bdd_satprefix(input));
     todo_.push(local_vars(input, input, vars));
-    cube_.push(bddtrue);
   }
 
   bdd
@@ -138,10 +144,8 @@ namespace spot
 	    l.g1 = ret_;
 	    cube_.pop();
 	    {
-	      bdd f0s_min = l.f0_min - l.g0;
-	      bdd f1s_min = l.f1_min - l.g1;
 	      bdd fs_max = l.f0_max & l.f1_max;
-	      bdd fs_min = fs_max & (f0s_min | f1s_min);
+	      bdd fs_min = fs_max & ((l.f0_min - l.g0) | (l.f1_min - l.g1));
 	      todo_.push(local_vars(fs_min, fs_max, l.vars));
 	    }
 	    continue;
diff --git a/src/misc/minato.hh b/src/misc/minato.hh
index 963e57fc1..0c697898b 100644
--- a/src/misc/minato.hh
+++ b/src/misc/minato.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -65,17 +65,17 @@ namespace spot
     /// Internal variables for minato_isop.
     struct local_vars
     {
-      // If you are following the paper, f_min and f_max corresponds
-      // to the pair of BDD function used to encode the ternary function `f'
+      // If you are following the paper, f_min and f_max correspond
+      // to the pair of BDD functions used to encode the ternary function f
       // (see Section 3.4).
       // Also note that f0, f0', and f0'' all share the same _max function.
       // Likewise for f1, f1', and f1''.
       bdd f_min, f_max;
       // Because we need a non-recursive version of the algorithm,
-      // we had to split it in four step (each step is separated
+      // we had to split it in four steps (each step is separated
       // from the other by a call to ISOP in the original algorithm).
       enum { FirstStep, SecondStep, ThirdStep, FourthStep } step;
-      // The list of variable to factorize.  This is an addition to
+      // The list of variables to factorize.  This is an addition to
       // the original algorithm.
       bdd vars;
       bdd v1;