16#include <core/Solver.h>
17#include <simp/SimpSolver.h>
20#error "Expected HAVE_GLUCOSE"
23void convert(
const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
25 dest.capacity(bv.size());
27 for(
const auto &literal : bv)
29 if(!literal.is_false())
30 dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
36 dest.capacity(bv.size());
38 for(
const auto &literal : bv)
40 if(!literal.is_true())
41 dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
83 catch(Glucose::OutOfMemoryException)
87 throw std::bad_alloc();
93 return "Glucose Syrup without simplifier";
98 return "Glucose Syrup with simplifier";
115 for(
const auto &literal : bv)
117 if(literal.is_true())
119 else if(!literal.is_false())
122 literal.var_no() < (
unsigned)
solver->nVars(),
123 "variable not added yet");
127 Glucose::vec<Glucose::Lit> c;
144 static size_t cnf_clause_index = 0;
152 bv, cnf, cnf_clause_index, !clause_removed);
157 catch(Glucose::OutOfMemoryException)
161 throw std::bad_alloc();
180 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
186 bool has_false =
false;
188 for(
const auto &literal : assumptions)
190 if(literal.is_false())
196 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
201 Glucose::vec<Glucose::Lit> solver_assumptions;
204 if(
solver->solve(solver_assumptions))
206 log.status() <<
"SAT checker: instance is SATISFIABLE"
213 log.status() <<
"SAT checker: instance is UNSATISFIABLE"
222 catch(Glucose::OutOfMemoryException)
226 throw std::bad_alloc();
238 bool sign = a.
sign();
241 solver->model.growTo(v + 1);
243 solver->model[v] = Glucose::lbool(value);
245 catch(Glucose::OutOfMemoryException)
249 throw std::bad_alloc();
268 for(
int i=0; i<
solver->conflict.size(); i++)
269 if(var(
solver->conflict[i])==v)
288 catch(Glucose::OutOfMemoryException)
292 throw std::bad_alloc();
cnf_solvert(message_handlert &message_handler)
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual size_t no_variables() const override
std::unique_ptr< clause_hardness_collectort > solver_hardness
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
~satcheck_glucose_baset() override
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly ...
void lcnf(const bvt &bv) override
std::unique_ptr< Glucose::Solver > solver
void set_polarity(literalt a, bool value)
satcheck_glucose_baset(message_handlert &message_handler)
tvt l_get(literalt a) const override
resultt do_prop_solve(const bvt &assumptions) override
void set_assignment(literalt a, bool value) override
std::string solver_text() const override
void set_frozen(literalt a) override
std::string solver_text() const override
bool is_eliminated(literalt a) const
std::vector< literalt > bvt
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
void convert_assumptions(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.