cprover
satcheck_minisat2.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "satcheck_minisat2.h"
10 
11 #ifndef _MSC_VER
12 #include <inttypes.h>
13 #include <signal.h>
14 #include <unistd.h>
15 #endif
16 
17 #include <limits>
18 #include <stack>
19 
20 #include <util/invariant.h>
21 #include <util/threeval.h>
22 
23 #include <minisat/core/Solver.h>
24 #include <minisat/simp/SimpSolver.h>
25 
26 #ifndef HAVE_MINISAT2
27 #error "Expected HAVE_MINISAT2"
28 #endif
29 
30 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
31 {
33  bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
34  dest.capacity(static_cast<int>(bv.size()));
35 
36  forall_literals(it, bv)
37  if(!it->is_false())
38  dest.push(Minisat::mkLit(it->var_no(), it->sign()));
39 }
40 
41 template<typename T>
43 {
44  if(a.is_true())
45  return tvt(true);
46  else if(a.is_false())
47  return tvt(false);
48 
49  tvt result;
50 
51  if(a.var_no()>=(unsigned)solver->model.size())
52  return tvt::unknown();
53 
54  using Minisat::lbool;
55 
56  if(solver->model[a.var_no()]==l_True)
57  result=tvt(true);
58  else if(solver->model[a.var_no()]==l_False)
59  result=tvt(false);
60  else
61  return tvt::unknown();
62 
63  if(a.sign())
64  result=!result;
65 
66  return result;
67 }
68 
69 template<typename T>
71 {
73 
74  try
75  {
76  add_variables();
77  solver->setPolarity(a.var_no(), value);
78  }
79  catch(Minisat::OutOfMemoryException)
80  {
81  messaget::error() << "SAT checker ran out of memory" << eom;
82  status = statust::ERROR;
83  throw std::bad_alloc();
84  }
85 }
86 
87 template<typename T>
89 {
90  solver->interrupt();
91 }
92 
93 template<typename T>
95 {
96  solver->clearInterrupt();
97 }
98 
100 {
101  return "MiniSAT 2.2.1 without simplifier";
102 }
103 
105 {
106  return "MiniSAT 2.2.1 with simplifier";
107 }
108 
109 template<typename T>
111 {
112  while((unsigned)solver->nVars()<no_variables())
113  solver->newVar();
114 }
115 
116 template<typename T>
118 {
119  try
120  {
121  add_variables();
122 
123  forall_literals(it, bv)
124  {
125  if(it->is_true())
126  return;
127  else if(!it->is_false())
128  {
129  INVARIANT(
130  it->var_no() < (unsigned)solver->nVars(), "variable not added yet");
131  }
132  }
133 
134  Minisat::vec<Minisat::Lit> c;
135 
136  convert(bv, c);
137 
138  // Note the underscore.
139  // Add a clause to the solver without making superflous internal copy.
140 
141  solver->addClause_(c);
142 
143  clause_counter++;
144  }
145  catch(Minisat::OutOfMemoryException)
146  {
147  messaget::error() << "SAT checker ran out of memory" << eom;
148  status = statust::ERROR;
149  throw std::bad_alloc();
150  }
151 }
152 
153 #ifndef _WIN32
154 
155 static Minisat::Solver *solver_to_interrupt=nullptr;
156 
157 static void interrupt_solver(int signum)
158 {
159  solver_to_interrupt->interrupt();
160 }
161 
162 #endif
163 
164 template<typename T>
166 {
167  PRECONDITION(status != statust::ERROR);
168 
169  {
170  messaget::status() <<
171  (no_variables()-1) << " variables, " <<
172  solver->nClauses() << " clauses" << eom;
173  }
174 
175  try
176  {
177  add_variables();
178 
179  if(!solver->okay())
180  {
181  messaget::status() <<
182  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
183  }
184  else
185  {
186  // if assumptions contains false, we need this to be UNSAT
187  bool has_false=false;
188 
189  forall_literals(it, assumptions)
190  if(it->is_false())
191  has_false=true;
192 
193  if(has_false)
194  {
195  messaget::status() <<
196  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
197  }
198  else
199  {
200  Minisat::vec<Minisat::Lit> solver_assumptions;
201  convert(assumptions, solver_assumptions);
202 
203  using Minisat::lbool;
204 
205 #ifndef _WIN32
206 
207  void (*old_handler)(int)=SIG_ERR;
208 
209  if(time_limit_seconds!=0)
210  {
212  old_handler=signal(SIGALRM, interrupt_solver);
213  if(old_handler==SIG_ERR)
214  warning() << "Failed to set solver time limit" << eom;
215  else
216  alarm(time_limit_seconds);
217  }
218 
219  lbool solver_result=solver->solveLimited(solver_assumptions);
220 
221  if(old_handler!=SIG_ERR)
222  {
223  alarm(0);
224  signal(SIGALRM, old_handler);
226  }
227 
228 #else // _WIN32
229 
230  if(time_limit_seconds!=0)
231  {
232  messaget::warning() <<
233  "Time limit ignored (not supported on Win32 yet)" << messaget::eom;
234  }
235 
236  lbool solver_result=
237  solver->solve(solver_assumptions) ? l_True : l_False;
238 
239 #endif
240 
241  if(solver_result==l_True)
242  {
243  messaget::status() <<
244  "SAT checker: instance is SATISFIABLE" << eom;
245  CHECK_RETURN(solver->model.size()>0);
246  status=statust::SAT;
247  return resultt::P_SATISFIABLE;
248  }
249  else if(solver_result==l_False)
250  {
251  messaget::status() <<
252  "SAT checker: instance is UNSATISFIABLE" << eom;
253  }
254  else
255  {
256  messaget::status() <<
257  "SAT checker: timed out or other error" << eom;
258  status=statust::ERROR;
259  return resultt::P_ERROR;
260  }
261  }
262  }
263 
264  status=statust::UNSAT;
265  return resultt::P_UNSATISFIABLE;
266  }
267  catch(Minisat::OutOfMemoryException)
268  {
269  messaget::error() <<
270  "SAT checker ran out of memory" << eom;
271  status=statust::ERROR;
272  return resultt::P_ERROR;
273  }
274 }
275 
276 template<typename T>
278 {
280 
281  try
282  {
283  unsigned v = a.var_no();
284  bool sign = a.sign();
285 
286  // MiniSat2 kills the model in case of UNSAT
287  solver->model.growTo(v + 1);
288  value ^= sign;
289  solver->model[v] = Minisat::lbool(value);
290  }
291  catch(Minisat::OutOfMemoryException)
292  {
293  messaget::error() << "SAT checker ran out of memory" << eom;
294  status = statust::ERROR;
295  throw std::bad_alloc();
296  }
297 }
298 
299 template<typename T>
301  solver(_solver), time_limit_seconds(0)
302 {
303 }
304 
305 template<>
307 {
308  delete solver;
309 }
310 
311 template<>
313 {
314  delete solver;
315 }
316 
317 template<typename T>
319 {
320  int v=a.var_no();
321 
322  for(int i=0; i<solver->conflict.size(); i++)
323  if(var(solver->conflict[i])==v)
324  return true;
325 
326  return false;
327 }
328 
329 template<typename T>
331 {
332  assumptions=bv;
333 
334  forall_literals(it, assumptions)
335  if(it->is_true())
336  {
337  assumptions.clear();
338  break;
339  }
340 }
341 
343  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
344 {
345 }
346 
348  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
349 {
350 }
351 
353 {
354  try
355  {
356  if(!a.is_constant())
357  {
358  add_variables();
359  solver->setFrozen(a.var_no(), true);
360  }
361  }
362  catch(Minisat::OutOfMemoryException)
363  {
364  messaget::error() << "SAT checker ran out of memory" << eom;
366  throw std::bad_alloc();
367  }
368 }
369 
371 {
373 
374  return solver->isEliminated(a.var_no());
375 }
virtual void lcnf(const bvt &bv) final
static tvt unknown()
Definition: threeval.h:33
virtual const std::string solver_text()
void set_polarity(literalt a, bool value)
virtual const std::string solver_text() final
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual void set_frozen(literalt a) final
#define forall_literals(it, bv)
Definition: literal.h:202
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
virtual void set_assignment(literalt a, bool value) override
mstreamt & warning() const
Definition: message.h:307
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
static Minisat::Solver * solver_to_interrupt
int solver(std::istream &in)
virtual bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
mstreamt & error() const
Definition: message.h:302
var_not var_no() const
Definition: literal.h:82
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
resultt
Definition: prop.h:96
mstreamt & status() const
Definition: message.h:317
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
bool is_eliminated(literalt a) const
virtual ~satcheck_minisat2_baset()
virtual void set_assumptions(const bvt &_assumptions) override
virtual tvt l_get(literalt a) const final
static void interrupt_solver(int signum)
std::vector< literalt > bvt
Definition: literal.h:200
virtual resultt prop_solve() override
bool is_false() const
Definition: literal.h:160