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 
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  log.error() << "SAT checker ran out of memory" << messaget::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  log.error() << "SAT checker ran out of memory" << messaget::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  log.statistics() << (no_variables() - 1) << " variables, "
171  << solver->nClauses() << " clauses" << messaget::eom;
172 
173  try
174  {
175  add_variables();
176 
177  if(!solver->okay())
178  {
179  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
180  << messaget::eom;
181  status = statust::UNSAT;
182  return resultt::P_UNSATISFIABLE;
183  }
184 
185  // if assumptions contains false, we need this to be UNSAT
186  for(const auto &assumption : assumptions)
187  {
188  if(assumption.is_false())
189  {
190  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
191  << messaget::eom;
192  status = statust::UNSAT;
193  return resultt::P_UNSATISFIABLE;
194  }
195  }
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  log.warning() << "Failed to set solver time limit" << messaget::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  log.warning() << "Time limit ignored (not supported on Win32 yet)"
230  << messaget::eom;
231  }
232 
233  lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
234 
235 #endif
236 
237  if(solver_result == l_True)
238  {
239  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
240  CHECK_RETURN(solver->model.size() > 0);
241  status = statust::SAT;
242  return resultt::P_SATISFIABLE;
243  }
244 
245  if(solver_result == l_False)
246  {
247  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
248  status = statust::UNSAT;
249  return resultt::P_UNSATISFIABLE;
250  }
251 
252  log.status() << "SAT checker: timed out or other error" << messaget::eom;
253  status = statust::ERROR;
254  return resultt::P_ERROR;
255  }
256  catch(const Minisat::OutOfMemoryException &)
257  {
258  log.error() << "SAT checker ran out of memory" << messaget::eom;
259  status=statust::ERROR;
260  return resultt::P_ERROR;
261  }
262 }
263 
264 template<typename T>
266 {
268 
269  try
270  {
271  unsigned v = a.var_no();
272  bool sign = a.sign();
273 
274  // MiniSat2 kills the model in case of UNSAT
275  solver->model.growTo(v + 1);
276  value ^= sign;
277  solver->model[v] = Minisat::lbool(value);
278  }
279  catch(const Minisat::OutOfMemoryException &)
280  {
281  log.error() << "SAT checker ran out of memory" << messaget::eom;
282  status = statust::ERROR;
283  throw std::bad_alloc();
284  }
285 }
286 
287 template <typename T>
289  T *_solver,
290  message_handlert &message_handler)
291  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
292 {
293 }
294 
295 template<>
297 {
298  delete solver;
299 }
300 
301 template<>
303 {
304  delete solver;
305 }
306 
307 template<typename T>
309 {
310  int v=a.var_no();
311 
312  for(int i=0; i<solver->conflict.size(); i++)
313  if(var(solver->conflict[i])==v)
314  return true;
315 
316  return false;
317 }
318 
319 template<typename T>
321 {
322  // We filter out 'true' assumptions which cause an assertion violation
323  // in Minisat2.
324  assumptions.clear();
325  for(const auto &assumption : bv)
326  {
327  if(!assumption.is_true())
328  {
329  assumptions.push_back(assumption);
330  }
331  }
332 }
333 
335  message_handlert &message_handler)
336  : satcheck_minisat2_baset<Minisat::Solver>(
337  new Minisat::Solver,
338  message_handler)
339 {
340 }
341 
343  message_handlert &message_handler)
344  : satcheck_minisat2_baset<Minisat::SimpSolver>(
345  new Minisat::SimpSolver,
346  message_handler)
347 {
348 }
349 
351 {
352  try
353  {
354  if(!a.is_constant())
355  {
356  add_variables();
357  solver->setFrozen(a.var_no(), true);
358  }
359  }
360  catch(const Minisat::OutOfMemoryException &)
361  {
362  log.error() << "SAT checker ran out of memory" << messaget::eom;
364  throw std::bad_alloc();
365  }
366 }
367 
369 {
371 
372  return solver->isEliminated(a.var_no());
373 }
satcheck_minisat2_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_minisat2.cpp:70
satcheck_minisat2_baset
Definition: satcheck_minisat2.h:28
satcheck_minisat_simplifiert::solver_text
const std::string solver_text() override final
Definition: satcheck_minisat2.cpp:104
satcheck_minisat2_baset::add_variables
void add_variables()
Definition: satcheck_minisat2.cpp:110
satcheck_minisat2_baset::l_get
tvt l_get(literalt a) const override final
Definition: satcheck_minisat2.cpp:42
satcheck_minisat2_baset::interrupt
void interrupt()
Definition: satcheck_minisat2.cpp:88
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
satcheck_minisat_simplifiert::satcheck_minisat_simplifiert
satcheck_minisat_simplifiert(message_handlert &message_handler)
Definition: satcheck_minisat2.cpp:342
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
satcheck_minisat2_baset::lcnf
void lcnf(const bvt &bv) override final
Definition: satcheck_minisat2.cpp:117
invariant.h
satcheck_minisat2_baset::solver
T * solver
Definition: satcheck_minisat2.h:68
convert
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
Definition: satcheck_minisat2.cpp:30
messaget::eom
static eomt eom
Definition: message.h:283
literalt::var_no
var_not var_no() const
Definition: literal.h:83
satcheck_minisat2_baset::clear_interrupt
void clear_interrupt()
Definition: satcheck_minisat2.cpp:94
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
cnf_solvert
Definition: cnf.h:70
cnf_solvert::statust::ERROR
@ ERROR
satcheck_minisat2_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_minisat2.cpp:166
satcheck_minisat_simplifiert::set_frozen
void set_frozen(literalt a) override final
Definition: satcheck_minisat2.cpp:350
literalt::is_true
bool is_true() const
Definition: literal.h:156
satcheck_minisat2_baset::is_in_conflict
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
Definition: satcheck_minisat2.cpp:308
messaget::error
mstreamt & error() const
Definition: message.h:385
satcheck_minisat_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_minisat2.cpp:368
cnf_solvert::status
statust status
Definition: cnf.h:84
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
satcheck_minisat2_baset::satcheck_minisat2_baset
satcheck_minisat2_baset(T *, message_handlert &message_handler)
Definition: satcheck_minisat2.cpp:288
literalt::is_false
bool is_false() const
Definition: literal.h:161
satcheck_minisat2.h
satcheck_minisat2_baset::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: satcheck_minisat2.cpp:320
message_handlert
Definition: message.h:27
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:99
Minisat
Definition: satcheck_minisat2.h:21
tvt
Definition: threeval.h:20
literalt::sign
bool sign() const
Definition: literal.h:88
satcheck_minisat_no_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_minisat2.cpp:99
interrupt_solver
static void interrupt_solver(int signum)
Definition: satcheck_minisat2.cpp:157
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
literalt
Definition: literal.h:26
propt::log
messaget log
Definition: prop.h:130
solver_to_interrupt
static Minisat::Solver * solver_to_interrupt
Definition: satcheck_minisat2.cpp:155
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert
satcheck_minisat_no_simplifiert(message_handlert &message_handler)
Definition: satcheck_minisat2.cpp:334
satcheck_minisat2_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_minisat2.cpp:265
satcheck_minisat2_baset::~satcheck_minisat2_baset
virtual ~satcheck_minisat2_baset()