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  for(const auto &literal : bv)
32  {
33  if(!literal.is_false())
34  dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
35  }
36 }
37 
38 template<typename T>
40 {
41  if(a.is_true())
42  return tvt(true);
43  else if(a.is_false())
44  return tvt(false);
45 
46  tvt result;
47 
48  if(a.var_no()>=(unsigned)solver->model.size())
50 
51  using Glucose::lbool;
52 
53  if(solver->model[a.var_no()]==l_True)
54  result=tvt(true);
55  else if(solver->model[a.var_no()]==l_False)
56  result=tvt(false);
57  else
59 
60  if(a.sign())
61  result=!result;
62 
63  return result;
64 }
65 
66 template<typename T>
68 {
70 
71  try
72  {
73  add_variables();
74  solver->setPolarity(a.var_no(), value);
75  }
76  catch(Glucose::OutOfMemoryException)
77  {
78  log.error() << "SAT checker ran out of memory" << messaget::eom;
79  status = statust::ERROR;
80  throw std::bad_alloc();
81  }
82 }
83 
85 {
86  return "Glucose Syrup without simplifier";
87 }
88 
90 {
91  return "Glucose Syrup with simplifier";
92 }
93 
94 template<typename T>
96 {
97  while((unsigned)solver->nVars()<no_variables())
98  solver->newVar();
99 }
100 
101 template<typename T>
103 {
104  try
105  {
106  add_variables();
107 
108  for(const auto &literal : bv)
109  {
110  if(literal.is_true())
111  return;
112  else if(!literal.is_false())
113  {
114  INVARIANT(
115  literal.var_no() < (unsigned)solver->nVars(),
116  "variable not added yet");
117  }
118  }
119 
120  Glucose::vec<Glucose::Lit> c;
121 
122  convert(bv, c);
123 
124  // Note the underscore.
125  // Add a clause to the solver without making superflous internal copy.
126 
127  solver->addClause_(c);
128 
129  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
130  // To map clauses to lines of program code, track clause indices in the
131  // dimacs cnf output. Dimacs output is generated after processing
132  // clauses to remove duplicates and clauses that are trivially true.
133  // Here, a clause is checked to see if it can be thus eliminated. If
134  // not, add the clause index to list of clauses in
135  // solver_hardnesst::register_clause().
136  static size_t cnf_clause_index = 0;
137  bvt cnf;
138  bool clause_removed = process_clause(bv, cnf);
139 
140  if(!clause_removed)
141  cnf_clause_index++;
142 
143  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
144  });
145 
146  clause_counter++;
147  }
148  catch(Glucose::OutOfMemoryException)
149  {
150  log.error() << "SAT checker ran out of memory" << messaget::eom;
151  status = statust::ERROR;
152  throw std::bad_alloc();
153  }
154 }
155 
156 template <typename T>
158 {
159  PRECONDITION(status != statust::ERROR);
160 
161  // We start counting at 1, thus there is one variable fewer.
162  log.statistics() << (no_variables() - 1) << " variables, "
163  << solver->nClauses() << " clauses" << messaget::eom;
164 
165  try
166  {
167  add_variables();
168 
169  if(!solver->okay())
170  {
171  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
172  << messaget::eom;
173  }
174  else
175  {
176  // if assumptions contains false, we need this to be UNSAT
177  bool has_false = false;
178 
179  for(const auto &literal : assumptions)
180  {
181  if(literal.is_false())
182  has_false = true;
183  }
184 
185  if(has_false)
186  {
187  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
188  << messaget::eom;
189  }
190  else
191  {
192  Glucose::vec<Glucose::Lit> solver_assumptions;
193  convert(assumptions, solver_assumptions);
194 
195  if(solver->solve(solver_assumptions))
196  {
197  log.status() << "SAT checker: instance is SATISFIABLE"
198  << messaget::eom;
199  status = statust::SAT;
200  return resultt::P_SATISFIABLE;
201  }
202  else
203  {
204  log.status() << "SAT checker: instance is UNSATISFIABLE"
205  << messaget::eom;
206  }
207  }
208  }
209 
210  status = statust::UNSAT;
211  return resultt::P_UNSATISFIABLE;
212  }
213  catch(Glucose::OutOfMemoryException)
214  {
215  log.error() << "SAT checker ran out of memory" << messaget::eom;
216  status = statust::ERROR;
217  throw std::bad_alloc();
218  }
219 }
220 
221 template<typename T>
223 {
225 
226  try
227  {
228  unsigned v = a.var_no();
229  bool sign = a.sign();
230 
231  // MiniSat2 kills the model in case of UNSAT
232  solver->model.growTo(v + 1);
233  value ^= sign;
234  solver->model[v] = Glucose::lbool(value);
235  }
236  catch(Glucose::OutOfMemoryException)
237  {
238  log.error() << "SAT checker ran out of memory" << messaget::eom;
239  status = statust::ERROR;
240  throw std::bad_alloc();
241  }
242 }
243 
244 template <typename T>
246  T *_solver,
247  message_handlert &message_handler)
248  : cnf_solvert(message_handler), solver(_solver)
249 {
250 }
251 
252 template<>
254 {
255  delete solver;
256 }
257 
258 template<>
260 {
261  delete solver;
262 }
263 
264 template<typename T>
266 {
267  int v=a.var_no();
268 
269  for(int i=0; i<solver->conflict.size(); i++)
270  if(var(solver->conflict[i])==v)
271  return true;
272 
273  return false;
274 }
275 
276 template<typename T>
278 {
279  assumptions=bv;
280 
281  for(const auto &literal : assumptions)
282  {
283  INVARIANT(
284  !literal.is_constant(), "assumption literals must not be constant");
285  }
286 }
287 
289  message_handlert &message_handler)
290  : satcheck_glucose_baset<Glucose::Solver>(
291  new Glucose::Solver,
292  message_handler)
293 {
294 }
295 
297  message_handlert &message_handler)
298  : satcheck_glucose_baset<Glucose::SimpSolver>(
299  new Glucose::SimpSolver,
300  message_handler)
301 {
302 }
303 
305 {
306  try
307  {
308  if(!a.is_constant())
309  {
310  add_variables();
311  solver->setFrozen(a.var_no(), true);
312  }
313  }
314  catch(Glucose::OutOfMemoryException)
315  {
316  log.error() << "SAT checker ran out of memory" << messaget::eom;
318  throw std::bad_alloc();
319  }
320 }
321 
323 {
325 
326  return solver->isEliminated(a.var_no());
327 }
statust status
Definition: cnf.h:86
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
bool is_constant() const
Definition: literal.h:166
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
resultt
Definition: prop.h:99
messaget log
Definition: prop.h:130
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
satcheck_glucose_baset(T *, message_handlert &message_handler)
void set_assumptions(const bvt &_assumptions) override
void lcnf(const bvt &bv) override
void set_polarity(literalt a, bool value)
resultt do_prop_solve() override
virtual ~satcheck_glucose_baset()
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
satcheck_glucose_no_simplifiert(message_handlert &message_handler)
const std::string solver_text() override
satcheck_glucose_simplifiert(message_handlert &message_handler)
void set_frozen(literalt a) override
bool is_eliminated(literalt a) const
Definition: threeval.h:20
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
std::vector< literalt > bvt
Definition: literal.h:201
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
A structure that facilitates collecting the complexity statistics from a decision procedure.
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.