17#include <core/Solver.h>
18#include <simp/SimpSolver.h>
21#error "Expected HAVE_GLUCOSE"
26 dest.capacity(bv.size());
45 if(
a.var_no()>=(
unsigned)
solver->model.size())
71 solver->setPolarity(
a.var_no(), value);
73 catch(Glucose::OutOfMemoryException)
75 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
76 status = statust::ERROR;
77 throw std::bad_alloc();
83 return "Glucose Syrup without simplifier";
88 return "Glucose Syrup with simplifier";
94 while((
unsigned)
solver->nVars()<no_variables())
113 "variable not added yet");
117 Glucose::vec<Glucose::Lit>
c;
141 solver_hardness->register_clause(
147 catch(Glucose::OutOfMemoryException)
149 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
150 status = statust::ERROR;
151 throw std::bad_alloc();
161 log.statistics() << (no_variables() - 1) <<
" variables, "
170 log.status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
178 for(
const auto &
literal : assumptions)
186 log.status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
196 log.status() <<
"SAT checker: instance is SATISFIABLE"
198 status = statust::SAT;
199 return resultt::P_SATISFIABLE;
203 log.status() <<
"SAT checker: instance is UNSATISFIABLE"
209 status = statust::UNSAT;
210 return resultt::P_UNSATISFIABLE;
212 catch(Glucose::OutOfMemoryException)
214 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
215 status = statust::ERROR;
216 throw std::bad_alloc();
227 unsigned v =
a.var_no();
228 bool sign =
a.sign();
231 solver->model.growTo(v + 1);
233 solver->model[v] = Glucose::lbool(value);
235 catch(Glucose::OutOfMemoryException)
237 log.error() <<
"SAT checker ran out of memory" <<
messaget::eom;
238 status = statust::ERROR;
239 throw std::bad_alloc();
258 for(
int i=0;
i<
solver->conflict.size();
i++)
259 if(var(
solver->conflict[
i])==v)
270 for(
const auto &
literal : assumptions)
273 !
literal.is_constant(),
"assumption literals must not be constant");
287 solver->setFrozen(
a.var_no(),
true);
290 catch(Glucose::OutOfMemoryException)
294 throw std::bad_alloc();
302 return solver->isEliminated(
a.var_no());
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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 set_assumptions(const bvt &_assumptions) override
void lcnf(const bvt &bv) override
std::unique_ptr< Glucose::SimpSolver > solver
void set_polarity(literalt a, bool value)
satcheck_glucose_baset(message_handlert &message_handler)
resultt do_prop_solve() override
tvt l_get(literalt a) const override
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
const std::string solver_text() override
void set_frozen(literalt a) override
bool is_eliminated(literalt a) const
std::vector< literalt > bvt
std::unique_ptr< T > util_make_unique(Ts &&... ts)
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.