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 <stack>
18 
19 #include <util/invariant.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 
29 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
30 {
31  dest.capacity(bv.size());
32 
33  forall_literals(it, bv)
34  if(!it->is_false())
35  dest.push(Minisat::mkLit(it->var_no(), it->sign()));
36 }
37 
38 template<typename T>
40 {
41  if(a.is_true())
42  return tvt(true);
43  else if(a.is_false())
44  return tvt(false);
45 
46  tvt result;
47 
48  if(a.var_no()>=(unsigned)solver->model.size())
49  return tvt::unknown();
50 
51  using Minisat::lbool;
52 
53  if(solver->model[a.var_no()]==l_True)
54  result=tvt(true);
55  else if(solver->model[a.var_no()]==l_False)
56  result=tvt(false);
57  else
58  return tvt::unknown();
59 
60  if(a.sign())
61  result=!result;
62 
63  return result;
64 }
65 
66 template<typename T>
68 {
70 
71  try
72  {
73  add_variables();
74  solver->setPolarity(a.var_no(), value);
75  }
76  catch(Minisat::OutOfMemoryException)
77  {
78  messaget::error() << "SAT checker ran out of memory" << eom;
79  status = statust::ERROR;
80  throw std::bad_alloc();
81  }
82 }
83 
84 template<typename T>
86 {
87  solver->interrupt();
88 }
89 
90 template<typename T>
92 {
93  solver->clearInterrupt();
94 }
95 
97 {
98  return "MiniSAT 2.2.1 without simplifier";
99 }
100 
102 {
103  return "MiniSAT 2.2.1 with simplifier";
104 }
105 
106 template<typename T>
108 {
109  while((unsigned)solver->nVars()<no_variables())
110  solver->newVar();
111 }
112 
113 template<typename T>
115 {
116  try
117  {
118  add_variables();
119 
120  forall_literals(it, bv)
121  {
122  if(it->is_true())
123  return;
124  else if(!it->is_false())
125  {
126  INVARIANT(
127  it->var_no() < (unsigned)solver->nVars(), "variable not added yet");
128  }
129  }
130 
131  Minisat::vec<Minisat::Lit> c;
132 
133  convert(bv, c);
134 
135  // Note the underscore.
136  // Add a clause to the solver without making superflous internal copy.
137 
138  solver->addClause_(c);
139 
140  clause_counter++;
141  }
142  catch(Minisat::OutOfMemoryException)
143  {
144  messaget::error() << "SAT checker ran out of memory" << eom;
145  status = statust::ERROR;
146  throw std::bad_alloc();
147  }
148 }
149 
150 #ifndef _WIN32
151 
152 static Minisat::Solver *solver_to_interrupt=nullptr;
153 
154 static void interrupt_solver(int signum)
155 {
156  solver_to_interrupt->interrupt();
157 }
158 
159 #endif
160 
161 template<typename T>
163 {
164  PRECONDITION(status != statust::ERROR);
165 
166  {
167  messaget::status() <<
168  (no_variables()-1) << " variables, " <<
169  solver->nClauses() << " clauses" << eom;
170  }
171 
172  try
173  {
174  add_variables();
175 
176  if(!solver->okay())
177  {
178  messaget::status() <<
179  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
180  }
181  else
182  {
183  // if assumptions contains false, we need this to be UNSAT
184  bool has_false=false;
185 
186  forall_literals(it, assumptions)
187  if(it->is_false())
188  has_false=true;
189 
190  if(has_false)
191  {
192  messaget::status() <<
193  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
194  }
195  else
196  {
197  Minisat::vec<Minisat::Lit> solver_assumptions;
198  convert(assumptions, solver_assumptions);
199 
200  using Minisat::lbool;
201 
202 #ifndef _WIN32
203 
204  void (*old_handler)(int)=SIG_ERR;
205 
206  if(time_limit_seconds!=0)
207  {
209  old_handler=signal(SIGALRM, interrupt_solver);
210  if(old_handler==SIG_ERR)
211  warning() << "Failed to set solver time limit" << eom;
212  else
213  alarm(time_limit_seconds);
214  }
215 
216  lbool solver_result=solver->solveLimited(solver_assumptions);
217 
218  if(old_handler!=SIG_ERR)
219  {
220  alarm(0);
221  signal(SIGALRM, old_handler);
223  }
224 
225 #else // _WIN32
226 
227  if(time_limit_seconds!=0)
228  {
229  messaget::warning() <<
230  "Time limit ignored (not supported on Win32 yet)" << messaget::eom;
231  }
232 
233  lbool solver_result=
234  solver->solve(solver_assumptions) ? l_True : l_False;
235 
236 #endif
237 
238  if(solver_result==l_True)
239  {
240  messaget::status() <<
241  "SAT checker: instance is SATISFIABLE" << eom;
242  CHECK_RETURN(solver->model.size()>0);
243  status=statust::SAT;
244  return resultt::P_SATISFIABLE;
245  }
246  else if(solver_result==l_False)
247  {
248  messaget::status() <<
249  "SAT checker: instance is UNSATISFIABLE" << eom;
250  }
251  else
252  {
253  messaget::status() <<
254  "SAT checker: timed out or other error" << eom;
255  status=statust::ERROR;
256  return resultt::P_ERROR;
257  }
258  }
259  }
260 
261  status=statust::UNSAT;
262  return resultt::P_UNSATISFIABLE;
263  }
264  catch(Minisat::OutOfMemoryException)
265  {
266  messaget::error() <<
267  "SAT checker ran out of memory" << eom;
268  status=statust::ERROR;
269  return resultt::P_ERROR;
270  }
271 }
272 
273 template<typename T>
275 {
277 
278  try
279  {
280  unsigned v = a.var_no();
281  bool sign = a.sign();
282 
283  // MiniSat2 kills the model in case of UNSAT
284  solver->model.growTo(v + 1);
285  value ^= sign;
286  solver->model[v] = Minisat::lbool(value);
287  }
288  catch(Minisat::OutOfMemoryException)
289  {
290  messaget::error() << "SAT checker ran out of memory" << eom;
291  status = statust::ERROR;
292  throw std::bad_alloc();
293  }
294 }
295 
296 template<typename T>
298  solver(_solver), time_limit_seconds(0)
299 {
300 }
301 
302 template<>
304 {
305  delete solver;
306 }
307 
308 template<>
310 {
311  delete solver;
312 }
313 
314 template<typename T>
316 {
317  int v=a.var_no();
318 
319  for(int i=0; i<solver->conflict.size(); i++)
320  if(var(solver->conflict[i])==v)
321  return true;
322 
323  return false;
324 }
325 
326 template<typename T>
328 {
329  assumptions=bv;
330 
331  forall_literals(it, assumptions)
332  if(it->is_true())
333  {
334  assumptions.clear();
335  break;
336  }
337 }
338 
340  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
341 {
342 }
343 
345  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
346 {
347 }
348 
350 {
351  try
352  {
353  if(!a.is_constant())
354  {
355  add_variables();
356  solver->setFrozen(a.var_no(), true);
357  }
358  }
359  catch(Minisat::OutOfMemoryException)
360  {
361  messaget::error() << "SAT checker ran out of memory" << eom;
363  throw std::bad_alloc();
364  }
365 }
366 
368 {
370 
371  return solver->isEliminated(a.var_no());
372 }
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:245
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:205
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
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:230
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