13 #include <zchaff_solver.h> 19 solver->set_variable_number(0);
39 "variable number shall be within bounds");
66 for(clausest::const_iterator it=
clauses.begin();
70 reinterpret_cast<int*>(&((*it)[0])), it->size());
95 msg=
"SAT checker: instance is UNSATISFIABLE";
99 msg=
"SAT checker: instance is SATISFIABLE";
103 msg=
"SAT checker failed: UNDETERMINED";
107 msg=
"SAT checker failed: Time out";
111 msg=
"SAT checker failed: Out of memory";
115 msg=
"SAT checker failed: ABORTED";
119 msg=
"SAT checker failed: unknown result";
129 for(
unsigned i=1; i<
solver->variables().size(); i++)
131 solver->variables()[i].value() == 0 ||
132 solver->variables()[i].value() == 1,
133 "all variables shall have been assigned");
140 cout <<
"DEBUG L" << i <<
":" <<
get(i) <<
'\n';
147 return P_UNSATISFIABLE;
153 return P_SATISFIABLE;
166 solver->variables()[v].set_value(value);
virtual const std::string solver_text()
virtual ~satcheck_zchaff_baset()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
satcheck_zchaff_baset(CSolver *_solver)
virtual void set_assignment(literalt a, bool value)
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
mstreamt & result() const
mstreamt & status() const
virtual ~satcheck_zchafft()
virtual size_t no_variables() const override