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