Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / Encoders / naiveencoder.cc

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 959662823fe58c0f11299222e2936100de7bb8e7..ac20be5ce06e28572ba61a331f3094fa24a6202e 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -11,32 +11,37 @@
 #include "table.h"
 #include "tableentry.h"
 #include "order.h"
+#include "tunable.h"
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-       HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
-       while(hasNextBoolean(iterator)) {
-               Boolean *boolean = nextBoolean(iterator);
-               naiveEncodingConstraint(boolean);
+       if(This->isUnSAT()){
+               return;
+       }
+       SetIteratorBooleanEdge *iterator = This->getConstraints();
+       while (iterator->hasNext()) {
+               BooleanEdge b = iterator->next();
+               naiveEncodingConstraint(This, b.getBoolean());
        }
-       deleteIterBoolean(iterator);
+       delete iterator;
 }
 
-void naiveEncodingConstraint(Boolean *This) {
-       switch (GETBOOLEANTYPE(This)) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
+       switch (This->type) {
        case BOOLEANVAR: {
                return;
        }
        case ORDERCONST: {
-               ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+               if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+                       ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
                return;
        }
        case LOGICOP: {
-               naiveEncodingLogicOp((BooleanLogic *) This);
+               naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
                return;
        }
        case PREDICATEOP: {
-               naiveEncodingPredicate((BooleanPredicate *) This);
+               naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
                return;
        }
        default:
@@ -44,65 +49,45 @@ void naiveEncodingConstraint(Boolean *This) {
        }
 }
 
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
        for (uint i = 0; i < This->inputs.getSize(); i++) {
-               naiveEncodingConstraint(This->inputs.get(i));
+               naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
        }
 }
 
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
        FunctionEncoding *encoding = This->getFunctionEncoding();
-       if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
-               setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS);
+       if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+               This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 
        for (uint i = 0; i < This->inputs.getSize(); i++) {
                Element *element = This->inputs.get(i);
-               naiveEncodingElement(element);
+               naiveEncodingElement(csolver, element);
        }
 }
 
-void naiveEncodingElement(Element *This) {
-       ElementEncoding *encoding = getElementEncoding(This);
-       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, BINARYINDEX);
-               encodingArrayInitialization(encoding);
+void naiveEncodingElement(CSolver *csolver, Element *This) {
+       ElementEncoding *encoding = This->getElementEncoding();
+       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+               if (This->type != ELEMCONST) {
+                       model_print("INFO: naive encoder is making the decision about element %p....\n", This);
+               }
+               uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
+               if (enc == ELEM_UNASSIGNED)
+                       enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
+               encoding->setElementEncodingType((ElementEncodingType)enc);
+               encoding->encodingArrayInitialization();
        }
 
-       if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
+       if (This->type == ELEMFUNCRETURN) {
                ElementFunction *function = (ElementFunction *) This;
                for (uint i = 0; i < function->inputs.getSize(); i++) {
                        Element *element = function->inputs.get(i);
-                       naiveEncodingElement(element);
+                       naiveEncodingElement(csolver, element);
                }
-               FunctionEncoding *encoding = getElementFunctionEncoding(function);
-               if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
-                       setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
-       }
-}
-
-uint getSizeEncodingArray(ElementEncoding *This, uint setSize) {
-       switch (This->type) {
-       case BINARYINDEX:
-               return NEXTPOW2(setSize);
-       case ONEHOT:
-       case UNARY:
-               return setSize;
-       default:
-               ASSERT(0);
+               FunctionEncoding *encoding = function->getElementFunctionEncoding();
+               if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+                       function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
        }
-       return -1;
 }
 
-void encodingArrayInitialization(ElementEncoding *This) {
-       Element *element = This->element;
-       Set *set = getElementSet(element);
-       ASSERT(set->isRange == false);
-       uint size = getSizeVectorInt(set->members);
-       uint encSize = getSizeEncodingArray(This, size);
-       allocEncodingArrayElement(This, encSize);
-       allocInUseArrayElement(This, encSize);
-       for (uint i = 0; i < size; i++) {
-               This->encodingArray[i] = getVectorInt(set->members, i);
-               setInUseElement(This, i);
-       }
-}