Fix tabbing

[satune.git] / src / Translator / sattranslator.cc

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index d670a94fdff895d795ff6240233d3ff6d84369bf..f69bff748e94687253515df5aad60d0c38138d70 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -37,10 +37,15 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
 
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint index = 0;
+       bool overflow = true;
        for (uint i = 0; i < elemEnc->numVars; i++) {
-               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) {
                        index = i;
+                       overflow = false;
+               }
        }
+       if (overflow)
+               model_print("WARNING: Element has undefined value!\n");
        ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
        return elemEnc->encodingArray[index];
 }
@@ -57,9 +62,9 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
-       ElementEncoding *elemEnc = getElementEncoding(element);
+       ElementEncoding *elemEnc = element->getElementEncoding();
        if (elemEnc->numVars == 0)//case when the set has only one item
-               return getElementSet(element)->getElement(0);
+               return element->getRange()->getElement(0);
        switch (elemEnc->type) {
        case ONEHOT:
                return getElementValueOneHotSATTranslator(This, elemEnc);
@@ -67,8 +72,6 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
                return getElementValueUnarySATTranslator(This, elemEnc);
        case BINARYINDEX:
                return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-       case ONEHOTBINARY:
-               ASSERT(0);
                break;
        case BINARYVAL:
                ASSERT(0);