43 case 0: result=
tvt(
false);
break;
44 case 1: result=
tvt(
true);
break;
56 return std::string(
"Limmat version ")+version_Limmat();
61 for(clausest::iterator it=
clauses.begin();
66 int *clause=
new int[it->size()+1];
68 for(
unsigned j=0; j<it->size(); j++)
69 clause[j]=(*it)[j].dimacs();
74 add_Limmat(
solver, clause);
86 std::to_string(maxvar_Limmat(
solver))+
" variables, "+
87 std::to_string(clauses_Limmat(
solver))+
" clauses";
99 msg=
"SAT checker: instance is UNSATISFIABLE";
103 msg=
"SAT checker: instance is SATISFIABLE";
107 msg=
"SAT checker failed: unknown result";
117 return P_UNSATISFIABLE;
124 for(
const int *a=assignment_Limmat(
solver); *a!=0; a++)
133 return P_SATISFIABLE;
virtual ~satcheck_limmatt()
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
static mstreamt & eom(mstreamt &m)
virtual const std::string solver_text()
virtual size_t no_variables() const override
std::vector< unsigned char > assignment