13#include <zchaff_solver.h>
19 solver->set_variable_number(0);
39 "variable number shall be within bounds");
43 case 0: result=
tvt(
false);
break;
44 case 1: result=
tvt(
true);
break;
66 for(clausest::const_iterator it=
clauses.begin();
70 reinterpret_cast<int*
>(&((*it)[0])), it->size());
82 std::to_string(
solver->num_variables())+
" variables, "+
83 std::to_string(
solver->clauses().size())+
" clauses";
87 SAT_StatusT result=(SAT_StatusT)
solver->solve();
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";
126 if(result==SATISFIABLE)
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");
137 if(result==SATISFIABLE)
140 cout <<
"DEBUG L" << i <<
":" << get(i) <<
'\n';
144 if(result==UNSATISFIABLE)
150 if(result==SATISFIABLE)
166 solver->variables()[v].set_value(value);
virtual size_t no_variables() const override
mstreamt & statistics() const
mstreamt & status() const
resultt do_prop_solve() override
virtual ~satcheck_zchaff_baset()
const std::string solver_text() override
void set_assignment(literalt a, bool value) override
satcheck_zchaff_baset(CSolver *_solver)
tvt l_get(literalt a) const override
virtual ~satcheck_zchafft()
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.