#include "predicate.h"
#include "set.h"
-SATEncoder::SATEncoder(CSolver * _solver) :
+SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver) {
}
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
- HSIteratorBoolean *iterator = csolver->getConstraints();
+ SetIteratorBoolean *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
Boolean *constraint = iterator->next();
Edge c = encodeConstraintSATEncoder(constraint);
Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
Edge result;
if (booledgeMap.contains(constraint)) {
- Edge e={(Node *) booledgeMap.get(constraint)};
+ Edge e = {(Node *) booledgeMap.get(constraint)};
return e;
}
-
+
switch (constraint->type) {
case ORDERCONST:
- result=encodeOrderSATEncoder((BooleanOrder *) constraint);
+ result = encodeOrderSATEncoder((BooleanOrder *) constraint);
break;
case BOOLEANVAR:
- result=encodeVarSATEncoder((BooleanVar *) constraint);
+ result = encodeVarSATEncoder((BooleanVar *) constraint);
break;
case LOGICOP:
- result=encodeLogicSATEncoder((BooleanLogic *) constraint);
+ result = encodeLogicSATEncoder((BooleanLogic *) constraint);
break;
case PREDICATEOP:
- result=encodePredicateSATEncoder((BooleanPredicate *) constraint);
+ result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
break;
default:
model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
switch (constraint->op) {
- case L_AND:
+ case SATC_AND:
return constraintAND(cnf, constraint->inputs.getSize(), array);
- case L_OR:
+ case SATC_OR:
return constraintOR(cnf, constraint->inputs.getSize(), array);
- case L_NOT:
+ case SATC_NOT:
return constraintNegate(array[0]);
- case L_XOR:
+ case SATC_XOR:
return constraintXOR(cnf, array[0], array[1]);
- case L_IMPLIES:
+ case SATC_IFF:
+ return constraintIFF(cnf, array[0], array[1]);
+ case SATC_IMPLIES:
return constraintIMPLIES(cnf, array[0], array[1]);
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
/* Check to see if we have already encoded this element. */
if (getElementEncoding(element)->variables != NULL)
return;
-
+
/* Need to encode. */
switch ( element->type) {
case ELEMFUNCRETURN: