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  for(const auto &literal : bv)
37  {
38  if(!literal.is_false())
39  dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
40  }
41 }
42 
43 template<typename T>
45 {
46  if(a.is_true())
47  return tvt(true);
48  else if(a.is_false())
49  return tvt(false);
50 
51  tvt result;
52 
53  if(a.var_no()>=(unsigned)solver->model.size())
54  return tvt::unknown();
55 
56  using Minisat::lbool;
57 
58  if(solver->model[a.var_no()]==l_True)
59  result=tvt(true);
60  else if(solver->model[a.var_no()]==l_False)
61  result=tvt(false);
62  else
63  return tvt::unknown();
64 
65  if(a.sign())
66  result=!result;
67 
68  return result;
69 }
70 
71 template<typename T>
73 {
75 
76  try
77  {
78  add_variables();
79  solver->setPolarity(a.var_no(), value);
80  }
81  catch(Minisat::OutOfMemoryException)
82  {
83  log.error() << "SAT checker ran out of memory" << messaget::eom;
84  status = statust::ERROR;
85  throw std::bad_alloc();
86  }
87 }
88 
89 template<typename T>
91 {
92  solver->interrupt();
93 }
94 
95 template<typename T>
97 {
98  solver->clearInterrupt();
99 }
100 
102 {
103  return "MiniSAT 2.2.1 without simplifier";
104 }
105 
107 {
108  return "MiniSAT 2.2.1 with simplifier";
109 }
110 
111 template<typename T>
113 {
114  while((unsigned)solver->nVars()<no_variables())
115  solver->newVar();
116 }
117 
118 template<typename T>
120 {
121  try
122  {
123  add_variables();
124 
125  for(const auto &literal : bv)
126  {
127  if(literal.is_true())
128  return;
129  else if(!literal.is_false())
130  {
131  INVARIANT(
132  literal.var_no() < (unsigned)solver->nVars(),
133  "variable not added yet");
134  }
135  }
136 
137  Minisat::vec<Minisat::Lit> c;
138 
139  convert(bv, c);
140 
141  // Note the underscore.
142  // Add a clause to the solver without making superflous internal copy.
143 
144  solver->addClause_(c);
145 
146  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
147  // To map clauses to lines of program code, track clause indices in the
148  // dimacs cnf output. Dimacs output is generated after processing
149  // clauses to remove duplicates and clauses that are trivially true.
150  // Here, a clause is checked to see if it can be thus eliminated. If
151  // not, add the clause index to list of clauses in
152  // solver_hardnesst::register_clause().
153  static size_t cnf_clause_index = 0;
154  bvt cnf;
155  bool clause_removed = process_clause(bv, cnf);
156 
157  if(!clause_removed)
158  cnf_clause_index++;
159 
160  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
161  });
162 
163  clause_counter++;
164  }
165  catch(const Minisat::OutOfMemoryException &)
166  {
167  log.error() << "SAT checker ran out of memory" << messaget::eom;
168  status = statust::ERROR;
169  throw std::bad_alloc();
170  }
171 }
172 
173 #ifndef _WIN32
174 
175 static Minisat::Solver *solver_to_interrupt=nullptr;
176 
177 static void interrupt_solver(int signum)
178 {
179  (void)signum; // unused parameter -- just removing the name trips up cpplint
180  solver_to_interrupt->interrupt();
181 }
182 
183 #endif
184 
185 template <typename T>
187 {
188  PRECONDITION(status != statust::ERROR);
189 
190  log.statistics() << (no_variables() - 1) << " variables, "
191  << solver->nClauses() << " clauses" << messaget::eom;
192 
193  try
194  {
195  add_variables();
196 
197  if(!solver->okay())
198  {
199  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
200  << messaget::eom;
201  status = statust::UNSAT;
202  return resultt::P_UNSATISFIABLE;
203  }
204 
205  // if assumptions contains false, we need this to be UNSAT
206  for(const auto &assumption : assumptions)
207  {
208  if(assumption.is_false())
209  {
210  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
211  << messaget::eom;
212  status = statust::UNSAT;
213  return resultt::P_UNSATISFIABLE;
214  }
215  }
216 
217  Minisat::vec<Minisat::Lit> solver_assumptions;
218  convert(assumptions, solver_assumptions);
219 
220  using Minisat::lbool;
221 
222 #ifndef _WIN32
223 
224  void (*old_handler)(int) = SIG_ERR;
225 
226  if(time_limit_seconds != 0)
227  {
229  old_handler = signal(SIGALRM, interrupt_solver);
230  if(old_handler == SIG_ERR)
231  log.warning() << "Failed to set solver time limit" << messaget::eom;
232  else
233  alarm(time_limit_seconds);
234  }
235 
236  lbool solver_result = solver->solveLimited(solver_assumptions);
237 
238  if(old_handler != SIG_ERR)
239  {
240  alarm(0);
241  signal(SIGALRM, old_handler);
243  }
244 
245 #else // _WIN32
246 
247  if(time_limit_seconds != 0)
248  {
249  log.warning() << "Time limit ignored (not supported on Win32 yet)"
250  << messaget::eom;
251  }
252 
253  lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
254 
255 #endif
256 
257  if(solver_result == l_True)
258  {
259  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
260  CHECK_RETURN(solver->model.size() > 0);
261  status = statust::SAT;
262  return resultt::P_SATISFIABLE;
263  }
264 
265  if(solver_result == l_False)
266  {
267  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
268  status = statust::UNSAT;
269  return resultt::P_UNSATISFIABLE;
270  }
271 
272  log.status() << "SAT checker: timed out or other error" << messaget::eom;
273  status = statust::ERROR;
274  return resultt::P_ERROR;
275  }
276  catch(const Minisat::OutOfMemoryException &)
277  {
278  log.error() << "SAT checker ran out of memory" << messaget::eom;
279  status=statust::ERROR;
280  return resultt::P_ERROR;
281  }
282 }
283 
284 template<typename T>
286 {
288 
289  try
290  {
291  unsigned v = a.var_no();
292  bool sign = a.sign();
293 
294  // MiniSat2 kills the model in case of UNSAT
295  solver->model.growTo(v + 1);
296  value ^= sign;
297  solver->model[v] = Minisat::lbool(value);
298  }
299  catch(const Minisat::OutOfMemoryException &)
300  {
301  log.error() << "SAT checker ran out of memory" << messaget::eom;
302  status = statust::ERROR;
303  throw std::bad_alloc();
304  }
305 }
306 
307 template <typename T>
309  T *_solver,
310  message_handlert &message_handler)
311  : cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
312 {
313 }
314 
315 template<>
317 {
318  delete solver;
319 }
320 
321 template<>
323 {
324  delete solver;
325 }
326 
327 template<typename T>
329 {
330  int v=a.var_no();
331 
332  for(int i=0; i<solver->conflict.size(); i++)
333  if(var(solver->conflict[i])==v)
334  return true;
335 
336  return false;
337 }
338 
339 template<typename T>
341 {
342  // We filter out 'true' assumptions which cause an assertion violation
343  // in Minisat2.
344  assumptions.clear();
345  for(const auto &assumption : bv)
346  {
347  if(!assumption.is_true())
348  {
349  assumptions.push_back(assumption);
350  }
351  }
352 }
353 
355  message_handlert &message_handler)
356  : satcheck_minisat2_baset<Minisat::Solver>(
357  new Minisat::Solver,
358  message_handler)
359 {
360 }
361 
363  message_handlert &message_handler)
364  : satcheck_minisat2_baset<Minisat::SimpSolver>(
365  new Minisat::SimpSolver,
366  message_handler)
367 {
368 }
369 
371 {
372  try
373  {
374  if(!a.is_constant())
375  {
376  add_variables();
377  solver->setFrozen(a.var_no(), true);
378  }
379  }
380  catch(const Minisat::OutOfMemoryException &)
381  {
382  log.error() << "SAT checker ran out of memory" << messaget::eom;
384  throw std::bad_alloc();
385  }
386 }
387 
389 {
391 
392  return solver->isEliminated(a.var_no());
393 }
satcheck_minisat2_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_minisat2.cpp:72
satcheck_minisat2_baset
Definition: satcheck_minisat2.h:30
satcheck_minisat_simplifiert::solver_text
const std::string solver_text() override final
Definition: satcheck_minisat2.cpp:106
satcheck_minisat2_baset::add_variables
void add_variables()
Definition: satcheck_minisat2.cpp:112
satcheck_minisat2_baset::l_get
tvt l_get(literalt a) const override final
Definition: satcheck_minisat2.cpp:44
satcheck_minisat2_baset::interrupt
void interrupt()
Definition: satcheck_minisat2.cpp:90
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:362
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:119
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:96
cnf_solvert
Definition: cnf.h:72
cnf_solvert::statust::ERROR
@ ERROR
satcheck_minisat2_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_minisat2.cpp:186
solver_hardnesst::register_clause
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.
Definition: solver_hardness.cpp:92
satcheck_minisat_simplifiert::set_frozen
void set_frozen(literalt a) override final
Definition: satcheck_minisat2.cpp:370
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:328
messaget::error
mstreamt & error() const
Definition: message.h:399
satcheck_minisat_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_minisat2.cpp:388
cnf_solvert::status
statust status
Definition: cnf.h:86
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:308
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:340
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:101
interrupt_solver
static void interrupt_solver(int signum)
Definition: satcheck_minisat2.cpp:177
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:368
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:175
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:354
satcheck_minisat2_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_minisat2.cpp:285
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()