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  PRECONDITION(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
satcheck_minisat1_baset
Definition: satcheck_minisat.h:18
satcheck_minisat1_baset::assumptions
bvt assumptions
Definition: satcheck_minisat.h:48
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
satcheck_minisat1_baset::l_get
virtual tvt l_get(literalt a) const override
Definition: satcheck_minisat.cpp:84
bvt
std::vector< literalt > bvt
Definition: literal.h:200
satcheck_minisat1_coret::satcheck_minisat1_coret
satcheck_minisat1_coret()
Definition: satcheck_minisat.cpp:250
satcheck_minisat1_baset::is_in_conflict
virtual bool is_in_conflict(literalt l) const override
Returns true if an assumption is in the final conflict.
Definition: satcheck_minisat.cpp:207
literalt::var_no
var_not var_no() const
Definition: literal.h:82
satcheck_minisat1_baset::add_variables
void add_variables()
Definition: satcheck_minisat.cpp:116
satcheck_minisat1_coret::prop_solve
virtual resultt prop_solve() override
Definition: satcheck_minisat.cpp:268
cnf_solvert
Definition: cnf.h:66
satcheck_minisat1_coret::is_in_core
virtual bool is_in_core(literalt l) const
Definition: satcheck_minisat.h:85
satcheck_minisat1_prooft::satcheck_minisat1_prooft
satcheck_minisat1_prooft()
Definition: satcheck_minisat.cpp:236
satcheck_minisat1_coret::solver_text
virtual const std::string solver_text() override
Definition: satcheck_minisat.cpp:283
satcheck_minisat1t::satcheck_minisat1t
satcheck_minisat1t()
Definition: satcheck_minisat.cpp:230
satcheck_minisat1_prooft
Definition: satcheck_minisat.h:58
satcheck_minisat1_baset::lcnf
virtual void lcnf(const bvt &bv) final
Definition: satcheck_minisat.cpp:122
satcheck_minisat1_baset::has_is_in_conflict
virtual bool has_is_in_conflict() const override
Definition: satcheck_minisat.h:40
satcheck_minisat1_coret::~satcheck_minisat1_coret
~satcheck_minisat1_coret()
Definition: satcheck_minisat.cpp:254
satcheck_minisat1t
Definition: satcheck_minisat.h:52
satcheck_minisat1_prooft::solver_text
virtual const std::string solver_text() override
Definition: satcheck_minisat.cpp:263
satcheck_minisat1_coret::has_in_core
virtual bool has_in_core() const
Definition: satcheck_minisat.h:83
satcheck_minisat1_prooft::proof
class Proof * proof
Definition: satcheck_minisat.h:70
propt::resultt
resultt
Definition: prop.h:96
satcheck_minisat1_baset::solver_text
virtual const std::string solver_text() override
Definition: satcheck_minisat.cpp:111
tvt
Definition: threeval.h:19
satcheck_minisat1_prooft::minisat_proof
class minisat_prooft * minisat_proof
Definition: satcheck_minisat.h:71
satcheck_minisat1_prooft::~satcheck_minisat1_prooft
~satcheck_minisat1_prooft()
Definition: satcheck_minisat.cpp:244
satcheck_minisat1_coret::in_core
std::vector< bool > in_core
Definition: satcheck_minisat.h:92
satcheck_minisat1_baset::empty_clause_added
bool empty_clause_added
Definition: satcheck_minisat.h:49
satcheck_minisat1_baset::has_set_assumptions
virtual bool has_set_assumptions() const override
Definition: satcheck_minisat.h:39
resolution_proof.h
satcheck_minisat1_baset::set_assumptions
virtual void set_assumptions(const bvt &_assumptions) override
Definition: satcheck_minisat.cpp:220
satcheck_minisat1_baset::prop_solve
virtual resultt prop_solve() override
Definition: satcheck_minisat.cpp:153
satcheck_minisat1_baset::solver
class Solver * solver
Definition: satcheck_minisat.h:46
literalt
Definition: literal.h:24
satcheck_minisat1_prooft::get_resolution_proof
simple_prooft & get_resolution_proof()
Definition: satcheck_minisat.cpp:288
resolution_prooft< clauset >
satcheck_minisat1_coret
Definition: satcheck_minisat.h:74
satcheck_minisat1_baset::set_assignment
virtual void set_assignment(literalt a, bool value) override
Definition: satcheck_minisat.cpp:198
satcheck_minisat1_baset::satcheck_minisat1_baset
satcheck_minisat1_baset()
Definition: satcheck_minisat.h:21
cnf.h
satcheck_minisat1_baset::~satcheck_minisat1_baset
virtual ~satcheck_minisat1_baset()
Definition: satcheck_minisat.cpp:258
minisat_prooft
Definition: satcheck_minisat.cpp:32