cprover
satcheck_minisat.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
12 
13 #include <vector>
14 
15 #include "cnf.h"
16 #include "resolution_proof.h"
17 
19 {
20 public:
22  {
23  }
24 
25  virtual ~satcheck_minisat1_baset();
26 
27  const std::string solver_text() override;
28  tvt l_get(literalt a) const override;
29 
30  void lcnf(const bvt &bv) final;
31 
32  void set_assignment(literalt a, bool value) override;
33 
34  // extra MiniSat feature: solve with assumptions
35  void set_assumptions(const bvt &_assumptions) override;
36 
37  // features
38  bool has_set_assumptions() const override
39  {
40  return true;
41  }
42  bool has_is_in_conflict() const override
43  {
44  return true;
45  }
46 
47  bool is_in_conflict(literalt l) const override;
48 
49 protected:
50  resultt do_prop_solve() override;
51 
52  // NOLINTNEXTLINE(readability/identifiers)
53  class Solver *solver;
54  void add_variables();
57 };
58 
60 {
61 public:
63 };
64 
66 {
67 public:
70 
71  const std::string solver_text() override;
73  // void set_partition_id(unsigned p_id);
74 
75 protected:
76  // NOLINTNEXTLINE(readability/identifiers)
77  class Proof *proof;
79 };
80 
82 {
83 public:
86 
87  const std::string solver_text() override;
88 
89  bool has_in_core() const
90  {
91  return true;
92  }
93 
94  bool is_in_core(literalt l) const
95  {
96  PRECONDITION(l.var_no() < in_core.size());
97  return in_core[l.var_no()];
98  }
99 
100 protected:
101  std::vector<bool> in_core;
102 
103  resultt do_prop_solve() override;
104 };
105 #endif // CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
var_not var_no() const
Definition: literal.h:83
resultt
Definition: prop.h:99
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
bool has_set_assumptions() const override
resultt do_prop_solve() override
bool is_in_conflict(literalt l) const override
Returns true if an assumption is in the final conflict.
void lcnf(const bvt &bv) final
bool has_is_in_conflict() const override
tvt l_get(literalt a) const override
void set_assumptions(const bvt &_assumptions) override
resultt do_prop_solve() override
std::vector< bool > in_core
const std::string solver_text() override
bool is_in_core(literalt l) const
const std::string solver_text() override
class minisat_prooft * minisat_proof
simple_prooft & get_resolution_proof()
Definition: threeval.h:20
CNF Generation, via Tseitin.
std::vector< literalt > bvt
Definition: literal.h:201
resultt
The result of goto verifying.
Definition: properties.h:44
#define PRECONDITION(CONDITION)
Definition: invariant.h:464