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 #include <stack>
12 
13 #include <util/invariant.h>
14 #include <util/make_unique.h>
15 #include <util/threeval.h>
16 
17 #include <core/Solver.h>
18 #include <simp/SimpSolver.h>
19 
20 #ifndef HAVE_GLUCOSE
21 #error "Expected HAVE_GLUCOSE"
22 #endif
23 
24 void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
25 {
26  dest.capacity(bv.size());
27 
28  for(const auto &literal : bv)
29  {
30  if(!literal.is_false())
31  dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
32  }
33 }
34 
35 template<typename T>
37 {
38  if(a.is_true())
39  return tvt(true);
40  else if(a.is_false())
41  return tvt(false);
42 
43  tvt result;
44 
45  if(a.var_no()>=(unsigned)solver->model.size())
47 
48  using Glucose::lbool;
49 
50  if(solver->model[a.var_no()]==l_True)
51  result=tvt(true);
52  else if(solver->model[a.var_no()]==l_False)
53  result=tvt(false);
54  else
56 
57  if(a.sign())
58  result=!result;
59 
60  return result;
61 }
62 
63 template<typename T>
65 {
67 
68  try
69  {
70  add_variables();
71  solver->setPolarity(a.var_no(), value);
72  }
73  catch(Glucose::OutOfMemoryException)
74  {
75  log.error() << "SAT checker ran out of memory" << messaget::eom;
76  status = statust::ERROR;
77  throw std::bad_alloc();
78  }
79 }
80 
82 {
83  return "Glucose Syrup without simplifier";
84 }
85 
87 {
88  return "Glucose Syrup with simplifier";
89 }
90 
91 template<typename T>
93 {
94  while((unsigned)solver->nVars()<no_variables())
95  solver->newVar();
96 }
97 
98 template<typename T>
100 {
101  try
102  {
103  add_variables();
104 
105  for(const auto &literal : bv)
106  {
107  if(literal.is_true())
108  return;
109  else if(!literal.is_false())
110  {
111  INVARIANT(
112  literal.var_no() < (unsigned)solver->nVars(),
113  "variable not added yet");
114  }
115  }
116 
117  Glucose::vec<Glucose::Lit> c;
118 
119  convert(bv, c);
120 
121  // Note the underscore.
122  // Add a clause to the solver without making superflous internal copy.
123 
124  solver->addClause_(c);
125 
126  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
127  // To map clauses to lines of program code, track clause indices in the
128  // dimacs cnf output. Dimacs output is generated after processing
129  // clauses to remove duplicates and clauses that are trivially true.
130  // Here, a clause is checked to see if it can be thus eliminated. If
131  // not, add the clause index to list of clauses in
132  // solver_hardnesst::register_clause().
133  static size_t cnf_clause_index = 0;
134  bvt cnf;
135  bool clause_removed = process_clause(bv, cnf);
136 
137  if(!clause_removed)
138  cnf_clause_index++;
139 
140  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
141  });
142 
143  clause_counter++;
144  }
145  catch(Glucose::OutOfMemoryException)
146  {
147  log.error() << "SAT checker ran out of memory" << messaget::eom;
148  status = statust::ERROR;
149  throw std::bad_alloc();
150  }
151 }
152 
153 template <typename T>
155 {
156  PRECONDITION(status != statust::ERROR);
157 
158  // We start counting at 1, thus there is one variable fewer.
159  log.statistics() << (no_variables() - 1) << " variables, "
160  << solver->nClauses() << " clauses" << messaget::eom;
161 
162  try
163  {
164  add_variables();
165 
166  if(!solver->okay())
167  {
168  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
169  << messaget::eom;
170  }
171  else
172  {
173  // if assumptions contains false, we need this to be UNSAT
174  bool has_false = false;
175 
176  for(const auto &literal : assumptions)
177  {
178  if(literal.is_false())
179  has_false = true;
180  }
181 
182  if(has_false)
183  {
184  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
185  << messaget::eom;
186  }
187  else
188  {
189  Glucose::vec<Glucose::Lit> solver_assumptions;
190  convert(assumptions, solver_assumptions);
191 
192  if(solver->solve(solver_assumptions))
193  {
194  log.status() << "SAT checker: instance is SATISFIABLE"
195  << messaget::eom;
196  status = statust::SAT;
197  return resultt::P_SATISFIABLE;
198  }
199  else
200  {
201  log.status() << "SAT checker: instance is UNSATISFIABLE"
202  << messaget::eom;
203  }
204  }
205  }
206 
207  status = statust::UNSAT;
208  return resultt::P_UNSATISFIABLE;
209  }
210  catch(Glucose::OutOfMemoryException)
211  {
212  log.error() << "SAT checker ran out of memory" << messaget::eom;
213  status = statust::ERROR;
214  throw std::bad_alloc();
215  }
216 }
217 
218 template<typename T>
220 {
222 
223  try
224  {
225  unsigned v = a.var_no();
226  bool sign = a.sign();
227 
228  // MiniSat2 kills the model in case of UNSAT
229  solver->model.growTo(v + 1);
230  value ^= sign;
231  solver->model[v] = Glucose::lbool(value);
232  }
233  catch(Glucose::OutOfMemoryException)
234  {
235  log.error() << "SAT checker ran out of memory" << messaget::eom;
236  status = statust::ERROR;
237  throw std::bad_alloc();
238  }
239 }
240 
241 template <typename T>
243  message_handlert &message_handler)
244  : cnf_solvert(message_handler), solver(util_make_unique<T>())
245 {
246 }
247 
248 template <typename T>
250 
251 template<typename T>
253 {
254  int v=a.var_no();
255 
256  for(int i=0; i<solver->conflict.size(); i++)
257  if(var(solver->conflict[i])==v)
258  return true;
259 
260  return false;
261 }
262 
263 template<typename T>
265 {
266  assumptions=bv;
267 
268  for(const auto &literal : assumptions)
269  {
270  INVARIANT(
271  !literal.is_constant(), "assumption literals must not be constant");
272  }
273 }
274 
277 
279 {
280  try
281  {
282  if(!a.is_constant())
283  {
284  add_variables();
285  solver->setFrozen(a.var_no(), true);
286  }
287  }
288  catch(Glucose::OutOfMemoryException)
289  {
290  log.error() << "SAT checker ran out of memory" << messaget::eom;
292  throw std::bad_alloc();
293  }
294 }
295 
297 {
299 
300  return solver->isEliminated(a.var_no());
301 }
satcheck_glucose_baset< Glucose::Solver >
satcheck_glucose_simplifiert::set_frozen
void set_frozen(literalt a) override
Definition: satcheck_glucose.cpp:278
satcheck_glucose_baset::~satcheck_glucose_baset
~satcheck_glucose_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
satcheck_glucose_baset::add_variables
void add_variables()
Definition: satcheck_glucose.cpp:92
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
invariant.h
satcheck_glucose_baset::set_assignment
void set_assignment(literalt a, bool value) override
Definition: satcheck_glucose.cpp:219
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:264
satcheck_glucose_baset< Glucose::SimpSolver >::solver
std::unique_ptr< Glucose::SimpSolver > solver
Definition: satcheck_glucose.h:77
cnf_solvert
Definition: cnf.h:73
cnf_solvert::statust::ERROR
@ ERROR
solver_hardnesst::register_clause
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.
Definition: solver_hardness.cpp:87
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
literalt::is_true
bool is_true() const
Definition: literal.h:156
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
cnf_solvert::status
statust status
Definition: cnf.h:87
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:36
satcheck_glucose_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_glucose.cpp:86
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:252
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:97
satcheck_glucose_no_simplifiert::solver_text
const std::string solver_text() override
Definition: satcheck_glucose.cpp:81
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:24
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:42
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:407
literalt
Definition: literal.h:26
satcheck_glucose_baset::lcnf
void lcnf(const bvt &bv) override
Definition: satcheck_glucose.cpp:99
satcheck_glucose_simplifiert::is_eliminated
bool is_eliminated(literalt a) const
Definition: satcheck_glucose.cpp:296
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
satcheck_glucose_baset::satcheck_glucose_baset
satcheck_glucose_baset(message_handlert &message_handler)
Definition: satcheck_glucose.cpp:242
propt::log
messaget log
Definition: prop.h:128
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:423
satcheck_glucose_baset::do_prop_solve
resultt do_prop_solve() override
Definition: satcheck_glucose.cpp:154
satcheck_glucose_baset::set_polarity
void set_polarity(literalt a, bool value)
Definition: satcheck_glucose.cpp:64
with_solver_hardness
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
Definition: hardness_collector.h:32