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}
35void convert_assumptions(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
36{
37 dest.capacity(bv.size());
38
39 for(const auto &literal : bv)
40 {
41 if(!literal.is_true())
42 dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
43 }
44}
46template<typename T>
48{
49 if(a.is_true())
50 return tvt(true);
51 else if(a.is_false())
52 return tvt(false);
53
54 tvt result;
55
56 if(a.var_no()>=(unsigned)solver->model.size())
59 using Glucose::lbool;
60
61 if(solver->model[a.var_no()]==l_True)
62 result=tvt(true);
63 else if(solver->model[a.var_no()]==l_False)
64 result=tvt(false);
65 else
67
68 if(a.sign())
69 result=!result;
70
71 return result;
72}
73
74template<typename T>
76{
77 PRECONDITION(!a.is_constant());
78
79 try
80 {
81 add_variables();
82 solver->setPolarity(a.var_no(), value);
83 }
84 catch(Glucose::OutOfMemoryException)
85 {
86 log.error() << "SAT checker ran out of memory" << messaget::eom;
87 status = statust::ERROR;
88 throw std::bad_alloc();
89 }
90}
91
93{
94 return "Glucose Syrup without simplifier";
95}
96
98{
99 return "Glucose Syrup with simplifier";
100}
101
102template<typename T>
104{
105 while((unsigned)solver->nVars()<no_variables())
106 solver->newVar();
107}
108
109template<typename T>
111{
112 try
113 {
114 add_variables();
115
116 for(const auto &literal : bv)
117 {
118 if(literal.is_true())
119 return;
120 else if(!literal.is_false())
121 {
122 INVARIANT(
123 literal.var_no() < (unsigned)solver->nVars(),
124 "variable not added yet");
125 }
126 }
127
128 Glucose::vec<Glucose::Lit> c;
129
130 convert(bv, c);
131
132 // Note the underscore.
133 // Add a clause to the solver without making superflous internal copy.
134
135 solver->addClause_(c);
136
137 if(solver_hardness)
138 {
139 // To map clauses to lines of program code, track clause indices in the
140 // dimacs cnf output. Dimacs output is generated after processing
141 // clauses to remove duplicates and clauses that are trivially true.
142 // Here, a clause is checked to see if it can be thus eliminated. If
143 // not, add the clause index to list of clauses in
144 // solver_hardnesst::register_clause().
145 static size_t cnf_clause_index = 0;
146 bvt cnf;
147 bool clause_removed = process_clause(bv, cnf);
148
149 if(!clause_removed)
151
152 solver_hardness->register_clause(
154 }
155
156 clause_counter++;
157 }
158 catch(Glucose::OutOfMemoryException)
159 {
160 log.error() << "SAT checker ran out of memory" << messaget::eom;
161 status = statust::ERROR;
162 throw std::bad_alloc();
163 }
164}
165
166template <typename T>
168{
169 PRECONDITION(status != statust::ERROR);
170
171 // We start counting at 1, thus there is one variable fewer.
172 log.statistics() << (no_variables() - 1) << " variables, "
173 << solver->nClauses() << " clauses" << messaget::eom;
174
175 try
176 {
177 add_variables();
178
179 if(!solver->okay())
180 {
181 log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
182 << messaget::eom;
183 }
184 else
185 {
186 // if assumptions contains false, we need this to be UNSAT
187 bool has_false = false;
188
189 for(const auto &literal : assumptions)
190 {
191 if(literal.is_false())
192 has_false = true;
193 }
194
195 if(has_false)
196 {
197 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
198 << messaget::eom;
199 }
200 else
201 {
202 Glucose::vec<Glucose::Lit> solver_assumptions;
204
205 if(solver->solve(solver_assumptions))
206 {
207 log.status() << "SAT checker: instance is SATISFIABLE"
208 << messaget::eom;
209 status = statust::SAT;
210 return resultt::P_SATISFIABLE;
211 }
212 else
213 {
214 log.status() << "SAT checker: instance is UNSATISFIABLE"
215 << messaget::eom;
216 }
217 }
218 }
219
220 status = statust::UNSAT;
221 return resultt::P_UNSATISFIABLE;
222 }
223 catch(Glucose::OutOfMemoryException)
224 {
225 log.error() << "SAT checker ran out of memory" << messaget::eom;
226 status = statust::ERROR;
227 throw std::bad_alloc();
228 }
229}
230
231template<typename T>
233{
234 PRECONDITION(!a.is_constant());
235
236 try
237 {
238 unsigned v = a.var_no();
239 bool sign = a.sign();
240
241 // MiniSat2 kills the model in case of UNSAT
242 solver->model.growTo(v + 1);
243 value ^= sign;
244 solver->model[v] = Glucose::lbool(value);
245 }
246 catch(Glucose::OutOfMemoryException)
247 {
248 log.error() << "SAT checker ran out of memory" << messaget::eom;
249 status = statust::ERROR;
250 throw std::bad_alloc();
251 }
252}
253
254template <typename T>
256 message_handlert &message_handler)
257 : cnf_solvert(message_handler), solver(util_make_unique<T>())
258{
259}
260
261template <typename T>
263
264template<typename T>
266{
267 int v=a.var_no();
268
269 for(int i=0; i<solver->conflict.size(); i++)
270 if(var(solver->conflict[i])==v)
271 return true;
272
273 return false;
274}
275
278
280{
281 try
282 {
283 if(!a.is_constant())
284 {
286 solver->setFrozen(a.var_no(), true);
287 }
288 }
289 catch(Glucose::OutOfMemoryException)
290 {
291 log.error() << "SAT checker ran out of memory" << messaget::eom;
293 throw std::bad_alloc();
294 }
295}
296
298{
299 PRECONDITION(!a.is_constant());
300
301 return solver->isEliminated(a.var_no());
302}
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ait()
Definition ai.h:566
statust status
Definition cnf.h:87
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
resultt
Definition prop.h:101
messaget log
Definition prop.h:134
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 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)
tvt l_get(literalt a) const override
resultt do_prop_solve(const bvt &assumptions) override
void set_assignment(literalt a, bool value) override
std::string solver_text() const override
void set_frozen(literalt a) override
std::string solver_text() const 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)
void convert_assumptions(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423