cprover
Loading...
Searching...
No Matches
satcheck_glucose.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_GLUCOSE_H
11#define CPROVER_SOLVERS_SAT_SATCHECK_GLUCOSE_H
12
13#include "cnf.h"
14
16
17#include <memory>
18
19// Select one: basic solver or with simplification.
20// Note that the solver with simplifier isn't really robust
21// when used incrementally, as variables may disappear
22// unless set to 'frozen'.
23
24namespace Glucose // NOLINT(readability/namespace)
25{
26class Solver; // NOLINT(readability/identifiers)
27class SimpSolver; // NOLINT(readability/identifiers)
28}
29
30template <typename T>
32{
33public:
34 explicit satcheck_glucose_baset(message_handlert &message_handler);
38
39 tvt l_get(literalt a) const override;
40
41 void lcnf(const bvt &bv) override;
42 void set_assignment(literalt a, bool value) override;
43
44 // extra MiniSat feature: solve with assumptions
45 void set_assumptions(const bvt &_assumptions) override;
46
47 // extra MiniSat feature: default branching decision
48 void set_polarity(literalt a, bool value);
49
50 bool is_in_conflict(literalt a) const override;
51 bool has_set_assumptions() const override
52 {
53 return true;
54 }
55 bool has_is_in_conflict() const override
56 {
57 return true;
58 }
59
60protected:
61 resultt do_prop_solve() override;
62
63 std::unique_ptr<T> solver;
64
65 void add_variables();
67};
68
70 public satcheck_glucose_baset<Glucose::Solver>
71{
72public:
74 const std::string solver_text() override;
75};
76
78 public satcheck_glucose_baset<Glucose::SimpSolver>
79{
80public:
81 using satcheck_glucose_baset<Glucose::SimpSolver>::satcheck_glucose_baset;
82 const std::string solver_text() override;
83 void set_frozen(literalt a) override;
84 bool is_eliminated(literalt a) const;
85};
86
87#endif // CPROVER_SOLVERS_SAT_SATCHECK_GLUCOSE_H
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
~satcheck_glucose_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
void set_assumptions(const bvt &_assumptions) override
bool has_set_assumptions() const override
void lcnf(const bvt &bv) override
std::unique_ptr< T > solver
void set_polarity(literalt a, bool value)
resultt do_prop_solve() override
tvt l_get(literalt a) const override
bool has_is_in_conflict() const override
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
const std::string solver_text() override
void set_frozen(literalt a) override
bool is_eliminated(literalt a) const
Definition: threeval.h:20
CNF Generation, via Tseitin.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition: literal.h:201
resultt
The result of goto verifying.
Definition: properties.h:45