Warning message when value of element is undefined in results retrieved from SAT...

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

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 792d58b38bc62f7370b253b68e65007bb7cd2e64..1e955969554bb8b76c2b0c76f008cb23711fb231 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -37,27 +37,35 @@ 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];
 }
 
 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint i;
+       bool overflow = true;
        for (i = 0; i < elemEnc->numVars; i++) {
                if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+                       overflow = false;
                        break;
                }
        }
-
+       if(overflow)
+               model_print("WARNING: Element has undefined value!\n");
        return elemEnc->encodingArray[i];
 }
 
 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 element->getRange()->getElement(0);
        switch (elemEnc->type) {