Go to the documentation of this file.
20 #include <core/Solver.h>
21 #include <simp/SimpSolver.h>
24 #error "Expected HAVE_GLUCOSE"
27 void convert(
const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
29 dest.capacity(bv.size());
33 dest.push(Glucose::mkLit(it->var_no(), it->sign()));
74 catch(Glucose::OutOfMemoryException)
76 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
77 status = statust::ERROR;
78 throw std::bad_alloc();
84 return "Glucose Syrup without simplifier";
89 return "Glucose Syrup with simplifier";
95 while((
unsigned)
solver->nVars()<no_variables())
110 else if(!it->is_false())
112 it->var_no() < (
unsigned)
solver->nVars(),
"variable not added yet");
115 Glucose::vec<Glucose::Lit> c;
126 catch(Glucose::OutOfMemoryException)
128 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
129 status = statust::ERROR;
130 throw std::bad_alloc();
134 template <
typename T>
140 log.statistics() << (no_variables() - 1) <<
" variables, "
149 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
155 bool has_false =
false;
163 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
168 Glucose::vec<Glucose::Lit> solver_assumptions;
169 convert(assumptions, solver_assumptions);
171 if(
solver->solve(solver_assumptions))
173 log.status() <<
"SAT checker: instance is SATISFIABLE"
175 status = statust::SAT;
176 return resultt::P_SATISFIABLE;
180 log.status() <<
"SAT checker: instance is UNSATISFIABLE"
186 status = statust::UNSAT;
187 return resultt::P_UNSATISFIABLE;
189 catch(Glucose::OutOfMemoryException)
191 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
192 status = statust::ERROR;
193 throw std::bad_alloc();
205 bool sign = a.
sign();
208 solver->model.growTo(v + 1);
210 solver->model[v] = Glucose::lbool(value);
212 catch(Glucose::OutOfMemoryException)
214 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
215 status = statust::ERROR;
216 throw std::bad_alloc();
220 template <
typename T>
245 for(
int i=0; i<
solver->conflict.size(); i++)
246 if(var(
solver->conflict[i])==v)
258 INVARIANT(!it->is_constant(),
"assumption literals must not be constant");
287 catch(Glucose::OutOfMemoryException)
291 throw std::bad_alloc();
void set_frozen(literalt a) override
satcheck_glucose_simplifiert(message_handlert &message_handler)
satcheck_glucose_baset(T *, message_handlert &message_handler)
std::vector< literalt > bvt
void set_assignment(literalt a, bool value) override
void set_assumptions(const bvt &_assumptions) override
#define forall_literals(it, bv)
satcheck_glucose_no_simplifiert(message_handlert &message_handler)
#define PRECONDITION(CONDITION)
tvt l_get(literalt a) const override
const std::string solver_text() override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
const std::string solver_text() override
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
int solver(std::istream &in)
virtual ~satcheck_glucose_baset()
void lcnf(const bvt &bv) override
bool is_eliminated(literalt a) const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
resultt do_prop_solve() override
void set_polarity(literalt a, bool value)