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 }
satcheck_minisat2_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_minisat2.cpp:71
satcheck_minisat2_baset< Minisat::Solver >
satcheck_minisat_simplifiert::solver_text
const std::string solver_text() override final
Definition: satcheck_minisat2.cpp:107
satcheck_minisat2_baset::add_variables
void add_variables()
Definition: satcheck_minisat2.cpp:113
satcheck_minisat2_baset::l_get
tvt l_get(literalt a) const override final
Definition: satcheck_minisat2.cpp:43
satcheck_minisat2_baset::interrupt
void interrupt()
Definition: satcheck_minisat2.cpp:91
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
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:120
invariant.h
convert
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
Definition: satcheck_minisat2.cpp:29
messaget::eom
static eomt eom
Definition: message.h:297
literalt::var_no
var_not var_no() const
Definition: literal.h:83
satcheck_minisat2_baset::satcheck_minisat2_baset
satcheck_minisat2_baset(message_handlert &message_handler)
Definition: satcheck_minisat2.cpp:309
satcheck_minisat2_baset::clear_interrupt
void clear_interrupt()
Definition: satcheck_minisat2.cpp:97
satcheck_minisat2_baset< Minisat::SimpSolver >::solver
std::unique_ptr< Minisat::SimpSolver > solver
Definition: satcheck_minisat2.h:88
cnf_solvert
Definition: cnf.h:73
cnf_solvert::statust::ERROR
@ ERROR
satcheck_minisat2_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_minisat2.cpp:187
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:87
satcheck_minisat_simplifiert::set_frozen
void set_frozen(literalt a) override final
Definition: satcheck_minisat2.cpp:350
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
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:321
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
satcheck_minisat_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_minisat2.cpp:368
cnf_solvert::status
statust status
Definition: cnf.h:87
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:333
message_handlert
Definition: message.h:28
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:97
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:42
satcheck_minisat_no_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_minisat2.cpp:102
interrupt_solver
static void interrupt_solver(int signum)
Definition: satcheck_minisat2.cpp:178
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:407
literalt
Definition: literal.h:26
satcheck_minisat2_baset::~satcheck_minisat2_baset
~satcheck_minisat2_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
propt::log
messaget log
Definition: prop.h:128
solver_to_interrupt
static Minisat::Solver * solver_to_interrupt
Definition: satcheck_minisat2.cpp:176
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:423
satcheck_minisat2_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_minisat2.cpp:286
with_solver_hardness
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
Definition: hardness_collector.h:32