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  virtual const std::string solver_text() override;
28  virtual resultt prop_solve() override;
29  virtual tvt l_get(literalt a) const override;
30 
31  virtual void lcnf(const bvt &bv) final;
32 
33  virtual void set_assignment(literalt a, bool value) override;
34 
35  // extra MiniSat feature: solve with assumptions
36  virtual void set_assumptions(const bvt &_assumptions) override;
37 
38  // features
39  virtual bool has_set_assumptions() const override { return true; }
40  virtual bool has_is_in_conflict() const override { return true; }
41 
42  virtual bool is_in_conflict(literalt l) const override;
43 
44 protected:
45  // NOLINTNEXTLINE(readability/identifiers)
46  class Solver *solver;
47  void add_variables();
50 };
51 
53 {
54 public:
56 };
57 
59 {
60 public:
63 
64  virtual const std::string solver_text() override;
66  // void set_partition_id(unsigned p_id);
67 
68 protected:
69  // NOLINTNEXTLINE(readability/identifiers)
70  class Proof *proof;
72 };
73 
75 {
76 public:
79 
80  virtual const std::string solver_text() override;
81  virtual resultt prop_solve() override;
82 
83  virtual bool has_in_core() const { return true; }
84 
85  virtual bool is_in_core(literalt l) const
86  {
87  assert(l.var_no()<in_core.size());
88  return in_core[l.var_no()];
89  }
90 
91 protected:
92  std::vector<bool> in_core;
93 };
94 #endif // CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
CNF Generation, via Tseitin.
virtual void lcnf(const bvt &bv) final
class minisat_prooft * minisat_proof
virtual resultt prop_solve() override
virtual tvt l_get(literalt a) const override
Definition: threeval.h:19
virtual void set_assumptions(const bvt &_assumptions) override
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
simple_prooft & get_resolution_proof()
virtual bool is_in_core(literalt l) const
std::vector< bool > in_core
virtual const std::string solver_text() override
virtual resultt prop_solve() override
virtual bool has_is_in_conflict() const override
virtual void set_assignment(literalt a, bool value) override
virtual const std::string solver_text() override
virtual bool has_in_core() const
std::vector< literalt > bvt
Definition: literal.h:197
virtual bool is_in_conflict(literalt l) const override
virtual bool has_set_assumptions() const override
virtual const std::string solver_text() override