28 return "External SAT solver";
44 std::ofstream out(cnf_file);
57 if(!literal.is_constant())
58 out << literal.dimacs() <<
" 0\n";
67 std::ostringstream response_ostream;
68 auto cmd_result =
run(
solver_cmd, {
"", cnf_file},
"", response_ostream,
"");
71 return response_ostream.str();
76 std::istringstream response_istream(solver_output);
79 std::vector<bool> assigned_variables(
no_variables(),
false);
82 while(getline(response_istream, line))
89 log.
error() <<
"external SAT solver has provided an unexpected "
90 "response in results.\nUnexpected reponse: "
95 auto status = parts[1];
97 if(status ==
"UNSATISFIABLE")
101 if(status ==
"SATISFIABLE")
105 if(status ==
"TIMEOUT")
118 assignments.erase(assignments.begin());
120 for(
auto &assignment_string : assignments)
124 signed long long as_long = std::stol(assignment_string);
125 size_t index = std::labs(as_long);
127 if(index >= number_of_variables)
129 log.
error() <<
"SAT assignment " << as_long
130 <<
" out of range of CBMC largest variable of "
135 assigned_variables[index] =
true;
139 log.
error() <<
"SAT assignment " << assignment_string
140 <<
" caused an exception while processing"
154 if(!assigned_variables[index])
156 log.
error() <<
"No assignment was found for literal: " << index
164 log.
error() <<
"external SAT solver has provided an unexpected response"
size_t no_clauses() const override
virtual size_t no_variables() const override
static void write_dimacs_clause(const bvt &, std::ostream &, bool break_lines)
std::string execute_solver(std::string)
external_satt(message_handlert &message_handler, std::string cmd)
resultt do_prop_solve() override
void set_assignment(literalt, bool) override
void write_cnf_file(std::string)
bool is_in_conflict(literalt) const override
Returns true if an assumption is in the final conflict.
resultt parse_result(std::string)
const std::string solver_text() override
mstreamt & status() const
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
literalt const_literal(bool value)
int run(const std::string &what, const std::vector< std::string > &argv)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)