Go to the documentation of this file.
6 #ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
7 #define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
38 #endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
resultt
The result of goto verifying.
void write_cnf_file(std::string)
resultt do_prop_solve() override
external_satt(message_handlert &message_handler, std::string cmd)
bool is_in_conflict(literalt) const override
Returns true if an assumption is in the final conflict.
bool has_set_assumptions() const override final
const std::string solver_text() override
bool has_is_in_conflict() const override final
void set_assignment(literalt, bool) override
std::string execute_solver(std::string)
resultt parse_result(std::string)