cprover
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()));
35 for(const auto &literal : bv)
36 {
37 if(!literal.is_false())
38 dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
39 }
40}
42template<typename T>
44{
45 if(a.is_true())
46 return tvt(true);
47 else if(a.is_false())
48 return tvt(false);
49
50 tvt result;
52 if(a.var_no()>=(unsigned)solver->model.size())
53 return tvt::unknown();
55 using Minisat::lbool;
57 if(solver->model[a.var_no()]==l_True)
58 result=tvt(true);
59 else if(solver->model[a.var_no()]==l_False)
60 result=tvt(false);
61 else
62 return tvt::unknown();
63
64 if(a.sign())
65 result=!result;
66
67 return result;
68}
69
70template<typename T>
74
75 using Minisat::lbool;
76
77 try
78 {
79 add_variables();
80 solver->setPolarity(a.var_no(), value ? l_True : l_False);
81 }
82 catch(Minisat::OutOfMemoryException)
83 {
84 log.error() << "SAT checker ran out of memory" << messaget::eom;
85 status = statust::ERROR;
86 throw std::bad_alloc();
87 }
88}
89
90template<typename T>
92{
93 solver->interrupt();
94}
95
96template<typename T>
98{
99 solver->clearInterrupt();
100}
101
103{
104 return "MiniSAT 2.2.1 without simplifier";
105}
106
108{
109 return "MiniSAT 2.2.1 with simplifier";
110}
111
112template<typename T>
114{
115 while((unsigned)solver->nVars()<no_variables())
116 solver->newVar();
117}
118
119template<typename T>
121{
122 try
123 {
124 add_variables();
125
126 for(const auto &literal : bv)
127 {
128 if(literal.is_true())
129 return;
130 else if(!literal.is_false())
131 {
132 INVARIANT(
133 literal.var_no() < (unsigned)solver->nVars(),
134 "variable not added yet");
135 }
136 }
137
138 Minisat::vec<Minisat::Lit> c;
139
140 convert(bv, c);
141
142 // Note the underscore.
143 // Add a clause to the solver without making superflous internal copy.
144
145 solver->addClause_(c);
146
147 if(solver_hardness)
148 {
149 // To map clauses to lines of program code, track clause indices in the
150 // dimacs cnf output. Dimacs output is generated after processing
151 // clauses to remove duplicates and clauses that are trivially true.
152 // Here, a clause is checked to see if it can be thus eliminated. If
153 // not, add the clause index to list of clauses in
154 // solver_hardnesst::register_clause().
155 static size_t cnf_clause_index = 0;
156 bvt cnf;
157 bool clause_removed = process_clause(bv, cnf);
158
159 if(!clause_removed)
160 cnf_clause_index++;
161
162 solver_hardness->register_clause(
163 bv, cnf, cnf_clause_index, !clause_removed);
164 }
165
166 clause_counter++;
167 }
168 catch(const Minisat::OutOfMemoryException &)
169 {
170 log.error() << "SAT checker ran out of memory" << messaget::eom;
171 status = statust::ERROR;
172 throw std::bad_alloc();
173 }
174}
175
176#ifndef _WIN32
177
178static Minisat::Solver *solver_to_interrupt=nullptr;
179
180static void interrupt_solver(int signum)
181{
182 (void)signum; // unused parameter -- just removing the name trips up cpplint
183 solver_to_interrupt->interrupt();
184}
185
186#endif
187
188template <typename T>
190{
191 PRECONDITION(status != statust::ERROR);
192
193 log.statistics() << (no_variables() - 1) << " variables, "
194 << solver->nClauses() << " clauses" << messaget::eom;
195
196 try
197 {
198 add_variables();
199
200 if(!solver->okay())
201 {
202 log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
203 << messaget::eom;
204 status = statust::UNSAT;
205 return resultt::P_UNSATISFIABLE;
206 }
207
208 // if assumptions contains false, we need this to be UNSAT
209 for(const auto &assumption : assumptions)
210 {
211 if(assumption.is_false())
212 {
213 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
214 << messaget::eom;
215 status = statust::UNSAT;
216 return resultt::P_UNSATISFIABLE;
217 }
218 }
219
220 Minisat::vec<Minisat::Lit> solver_assumptions;
221 convert(assumptions, solver_assumptions);
222
223 using Minisat::lbool;
224
225#ifndef _WIN32
226
227 void (*old_handler)(int) = SIG_ERR;
228
229 if(time_limit_seconds != 0)
230 {
232 old_handler = signal(SIGALRM, interrupt_solver);
233 if(old_handler == SIG_ERR)
234 log.warning() << "Failed to set solver time limit" << messaget::eom;
235 else
236 alarm(time_limit_seconds);
237 }
238
239 lbool solver_result = solver->solveLimited(solver_assumptions);
240
241 if(old_handler != SIG_ERR)
242 {
243 alarm(0);
244 signal(SIGALRM, old_handler);
246 }
247
248#else // _WIN32
249
250 if(time_limit_seconds != 0)
251 {
252 log.warning() << "Time limit ignored (not supported on Win32 yet)"
253 << messaget::eom;
254 }
255
256 lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
257
258#endif
259
260 if(solver_result == l_True)
261 {
262 log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
263 CHECK_RETURN(solver->model.size() > 0);
264 status = statust::SAT;
265 return resultt::P_SATISFIABLE;
266 }
267
268 if(solver_result == l_False)
269 {
270 log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
271 status = statust::UNSAT;
272 return resultt::P_UNSATISFIABLE;
273 }
274
275 log.status() << "SAT checker: timed out or other error" << messaget::eom;
276 status = statust::ERROR;
277 return resultt::P_ERROR;
278 }
279 catch(const Minisat::OutOfMemoryException &)
280 {
281 log.error() << "SAT checker ran out of memory" << messaget::eom;
282 status=statust::ERROR;
283 return resultt::P_ERROR;
284 }
285}
286
287template<typename T>
289{
291
292 try
293 {
294 unsigned v = a.var_no();
295 bool sign = a.sign();
296
297 // MiniSat2 kills the model in case of UNSAT
298 solver->model.growTo(v + 1);
299 value ^= sign;
300 solver->model[v] = Minisat::lbool(value);
301 }
302 catch(const Minisat::OutOfMemoryException &)
303 {
304 log.error() << "SAT checker ran out of memory" << messaget::eom;
305 status = statust::ERROR;
306 throw std::bad_alloc();
307 }
308}
309
310template <typename T>
312 message_handlert &message_handler)
313 : cnf_solvert(message_handler),
315 time_limit_seconds(0)
316{
317}
318
319template <typename T>
321
322template<typename T>
324{
325 int v=a.var_no();
326
327 for(int i=0; i<solver->conflict.size(); i++)
328 if(var(solver->conflict[i])==v)
329 return true;
330
331 return false;
332}
333
334template<typename T>
336{
337 // We filter out 'true' assumptions which cause an assertion violation
338 // in Minisat2.
339 assumptions.clear();
340 for(const auto &assumption : bv)
341 {
342 if(!assumption.is_true())
343 {
344 assumptions.push_back(assumption);
345 }
346 }
347}
348
351
353{
354 try
355 {
356 if(!a.is_constant())
357 {
359 solver->setFrozen(a.var_no(), true);
360 }
361 }
362 catch(const Minisat::OutOfMemoryException &)
363 {
364 log.error() << "SAT checker ran out of memory" << messaget::eom;
366 throw std::bad_alloc();
367 }
368}
369
371{
373
374 return solver->isEliminated(a.var_no());
375}
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:97
messaget log
Definition: prop.h:128
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 ...
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
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
const std::string solver_text() override
void set_frozen(literalt a) override final
bool is_eliminated(literalt a) const
const std::string solver_text() 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
static Minisat::Solver * solver_to_interrupt
static void interrupt_solver(int signum)
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
int solver(std::istream &in)
#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