cprover
satcheck_glucose.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_glucose.h"
10 
11 #ifndef _MSC_VER
12 #include <inttypes.h>
13 #endif
14 
15 #include <cassert>
16 #include <stack>
17 
18 #include <util/threeval.h>
19 
20 #include <core/Solver.h>
21 #include <simp/SimpSolver.h>
22 
23 #ifndef HAVE_GLUCOSE
24 #error "Expected HAVE_GLUCOSE"
25 #endif
26 
27 void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
28 {
29  dest.capacity(bv.size());
30 
31  forall_literals(it, bv)
32  if(!it->is_false())
33  dest.push(Glucose::mkLit(it->var_no(), it->sign()));
34 }
35 
36 template<typename T>
38 {
39  if(a.is_true())
40  return tvt(true);
41  else if(a.is_false())
42  return tvt(false);
43 
44  tvt result;
45 
46  if(a.var_no()>=(unsigned)solver->model.size())
48 
49  using Glucose::lbool;
50 
51  if(solver->model[a.var_no()]==l_True)
52  result=tvt(true);
53  else if(solver->model[a.var_no()]==l_False)
54  result=tvt(false);
55  else
57 
58  if(a.sign())
59  result=!result;
60 
61  return result;
62 }
63 
64 template<typename T>
66 {
67  assert(!a.is_constant());
68  add_variables();
69  solver->setPolarity(a.var_no(), value);
70 }
71 
73 {
74  return "Glucose Syrup without simplifier";
75 }
76 
78 {
79  return "Glucose Syrup with simplifier";
80 }
81 
82 template<typename T>
84 {
85  while((unsigned)solver->nVars()<no_variables())
86  solver->newVar();
87 }
88 
89 template<typename T>
91 {
92  add_variables();
93 
94  forall_literals(it, bv)
95  {
96  if(it->is_true())
97  return;
98  else if(!it->is_false())
99  assert(it->var_no()<(unsigned)solver->nVars());
100  }
101 
102  Glucose::vec<Glucose::Lit> c;
103 
104  convert(bv, c);
105 
106  // Note the underscore.
107  // Add a clause to the solver without making superflous internal copy.
108 
109  solver->addClause_(c);
110 
111  clause_counter++;
112 }
113 
114 template<typename T>
116 {
117  assert(status!=ERROR);
118 
119  // We start counting at 1, thus there is one variable fewer.
120  {
121  messaget::status() <<
122  (no_variables()-1) << " variables, " <<
123  solver->nClauses() << " clauses" << eom;
124  }
125 
126  add_variables();
127 
128  if(!solver->okay())
129  {
130  messaget::status() <<
131  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
132  }
133  else
134  {
135  // if assumptions contains false, we need this to be UNSAT
136  bool has_false=false;
137 
138  forall_literals(it, assumptions)
139  if(it->is_false())
140  has_false=true;
141 
142  if(has_false)
143  {
144  messaget::status() <<
145  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
146  }
147  else
148  {
149  Glucose::vec<Glucose::Lit> solver_assumptions;
150  convert(assumptions, solver_assumptions);
151 
152  if(solver->solve(solver_assumptions))
153  {
154  messaget::status() <<
155  "SAT checker: instance is SATISFIABLE" << eom;
156  assert(!solver->model.empty());
157  status=SAT;
158  return P_SATISFIABLE;
159  }
160  else
161  {
162  messaget::status() <<
163  "SAT checker: instance is UNSATISFIABLE" << eom;
164  }
165  }
166  }
167 
168  status=UNSAT;
169  return P_UNSATISFIABLE;
170 }
171 
172 template<typename T>
174 {
175  assert(!a.is_constant());
176 
177  unsigned v=a.var_no();
178  bool sign=a.sign();
179 
180  // MiniSat2 kills the model in case of UNSAT
181  solver->model.growTo(v+1);
182  value^=sign;
183  solver->model[v]=Glucose::lbool(value);
184 }
185 
186 template<typename T>
188  solver(_solver)
189 {
190 }
191 
192 template<>
194 {
195  delete solver;
196 }
197 
198 template<>
200 {
201  delete solver;
202 }
203 
204 template<typename T>
206 {
207  int v=a.var_no();
208 
209  for(int i=0; i<solver->conflict.size(); i++)
210  if(var(solver->conflict[i])==v)
211  return true;
212 
213  return false;
214 }
215 
216 template<typename T>
218 {
219  assumptions=bv;
220 
221  forall_literals(it, assumptions)
222  assert(!it->is_constant());
223 }
224 
226  satcheck_glucose_baset<Glucose::Solver>(new Glucose::Solver)
227 {
228 }
229 
231  satcheck_glucose_baset<Glucose::SimpSolver>(new Glucose::SimpSolver)
232 {
233 }
234 
236 {
237  if(!a.is_constant())
238  {
239  add_variables();
240  solver->setFrozen(a.var_no(), true);
241  }
242 }
243 
245 {
246  assert(!a.is_constant());
247 
248  return solver->isEliminated(a.var_no());
249 }
mstreamt & status()
Definition: message.h:238
#define forall_literals(it, bv)
Definition: literal.h:199
virtual resultt prop_solve()
bool is_true() const
Definition: literal.h:155
virtual const std::string solver_text()
virtual void set_frozen(literalt a)
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
virtual void set_assumptions(const bvt &_assumptions)
virtual ~satcheck_glucose_baset()
bool is_eliminated(literalt a) const
virtual const std::string solver_text()
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
bool is_constant() const
Definition: literal.h:165
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
bool sign() const
Definition: literal.h:87
virtual bool is_in_conflict(literalt a) const
std::vector< literalt > bvt
Definition: literal.h:197
void set_polarity(literalt a, bool value)
virtual void lcnf(const bvt &bv)
bool is_false() const
Definition: literal.h:160