void addClause(CNF *cnf, uint numliterals, int *literals){
cnf->clausecount++;
- for(uint i=0; i< numliterals; i++)
- model_print("%d ", literals[i]);
- model_print("\n");
addArrayClauseLiteral(cnf->solver, numliterals, literals);
}
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
- model_print("**********************************************************\n");
- constraint.print();
- model_print("\n");
Edge c = encodeConstraintSATEncoder(constraint);
- model_print("&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n");
- printCNF(c);
- model_print("\n");
addConstraintCNF(cnf, c);
}
delete iterator;