diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 11a6a78db..8b2367339 100644
--- a/src/misc/Makefile.am
+++ b/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
diff --git a/src/misc/satsolver.cc b/src/misc/satsolver.cc
new file mode 100644
index 000000000..224881cab
--- /dev/null
+++ b/src/misc/satsolver.cc
@@ -0,0 +1,70 @@
+// -*- 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 .
+
+#include "config.h"
+#include "formater.hh"
+#include
+#include
+#include
+
+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);
+ }
+}
diff --git a/src/misc/satsolver.hh b/src/misc/satsolver.hh
new file mode 100644
index 000000000..fe559919b
--- /dev/null
+++ b/src/misc/satsolver.hh
@@ -0,0 +1,46 @@
+// -*- 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 .
+
+#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
+ /// SPOT_SATSOLVER environment variable.
+ ///
+ /// Note that temporary_file instances implement the
+ /// printable interface.
+ SPOT_API int
+ satsolver(printable* input, printable* output);
+}
+
+#endif // SPOT_MISC_SATSOLVER_HH
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index e2bc00c7f..9fe24d15f 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/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());
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 2fbb8fc58..9f482498d 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/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());