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

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index d49883e447642641fdd2f0f4073015763ebc7887..1e955969554bb8b76c2b0c76f008cb23711fb231 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -37,22 +37,30 @@ 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];
 }