From 93ff173fb80070dd48c884449095d0a7bc65160f Mon Sep 17 00:00:00 2001 From: Hamed Date: Tue, 11 Jul 2017 19:24:10 -0700 Subject: [PATCH] One-hot encoding sat solution translator --- src/Backend/sattranslator.c | 9 +++++++++ src/Backend/sattranslator.h | 1 + 2 files changed, 10 insertions(+) diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index a768a4f..f6827f5 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -13,6 +13,15 @@ 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--) { + 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){ case ONEHOT: diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h index 5378cdd..ea0085c 100644 --- a/src/Backend/sattranslator.h +++ b/src/Backend/sattranslator.h @@ -11,6 +11,7 @@ #include "classlist.h" bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean); +uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueSATTranslator(CSolver* This, Element* element); #endif /* SATTRANSLATOR_H */ -- 2.34.1