From fd09b2b8edb8d7151cb4fdd861da7d643f176295 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Thu, 26 Jul 2018 12:48:24 -0700 Subject: [PATCH] Warning message when value of element is undefined in results retrieved from SAT Solver --- src/Translator/sattranslator.cc | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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]; } -- 2.34.1