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 <stack>
16 
17 #include <util/invariant.h>
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 {
68 
69  try
70  {
71  add_variables();
72  solver->setPolarity(a.var_no(), value);
73  }
74  catch(Glucose::OutOfMemoryException)
75  {
76  messaget::error() << "SAT checker ran out of memory" << eom;
77  status = statust::ERROR;
78  throw std::bad_alloc();
79  }
80 }
81 
83 {
84  return "Glucose Syrup without simplifier";
85 }
86 
88 {
89  return "Glucose Syrup with simplifier";
90 }
91 
92 template<typename T>
94 {
95  while((unsigned)solver->nVars()<no_variables())
96  solver->newVar();
97 }
98 
99 template<typename T>
101 {
102  try
103  {
104  add_variables();
105 
106  forall_literals(it, bv)
107  {
108  if(it->is_true())
109  return;
110  else if(!it->is_false())
111  INVARIANT(
112  it->var_no() < (unsigned)solver->nVars(), "variable not added yet");
113  }
114 
115  Glucose::vec<Glucose::Lit> c;
116 
117  convert(bv, c);
118 
119  // Note the underscore.
120  // Add a clause to the solver without making superflous internal copy.
121 
122  solver->addClause_(c);
123 
124  clause_counter++;
125  }
126  catch(Glucose::OutOfMemoryException)
127  {
128  messaget::error() << "SAT checker ran out of memory" << eom;
129  status = statust::ERROR;
130  throw std::bad_alloc();
131  }
132 }
133 
134 template<typename T>
136 {
137  PRECONDITION(status != statust::ERROR);
138 
139  // We start counting at 1, thus there is one variable fewer.
140  {
141  messaget::status() <<
142  (no_variables()-1) << " variables, " <<
143  solver->nClauses() << " clauses" << eom;
144  }
145 
146  try
147  {
148  add_variables();
149 
150  if(!solver->okay())
151  {
153  << "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
154  }
155  else
156  {
157  // if assumptions contains false, we need this to be UNSAT
158  bool has_false = false;
159 
160  forall_literals(it, assumptions)
161  if(it->is_false())
162  has_false = true;
163 
164  if(has_false)
165  {
167  << "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
168  }
169  else
170  {
171  Glucose::vec<Glucose::Lit> solver_assumptions;
172  convert(assumptions, solver_assumptions);
173 
174  if(solver->solve(solver_assumptions))
175  {
176  messaget::status() << "SAT checker: instance is SATISFIABLE" << eom;
177  status = statust::SAT;
178  return resultt::P_SATISFIABLE;
179  }
180  else
181  {
182  messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom;
183  }
184  }
185  }
186 
187  status = statust::UNSAT;
188  return resultt::P_UNSATISFIABLE;
189  }
190  catch(Glucose::OutOfMemoryException)
191  {
192  messaget::error() << "SAT checker ran out of memory" << eom;
193  status = statust::ERROR;
194  throw std::bad_alloc();
195  }
196 }
197 
198 template<typename T>
200 {
202 
203  try
204  {
205  unsigned v = a.var_no();
206  bool sign = a.sign();
207 
208  // MiniSat2 kills the model in case of UNSAT
209  solver->model.growTo(v + 1);
210  value ^= sign;
211  solver->model[v] = Glucose::lbool(value);
212  }
213  catch(Glucose::OutOfMemoryException)
214  {
215  messaget::error() << "SAT checker ran out of memory" << eom;
216  status = statust::ERROR;
217  throw std::bad_alloc();
218  }
219 }
220 
221 template<typename T>
223  solver(_solver)
224 {
225 }
226 
227 template<>
229 {
230  delete solver;
231 }
232 
233 template<>
235 {
236  delete solver;
237 }
238 
239 template<typename T>
241 {
242  int v=a.var_no();
243 
244  for(int i=0; i<solver->conflict.size(); i++)
245  if(var(solver->conflict[i])==v)
246  return true;
247 
248  return false;
249 }
250 
251 template<typename T>
253 {
254  assumptions=bv;
255 
256  forall_literals(it, assumptions)
257  INVARIANT(!it->is_constant(), "assumption literals must not be constant");
258 }
259 
261  satcheck_glucose_baset<Glucose::Solver>(new Glucose::Solver)
262 {
263 }
264 
266  satcheck_glucose_baset<Glucose::SimpSolver>(new Glucose::SimpSolver)
267 {
268 }
269 
271 {
272  try
273  {
274  if(!a.is_constant())
275  {
276  add_variables();
277  solver->setFrozen(a.var_no(), true);
278  }
279  }
280  catch(Glucose::OutOfMemoryException)
281  {
282  messaget::error() << "SAT checker ran out of memory" << eom;
284  throw std::bad_alloc();
285  }
286 }
287 
289 {
291 
292  return solver->isEliminated(a.var_no());
293 }
satcheck_glucose_baset
Definition: satcheck_glucose.h:27
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
satcheck_glucose_simplifiert::set_frozen
virtual void set_frozen(literalt a)
Definition: satcheck_glucose.cpp:270
satcheck_glucose_baset::prop_solve
virtual resultt prop_solve()
Definition: satcheck_glucose.cpp:135
satcheck_glucose_baset::add_variables
void add_variables()
Definition: satcheck_glucose.cpp:93
satcheck_glucose_baset::lcnf
virtual void lcnf(const bvt &bv)
Definition: satcheck_glucose.cpp:100
bvt
std::vector< literalt > bvt
Definition: literal.h:200
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:401
satcheck_glucose_baset::solver
T * solver
Definition: satcheck_glucose.h:50
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
invariant.h
messaget::eom
static eomt eom
Definition: message.h:284
satcheck_glucose.h
literalt::var_no
var_not var_no() const
Definition: literal.h:82
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:202
cnf_solvert::statust::ERROR
literalt::is_true
bool is_true() const
Definition: literal.h:155
messaget::error
mstreamt & error() const
Definition: message.h:386
Glucose
Definition: satcheck_glucose.h:20
satcheck_glucose_simplifiert::solver_text
virtual const std::string solver_text()
Definition: satcheck_glucose.cpp:87
literalt::is_false
bool is_false() const
Definition: literal.h:160
satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert
satcheck_glucose_no_simplifiert()
Definition: satcheck_glucose.cpp:260
satcheck_glucose_no_simplifiert::solver_text
virtual const std::string solver_text()
Definition: satcheck_glucose.cpp:82
propt::resultt
resultt
Definition: prop.h:96
satcheck_glucose_simplifiert::satcheck_glucose_simplifiert
satcheck_glucose_simplifiert()
Definition: satcheck_glucose.cpp:265
tvt
Definition: threeval.h:19
literalt::sign
bool sign() const
Definition: literal.h:87
convert
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
Definition: satcheck_glucose.cpp:27
satcheck_glucose_baset::is_in_conflict
virtual bool is_in_conflict(literalt a) const
Returns true if an assumption is in the final conflict.
Definition: satcheck_glucose.cpp:240
satcheck_glucose_baset::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: satcheck_glucose.cpp:252
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
literalt
Definition: literal.h:24
satcheck_glucose_baset::set_assignment
virtual void set_assignment(literalt a, bool value)
Definition: satcheck_glucose.cpp:199
satcheck_glucose_baset::~satcheck_glucose_baset
virtual ~satcheck_glucose_baset()
satcheck_glucose_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_glucose.cpp:288
satcheck_glucose_baset::satcheck_glucose_baset
satcheck_glucose_baset(T *)
Definition: satcheck_glucose.cpp:222
tvt::tv_enumt::TV_UNKNOWN
satcheck_glucose_baset::l_get
virtual tvt l_get(literalt a) const
Definition: satcheck_glucose.cpp:37
literalt::is_constant
bool is_constant() const
Definition: literal.h:165
satcheck_glucose_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_glucose.cpp:65