Restructure transforms a little and run make tabbing

[satune.git] / src / Backend / satencoder.cc

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 175cfc9d48c50e681f6f5e93a8e5c0a2128a9e13..1d6b4f4e7dc91c65d1643e92e62333ffba08125d 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -12,7 +12,7 @@
 #include "predicate.h"
 #include "set.h"
 
-SATEncoder::SATEncoder(CSolver * _solver) :
+SATEncoder::SATEncoder(CSolver *_solver) :
        cnf(createCNF()),
        solver(_solver) {
 }
@@ -26,7 +26,7 @@ int SATEncoder::solve() {
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
-       HSIteratorBoolean *iterator = csolver->getConstraints();
+       SetIteratorBoolean *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                Boolean *constraint = iterator->next();
                Edge c = encodeConstraintSATEncoder(constraint);
@@ -38,22 +38,22 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 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);
@@ -85,15 +85,17 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
                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);
@@ -131,7 +133,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) {
        /* Check to see if we have already encoded this element. */
        if (getElementEncoding(element)->variables != NULL)
                return;
-       
+
        /* Need to encode. */
        switch ( element->type) {
        case ELEMFUNCRETURN: