From 3b10bb3b8c380696104a69ba7e45dbb12084aa76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 19 Jul 2013 17:59:28 +0200 Subject: [PATCH] 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 | 2 ++ src/misc/satsolver.cc | 70 +++++++++++++++++++++++++++++++++++++++ src/misc/satsolver.hh | 46 +++++++++++++++++++++++++ src/tgbaalgos/dtbasat.cc | 16 ++------- src/tgbaalgos/dtgbasat.cc | 14 ++------ 5 files changed, 122 insertions(+), 26 deletions(-) create mode 100644 src/misc/satsolver.cc create mode 100644 src/misc/satsolver.hh 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());