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(const 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  (void)signum; // unused parameter -- just removing the name trips up cpplint
160  solver_to_interrupt->interrupt();
161 }
162 
163 #endif
164 
165 template<typename T>
167 {
168  PRECONDITION(status != statust::ERROR);
169 
170  {
171  messaget::status() <<
172  (no_variables()-1) << " variables, " <<
173  solver->nClauses() << " clauses" << eom;
174  }
175 
176  try
177  {
178  add_variables();
179 
180  if(!solver->okay())
181  {
182  messaget::status() <<
183  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
184  }
185  else
186  {
187  // if assumptions contains false, we need this to be UNSAT
188  bool has_false=false;
189 
190  forall_literals(it, assumptions)
191  if(it->is_false())
192  has_false=true;
193 
194  if(has_false)
195  {
196  messaget::status() <<
197  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
198  }
199  else
200  {
201  Minisat::vec<Minisat::Lit> solver_assumptions;
202  convert(assumptions, solver_assumptions);
203 
204  using Minisat::lbool;
205 
206 #ifndef _WIN32
207 
208  void (*old_handler)(int)=SIG_ERR;
209 
210  if(time_limit_seconds!=0)
211  {
213  old_handler=signal(SIGALRM, interrupt_solver);
214  if(old_handler==SIG_ERR)
215  warning() << "Failed to set solver time limit" << eom;
216  else
217  alarm(time_limit_seconds);
218  }
219 
220  lbool solver_result=solver->solveLimited(solver_assumptions);
221 
222  if(old_handler!=SIG_ERR)
223  {
224  alarm(0);
225  signal(SIGALRM, old_handler);
227  }
228 
229 #else // _WIN32
230 
231  if(time_limit_seconds!=0)
232  {
233  messaget::warning() <<
234  "Time limit ignored (not supported on Win32 yet)" << messaget::eom;
235  }
236 
237  lbool solver_result=
238  solver->solve(solver_assumptions) ? l_True : l_False;
239 
240 #endif
241 
242  if(solver_result==l_True)
243  {
244  messaget::status() <<
245  "SAT checker: instance is SATISFIABLE" << eom;
246  CHECK_RETURN(solver->model.size()>0);
247  status=statust::SAT;
248  return resultt::P_SATISFIABLE;
249  }
250  else if(solver_result==l_False)
251  {
252  messaget::status() <<
253  "SAT checker: instance is UNSATISFIABLE" << eom;
254  }
255  else
256  {
257  messaget::status() <<
258  "SAT checker: timed out or other error" << eom;
259  status=statust::ERROR;
260  return resultt::P_ERROR;
261  }
262  }
263  }
264 
265  status=statust::UNSAT;
266  return resultt::P_UNSATISFIABLE;
267  }
268  catch(const Minisat::OutOfMemoryException &)
269  {
270  messaget::error() <<
271  "SAT checker ran out of memory" << eom;
272  status=statust::ERROR;
273  return resultt::P_ERROR;
274  }
275 }
276 
277 template<typename T>
279 {
281 
282  try
283  {
284  unsigned v = a.var_no();
285  bool sign = a.sign();
286 
287  // MiniSat2 kills the model in case of UNSAT
288  solver->model.growTo(v + 1);
289  value ^= sign;
290  solver->model[v] = Minisat::lbool(value);
291  }
292  catch(const Minisat::OutOfMemoryException &)
293  {
294  messaget::error() << "SAT checker ran out of memory" << eom;
295  status = statust::ERROR;
296  throw std::bad_alloc();
297  }
298 }
299 
300 template<typename T>
302  solver(_solver), time_limit_seconds(0)
303 {
304 }
305 
306 template<>
308 {
309  delete solver;
310 }
311 
312 template<>
314 {
315  delete solver;
316 }
317 
318 template<typename T>
320 {
321  int v=a.var_no();
322 
323  for(int i=0; i<solver->conflict.size(); i++)
324  if(var(solver->conflict[i])==v)
325  return true;
326 
327  return false;
328 }
329 
330 template<typename T>
332 {
333  assumptions=bv;
334 
335  forall_literals(it, assumptions)
336  if(it->is_true())
337  {
338  assumptions.clear();
339  break;
340  }
341 }
342 
344  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
345 {
346 }
347 
349  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
350 {
351 }
352 
354 {
355  try
356  {
357  if(!a.is_constant())
358  {
359  add_variables();
360  solver->setFrozen(a.var_no(), true);
361  }
362  }
363  catch(const Minisat::OutOfMemoryException &)
364  {
365  messaget::error() << "SAT checker ran out of memory" << eom;
367  throw std::bad_alloc();
368  }
369 }
370 
372 {
374 
375  return solver->isEliminated(a.var_no());
376 }
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:470
virtual void set_frozen(literalt a) final
#define forall_literals(it, bv)
Definition: literal.h:202
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
virtual void set_assignment(literalt a, bool value) override
mstreamt & warning() const
Definition: message.h:391
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:386
var_not var_no() const
Definition: literal.h:82
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
resultt
Definition: prop.h:96
static eomt eom
Definition: message.h:284
mstreamt & status() const
Definition: message.h:401
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