satsolver: new function

Uses the value of the SPOT_SATSOLVER environment variable
to decide how to call the SAT solver.

* src/misc/satsolver.cc, src/misc/satsolver.hh: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use satsolver().

src/misc/Makefile.am

@@ -51,6 +51,7 @@ misc_HEADERS = \
   optionmap.hh \
   position.hh \
   random.hh \
+  satsolver.hh \
   timer.hh \
   tmpfile.hh \
   unique_ptr.hh \
@@ -69,6 +70,7 @@ libmisc_la_SOURCES = \
   minato.cc \
   optionmap.cc \
   random.cc \
+  satsolver.cc \
   timer.cc \
   tmpfile.cc \
   version.cc

src/misc/satsolver.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "config.h"
+#include "formater.hh"
+#include <cstdlib>
+#include <sstream>
+#include <stdexcept>
+
+namespace spot
+{
+  namespace
+  {
+    struct satsolver_command: formater
+    {
+      const char* satsolver;
+
+      satsolver_command()
+      {
+	satsolver = getenv("SPOT_SATSOLVER");
+	if (!satsolver)
+	  {
+	    satsolver = "glucose %I >%O";
+	    return;
+	  }
+	prime(satsolver);
+	if (!has('I'))
+	  throw std::runtime_error("SPOT_SATSOLVER should contain %I to "
+				   "indicate how to use the input filename.");
+	if (!has('O'))
+	  throw std::runtime_error("SPOT_SATSOLVER should contain %O to "
+				   "indicate how to use the output filename.");
+      }
+
+      int
+      run(printable* in, printable* out)
+      {
+	declare('I', in);
+	declare('O', out);
+	std::ostringstream s;
+	format(s, satsolver);
+	return system(s.str().c_str());
+      }
+    };
+  }
+
+  int satsolver(printable* input, printable* output)
+  {
+    // Make this static, so the SPOT_SATSOLVER lookup is done only on
+    // the first call to run_sat().
+    static satsolver_command cmd;
+    return cmd.run(input, output);
+  }
+}

src/misc/satsolver.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_MISC_SATSOLVER_HH
+#define SPOT_MISC_SATSOLVER_HH
+
+#include "common.hh"
+
+namespace spot
+{
+  class printable;
+
+  /// \brief Run a SAT solver.
+  ///
+  /// Run a SAT solver using the input in file \a input,
+  /// and sending output in file \a output.
+  ///
+  /// These two arguments are instance of printable, as
+  /// they will be evaluated in a %-escaped string such as
+  ///    "satsolver %I >%O"
+  /// This command can be overridden using the
+  /// <code>SPOT_SATSOLVER</code> environment variable.
+  ///
+  /// Note that temporary_file instances implement the
+  /// printable interface.
+  SPOT_API int
+  satsolver(printable* input, printable* output);
+}
+
+#endif // SPOT_MISC_SATSOLVER_HH

src/tgbaalgos/dtbasat.cc

@@ -29,6 +29,7 @@
 #include "ltlast/constant.hh"
 #include "stats.hh"
 #include "misc/tmpfile.hh"
+#include "misc/satsolver.hh"
 
 // If the following DEBUG macro is set to 1, the temporary files used
 // to communicate with the SAT-solver will be left in the current
@@ -60,7 +61,6 @@ namespace spot
 {
   namespace
   {
-
     static bdd_dict* debug_dict = 0;
 
     struct transition
@@ -707,25 +707,13 @@ namespace spot
 
 	cnf = create_tmpfile("dtba-sat-", ".cnf");
 
-	// FIXME: we should use proper temporary names
 	std::fstream cnfs(cnf->name(),
 			  std::ios_base::trunc | std::ios_base::out);
 	dtba_to_sat(cnfs, a, *current);
 	cnfs.close();
 
 	out = create_tmpfile("dtba-sat-", ".out");
-
-	const char* satsolver = getenv("SATSOLVER");
-	if (!satsolver)
-	  satsolver = "glucose";
-
-	std::string s(satsolver);
-	s += " ";
-	s += cnf->name();
-	s += " > ";
-	s += out->name();
-	system(s.c_str());
-
+	satsolver(cnf, out);
 	current_solution = get_solution(out->name());
       }
     while (target_state_number == -1 && !current_solution.empty());

src/tgbaalgos/dtgbasat.cc

@@ -30,6 +30,7 @@
 #include "stats.hh"
 #include "ltlenv/defaultenv.hh"
 #include "misc/tmpfile.hh"
+#include "misc/satsolver.hh"
 
 // If the following DEBUG macro is set to 1, the temporary files used
 // to communicate with the SAT-solver will be left in the current
@@ -902,18 +903,7 @@ namespace spot
 	cnfs.close();
 
 	out = create_tmpfile("dtba-sat-", ".out");
-
-	const char* satsolver = getenv("SATSOLVER");
-	if (!satsolver)
-	  satsolver = "glucose";
-
-	std::string s(satsolver);
-	s += " ";
-	s += cnf->name();
-	s += " > ";
-	s += out->name();
-	system(s.c_str());
-
+	satsolver(cnf, out);
 	current_solution = get_solution(out->name());
       }
     while (!current_solution.empty());