26 return "External SAT solver";
56 out <<
literal.dimacs() <<
" 0\n";
87 log.
error() <<
"external SAT solver has provided an unexpected "
88 "response in results.\nUnexpected reponse: "
93 auto status =
parts[1];
95 if(status ==
"UNSATISFIABLE")
99 if(status ==
"SATISFIABLE")
103 if(status ==
"TIMEOUT")
116 assignments.erase(assignments.begin());
123 size_t index = std::labs(
as_long);
128 <<
" out of range of CBMC largest variable of "
138 <<
" caused an exception while processing"
154 log.
error() <<
"No assignment was found for literal: " << index
162 log.
error() <<
"external SAT solver has provided an unexpected response"
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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)