Bug Fixes + add more tracing prints + turning off some optimizations

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

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 4020ad625b49271aa1c255e10645ad312ef4aca2..720375db8b1ab5deedcebdfed70bdc5c90691f74 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,6 +29,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
+//                constraint.getBoolean()->print();
                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }
@@ -131,7 +132,7 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 void SATEncoder::encodeElementSATEncoder(Element *element) {
        /* Check to see if we have already encoded this element. */
-       if (getElementEncoding(element)->variables != NULL)
+       if (element->getElementEncoding()->variables != NULL)
                return;
 
        /* Need to encode. */
@@ -151,7 +152,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) {
 }
 
 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
-       switch (function->function->type) {
+       switch (function->getFunction()->type) {
        case TABLEFUNC:
                encodeTableElementFunctionSATEncoder(function);
                break;
@@ -164,7 +165,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
-       switch (getElementFunctionEncoding(function)->type) {
+       switch (function->getElementFunctionEncoding()->type) {
        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;