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  log.error() << "SAT checker ran out of memory" << messaget::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  log.error() << "SAT checker ran out of memory" << messaget::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  log.statistics() << (no_variables() - 1) << " variables, "
141  << solver->nClauses() << " clauses" << messaget::eom;
142 
143  try
144  {
145  add_variables();
146 
147  if(!solver->okay())
148  {
149  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
150  << messaget::eom;
151  }
152  else
153  {
154  // if assumptions contains false, we need this to be UNSAT
155  bool has_false = false;
156 
157  forall_literals(it, assumptions)
158  if(it->is_false())
159  has_false = true;
160 
161  if(has_false)
162  {
163  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
164  << messaget::eom;
165  }
166  else
167  {
168  Glucose::vec<Glucose::Lit> solver_assumptions;
169  convert(assumptions, solver_assumptions);
170 
171  if(solver->solve(solver_assumptions))
172  {
173  log.status() << "SAT checker: instance is SATISFIABLE"
174  << messaget::eom;
175  status = statust::SAT;
176  return resultt::P_SATISFIABLE;
177  }
178  else
179  {
180  log.status() << "SAT checker: instance is UNSATISFIABLE"
181  << messaget::eom;
182  }
183  }
184  }
185 
186  status = statust::UNSAT;
187  return resultt::P_UNSATISFIABLE;
188  }
189  catch(Glucose::OutOfMemoryException)
190  {
191  log.error() << "SAT checker ran out of memory" << messaget::eom;
192  status = statust::ERROR;
193  throw std::bad_alloc();
194  }
195 }
196 
197 template<typename T>
199 {
201 
202  try
203  {
204  unsigned v = a.var_no();
205  bool sign = a.sign();
206 
207  // MiniSat2 kills the model in case of UNSAT
208  solver->model.growTo(v + 1);
209  value ^= sign;
210  solver->model[v] = Glucose::lbool(value);
211  }
212  catch(Glucose::OutOfMemoryException)
213  {
214  log.error() << "SAT checker ran out of memory" << messaget::eom;
215  status = statust::ERROR;
216  throw std::bad_alloc();
217  }
218 }
219 
220 template <typename T>
222  T *_solver,
223  message_handlert &message_handler)
224  : cnf_solvert(message_handler), solver(_solver)
225 {
226 }
227 
228 template<>
230 {
231  delete solver;
232 }
233 
234 template<>
236 {
237  delete solver;
238 }
239 
240 template<typename T>
242 {
243  int v=a.var_no();
244 
245  for(int i=0; i<solver->conflict.size(); i++)
246  if(var(solver->conflict[i])==v)
247  return true;
248 
249  return false;
250 }
251 
252 template<typename T>
254 {
255  assumptions=bv;
256 
257  forall_literals(it, assumptions)
258  INVARIANT(!it->is_constant(), "assumption literals must not be constant");
259 }
260 
262  message_handlert &message_handler)
263  : satcheck_glucose_baset<Glucose::Solver>(
264  new Glucose::Solver,
265  message_handler)
266 {
267 }
268 
270  message_handlert &message_handler)
271  : satcheck_glucose_baset<Glucose::SimpSolver>(
272  new Glucose::SimpSolver,
273  message_handler)
274 {
275 }
276 
278 {
279  try
280  {
281  if(!a.is_constant())
282  {
283  add_variables();
284  solver->setFrozen(a.var_no(), true);
285  }
286  }
287  catch(Glucose::OutOfMemoryException)
288  {
289  log.error() << "SAT checker ran out of memory" << messaget::eom;
291  throw std::bad_alloc();
292  }
293 }
294 
296 {
298 
299  return solver->isEliminated(a.var_no());
300 }
satcheck_glucose_baset
Definition: satcheck_glucose.h:28
satcheck_glucose_simplifiert::set_frozen
void set_frozen(literalt a) override
Definition: satcheck_glucose.cpp:277
satcheck_glucose_simplifiert::satcheck_glucose_simplifiert
satcheck_glucose_simplifiert(message_handlert &message_handler)
Definition: satcheck_glucose.cpp:269
satcheck_glucose_baset::satcheck_glucose_baset
satcheck_glucose_baset(T *, message_handlert &message_handler)
Definition: satcheck_glucose.cpp:221
satcheck_glucose_baset::add_variables
void add_variables()
Definition: satcheck_glucose.cpp:93
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
satcheck_glucose_baset::solver
T * solver
Definition: satcheck_glucose.h:57
invariant.h
satcheck_glucose_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_glucose.cpp:198
messaget::eom
static eomt eom
Definition: message.h:297
satcheck_glucose.h
literalt::var_no
var_not var_no() const
Definition: literal.h:83
satcheck_glucose_baset::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: satcheck_glucose.cpp:253
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
cnf_solvert
Definition: cnf.h:70
cnf_solvert::statust::ERROR
@ ERROR
literalt::is_true
bool is_true() const
Definition: literal.h:156
messaget::error
mstreamt & error() const
Definition: message.h:399
Glucose
Definition: satcheck_glucose.h:21
cnf_solvert::status
statust status
Definition: cnf.h:84
satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert
satcheck_glucose_no_simplifiert(message_handlert &message_handler)
Definition: satcheck_glucose.cpp:261
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
literalt::is_false
bool is_false() const
Definition: literal.h:161
satcheck_glucose_baset::l_get
tvt l_get(literalt a) const override
Definition: satcheck_glucose.cpp:37
satcheck_glucose_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_glucose.cpp:87
satcheck_glucose_baset::is_in_conflict
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
Definition: satcheck_glucose.cpp:241
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
satcheck_glucose_no_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_glucose.cpp:82
tvt
Definition: threeval.h:20
literalt::sign
bool sign() const
Definition: literal.h:88
convert
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
Definition: satcheck_glucose.cpp:27
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
literalt
Definition: literal.h:26
satcheck_glucose_baset::~satcheck_glucose_baset
virtual ~satcheck_glucose_baset()
satcheck_glucose_baset::lcnf
void lcnf(const bvt &bv) override
Definition: satcheck_glucose.cpp:100
satcheck_glucose_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_glucose.cpp:295
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
propt::log
messaget log
Definition: prop.h:130
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
satcheck_glucose_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_glucose.cpp:135
satcheck_glucose_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_glucose.cpp:65