cprover
external_sat.h
Go to the documentation of this file.
1 
6 #ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
7 #define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
8 
9 #include "cnf_clause_list.h"
11 {
12 public:
13  explicit external_satt(message_handlert &message_handler, std::string cmd);
14 
15  bool has_set_assumptions() const override final
16  {
17  return false;
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 protected:
31  resultt do_prop_solve() override;
32  std::string solver_cmd;
33  void write_cnf_file(std::string);
34  std::string execute_solver(std::string);
35  resultt parse_result(std::string);
36 };
37 
38 #endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
cnf_clause_list.h
CNF Generation.
cnf_clause_list_assignmentt
Definition: cnf_clause_list.h:92
external_satt
Definition: external_sat.h:11
external_satt::write_cnf_file
void write_cnf_file(std::string)
Definition: external_sat.cpp:43
external_satt::solver_cmd
std::string solver_cmd
Definition: external_sat.h:32
external_satt::do_prop_solve
resultt do_prop_solve() override
Definition: external_sat.cpp:162
external_satt::external_satt
external_satt(message_handlert &message_handler, std::string cmd)
Definition: external_sat.cpp:23
external_satt::is_in_conflict
bool is_in_conflict(literalt) const override
Returns true if an assumption is in the final conflict.
Definition: external_sat.cpp:33
external_satt::has_set_assumptions
bool has_set_assumptions() const override final
Definition: external_sat.h:15
external_satt::solver_text
const std::string solver_text() override
Definition: external_sat.cpp:28
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
external_satt::has_is_in_conflict
bool has_is_in_conflict() const override final
Definition: external_sat.h:20
literalt
Definition: literal.h:26
external_satt::set_assignment
void set_assignment(literalt, bool) override
Definition: external_sat.cpp:38
external_satt::execute_solver
std::string execute_solver(std::string)
Definition: external_sat.cpp:57
external_satt::parse_result
resultt parse_result(std::string)
Definition: external_sat.cpp:67