cprover
Loading...
Searching...
No Matches
satcheck_minisat.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
20public:
22 {
23 }
24
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
49protected:
50 resultt do_prop_solve() override;
51
52 // NOLINTNEXTLINE(readability/identifiers)
53 class Solver *solver;
54 void add_variables();
57};
58
60{
61public:
63};
64
66{
67public:
70
71 const std::string solver_text() override;
73 // void set_partition_id(unsigned p_id);
74
75protected:
76 // NOLINTNEXTLINE(readability/identifiers)
77 class Proof *proof;
79};
80
82{
83public:
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
100protected:
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
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:45
#define PRECONDITION(CONDITION)
Definition invariant.h:463