Commit 9c98975c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

sat: factor the creation of temporary files

* src/misc/satsolver.hh, src/misc/satsolver.cc: Present
the SAT solver as an object with a stream interface, to
prepare for a better implementation.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc:
Adjust to the new interface, removing all the handling
of temporary files.
* src/tgbatest/readsat.cc: Adjust.
parent 1853bdd5
...@@ -83,18 +83,10 @@ namespace spot ...@@ -83,18 +83,10 @@ namespace spot
}; };
} }
int satsolver(printable* input, printable* output) satsolver::solution
{
// 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_get_solution(const char* filename) satsolver_get_solution(const char* filename)
{ {
sat_solution sol; satsolver::solution sol;
std::istream* in; std::istream* in;
if (filename[0] == '-' && filename[1] == 0) if (filename[0] == '-' && filename[1] == 0)
in = &std::cin; in = &std::cin;
...@@ -130,4 +122,47 @@ namespace spot ...@@ -130,4 +122,47 @@ namespace spot
return sol; 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;
}
} }
...@@ -21,8 +21,10 @@ ...@@ -21,8 +21,10 @@
#define SPOT_MISC_SATSOLVER_HH #define SPOT_MISC_SATSOLVER_HH
#include "common.hh" #include "common.hh"
#include "tmpfile.hh"
#include <vector> #include <vector>
#include <stdexcept> #include <stdexcept>
#include <iosfwd>
namespace spot namespace spot
{ {
...@@ -65,29 +67,37 @@ 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, /// Call start() to create some temporary file, then send DIMACs
/// and sending output in file \a output. /// text to the stream returned by operator(), and finally call
/// get_solution().
/// ///
/// These two arguments are instance of printable, as /// The satsolver called can be configured via the
/// they will be evaluated in a %-escaped string such as /// <code>SPOT_SATSOLVER</code> environment variable. It
/// "satsolver %I >%O" /// defaults to
/// This command can be overridden using the /// "satsolver -verb=0 %I >%O"
/// <code>SPOT_SATSOLVER</code> environment variable. /// where %I and %O are replaced by input and output files.
/// class SPOT_API satsolver
/// Note that temporary_file instances implement the {
/// printable interface. public:
SPOT_API int satsolver();
satsolver(printable* input, printable* output); ~satsolver();
void start();
std::ostream& operator()();
typedef std::vector<int> sat_solution; typedef std::vector<int> solution;
typedef std::pair<int, solution> solution_pair;
solution_pair get_solution();
private:
temporary_file* cnf_tmp_;
std::ostream* cnf_stream_;
};
/// \brief Extract the solution of a SAT solver output. /// \brief Extract the solution of a SAT solver output.
SPOT_API sat_solution SPOT_API satsolver::solution
satsolver_get_solution(const char* filename); satsolver_get_solution(const char* filename);
} }
#endif // SPOT_MISC_SATSOLVER_HH #endif // SPOT_MISC_SATSOLVER_HH
...@@ -18,7 +18,6 @@ ...@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream> #include <iostream>
#include <fstream>
#include <sstream> #include <sstream>
#include "dtbasat.hh" #include "dtbasat.hh"
#include "reachiter.hh" #include "reachiter.hh"
...@@ -29,25 +28,16 @@ ...@@ -29,25 +28,16 @@
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "stats.hh" #include "stats.hh"
#include "misc/tmpfile.hh"
#include "misc/satsolver.hh" #include "misc/satsolver.hh"
// If the following DEBUG macro is set to 1, the temporary files used // If you set the SPOT_TMPKEEP environment variable the temporary
// to communicate with the SAT-solver will be left in the current // file used to communicate with the sat solver will be left in
// directory. (The files dtba-sat.cnf and dtba-sat.out contain the // the current directory.
// input and output for the last successful minimization attempted, or
// for the only failed attempt if the minimization failed.)
// //
// Additionally, the CNF file will be output with a comment before // Additionally, if the following DEBUG macro is set to 1, the CNF
// each clause, and an additional output file (dtba-sat.dbg) will be // file will be output with a comment before each clause, and an
// created with a list of all positive variables in the result and // additional output file (dtba-sat.dbg) will be created with a list
// their meaning. // 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.
#define DEBUG 0 #define DEBUG 0
#if DEBUG #if DEBUG
...@@ -820,8 +810,8 @@ namespace spot ...@@ -820,8 +810,8 @@ namespace spot
} }
static tgba_explicit_number* static tgba_explicit_number*
sat_build(const sat_solution& solution, dict& satdict, const tgba* aut, sat_build(const satsolver::solution& solution, dict& satdict,
bool state_based) const tgba* aut, bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); bdd_dict* autdict = aut->get_dict();
tgba_explicit_number* a = new tgba_explicit_number(autdict); tgba_explicit_number* a = new tgba_explicit_number(autdict);
...@@ -847,7 +837,7 @@ namespace spot ...@@ -847,7 +837,7 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::set<int> acc_states; std::set<int> acc_states;
std::set<src_cond> seen_trans; std::set<src_cond> seen_trans;
for (sat_solution::const_iterator i = solution.begin(); for (satsolver::solution::const_iterator i = solution.begin();
i != solution.end(); ++i) i != solution.end(); ++i)
{ {
int v = *i; int v = *i;
...@@ -930,17 +920,6 @@ namespace spot ...@@ -930,17 +920,6 @@ namespace spot
a->merge_transitions(); a->merge_transitions();
return a; 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* tgba_explicit_number*
...@@ -949,50 +928,19 @@ namespace spot ...@@ -949,50 +928,19 @@ namespace spot
{ {
trace << "dtba_sat_synthetize(..., states = " << target_state_number trace << "dtba_sat_synthetize(..., states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", state_based = " << state_based << ")\n";
dict* current = 0; dict d;
temporary_file* cnf = 0; d.cand_size = target_state_number;
temporary_file* out = 0;
current = new dict; satsolver solver;
current->cand_size = target_state_number; satsolver::solution_pair solution;
try dtba_to_sat(solver(), a, d, state_based);
{ solution = solver.get_solution();
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());
tgba_explicit_number* res = 0; tgba_explicit_number* res = 0;
if (!solution.empty()) if (!solution.second.empty())
res = sat_build(solution, *current, a, state_based); 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"; trace << "dtba_sat_synthetize(...) = " << res << "\n";
return res; return res;
} }
......
...@@ -18,7 +18,6 @@ ...@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream> #include <iostream>
#include <fstream>
#include <sstream> #include <sstream>
#include "dtgbasat.hh" #include "dtgbasat.hh"
#include "reachiter.hh" #include "reachiter.hh"
...@@ -29,26 +28,17 @@ ...@@ -29,26 +28,17 @@
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "stats.hh" #include "stats.hh"
#include "ltlenv/defaultenv.hh" #include "ltlenv/defaultenv.hh"
#include "misc/tmpfile.hh"
#include "misc/satsolver.hh" #include "misc/satsolver.hh"
#include "isweakscc.hh" #include "isweakscc.hh"
// If the following DEBUG macro is set to 1, the temporary files used // If you set the SPOT_TMPKEEP environment variable the temporary
// to communicate with the SAT-solver will be left in the current // file used to communicate with the sat solver will be left in
// directory. (The files dtgba-sat.cnf and dtgba-sat.out contain the // the current directory.
// input and output for the last successful minimization attempted, or
// for the only failed attempt if the minimization failed.)
// //
// Additionally, the CNF file will be output with a comment before // Additionally, if the following DEBUG macro is set to 1, the CNF
// each clause, and an additional output file (dtgba-sat.dbg) will be // file will be output with a comment before each clause, and an
// created with a list of all positive variables in the result and // additional output file (dtgba-sat.dbg) will be created with a list
// their meaning. // 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.
#define DEBUG 0 #define DEBUG 0
#if DEBUG #if DEBUG
...@@ -851,8 +841,8 @@ namespace spot ...@@ -851,8 +841,8 @@ namespace spot
} }
static tgba_explicit_number* static tgba_explicit_number*
sat_build(const sat_solution& solution, dict& satdict, const tgba* aut, sat_build(const satsolver::solution& solution, dict& satdict,
bool state_based) const tgba* aut, bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); bdd_dict* autdict = aut->get_dict();
tgba_explicit_number* a = new tgba_explicit_number(autdict); tgba_explicit_number* a = new tgba_explicit_number(autdict);
...@@ -876,7 +866,7 @@ namespace spot ...@@ -876,7 +866,7 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::map<int, bdd> state_acc; std::map<int, bdd> state_acc;
std::set<src_cond> seen_trans; std::set<src_cond> seen_trans;
for (sat_solution::const_iterator i = solution.begin(); for (satsolver::solution::const_iterator i = solution.begin();
i != solution.end(); ++i) i != solution.end(); ++i)
{ {
int v = *i; int v = *i;
...@@ -950,17 +940,6 @@ namespace spot ...@@ -950,17 +940,6 @@ namespace spot
return a; 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* tgba_explicit_number*
...@@ -970,51 +949,21 @@ namespace spot ...@@ -970,51 +949,21 @@ namespace spot
trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number
<< ", states = " << target_state_number << ", states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", 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;
try dict d(a);
{ d.cand_size = target_state_number;
cnf = create_tmpfile("dtgba-sat-", ".cnf"); d.cand_nacc = target_acc_number;
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;
}
out = create_tmpfile("dtgba-sat-", ".out"); satsolver solver;
satsolver(cnf, out); satsolver::solution_pair solution;
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; tgba_explicit_number* res = 0;
if (!solution.empty()) if (!solution.second.empty())
res = sat_build(solution, *current, a, state_based); 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"; trace << "dtgba_sat_synthetize(...) = " << res << "\n";
return res; return res;
} }
......
...@@ -21,8 +21,8 @@ ...@@ -21,8 +21,8 @@
int main() int main()
{ {
spot::sat_solution sol = spot::satsolver_get_solution("-"); spot::satsolver::solution sol = spot::satsolver_get_solution("-");
for (spot::sat_solution::const_iterator i = sol.begin(); for (spot::satsolver::solution::const_iterator i = sol.begin();
i != sol.end(); ++i) i != sol.end(); ++i)
std::cout << ' ' << *i; std::cout << ' ' << *i;
std::cout << '\n'; std::cout << '\n';
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment