From 1f3b7e8002a556b32d861efc7661d108eb02bf54 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 3 Sep 2013 10:34:50 +0200
Subject: [PATCH] sat: catch cases where nbclause > INT_MAX and report them

* src/misc/satsolver.hh (clause_counter): New class.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use it.
---
 src/misc/satsolver.hh     | 38 ++++++++++++++++++++++++++++++++++++++
 src/tgbaalgos/dtbasat.cc  | 27 +++++++++++++++++++--------
 src/tgbaalgos/dtgbasat.cc | 27 +++++++++++++++++++--------
 3 files changed, 76 insertions(+), 16 deletions(-)

diff --git a/src/misc/satsolver.hh b/src/misc/satsolver.hh
index 0f0b08575..4d7ff4ca1 100644
--- a/src/misc/satsolver.hh
+++ b/src/misc/satsolver.hh
@@ -22,11 +22,49 @@
 
 #include "common.hh"
 #include <vector>
+#include <stdexcept>
 
 namespace spot
 {
   class printable;
 
+  class clause_counter
+  {
+  private:
+    int count_;
+
+  public:
+    clause_counter()
+      : count_(0)
+    {
+    }
+
+    void check() const
+    {
+      if (count_ < 0)
+	throw std::runtime_error("too many SAT clauses (more than INT_MAX)");
+    }
+
+    clause_counter& operator++()
+    {
+      ++count_;
+      check();
+      return *this;
+    }
+
+    clause_counter& operator+=(int n)
+    {
+      count_ += n;
+      check();
+      return *this;
+    }
+
+    int nb_clauses() const
+    {
+      return count_;
+    }
+  };
+
   /// \brief Run a SAT solver.
   ///
   /// Run a SAT solver using the input in file \a input,
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index 0a83b41dd..4b00e9179 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -299,7 +299,7 @@ namespace spot
     void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d,
 		     bool state_based)
     {
-      int nclauses = 0;
+      clause_counter nclauses;
       int ref_size = 0;
 
       scc_map sm(ref);
@@ -359,7 +359,7 @@ namespace spot
 	      }
  	  ++j;
  	}
-      if (!nclauses)
+      if (!nclauses.nb_clauses())
  	dout << "(none)\n";
 
       dout << "(1) the candidate automaton is complete\n";
@@ -636,7 +636,7 @@ namespace spot
 	    }
 	}
       out.seekp(0);
-      out << "p cnf " << d.nvars << " " << nclauses;
+      out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
     }
 
     static tgba_explicit_number*
@@ -769,11 +769,22 @@ namespace spot
     current = new dict;
     current->cand_size = target_state_number;
 
-    cnf = create_tmpfile("dtba-sat-", ".cnf");
-    std::fstream cnfs(cnf->name(),
-		      std::ios_base::trunc | std::ios_base::out);
-    dtba_to_sat(cnfs, a, *current, state_based);
-    cnfs.close();
+    try
+      {
+	cnf = create_tmpfile("dtba-sat-", ".cnf");
+	std::fstream cnfs(cnf->name(),
+			  std::ios_base::trunc | std::ios_base::out);
+	dtba_to_sat(cnfs, a, *current, state_based);
+	cnfs.close();
+      }
+    catch (...)
+      {
+	if (DEBUG)
+	  xrename(cnf->name(), "dtba-sat.cnf");
+	delete current;
+	delete cnf;
+	throw;
+      }
 
     out = create_tmpfile("dtba-sat-", ".out");
     satsolver(cnf, out);
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 0359f00e6..9e95dab44 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -476,7 +476,7 @@ namespace spot
     void dtgba_to_sat(std::ostream& out, const tgba* ref, dict& d,
 		      bool state_based)
     {
-      int nclauses = 0;
+      clause_counter nclauses;
       int ref_size = 0;
 
       scc_map sm(ref);
@@ -536,7 +536,7 @@ namespace spot
 	      }
  	  ++j;
  	}
-      if (!nclauses)
+      if (!nclauses.nb_clauses())
  	dout << "(none)\n";
 
       dout << "(8) the candidate automaton is complete\n";
@@ -847,7 +847,7 @@ namespace spot
 	    }
 	}
       out.seekp(0);
-      out << "p cnf " << d.nvars << " " << nclauses;
+      out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
     }
 
     static tgba_explicit_number*
@@ -977,11 +977,22 @@ namespace spot
     current->cand_size = target_state_number;
     current->cand_nacc = target_acc_number;
 
-    cnf = create_tmpfile("dtgba-sat-", ".cnf");
-    std::fstream cnfs(cnf->name(),
-		      std::ios_base::trunc | std::ios_base::out);
-    dtgba_to_sat(cnfs, a, *current, state_based);
-    cnfs.close();
+    try
+      {
+	cnf = create_tmpfile("dtgba-sat-", ".cnf");
+	std::fstream cnfs(cnf->name(),
+			  std::ios_base::trunc | std::ios_base::out);
+	dtgba_to_sat(cnfs, a, *current, state_based);
+	cnfs.close();
+      }
+    catch (...)
+      {
+	if (DEBUG)
+	  xrename(cnf->name(), "dgtba-sat.cnf");
+	delete current;
+	delete cnf;
+	throw;
+      }
 
     out = create_tmpfile("dtgba-sat-", ".out");
     satsolver(cnf, out);