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 _WIN32
12 # include <signal.h>
13 # include <unistd.h>
14 #endif
15 
16 #include <limits>
17 
18 #include <util/invariant.h>
19 #include <util/make_unique.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 {
32  bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
33  dest.capacity(static_cast<int>(bv.size()));
34 
35  for(const auto &literal : bv)
36  {
37  if(!literal.is_false())
38  dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
39  }
40 }
41 
42 template<typename T>
44 {
45  if(a.is_true())
46  return tvt(true);
47  else if(a.is_false())
48  return tvt(false);
49 
50  tvt result;
51 
52  if(a.var_no()>=(unsigned)solver->model.size())
53  return tvt::unknown();
54 
55  using Minisat::lbool;
56 
57  if(solver->model[a.var_no()]==l_True)
58  result=tvt(true);
59  else if(solver->model[a.var_no()]==l_False)
60  result=tvt(false);
61  else
62  return tvt::unknown();
63 
64  if(a.sign())
65  result=!result;
66 
67  return result;
68 }
69 
70 template<typename T>
72 {
74 
75  using Minisat::lbool;
76 
77  try
78  {
79  add_variables();
80  solver->setPolarity(a.var_no(), value ? l_True : l_False);
81  }
82  catch(Minisat::OutOfMemoryException)
83  {
84  log.error() << "SAT checker ran out of memory" << messaget::eom;
85  status = statust::ERROR;
86  throw std::bad_alloc();
87  }
88 }
89 
90 template<typename T>
92 {
93  solver->interrupt();
94 }
95 
96 template<typename T>
98 {
99  solver->clearInterrupt();
100 }
101 
103 {
104  return "MiniSAT 2.2.1 without simplifier";
105 }
106 
108 {
109  return "MiniSAT 2.2.1 with simplifier";
110 }
111 
112 template<typename T>
114 {
115  while((unsigned)solver->nVars()<no_variables())
116  solver->newVar();
117 }
118 
119 template<typename T>
121 {
122  try
123  {
124  add_variables();
125 
126  for(const auto &literal : bv)
127  {
128  if(literal.is_true())
129  return;
130  else if(!literal.is_false())
131  {
132  INVARIANT(
133  literal.var_no() < (unsigned)solver->nVars(),
134  "variable not added yet");
135  }
136  }
137 
138  Minisat::vec<Minisat::Lit> c;
139 
140  convert(bv, c);
141 
142  // Note the underscore.
143  // Add a clause to the solver without making superflous internal copy.
144 
145  solver->addClause_(c);
146 
147  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
148  // To map clauses to lines of program code, track clause indices in the
149  // dimacs cnf output. Dimacs output is generated after processing
150  // clauses to remove duplicates and clauses that are trivially true.
151  // Here, a clause is checked to see if it can be thus eliminated. If
152  // not, add the clause index to list of clauses in
153  // solver_hardnesst::register_clause().
154  static size_t cnf_clause_index = 0;
155  bvt cnf;
156  bool clause_removed = process_clause(bv, cnf);
157 
158  if(!clause_removed)
159  cnf_clause_index++;
160 
161  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
162  });
163 
164  clause_counter++;
165  }
166  catch(const Minisat::OutOfMemoryException &)
167  {
168  log.error() << "SAT checker ran out of memory" << messaget::eom;
169  status = statust::ERROR;
170  throw std::bad_alloc();
171  }
172 }
173 
174 #ifndef _WIN32
175 
176 static Minisat::Solver *solver_to_interrupt=nullptr;
177 
178 static void interrupt_solver(int signum)
179 {
180  (void)signum; // unused parameter -- just removing the name trips up cpplint
181  solver_to_interrupt->interrupt();
182 }
183 
184 #endif
185 
186 template <typename T>
188 {
189  PRECONDITION(status != statust::ERROR);
190 
191  log.statistics() << (no_variables() - 1) << " variables, "
192  << solver->nClauses() << " clauses" << messaget::eom;
193 
194  try
195  {
196  add_variables();
197 
198  if(!solver->okay())
199  {
200  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
201  << messaget::eom;
202  status = statust::UNSAT;
203  return resultt::P_UNSATISFIABLE;
204  }
205 
206  // if assumptions contains false, we need this to be UNSAT
207  for(const auto &assumption : assumptions)
208  {
209  if(assumption.is_false())
210  {
211  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
212  << messaget::eom;
213  status = statust::UNSAT;
214  return resultt::P_UNSATISFIABLE;
215  }
216  }
217 
218  Minisat::vec<Minisat::Lit> solver_assumptions;
219  convert(assumptions, solver_assumptions);
220 
221  using Minisat::lbool;
222 
223 #ifndef _WIN32
224 
225  void (*old_handler)(int) = SIG_ERR;
226 
227  if(time_limit_seconds != 0)
228  {
229  solver_to_interrupt = solver.get();
230  old_handler = signal(SIGALRM, interrupt_solver);
231  if(old_handler == SIG_ERR)
232  log.warning() << "Failed to set solver time limit" << messaget::eom;
233  else
234  alarm(time_limit_seconds);
235  }
236 
237  lbool solver_result = solver->solveLimited(solver_assumptions);
238 
239  if(old_handler != SIG_ERR)
240  {
241  alarm(0);
242  signal(SIGALRM, old_handler);
243  solver_to_interrupt = solver.get();
244  }
245 
246 #else // _WIN32
247 
248  if(time_limit_seconds != 0)
249  {
250  log.warning() << "Time limit ignored (not supported on Win32 yet)"
251  << messaget::eom;
252  }
253 
254  lbool solver_result = solver->solve(solver_assumptions) ? l_True : l_False;
255 
256 #endif
257 
258  if(solver_result == l_True)
259  {
260  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
261  CHECK_RETURN(solver->model.size() > 0);
262  status = statust::SAT;
263  return resultt::P_SATISFIABLE;
264  }
265 
266  if(solver_result == l_False)
267  {
268  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
269  status = statust::UNSAT;
270  return resultt::P_UNSATISFIABLE;
271  }
272 
273  log.status() << "SAT checker: timed out or other error" << messaget::eom;
274  status = statust::ERROR;
275  return resultt::P_ERROR;
276  }
277  catch(const Minisat::OutOfMemoryException &)
278  {
279  log.error() << "SAT checker ran out of memory" << messaget::eom;
280  status=statust::ERROR;
281  return resultt::P_ERROR;
282  }
283 }
284 
285 template<typename T>
287 {
289 
290  try
291  {
292  unsigned v = a.var_no();
293  bool sign = a.sign();
294 
295  // MiniSat2 kills the model in case of UNSAT
296  solver->model.growTo(v + 1);
297  value ^= sign;
298  solver->model[v] = Minisat::lbool(value);
299  }
300  catch(const Minisat::OutOfMemoryException &)
301  {
302  log.error() << "SAT checker ran out of memory" << messaget::eom;
303  status = statust::ERROR;
304  throw std::bad_alloc();
305  }
306 }
307 
308 template <typename T>
310  message_handlert &message_handler)
311  : cnf_solvert(message_handler),
312  solver(util_make_unique<T>()),
313  time_limit_seconds(0)
314 {
315 }
316 
317 template <typename T>
319 
320 template<typename T>
322 {
323  int v=a.var_no();
324 
325  for(int i=0; i<solver->conflict.size(); i++)
326  if(var(solver->conflict[i])==v)
327  return true;
328 
329  return false;
330 }
331 
332 template<typename T>
334 {
335  // We filter out 'true' assumptions which cause an assertion violation
336  // in Minisat2.
337  assumptions.clear();
338  for(const auto &assumption : bv)
339  {
340  if(!assumption.is_true())
341  {
342  assumptions.push_back(assumption);
343  }
344  }
345 }
346 
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 }
statust status
Definition: cnf.h:87
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
bool is_constant() const
Definition: literal.h:166
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
resultt
Definition: prop.h:97
messaget log
Definition: prop.h:128
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
std::unique_ptr< Minisat::SimpSolver > solver
~satcheck_minisat2_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
satcheck_minisat2_baset(message_handlert &message_handler)
void set_polarity(literalt a, bool value)
void lcnf(const bvt &bv) override final
tvt l_get(literalt a) const override final
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
const std::string solver_text() override
void set_frozen(literalt a) override final
bool is_eliminated(literalt a) const
const std::string solver_text() override final
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
std::vector< literalt > bvt
Definition: literal.h:201
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
static Minisat::Solver * solver_to_interrupt
static void interrupt_solver(int signum)
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
int solver(std::istream &in)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
A structure that facilitates collecting the complexity statistics from a decision procedure.
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.