cprover
satcheck_minisat.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_minisat.h"
10 
11 #include <cassert>
12 #include <stack>
13 
14 #include <util/threeval.h>
15 
16 #include <Solver.h>
17 #include <Proof.h>
18 
19 #ifndef HAVE_MINISAT
20 #error "Expected HAVE_MINISAT"
21 #endif
22 
23 void convert(const bvt &bv, vec<Lit> &dest)
24 {
25  dest.growTo(bv.size());
26 
27  for(unsigned i=0; i<bv.size(); i++)
28  dest[i]=Lit(bv[i].var_no(), bv[i].sign());
29 }
30 
31 class minisat_prooft:public ProofTraverser
32 {
33 public:
34  virtual void root(const vec<Lit> &c)
35  {
36  resolution_proof.clauses.push_back(clauset());
37  resolution_proof.clauses.back().is_root=true;
38  resolution_proof.clauses.back().root_clause.resize(c.size());
39 // resolution_proof.clauses.back().pid = resolution_proof.partition_id;
40 
41  for(int i=0; i<c.size(); i++)
42  {
43  resolution_proof.clauses.back().root_clause[i]=
44  literalt(var(c[i]), sign(c[i]));
45 // if(var(c[i]) > resolution_proof.no_vars)
46 // resolution_proof.no_vars = var(c[i]);
47  }
48  }
49 
50  virtual void chain(const vec<ClauseId> &cs, const vec<Var> &xs);
51 
52  virtual void deleted(ClauseId c) { }
53  virtual void done() { }
54  virtual ~minisat_prooft() { }
55 
57 };
58 
59 void minisat_prooft::chain(const vec<ClauseId> &cs, const vec<Var> &xs)
60 {
61  assert(cs.size()==xs.size()+1);
62 
63  resolution_proof.clauses.push_back(clauset());
65 
66  c.is_root=false;
67  // c.pid = resolution_proof.partition_id;
68  c.first_clause_id=cs[0];
69  c.steps.resize(xs.size());
70 
71  // copy clause IDs
72  int c_id=resolution_proof.clauses.size();
73 
74  for(int i=0; i<xs.size(); i++)
75  {
76  // must be decreasing
77  assert(cs[i]<c_id);
78  c.steps[i].clause_id=cs[i+1];
79  c.steps[i].pivot_var_no=xs[i];
80  }
81 }
82 
84 {
85  if(a.is_true())
86  return tvt(true);
87  else if(a.is_false())
88  return tvt(false);
89 
90  tvt result;
91 
92  assert(a.var_no()!=0);
93  assert(a.var_no()<(unsigned)solver->model.size());
94 
95  if(solver->model[a.var_no()]==l_True)
96  result=tvt(true);
97  else if(solver->model[a.var_no()]==l_False)
98  result=tvt(false);
99  else
101 
102  if(a.sign())
103  result=!result;
104 
105  return result;
106 }
107 
109 {
110  return "MiniSAT 1.14p";
111 }
112 
114 {
115  while((unsigned)solver->nVars()<no_variables())
116  solver->newVar();
117 }
118 
120 {
121  bvt new_bv;
122 
123  if(process_clause(bv, new_bv))
124  return;
125 
126  // Minisat can't do empty clauses
127  if(new_bv.empty())
128  {
129  empty_clause_added=true;
130  return;
131  }
132 
133  add_variables();
134 
135  vec<Lit> c;
136  convert(new_bv, c);
137 
138  for(unsigned i=0; i<new_bv.size(); i++)
139  assert(new_bv[i].var_no()<(unsigned)solver->nVars());
140 
141  solver->addClause(c);
142 
143  clause_counter++;
144 }
145 
147 {
148  assert(status!=ERROR);
149 
150  {
151  messaget::status() <<
152  (_no_variables-1) << " variables, " <<
153  solver->nClauses() << " clauses" << messaget::eom;
154  }
155 
156  add_variables();
157 
158  solver->simplifyDB();
159 
160  std::string msg;
161 
162  if(empty_clause_added)
163  {
164  msg="empty clause: instance is UNSATISFIABLE";
165  }
166  else if(!solver->okay())
167  {
168  msg="SAT checker inconsistent: instance is UNSATISFIABLE";
169  }
170  else
171  {
172  vec<Lit> MiniSat_assumptions;
173  convert(assumptions, MiniSat_assumptions);
174 
175  if(solver->solve(MiniSat_assumptions))
176  {
177  msg="SAT checker: instance is SATISFIABLE";
178  messaget::status() << msg << messaget::eom;
179  status=SAT;
180  return P_SATISFIABLE;
181  }
182  else
183  msg="SAT checker: instance is UNSATISFIABLE";
184  }
185 
186  messaget::status() << msg << messaget::eom;
187  status=UNSAT;
188  return P_UNSATISFIABLE;
189 }
190 
192 {
193  unsigned v=a.var_no();
194  bool sign=a.sign();
195  solver->model.growTo(v+1);
196  value^=sign;
197  solver->model[v]=lbool(value);
198 }
199 
201 {
202  int v=a.var_no();
203 
204  for(int i=0; i<solver->conflict.size(); i++)
205  {
206  if(var(solver->conflict[i])==v)
207  return true;
208  }
209 
210  return false;
211 }
212 
214 {
215  assumptions=bv;
216 
217  for(bvt::const_iterator it=assumptions.begin();
218  it!=assumptions.end();
219  it++)
220  assert(!it->is_constant());
221 }
222 
224 {
225  empty_clause_added=false;
226  solver=new Solver;
227 }
228 
230 {
232  proof=new Proof(*minisat_proof);
233  // solver=new Solver;
234  solver->proof=proof;
235 }
236 
238 {
239  delete proof;
240  delete minisat_proof;
241 }
242 
244 {
245 }
246 
248 {
249 }
250 
252 {
253  delete solver;
254 }
255 
257 {
258  return "MiniSAT + Proof";
259 }
260 
262 {
264 
266 
267  if(status==UNSAT)
268  {
269  in_core.resize(no_variables(), false);
271  }
272 
273  return r;
274 }
275 
277 {
278  return "MiniSAT + Core";
279 }
280 
282 {
284 }
stepst steps
virtual void lcnf(const bvt &bv) final
static int8_t r
Definition: irep_hash.h:59
class minisat_prooft * minisat_proof
mstreamt & status()
Definition: message.h:238
virtual ~minisat_prooft()
virtual void chain(const vec< ClauseId > &cs, const vec< Var > &xs)
virtual resultt prop_solve() override
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
simple_prooft resolution_proof
virtual void root(const vec< Lit > &c)
void build_core(std::vector< bool > &in_core)
virtual void deleted(ClauseId c)
virtual tvt l_get(literalt a) const override
bool is_true() const
Definition: literal.h:155
virtual void done()
Definition: threeval.h:19
virtual void set_assumptions(const bvt &_assumptions) override
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
simple_prooft & get_resolution_proof()
void convert(const bvt &bv, vec< Lit > &dest)
virtual const std::string solver_text() override
bool sign() const
Definition: literal.h:87
unsigned first_clause_id
virtual resultt prop_solve() override
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual void set_assignment(literalt a, bool value) override
virtual const std::string solver_text() override
std::vector< literalt > bvt
Definition: literal.h:197
virtual bool is_in_conflict(literalt l) const override
virtual const std::string solver_text() override
bool is_false() const
Definition: literal.h:160