cprover
Loading...
Searching...
No Matches
satcheck_minisat2.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "satcheck_minisat2.h"
10
11#ifndef _WIN32
12# include <signal.h>
13# include <unistd.h>
14#endif
15
16#include <limits>
17
18#include <util/invariant.h>
19#include <util/make_unique.h>
20#include <util/threeval.h>
21
22#include <minisat/core/Solver.h>
23#include <minisat/simp/SimpSolver.h>
24
25#ifndef HAVE_MINISAT2
26#error "Expected HAVE_MINISAT2"
27#endif
28
29void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
30{
32 bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
33 dest.capacity(static_cast<int>(bv.size()));
34
35 for(const auto &literal : bv)
36 {
37 if(!literal.is_false())
38 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
39 }
40}
42void convert_assumptions(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
45 bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
46 dest.capacity(static_cast<int>(bv.size()));
48 for(const auto &literal : bv)
49 {
50 // when converting assumptions, ignore 'true'
51 if(!literal.is_true())
52 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
53 }
54}
56template<typename T>
58{
59 if(a.is_true())
60 return tvt(true);
61 else if(a.is_false())
62 return tvt(false);
63
64 tvt result;
65
66 if(a.var_no()>=(unsigned)solver->model.size())
67 return tvt::unknown();
68
69 using Minisat::lbool;
70
71 if(solver->model[a.var_no()]==l_True)
72 result=tvt(true);
73 else if(solver->model[a.var_no()]==l_False)
74 result=tvt(false);
75 else
76 return tvt::unknown();
77
78 if(a.sign())
79 result=!result;
80
81 return result;
82}
83
84template<typename T>
86{
87 PRECONDITION(!a.is_constant());
88
89 using Minisat::lbool;
90
91 try
92 {
93 add_variables();
94 solver->setPolarity(a.var_no(), value ? l_True : l_False);
95 }
96 catch(Minisat::OutOfMemoryException)
97 {
98 log.error() << "SAT checker ran out of memory" << messaget::eom;
99 status = statust::ERROR;
100 throw std::bad_alloc();
101 }
102}
103
104template<typename T>
106{
107 solver->interrupt();
108}
109
110template<typename T>
112{
113 solver->clearInterrupt();
114}
115
117{
118 return "MiniSAT 2.2.1 without simplifier";
119}
120
122{
123 return "MiniSAT 2.2.1 with simplifier";
124}
125
126template<typename T>
128{
129 while((unsigned)solver->nVars()<no_variables())
130 solver->newVar();
131}
132
133template<typename T>
135{
136 try
137 {
138 add_variables();
139
140 for(const auto &literal : bv)
141 {
142 if(literal.is_true())
143 return;
144 else if(!literal.is_false())
145 {
146 INVARIANT(
147 literal.var_no() < (unsigned)solver->nVars(),
148 "variable not added yet");
149 }
150 }
151
152 Minisat::vec<Minisat::Lit> c;
153
154 convert(bv, c);
155
156 // Note the underscore.
157 // Add a clause to the solver without making superflous internal copy.
158
159 solver->addClause_(c);
160
161 if(solver_hardness)
162 {
163 // To map clauses to lines of program code, track clause indices in the
164 // dimacs cnf output. Dimacs output is generated after processing
165 // clauses to remove duplicates and clauses that are trivially true.
166 // Here, a clause is checked to see if it can be thus eliminated. If
167 // not, add the clause index to list of clauses in
168 // solver_hardnesst::register_clause().
169 static size_t cnf_clause_index = 0;
170 bvt cnf;
171 bool clause_removed = process_clause(bv, cnf);
172
173 if(!clause_removed)
175
176 solver_hardness->register_clause(
178 }
179
180 clause_counter++;
181 }
182 catch(const Minisat::OutOfMemoryException &)
183 {
184 log.error() << "SAT checker ran out of memory" << messaget::eom;
185 status = statust::ERROR;
186 throw std::bad_alloc();
187 }
188}
189
190#ifndef _WIN32
191
192static Minisat::Solver *solver_to_interrupt=nullptr;
193
194static void interrupt_solver(int signum)
195{
196 (void)signum; // unused parameter -- just removing the name trips up cpplint
197 solver_to_interrupt->interrupt();
198}
199
200#endif
201
202template <typename T>
204{
205 PRECONDITION(status != statust::ERROR);
206
207 log.statistics() << (no_variables() - 1) << " variables, "
208 << solver->nClauses() << " clauses" << messaget::eom;
209
210 try
211 {
212 add_variables();
213
214 if(!solver->okay())
215 {
216 log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
217 << messaget::eom;
218 status = statust::UNSAT;
219 return resultt::P_UNSATISFIABLE;
220 }
221
222 // if assumptions contains false, we need this to be UNSAT
223 for(const auto &assumption : assumptions)
224 {
225 if(assumption.is_false())
226 {
227 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
228 << messaget::eom;
229 status = statust::UNSAT;
230 return resultt::P_UNSATISFIABLE;
231 }
232 }
233
234 Minisat::vec<Minisat::Lit> solver_assumptions;
236
237 using Minisat::lbool;
238
239#ifndef _WIN32
240
242
243 if(time_limit_seconds != 0)
244 {
247 if(old_handler == SIG_ERR)
248 log.warning() << "Failed to set solver time limit" << messaget::eom;
249 else
250 alarm(time_limit_seconds);
251 }
252
254
255 if(old_handler != SIG_ERR)
256 {
257 alarm(0);
260 }
261
262#else // _WIN32
263
264 if(time_limit_seconds != 0)
265 {
266 log.warning() << "Time limit ignored (not supported on Win32 yet)"
267 << messaget::eom;
268 }
269
271
272#endif
273
274 if(solver_result == l_True)
275 {
276 log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
277 CHECK_RETURN(solver->model.size() > 0);
278 status = statust::SAT;
279 return resultt::P_SATISFIABLE;
280 }
281
283 {
284 log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
285 status = statust::UNSAT;
286 return resultt::P_UNSATISFIABLE;
287 }
288
289 log.status() << "SAT checker: timed out or other error" << messaget::eom;
290 status = statust::ERROR;
291 return resultt::P_ERROR;
292 }
293 catch(const Minisat::OutOfMemoryException &)
294 {
295 log.error() << "SAT checker ran out of memory" << messaget::eom;
296 status=statust::ERROR;
297 return resultt::P_ERROR;
298 }
299}
300
301template<typename T>
303{
304 PRECONDITION(!a.is_constant());
305
306 try
307 {
308 unsigned v = a.var_no();
309 bool sign = a.sign();
310
311 // MiniSat2 kills the model in case of UNSAT
312 solver->model.growTo(v + 1);
313 value ^= sign;
314 solver->model[v] = Minisat::lbool(value);
315 }
316 catch(const Minisat::OutOfMemoryException &)
317 {
318 log.error() << "SAT checker ran out of memory" << messaget::eom;
319 status = statust::ERROR;
320 throw std::bad_alloc();
321 }
322}
323
324template <typename T>
326 message_handlert &message_handler)
327 : cnf_solvert(message_handler),
329 time_limit_seconds(0)
330{
331}
332
333template <typename T>
335
336template<typename T>
338{
339 int v=a.var_no();
340
341 for(int i=0; i<solver->conflict.size(); i++)
342 if(var(solver->conflict[i])==v)
343 return true;
344
345 return false;
346}
347
350
352{
353 try
354 {
355 if(!a.is_constant())
356 {
358 solver->setFrozen(a.var_no(), true);
359 }
360 }
361 catch(const Minisat::OutOfMemoryException &)
362 {
363 log.error() << "SAT checker ran out of memory" << messaget::eom;
365 throw std::bad_alloc();
366 }
367}
368
370{
371 PRECONDITION(!a.is_constant());
372
373 return solver->isEliminated(a.var_no());
374}
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.
std::unique_ptr< Minisat::SimpSolver > solver
~satcheck_minisat2_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
resultt do_prop_solve(const bvt &) override
satcheck_minisat2_baset(message_handlert &message_handler)
void set_polarity(literalt a, bool value)
void lcnf(const bvt &bv) override final
tvt l_get(literalt a) const override final
void set_assignment(literalt a, bool value) override
std::string solver_text() const override
void set_frozen(literalt a) override final
bool is_eliminated(literalt a) const
std::string solver_text() const override final
Definition threeval.h:20
static tvt unknown()
Definition threeval.h:33
std::vector< literalt > bvt
Definition literal.h:201
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
void convert_assumptions(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
static Minisat::Solver * solver_to_interrupt
static void interrupt_solver(int signum)
void convert_assumptions(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
void convert(const bvt &bv, Minisat::vec< Minisat::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 CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423