13 #include <zchaff_solver.h> 19 solver->set_variable_number(0);
64 for(clausest::const_iterator it=
clauses.begin();
68 reinterpret_cast<int*>(&((*it)[0])), it->size());
93 msg=
"SAT checker: instance is UNSATISFIABLE";
97 msg=
"SAT checker: instance is SATISFIABLE";
101 msg=
"SAT checker failed: UNDETERMINED";
105 msg=
"SAT checker failed: Time out";
109 msg=
"SAT checker failed: Out of memory";
113 msg=
"SAT checker failed: ABORTED";
117 msg=
"SAT checker failed: unknown result";
127 for(
unsigned i=1; i<
solver->variables().size(); i++)
128 assert(
solver->variables()[i].value()==0 ||
129 solver->variables()[i].value()==1);
136 cout <<
"DEBUG L" << i <<
":" <<
get(i) <<
'\n';
143 return P_UNSATISFIABLE;
149 return P_SATISFIABLE;
162 solver->variables()[v].set_value(value);
virtual const std::string solver_text()
virtual ~satcheck_zchaff_baset()
satcheck_zchaff_baset(CSolver *_solver)
static mstreamt & eom(mstreamt &m)
virtual void set_assignment(literalt a, bool value)
int solver(std::istream &in)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
mstreamt & result() const
mstreamt & status() const
virtual ~satcheck_zchafft()
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual size_t no_variables() const override