From b318b151c83280a2f59f04027e89d86ca2a2d6a1 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 11 Sep 2013 14:36:08 +0200
Subject: [PATCH] satmin: ignore (s,l,d2) if (s,l,d1) is already in result

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
---
 src/tgbaalgos/dtbasat.cc  | 50 +++++++++++++++++++++++++++-------
 src/tgbaalgos/dtgbasat.cc | 56 ++++++++++++++++++++++++++++++---------
 2 files changed, 85 insertions(+), 21 deletions(-)

diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index 0af71e1ed..aca16088f 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -95,6 +95,32 @@ namespace spot
       }
     };
 
+    struct src_cond
+    {
+      int src;
+      bdd cond;
+
+      src_cond(int src, bdd cond)
+	: src(src), cond(cond)
+      {
+      }
+
+      bool operator<(const src_cond& other) const
+      {
+	if (this->src < other.src)
+	  return true;
+	if (this->src > other.src)
+	  return false;
+	return this->cond.id() < other.cond.id();
+      }
+
+      bool operator==(const src_cond& other) const
+      {
+	return (this->src == other.src
+		&& this->cond.id() == other.cond.id());
+      }
+    };
+
     struct state_pair
     {
       int a;
@@ -678,6 +704,7 @@ namespace spot
 
       dout << "--- transition variables ---\n";
       std::set<int> acc_states;
+      std::set<src_cond> seen_trans;
       for (sat_solution::const_iterator i = solution.begin();
 	   i != solution.end(); ++i)
 	{
@@ -694,17 +721,22 @@ namespace spot
 
 	  if (t != satdict.revtransid.end())
 	    {
-	      last_aut_trans = a->create_transition(t->second.src,
-						    t->second.dst);
-	      last_aut_trans->condition = t->second.cond;
-	      last_sat_trans = &t->second;
+	      // Skip (s,l,d2) if we have already seen some (s,l,d1).
+	      if (seen_trans.insert(src_cond(t->second.src,
+					     t->second.cond)).second)
+		{
+		  last_aut_trans = a->create_transition(t->second.src,
+							t->second.dst);
+		  last_aut_trans->condition = t->second.cond;
+		  last_sat_trans = &t->second;
 
-	      dout << v << "\t" << t->second << "δ\n";
+		  dout << v << "\t" << t->second << "δ\n";
 
-	      // Mark the transition as accepting if the source is.
-	      if (state_based
-		  && acc_states.find(t->second.src) != acc_states.end())
-		last_aut_trans->acceptance_conditions = acc;
+		  // Mark the transition as accepting if the source is.
+		  if (state_based
+		      && acc_states.find(t->second.src) != acc_states.end())
+		    last_aut_trans->acceptance_conditions = acc;
+		}
 	    }
 	  else
 	    {
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index c55ec7e67..2ab7331ba 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -96,6 +96,32 @@ namespace spot
       }
     };
 
+    struct src_cond
+    {
+      int src;
+      bdd cond;
+
+      src_cond(int src, bdd cond)
+	: src(src), cond(cond)
+      {
+      }
+
+      bool operator<(const src_cond& other) const
+      {
+	if (this->src < other.src)
+	  return true;
+	if (this->src > other.src)
+	  return false;
+	return this->cond.id() < other.cond.id();
+      }
+
+      bool operator==(const src_cond& other) const
+      {
+	return (this->src == other.src
+		&& this->cond.id() == other.cond.id());
+      }
+    };
+
     struct transition_acc
     {
       int src;
@@ -875,6 +901,7 @@ namespace spot
 
       dout << "--- transition variables ---\n";
       std::map<int, bdd> state_acc;
+      std::set<src_cond> seen_trans;
       for (sat_solution::const_iterator i = solution.begin();
 	   i != solution.end(); ++i)
 	{
@@ -891,19 +918,24 @@ namespace spot
 
 	  if (t != satdict.revtransid.end())
 	    {
-	      last_aut_trans = a->create_transition(t->second.src,
-						    t->second.dst);
-	      last_aut_trans->condition = t->second.cond;
-	      last_sat_trans = &t->second;
-
-	      dout << v << "\t" << t->second << "δ\n";
-
-	      if (state_based)
+	      // Skip (s,l,d2) if we have already seen some (s,l,d1).
+	      if (seen_trans.insert(src_cond(t->second.src,
+					     t->second.cond)).second)
 		{
-		  std::map<int, bdd>::const_iterator i =
-		    state_acc.find(t->second.src);
-		  if (i != state_acc.end())
-		    last_aut_trans->acceptance_conditions = i->second;
+		  last_aut_trans = a->create_transition(t->second.src,
+							t->second.dst);
+		  last_aut_trans->condition = t->second.cond;
+		  last_sat_trans = &t->second;
+
+		  dout << v << "\t" << t->second << "δ\n";
+
+		  if (state_based)
+		    {
+		      std::map<int, bdd>::const_iterator i =
+			state_acc.find(t->second.src);
+		      if (i != state_acc.end())
+			last_aut_trans->acceptance_conditions = i->second;
+		    }
 		}
 	    }
 	  else