cprover
Loading...
Searching...
No Matches
external_sat.h
Go to the documentation of this file.
1
5
6#ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
7#define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
8
9#include "cnf_clause_list.h"
11{
12public:
13 explicit external_satt(message_handlert &message_handler, std::string cmd);
14
15 bool has_set_assumptions() const override final
16 {
17 return true;
18 }
19
20 bool has_is_in_conflict() const override final
21 {
22 return false;
23 }
24
25 const std::string solver_text() override;
26
27 bool is_in_conflict(literalt) const override;
28 void set_assignment(literalt, bool) override;
29
30 void set_assumptions(const bvt &_assumptions) override
31 {
32 assumptions = _assumptions;
33 }
34
35protected:
36 std::string solver_cmd;
38
39 resultt do_prop_solve() override;
40 void write_cnf_file(std::string);
41 std::string execute_solver(std::string);
42 resultt parse_result(std::string);
43};
44
45#endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
std::string execute_solver(std::string)
void set_assumptions(const bvt &_assumptions) override
resultt do_prop_solve() override
std::string solver_cmd
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
CNF Generation.
std::vector< literalt > bvt
Definition literal.h:201
resultt
The result of goto verifying.
Definition properties.h:45