13 #include <zchaff_solver.h> 19 solver->set_variable_number(0);
41 case 0: result=
tvt(
false);
break;
42 case 1: result=
tvt(
true);
break;
64 for(clausest::const_iterator it=
clauses.begin();
68 reinterpret_cast<int*>(&((*it)[0])), it->size());
80 std::to_string(
solver->num_variables())+
" variables, "+
81 std::to_string(
solver->clauses().size())+
" clauses";
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";
124 if(result==SATISFIABLE)
127 for(
unsigned i=1; i<
solver->variables().size(); i++)
128 assert(
solver->variables()[i].value()==0 ||
129 solver->variables()[i].value()==1);
133 if(result==SATISFIABLE)
136 cout <<
"DEBUG L" << i <<
":" <<
get(i) <<
'\n';
140 if(result==UNSATISFIABLE)
143 return P_UNSATISFIABLE;
146 if(result==SATISFIABLE)
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)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
virtual ~satcheck_zchafft()
virtual size_t no_variables() const override