30 return "External SAT solver";
46 std::ofstream out(cnf_file);
60 std::ostringstream response_ostream;
61 auto cmd_result =
run(
solver_cmd, {
"", cnf_file},
"", response_ostream,
"");
64 return response_ostream.str();
69 std::istringstream response_istream(solver_output);
72 std::vector<bool> assigned_variables(
no_variables(),
false);
75 while(getline(response_istream, line))
82 log.
error() <<
"external SAT solver has provided an unexpected "
83 "response in results.\nUnexpected reponse: "
88 auto status = parts[1];
90 if(status ==
"UNSATISFIABLE")
94 if(status ==
"SATISFIABLE")
98 if(status ==
"TIMEOUT")
111 assignments.erase(assignments.begin());
113 for(
auto &assignment_string : assignments)
117 signed long long as_long = std::stol(assignment_string);
118 size_t index = std::labs(as_long);
120 if(index >= number_of_variables)
122 log.
error() <<
"SAT assignment " << as_long
123 <<
" out of range of CBMC largest variable of "
128 assigned_variables[index] =
true;
132 log.
error() <<
"SAT assignment " << assignment_string
133 <<
" caused an exception while processing"
147 if(!assigned_variables[index])
149 log.
error() <<
"No assignment was found for literal: " << index
157 log.
error() <<
"external SAT solver has provided an unexpected response"