6#ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
7#define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::string execute_solver(std::string)
void set_assumptions(const bvt &_assumptions) override
resultt do_prop_solve() override
bool has_is_in_conflict() const override final
void set_assignment(literalt, bool) override
void write_cnf_file(std::string)
bool has_set_assumptions() const override final
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
std::vector< literalt > bvt
resultt
The result of goto verifying.