From c717126d3b7f122082af90de4ec659eb3b0e33fd Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 12 Jul 2017 12:15:37 -0700 Subject: [PATCH] Adding unary encoding in sat solution translator ... --- src/Backend/sattranslator.c | 22 ++++++++++++++++++---- src/Backend/sattranslator.h | 1 + 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index f6827f5..f118e5b 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -13,6 +13,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index)); return elemEnc->encodingArray[index]; } + uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){ uint index=0; for(int i=elemEnc->numVars-1;i>=0;i--) { @@ -22,16 +23,28 @@ uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elem ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index)); return elemEnc->encodingArray[index]; } + +uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){ + uint index=0; + for(int i=elemEnc->numVars-1;i>=0;i--) { + if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) + index = i; + } + ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index)); + return elemEnc->encodingArray[index]; +} + uint64_t getElementValueSATTranslator(CSolver* This, Element* element){ - switch(getElementEncoding(element)->type){ + ElementEncoding* elemEnc = getElementEncoding(element); + switch(elemEnc->type){ case ONEHOT: - ASSERT(0); + getElementValueOneHotSATTranslator(This, elemEnc); break; case UNARY: - ASSERT(0); + getElementValueUnarySATTranslator(This, elemEnc); break; case BINARYINDEX: - return getElementValueBinaryIndexSATTranslator(This, getElementEncoding(element)); + return getElementValueBinaryIndexSATTranslator(This, elemEnc); case ONEHOTBINARY: ASSERT(0); break; @@ -42,6 +55,7 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){ ASSERT(0); break; } + return -1; } bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){ diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h index ea0085c..64ad37d 100644 --- a/src/Backend/sattranslator.h +++ b/src/Backend/sattranslator.h @@ -12,6 +12,7 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean); uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc); +uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueSATTranslator(CSolver* This, Element* element); #endif /* SATTRANSLATOR_H */ -- 2.34.1