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)
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)
129 status = statust::ERROR;
130 throw std::bad_alloc();
142 (no_variables()-1) <<
" variables, " <<
143 solver->nClauses() <<
" clauses" << eom;
153 <<
"SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
158 bool has_false =
false;
167 <<
"got FALSE as assumption: instance is UNSATISFIABLE" << eom;
171 Glucose::vec<Glucose::Lit> solver_assumptions;
172 convert(assumptions, solver_assumptions);
174 if(
solver->solve(solver_assumptions))
177 status = statust::SAT;
178 return resultt::P_SATISFIABLE;
187 status = statust::UNSAT;
188 return resultt::P_UNSATISFIABLE;
190 catch(Glucose::OutOfMemoryException)
193 status = statust::ERROR;
194 throw std::bad_alloc();
206 bool sign = a.
sign();
209 solver->model.growTo(v + 1);
211 solver->model[v] = Glucose::lbool(value);
213 catch(Glucose::OutOfMemoryException)
216 status = statust::ERROR;
217 throw std::bad_alloc();
244 for(
int i=0; i<
solver->conflict.size(); i++)
245 if(var(
solver->conflict[i])==v)
257 INVARIANT(!it->is_constant(),
"assumption literals must not be constant");
280 catch(Glucose::OutOfMemoryException)
284 throw std::bad_alloc();
satcheck_glucose_baset(T *)
#define forall_literals(it, bv)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
satcheck_glucose_simplifiert()
int solver(std::istream &in)
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual void set_frozen(literalt a)
#define PRECONDITION(CONDITION)
satcheck_glucose_no_simplifiert()
virtual void set_assumptions(const bvt &_assumptions)
virtual ~satcheck_glucose_baset()
bool is_eliminated(literalt a) const
virtual const std::string solver_text()
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
mstreamt & status() const
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
virtual bool is_in_conflict(literalt a) const
Returns true if an assumption is in the final conflict.
std::vector< literalt > bvt
void set_polarity(literalt a, bool value)
virtual void lcnf(const bvt &bv)