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()));
46 if(a.
var_no()>=(unsigned)solver->model.size())
51 if(solver->model[a.
var_no()]==l_True)
53 else if(solver->model[a.
var_no()]==l_False)
69 solver->setPolarity(a.
var_no(), value);
74 return "Glucose Syrup without simplifier";
79 return "Glucose Syrup with simplifier";
98 else if(!it->is_false())
99 assert(it->var_no()<(unsigned)
solver->nVars());
102 Glucose::vec<Glucose::Lit> c;
131 "SAT checker inconsistent: instance is UNSATISFIABLE" <<
eom;
136 bool has_false=
false;
145 "got FALSE as assumption: instance is UNSATISFIABLE" <<
eom;
149 Glucose::vec<Glucose::Lit> solver_assumptions;
152 if(
solver->solve(solver_assumptions))
155 "SAT checker: instance is SATISFIABLE" <<
eom;
156 assert(!
solver->model.empty());
158 return P_SATISFIABLE;
163 "SAT checker: instance is UNSATISFIABLE" <<
eom;
169 return P_UNSATISFIABLE;
181 solver->model.growTo(v+1);
183 solver->model[v]=Glucose::lbool(value);
209 for(
int i=0; i<
solver->conflict.size(); i++)
210 if(var(
solver->conflict[i])==v)
222 assert(!it->is_constant());
satcheck_glucose_baset(T *)
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
satcheck_glucose_simplifiert()
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual void set_frozen(literalt a)
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
void convert(const bvt &bv, Glucose::vec< Glucose::Lit > &dest)
virtual bool is_in_conflict(literalt a) const
virtual size_t no_variables() const override
std::vector< literalt > bvt
void set_polarity(literalt a, bool value)
virtual void lcnf(const bvt &bv)