Commit bd37625e authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE
Browse files

misc: Add 'SPOT_XCNF' environment variable

* spot/misc/satsolver.cc: Handle xcnf writing.
* spot/misc/satsolver.hh: Handle xcnf writing.
parent ef2355a5
...@@ -74,12 +74,30 @@ namespace spot ...@@ -74,12 +74,30 @@ namespace spot
// easy to check if psat_ was initialized or not. // easy to check if psat_ was initialized or not.
satsolver::satsolver() satsolver::satsolver()
: cnf_tmp_(nullptr), cnf_stream_(nullptr), nclauses_(0), nvars_(0), : cnf_tmp_(nullptr), cnf_stream_(nullptr), nclauses_(0), nvars_(0),
nassumptions_vars_(0), nsols_(0), psat_(nullptr) nassumptions_vars_(0), nsols_(0), psat_(nullptr), xcnf_tmp_(nullptr),
xcnf_stream_(nullptr), path_("")
{ {
if (cmd_.command_given()) // Check SPOT_XCNF env var.
static std::string path = []()
{
auto s = getenv("SPOT_XCNF");
return s ? s : "";
}();
if (!path.empty())
path_ = path;
bool satsolver_set = cmd_.command_given();
bool xcnf_set = xcnf_mode();
if (satsolver_set)
{ {
start(); start();
} }
else if (xcnf_set) // If !satsolver_set and xcnf_set.
{
throw std::runtime_error("XNCF generation requires an external SAT solver"
" to be defined with SPOT_SATSOLVER");
}
else else
{ {
psat_ = picosat_init(); psat_ = picosat_init();
...@@ -99,6 +117,21 @@ namespace spot ...@@ -99,6 +117,21 @@ namespace spot
delete cnf_tmp_; delete cnf_tmp_;
delete cnf_stream_; delete cnf_stream_;
} }
if (xcnf_mode())
{
xcnf_tmp_->close();
xcnf_stream_->close();
delete xcnf_tmp_;
delete xcnf_stream_;
}
}
bool
satsolver::xcnf_mode()
{
static bool res = !path_.empty();
return res;
} }
void satsolver::start() void satsolver::start()
...@@ -109,6 +142,15 @@ namespace spot ...@@ -109,6 +142,15 @@ namespace spot
// Add empty line for the header // Add empty line for the header
*cnf_stream_ << " \n"; *cnf_stream_ << " \n";
if (xcnf_mode()) // If xcnf mode.
{
xcnf_tmp_ = new std::ofstream(path_ + "/incr.tmp", std::ios_base::trunc);
xcnf_tmp_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
*xcnf_tmp_ << " \n+\n";
xcnf_stream_ = new std::ofstream(path_ + "/incr.xcnf", std::ios::trunc);
xcnf_stream_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
}
} }
// Must be called only when SPOT_SATSOLVER is given // Must be called only when SPOT_SATSOLVER is given
...@@ -118,6 +160,9 @@ namespace spot ...@@ -118,6 +160,9 @@ namespace spot
nclauses_ += 1; nclauses_ += 1;
if (nclauses_ < 0) if (nclauses_ < 0)
throw std::runtime_error(": too many SAT clauses (more than INT_MAX)."); throw std::runtime_error(": too many SAT clauses (more than INT_MAX).");
if (xcnf_mode())
*xcnf_tmp_ << '\n';
} }
void satsolver::adjust_nvars(int nvars) void satsolver::adjust_nvars(int nvars)
...@@ -156,6 +201,9 @@ namespace spot ...@@ -156,6 +201,9 @@ namespace spot
} }
else else
{ {
if (xcnf_mode())
*xcnf_tmp_ << v << ' ';
*cnf_stream_ << v << ' '; *cnf_stream_ << v << ' ';
if (!v) // ..., 0) if (!v) // ..., 0)
end_clause(); end_clause();
...@@ -174,6 +222,9 @@ namespace spot ...@@ -174,6 +222,9 @@ namespace spot
} }
else else
{ {
if (xcnf_mode())
*xcnf_tmp_ << v << ' ';
*cnf_stream_ << v << ' '; *cnf_stream_ << v << ' ';
if (!v) // 0 if (!v) // 0
end_clause(); end_clause();
...@@ -293,6 +344,30 @@ namespace spot ...@@ -293,6 +344,30 @@ namespace spot
p.second = satsolver_get_sol(output->name()); p.second = satsolver_get_sol(output->name());
delete output; delete output;
} }
if (xcnf_mode() && !p.second.empty())
{
// Update xcnf_tmp_ header
xcnf_tmp_->seekp(0);
*xcnf_tmp_ << "p cnf " << (get_nb_vars() + 1);
xcnf_tmp_->seekp(0, std::ios_base::end);
if (!*xcnf_tmp_)
throw std::runtime_error("Failed to update xcnf_tmp_ header");
// Copy xcnf_tmp_ into xcnf_stream_
xcnf_tmp_->close();
std::ifstream ifile(path_ + "/incr.tmp", std::ios::in);
*xcnf_stream_ << ifile.rdbuf();
*xcnf_stream_ << "X\n";
// Erase xcnf_tmp_ content
delete xcnf_tmp_;
xcnf_tmp_ = new std::ofstream(path_ + "/incr.tmp", std::ios_base::trunc);
xcnf_tmp_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
*xcnf_tmp_ << " \n";
*xcnf_tmp_ << "+\n";
}
return p; return p;
} }
......
...@@ -143,6 +143,10 @@ namespace spot ...@@ -143,6 +143,10 @@ namespace spot
satsolver::solution satsolver::solution
satsolver_get_sol(const char* filename); satsolver_get_sol(const char* filename);
/// \brief Check if <code>SPOT_XCNF</code> env var is set.
bool
xcnf_mode();
private: // variables private: // variables
/// \brief A satsolver_command. Check if SPOT_SATSOLVER is given. /// \brief A satsolver_command. Check if SPOT_SATSOLVER is given.
satsolver_command cmd_; satsolver_command cmd_;
...@@ -161,6 +165,12 @@ namespace spot ...@@ -161,6 +165,12 @@ namespace spot
/// \brief Picosat satsolver instance. /// \brief Picosat satsolver instance.
PicoSAT* psat_; PicoSAT* psat_;
// The next 2 pointers will be initialized if SPOT_XCNF env var
// is set. This recquires SPOT_SATSOLVER to be set as well.
std::ofstream* xcnf_tmp_;
std::ofstream* xcnf_stream_;
std::string path_;
}; };
/// \brief Extract the solution of a SAT solver output. /// \brief Extract the solution of a SAT solver output.
......
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