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  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 
144  [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
145  clause_counter++;
146  }
147  catch(const Minisat::OutOfMemoryException &)
148  {
149  log.error() << "SAT checker ran out of memory" << messaget::eom;
150  status = statust::ERROR;
151  throw std::bad_alloc();
152  }
153 }
154 
155 #ifndef _WIN32
156 
157 static Minisat::Solver *solver_to_interrupt=nullptr;
158 
159 static void interrupt_solver(int signum)
160 {
161  (void)signum; // unused parameter -- just removing the name trips up cpplint
162  solver_to_interrupt->interrupt();
163 }
164 
165 #endif
166 
167 template <typename T>
169 {
170  PRECONDITION(status != statust::ERROR);
171 
172  log.statistics() << (no_variables() - 1) << " variables, "
173  << solver->nClauses() << " clauses" << messaget::eom;
174 
175  try
176  {
177  add_variables();
178 
179  if(!solver->okay())
180  {
181  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
182  << messaget::eom;
183  status = statust::UNSAT;
184  return resultt::P_UNSATISFIABLE;
185  }
186 
187  // if assumptions contains false, we need this to be UNSAT
188  for(const auto &assumption : assumptions)
189  {
190  if(assumption.is_false())
191  {
192  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
193  << messaget::eom;
194  status = statust::UNSAT;
195  return resultt::P_UNSATISFIABLE;
196  }
197  }
198 
199  Minisat::vec<Minisat::Lit> solver_assumptions;
200  convert(assumptions, solver_assumptions);
201 
202  using Minisat::lbool;
203 
204 #ifndef _WIN32
205 
206  void (*old_handler)(int) = SIG_ERR;
207 
208  if(time_limit_seconds != 0)
209  {
211  old_handler = signal(SIGALRM, interrupt_solver);
212  if(old_handler == SIG_ERR)
213  log.warning() << "Failed to set solver time limit" << messaget::eom;
214  else
215  alarm(time_limit_seconds);
216  }
217 
218  lbool solver_result = solver->solveLimited(solver_assumptions);
219 
220  if(old_handler != SIG_ERR)
221  {
222  alarm(0);
223  signal(SIGALRM, old_handler);
225  }
226 
227 #else // _WIN32
228 
229  if(time_limit_seconds != 0)
230  {
231  log.warning() << "Time limit ignored (not supported on Win32 yet)"
232  << messaget::eom;
233  }
234 
235  lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
236 
237 #endif
238 
239  if(solver_result == l_True)
240  {
241  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
242  CHECK_RETURN(solver->model.size() > 0);
243  status = statust::SAT;
244  return resultt::P_SATISFIABLE;
245  }
246 
247  if(solver_result == l_False)
248  {
249  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
250  status = statust::UNSAT;
251  return resultt::P_UNSATISFIABLE;
252  }
253 
254  log.status() << "SAT checker: timed out or other error" << messaget::eom;
255  status = statust::ERROR;
256  return resultt::P_ERROR;
257  }
258  catch(const Minisat::OutOfMemoryException &)
259  {
260  log.error() << "SAT checker ran out of memory" << messaget::eom;
261  status=statust::ERROR;
262  return resultt::P_ERROR;
263  }
264 }
265 
266 template<typename T>
268 {
270 
271  try
272  {
273  unsigned v = a.var_no();
274  bool sign = a.sign();
275 
276  // MiniSat2 kills the model in case of UNSAT
277  solver->model.growTo(v + 1);
278  value ^= sign;
279  solver->model[v] = Minisat::lbool(value);
280  }
281  catch(const Minisat::OutOfMemoryException &)
282  {
283  log.error() << "SAT checker ran out of memory" << messaget::eom;
284  status = statust::ERROR;
285  throw std::bad_alloc();
286  }
287 }
288 
289 template <typename T>
291  T *_solver,
292  message_handlert &message_handler)
293  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
294 {
295 }
296 
297 template<>
299 {
300  delete solver;
301 }
302 
303 template<>
305 {
306  delete solver;
307 }
308 
309 template<typename T>
311 {
312  int v=a.var_no();
313 
314  for(int i=0; i<solver->conflict.size(); i++)
315  if(var(solver->conflict[i])==v)
316  return true;
317 
318  return false;
319 }
320 
321 template<typename T>
323 {
324  // We filter out 'true' assumptions which cause an assertion violation
325  // in Minisat2.
326  assumptions.clear();
327  for(const auto &assumption : bv)
328  {
329  if(!assumption.is_true())
330  {
331  assumptions.push_back(assumption);
332  }
333  }
334 }
335 
337  message_handlert &message_handler)
338  : satcheck_minisat2_baset<Minisat::Solver>(
339  new Minisat::Solver,
340  message_handler)
341 {
342 }
343 
345  message_handlert &message_handler)
346  : satcheck_minisat2_baset<Minisat::SimpSolver>(
347  new Minisat::SimpSolver,
348  message_handler)
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(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 }
satcheck_minisat2_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_minisat2.cpp:70
satcheck_minisat2_baset
Definition: satcheck_minisat2.h:30
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::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:344
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:84
convert
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
Definition: satcheck_minisat2.cpp:30
messaget::eom
static eomt eom
Definition: message.h:297
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
is_false
bool is_false(const literalt &l)
Definition: literal.h:197
satcheck_minisat2_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_minisat2.cpp:168
satcheck_minisat_simplifiert::set_frozen
void set_frozen(literalt a) override final
Definition: satcheck_minisat2.cpp:352
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:310
messaget::error
mstreamt & error() const
Definition: message.h:399
satcheck_minisat_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_minisat2.cpp:370
cnf_solvert::status
statust status
Definition: cnf.h:84
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
solver_hardnesst::register_clause
void register_clause(const bvt &bv)
Called e.g.
Definition: solver_hardness.cpp:90
satcheck_minisat2_baset::satcheck_minisat2_baset
satcheck_minisat2_baset(T *, message_handlert &message_handler)
Definition: satcheck_minisat2.cpp:290
satcheck_minisat2.h
satcheck_minisat2_baset::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: satcheck_minisat2.cpp:322
message_handlert
Definition: message.h:28
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:99
Minisat
Definition: satcheck_minisat2.h:23
tvt
Definition: threeval.h:20
literalt::sign
bool sign() const
Definition: literal.h:88
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:45
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:159
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:157
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:336
satcheck_minisat2_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_minisat2.cpp:267
with_solver_hardness
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
Definition: hardness_collector.h:32
satcheck_minisat2_baset::~satcheck_minisat2_baset
virtual ~satcheck_minisat2_baset()