cprover
Loading...
Searching...
No Matches
satcheck_glucose.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "satcheck_glucose.h"
10
11#include <stack>
12
13#include <util/invariant.h>
14#include <util/make_unique.h>
15#include <util/threeval.h>
16
17#include <core/Solver.h>
18#include <simp/SimpSolver.h>
19
20#ifndef HAVE_GLUCOSE
21#error "Expected HAVE_GLUCOSE"
22#endif
23
24void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
25{
26 dest.capacity(bv.size());
27
28 for(const auto &literal : bv)
29 {
30 if(!literal.is_false())
31 dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
32 }
33}
35template<typename T>
37{
38 if(a.is_true())
39 return tvt(true);
40 else if(a.is_false())
41 return tvt(false);
43 tvt result;
44
45 if(a.var_no()>=(unsigned)solver->model.size())
47
48 using Glucose::lbool;
49
50 if(solver->model[a.var_no()]==l_True)
51 result=tvt(true);
52 else if(solver->model[a.var_no()]==l_False)
53 result=tvt(false);
54 else
56
57 if(a.sign())
58 result=!result;
59
60 return result;
62
63template<typename T>
67
68 try
69 {
70 add_variables();
71 solver->setPolarity(a.var_no(), value);
72 }
73 catch(Glucose::OutOfMemoryException)
74 {
75 log.error() << "SAT checker ran out of memory" << messaget::eom;
76 status = statust::ERROR;
77 throw std::bad_alloc();
78 }
79}
80
82{
83 return "Glucose Syrup without simplifier";
84}
85
87{
88 return "Glucose Syrup with simplifier";
89}
90
91template<typename T>
93{
94 while((unsigned)solver->nVars()<no_variables())
95 solver->newVar();
96}
97
98template<typename T>
100{
101 try
102 {
103 add_variables();
104
105 for(const auto &literal : bv)
106 {
107 if(literal.is_true())
108 return;
109 else if(!literal.is_false())
110 {
111 INVARIANT(
112 literal.var_no() < (unsigned)solver->nVars(),
113 "variable not added yet");
114 }
115 }
116
117 Glucose::vec<Glucose::Lit> c;
118
119 convert(bv, c);
120
121 // Note the underscore.
122 // Add a clause to the solver without making superflous internal copy.
123
124 solver->addClause_(c);
125
126 if(solver_hardness)
127 {
128 // To map clauses to lines of program code, track clause indices in the
129 // dimacs cnf output. Dimacs output is generated after processing
130 // clauses to remove duplicates and clauses that are trivially true.
131 // Here, a clause is checked to see if it can be thus eliminated. If
132 // not, add the clause index to list of clauses in
133 // solver_hardnesst::register_clause().
134 static size_t cnf_clause_index = 0;
135 bvt cnf;
136 bool clause_removed = process_clause(bv, cnf);
137
138 if(!clause_removed)
139 cnf_clause_index++;
140
141 solver_hardness->register_clause(
142 bv, cnf, cnf_clause_index, !clause_removed);
143 }
144
145 clause_counter++;
146 }
147 catch(Glucose::OutOfMemoryException)
148 {
149 log.error() << "SAT checker ran out of memory" << messaget::eom;
150 status = statust::ERROR;
151 throw std::bad_alloc();
152 }
153}
154
155template <typename T>
157{
158 PRECONDITION(status != statust::ERROR);
159
160 // We start counting at 1, thus there is one variable fewer.
161 log.statistics() << (no_variables() - 1) << " variables, "
162 << solver->nClauses() << " clauses" << messaget::eom;
163
164 try
165 {
166 add_variables();
167
168 if(!solver->okay())
169 {
170 log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
171 << messaget::eom;
172 }
173 else
174 {
175 // if assumptions contains false, we need this to be UNSAT
176 bool has_false = false;
177
178 for(const auto &literal : assumptions)
179 {
180 if(literal.is_false())
181 has_false = true;
182 }
183
184 if(has_false)
185 {
186 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
187 << messaget::eom;
188 }
189 else
190 {
191 Glucose::vec<Glucose::Lit> solver_assumptions;
192 convert(assumptions, solver_assumptions);
193
194 if(solver->solve(solver_assumptions))
195 {
196 log.status() << "SAT checker: instance is SATISFIABLE"
197 << messaget::eom;
198 status = statust::SAT;
199 return resultt::P_SATISFIABLE;
200 }
201 else
202 {
203 log.status() << "SAT checker: instance is UNSATISFIABLE"
204 << messaget::eom;
205 }
206 }
207 }
208
209 status = statust::UNSAT;
210 return resultt::P_UNSATISFIABLE;
211 }
212 catch(Glucose::OutOfMemoryException)
213 {
214 log.error() << "SAT checker ran out of memory" << messaget::eom;
215 status = statust::ERROR;
216 throw std::bad_alloc();
217 }
218}
219
220template<typename T>
222{
224
225 try
226 {
227 unsigned v = a.var_no();
228 bool sign = a.sign();
229
230 // MiniSat2 kills the model in case of UNSAT
231 solver->model.growTo(v + 1);
232 value ^= sign;
233 solver->model[v] = Glucose::lbool(value);
234 }
235 catch(Glucose::OutOfMemoryException)
236 {
237 log.error() << "SAT checker ran out of memory" << messaget::eom;
238 status = statust::ERROR;
239 throw std::bad_alloc();
240 }
241}
242
243template <typename T>
245 message_handlert &message_handler)
246 : cnf_solvert(message_handler), solver(util_make_unique<T>())
247{
248}
249
250template <typename T>
252
253template<typename T>
255{
256 int v=a.var_no();
257
258 for(int i=0; i<solver->conflict.size(); i++)
259 if(var(solver->conflict[i])==v)
260 return true;
261
262 return false;
263}
264
265template<typename T>
267{
268 assumptions=bv;
269
270 for(const auto &literal : assumptions)
271 {
272 INVARIANT(
273 !literal.is_constant(), "assumption literals must not be constant");
274 }
275}
276
279
281{
282 try
283 {
284 if(!a.is_constant())
285 {
287 solver->setFrozen(a.var_no(), true);
288 }
289 }
290 catch(Glucose::OutOfMemoryException)
291 {
292 log.error() << "SAT checker ran out of memory" << messaget::eom;
294 throw std::bad_alloc();
295 }
296}
297
299{
301
302 return solver->isEliminated(a.var_no());
303}
statust status
Definition: cnf.h:87
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
bool is_constant() const
Definition: literal.h:166
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
resultt
Definition: prop.h:98
messaget log
Definition: prop.h:129
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
void lcnf(const bvt &bv) override
std::unique_ptr< Glucose::SimpSolver > solver
void set_polarity(literalt a, bool value)
satcheck_glucose_baset(message_handlert &message_handler)
resultt do_prop_solve() override
tvt l_get(literalt a) 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
std::vector< literalt > bvt
Definition: literal.h:201
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423