diff --git a/src/misc/satsolver.cc b/src/misc/satsolver.cc index 914fba7d1..95a1ed862 100644 --- a/src/misc/satsolver.cc +++ b/src/misc/satsolver.cc @@ -83,18 +83,10 @@ namespace spot }; } - 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); - } - - sat_solution + satsolver::solution satsolver_get_solution(const char* filename) { - sat_solution sol; + satsolver::solution sol; std::istream* in; if (filename[0] == '-' && filename[1] == 0) in = &std::cin; @@ -130,4 +122,47 @@ namespace spot return sol; } + satsolver::satsolver() + : cnf_tmp_(0), cnf_stream_(0) + { + start(); + } + + void satsolver::start() + { + cnf_tmp_ = create_tmpfile("sat-", ".cnf"); + cnf_stream_ = new std::fstream(cnf_tmp_->name(), + std::ios_base::trunc | std::ios_base::out); + cnf_stream_->exceptions(std::ifstream::failbit | std::ifstream::badbit); + } + + satsolver::~satsolver() + { + delete cnf_tmp_; + delete cnf_stream_; + } + + std::ostream& satsolver::operator()() + { + return *cnf_stream_; + } + + satsolver::solution_pair + satsolver::get_solution() + { + delete cnf_stream_; // Close the file. + cnf_stream_ = 0; + + temporary_file* output = create_tmpfile("sat-", ".out"); + solution_pair p; + + // Make this static, so the SPOT_SATSOLVER lookup is done only on + // the first call to run_sat(). + static satsolver_command cmd; + + p.first = cmd.run(cnf_tmp_, output); + p.second = satsolver_get_solution(output->name()); + delete output; + return p; + } } diff --git a/src/misc/satsolver.hh b/src/misc/satsolver.hh index 4d7ff4ca1..43aba9535 100644 --- a/src/misc/satsolver.hh +++ b/src/misc/satsolver.hh @@ -21,8 +21,10 @@ #define SPOT_MISC_SATSOLVER_HH #include "common.hh" +#include "tmpfile.hh" #include #include +#include namespace spot { @@ -65,29 +67,37 @@ namespace spot } }; - /// \brief Run a SAT solver. + /// \brief Interface with a SAT solver. /// - /// Run a SAT solver using the input in file \a input, - /// and sending output in file \a output. + /// Call start() to create some temporary file, then send DIMACs + /// text to the stream returned by operator(), and finally call + /// get_solution(). /// - /// 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); + /// The satsolver called can be configured via the + /// SPOT_SATSOLVER environment variable. It + /// defaults to + /// "satsolver -verb=0 %I >%O" + /// where %I and %O are replaced by input and output files. + class SPOT_API satsolver + { + public: + satsolver(); + ~satsolver(); + void start(); + std::ostream& operator()(); - typedef std::vector sat_solution; + typedef std::vector solution; + typedef std::pair solution_pair; + solution_pair get_solution(); + private: + temporary_file* cnf_tmp_; + std::ostream* cnf_stream_; + }; /// \brief Extract the solution of a SAT solver output. - SPOT_API sat_solution + SPOT_API satsolver::solution satsolver_get_solution(const char* filename); - } #endif // SPOT_MISC_SATSOLVER_HH diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index ece461b17..fad083ee2 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include -#include #include #include "dtbasat.hh" #include "reachiter.hh" @@ -29,25 +28,16 @@ #include "tgba/bddprint.hh" #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 -// directory. (The files dtba-sat.cnf and dtba-sat.out contain the -// input and output for the last successful minimization attempted, or -// for the only failed attempt if the minimization failed.) +// If you set the SPOT_TMPKEEP environment variable the temporary +// file used to communicate with the sat solver will be left in +// the current directory. // -// Additionally, the CNF file will be output with a comment before -// each clause, and an additional output file (dtba-sat.dbg) will be -// created with a list of all positive variables in the result and -// their meaning. -// -// Note that the code use unique temporary filenames, so it is safe to -// run several such minimizations in parallel. It only when DEBUG=1 -// that some of these files will be renamed to the above hard-coded -// names, possibly causing confusion if multiple minimizations are -// debugged in parallel and in the same directory. +// Additionally, if the following DEBUG macro is set to 1, the CNF +// file will be output with a comment before each clause, and an +// additional output file (dtba-sat.dbg) will be created with a list +// of all positive variables in the result and their meaning. #define DEBUG 0 #if DEBUG @@ -820,8 +810,8 @@ namespace spot } static tgba_explicit_number* - sat_build(const sat_solution& solution, dict& satdict, const tgba* aut, - bool state_based) + sat_build(const satsolver::solution& solution, dict& satdict, + const tgba* aut, bool state_based) { bdd_dict* autdict = aut->get_dict(); tgba_explicit_number* a = new tgba_explicit_number(autdict); @@ -847,7 +837,7 @@ namespace spot dout << "--- transition variables ---\n"; std::set acc_states; std::set seen_trans; - for (sat_solution::const_iterator i = solution.begin(); + for (satsolver::solution::const_iterator i = solution.begin(); i != solution.end(); ++i) { int v = *i; @@ -930,17 +920,6 @@ namespace spot a->merge_transitions(); return a; } - - static bool - xrename(const char* from, const char* to) - { - if (!rename(from, to)) - return false; - std::ostringstream msg; - msg << "cannot rename " << from << " to " << to; - perror(msg.str().c_str()); - return true; - } } tgba_explicit_number* @@ -949,50 +928,19 @@ namespace spot { trace << "dtba_sat_synthetize(..., states = " << target_state_number << ", state_based = " << state_based << ")\n"; - dict* current = 0; - temporary_file* cnf = 0; - temporary_file* out = 0; + dict d; + d.cand_size = target_state_number; - current = new dict; - current->cand_size = target_state_number; + satsolver solver; + satsolver::solution_pair solution; - try - { - cnf = create_tmpfile("dtba-sat-", ".cnf"); - std::fstream cnfs(cnf->name(), - std::ios_base::trunc | std::ios_base::out); - cnfs.exceptions(std::ifstream::failbit | std::ifstream::badbit); - 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); - - sat_solution solution = satsolver_get_solution(out->name()); + dtba_to_sat(solver(), a, d, state_based); + solution = solver.get_solution(); tgba_explicit_number* res = 0; - if (!solution.empty()) - res = sat_build(solution, *current, a, state_based); + if (!solution.second.empty()) + res = sat_build(solution.second, d, a, state_based); - delete current; - - if (DEBUG) - { - xrename(out->name(), "dtba-sat.out"); - xrename(cnf->name(), "dtba-sat.cnf"); - } - - delete out; - delete cnf; trace << "dtba_sat_synthetize(...) = " << res << "\n"; return res; } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 944f1f2a5..2be755505 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include -#include #include #include "dtgbasat.hh" #include "reachiter.hh" @@ -29,26 +28,17 @@ #include "ltlast/constant.hh" #include "stats.hh" #include "ltlenv/defaultenv.hh" -#include "misc/tmpfile.hh" #include "misc/satsolver.hh" #include "isweakscc.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 -// directory. (The files dtgba-sat.cnf and dtgba-sat.out contain the -// input and output for the last successful minimization attempted, or -// for the only failed attempt if the minimization failed.) +// If you set the SPOT_TMPKEEP environment variable the temporary +// file used to communicate with the sat solver will be left in +// the current directory. // -// Additionally, the CNF file will be output with a comment before -// each clause, and an additional output file (dtgba-sat.dbg) will be -// created with a list of all positive variables in the result and -// their meaning. -// -// Note that the code use unique temporary filenames, so it is safe to -// run several such minimizations in parallel. It only when DEBUG=1 -// that some of these files will be renamed to the above hard-coded -// names, possibly causing confusion if multiple minimizations are -// debugged in parallel and in the same directory. +// Additionally, if the following DEBUG macro is set to 1, the CNF +// file will be output with a comment before each clause, and an +// additional output file (dtgba-sat.dbg) will be created with a list +// of all positive variables in the result and their meaning. #define DEBUG 0 #if DEBUG @@ -851,8 +841,8 @@ namespace spot } static tgba_explicit_number* - sat_build(const sat_solution& solution, dict& satdict, const tgba* aut, - bool state_based) + sat_build(const satsolver::solution& solution, dict& satdict, + const tgba* aut, bool state_based) { bdd_dict* autdict = aut->get_dict(); tgba_explicit_number* a = new tgba_explicit_number(autdict); @@ -876,7 +866,7 @@ namespace spot dout << "--- transition variables ---\n"; std::map state_acc; std::set seen_trans; - for (sat_solution::const_iterator i = solution.begin(); + for (satsolver::solution::const_iterator i = solution.begin(); i != solution.end(); ++i) { int v = *i; @@ -950,17 +940,6 @@ namespace spot return a; } - - static bool - xrename(const char* from, const char* to) - { - if (!rename(from, to)) - return false; - std::ostringstream msg; - msg << "cannot rename " << from << " to " << to; - perror(msg.str().c_str()); - return true; - } } tgba_explicit_number* @@ -970,51 +949,21 @@ namespace spot trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number << ", states = " << target_state_number << ", state_based = " << state_based << ")\n"; - dict* current = 0; - temporary_file* cnf = 0; - temporary_file* out = 0; - current = new dict(a); - current->cand_size = target_state_number; - current->cand_nacc = target_acc_number; + dict d(a); + d.cand_size = target_state_number; + d.cand_nacc = target_acc_number; - try - { - cnf = create_tmpfile("dtgba-sat-", ".cnf"); - std::fstream cnfs(cnf->name(), - std::ios_base::trunc | std::ios_base::out); - cnfs.exceptions(std::ifstream::failbit | std::ifstream::badbit); - dtgba_to_sat(cnfs, a, *current, state_based); - cnfs.close(); - } - catch (...) - { - if (DEBUG) - xrename(cnf->name(), "dgtba-sat.cnf"); - delete current; - delete cnf; - throw; - } + satsolver solver; + satsolver::solution_pair solution; - out = create_tmpfile("dtgba-sat-", ".out"); - satsolver(cnf, out); - - sat_solution solution = satsolver_get_solution(out->name()); + dtgba_to_sat(solver(), a, d, state_based); + solution = solver.get_solution(); tgba_explicit_number* res = 0; - if (!solution.empty()) - res = sat_build(solution, *current, a, state_based); + if (!solution.second.empty()) + res = sat_build(solution.second, d, a, state_based); - delete current; - - if (DEBUG) - { - xrename(out->name(), "dtgba-sat.out"); - xrename(cnf->name(), "dtgba-sat.cnf"); - } - - delete out; - delete cnf; trace << "dtgba_sat_synthetize(...) = " << res << "\n"; return res; } diff --git a/src/tgbatest/readsat.cc b/src/tgbatest/readsat.cc index 61855f0ca..1395a94e5 100644 --- a/src/tgbatest/readsat.cc +++ b/src/tgbatest/readsat.cc @@ -21,8 +21,8 @@ int main() { - spot::sat_solution sol = spot::satsolver_get_solution("-"); - for (spot::sat_solution::const_iterator i = sol.begin(); + spot::satsolver::solution sol = spot::satsolver_get_solution("-"); + for (spot::satsolver::solution::const_iterator i = sol.begin(); i != sol.end(); ++i) std::cout << ' ' << *i; std::cout << '\n';