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 #endif
14 
15 #include <cassert>
16 #include <stack>
17 
18 #include <util/invariant.h>
19 #include <util/threeval.h>
20 #include <util/invariant.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 {
31  dest.capacity(bv.size());
32 
33  forall_literals(it, bv)
34  if(!it->is_false())
35  dest.push(Minisat::mkLit(it->var_no(), it->sign()));
36 }
37 
38 template<typename T>
40 {
41  if(a.is_true())
42  return tvt(true);
43  else if(a.is_false())
44  return tvt(false);
45 
46  tvt result;
47 
48  if(a.var_no()>=(unsigned)solver->model.size())
49  return tvt::unknown();
50 
51  using Minisat::lbool;
52 
53  if(solver->model[a.var_no()]==l_True)
54  result=tvt(true);
55  else if(solver->model[a.var_no()]==l_False)
56  result=tvt(false);
57  else
58  return tvt::unknown();
59 
60  if(a.sign())
61  result=!result;
62 
63  return result;
64 }
65 
66 template<typename T>
68 {
69  assert(!a.is_constant());
70  add_variables();
71  solver->setPolarity(a.var_no(), value);
72 }
73 
75 {
76  return "MiniSAT 2.2.1 without simplifier";
77 }
78 
80 {
81  return "MiniSAT 2.2.1 with simplifier";
82 }
83 
84 template<typename T>
86 {
87  while((unsigned)solver->nVars()<no_variables())
88  solver->newVar();
89 }
90 
91 template<typename T>
93 {
94  add_variables();
95 
96  forall_literals(it, bv)
97  {
98  if(it->is_true())
99  return;
100  else if(!it->is_false())
101  assert(it->var_no()<(unsigned)solver->nVars());
102  }
103 
104  Minisat::vec<Minisat::Lit> c;
105 
106  convert(bv, c);
107 
108  // Note the underscore.
109  // Add a clause to the solver without making superflous internal copy.
110 
111  solver->addClause_(c);
112 
113  clause_counter++;
114 }
115 
116 template<typename T>
118 {
119  assert(status!=statust::ERROR);
120 
121  {
122  messaget::status() <<
123  (no_variables()-1) << " variables, " <<
124  solver->nClauses() << " clauses" << eom;
125  }
126 
127  try
128  {
129  add_variables();
130 
131  if(!solver->okay())
132  {
133  messaget::status() <<
134  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
135  }
136  else
137  {
138  // if assumptions contains false, we need this to be UNSAT
139  bool has_false=false;
140 
141  forall_literals(it, assumptions)
142  if(it->is_false())
143  has_false=true;
144 
145  if(has_false)
146  {
147  messaget::status() <<
148  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
149  }
150  else
151  {
152  Minisat::vec<Minisat::Lit> solver_assumptions;
153  convert(assumptions, solver_assumptions);
154 
155  if(solver->solve(solver_assumptions))
156  {
157  messaget::status() <<
158  "SAT checker: instance is SATISFIABLE" << eom;
159  CHECK_RETURN(solver->model.size()>0);
160  status=statust::SAT;
161  return resultt::P_SATISFIABLE;
162  }
163  else
164  {
165  messaget::status() <<
166  "SAT checker: instance is UNSATISFIABLE" << eom;
167  }
168  }
169  }
170 
171  status=statust::UNSAT;
172  return resultt::P_UNSATISFIABLE;
173  }
174  catch(Minisat::OutOfMemoryException)
175  {
176  messaget::error() <<
177  "SAT checker ran out of memory" << eom;
178  status=statust::ERROR;
179  return resultt::P_ERROR;
180  }
181 }
182 
183 template<typename T>
185 {
186  assert(!a.is_constant());
187 
188  unsigned v=a.var_no();
189  bool sign=a.sign();
190 
191  // MiniSat2 kills the model in case of UNSAT
192  solver->model.growTo(v+1);
193  value^=sign;
194  solver->model[v]=Minisat::lbool(value);
195 }
196 
197 template<typename T>
199  solver(_solver)
200 {
201 }
202 
203 template<>
205 {
206  delete solver;
207 }
208 
209 template<>
211 {
212  delete solver;
213 }
214 
215 template<typename T>
217 {
218  int v=a.var_no();
219 
220  for(int i=0; i<solver->conflict.size(); i++)
221  if(var(solver->conflict[i])==v)
222  return true;
223 
224  return false;
225 }
226 
227 template<typename T>
229 {
230  assumptions=bv;
231 
232  forall_literals(it, assumptions)
233  if(it->is_true())
234  {
235  assumptions.clear();
236  break;
237  }
238 }
239 
241  satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
242 {
243 }
244 
246  satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
247 {
248 }
249 
251 {
252  if(!a.is_constant())
253  {
254  add_variables();
255  solver->setFrozen(a.var_no(), true);
256  }
257 }
258 
260 {
261  assert(!a.is_constant());
262 
263  return solver->isEliminated(a.var_no());
264 }
mstreamt & status()
Definition: message.h:238
virtual void lcnf(const bvt &bv) final
static tvt unknown()
Definition: threeval.h:33
virtual const std::string solver_text()
void set_polarity(literalt a, bool value)
virtual const std::string solver_text() final
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
virtual void set_frozen(literalt a) final
#define forall_literals(it, bv)
Definition: literal.h:199
virtual void set_assignment(literalt a, bool value) override
void convert(const bvt &bv, Minisat::vec< Minisat::Lit > &dest)
virtual bool is_in_conflict(literalt a) const override
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
bool is_eliminated(literalt a) const
mstreamt & error()
Definition: message.h:223
virtual ~satcheck_minisat2_baset()
virtual void set_assumptions(const bvt &_assumptions) override
virtual tvt l_get(literalt a) const final
std::vector< literalt > bvt
Definition: literal.h:197
virtual resultt prop_solve() override
bool is_false() const
Definition: literal.h:160