Warning message when value of element is undefined in results retrieved from SAT...
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 26 Jul 2018 19:48:24 +0000 (12:48 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 26 Jul 2018 19:48:24 +0000 (12:48 -0700)
src/Translator/sattranslator.cc

index d49883e..1e95596 100644 (file)
@@ -37,22 +37,30 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding
 
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint index = 0;
 
 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint index = 0;
+       bool overflow = true;
        for (uint i = 0; i < elemEnc->numVars; i++) {
        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;
                        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;
        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] )) ) {
        for (i = 0; i < elemEnc->numVars; i++) {
                if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+                       overflow = false;
                        break;
                }
        }
                        break;
                }
        }
-
+       if(overflow)
+               model_print("WARNING: Element has undefined value!\n");
        return elemEnc->encodingArray[i];
 }
 
        return elemEnc->encodingArray[i];
 }