X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FTranslator%2Fsattranslator.cc;h=1e955969554bb8b76c2b0c76f008cb23711fb231;hp=d49883e447642641fdd2f0f4073015763ebc7887;hb=fd09b2b8edb8d7151cb4fdd861da7d643f176295;hpb=15741847172c31b17658b9db8bdcfcf2e3297f57

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index d49883e..1e95596 100644
--- 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];
 }