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"