From 07e565ec8d703fd955dbebe767384ae2dbdfa504 Mon Sep 17 00:00:00 2001 From: Hamed <hamed.gorjiara@gmail.com> Date: Wed, 12 Jul 2017 13:18:52 -0700 Subject: [PATCH] Adding sat solution translator for binary value encoding --- src/Backend/sattranslator.c | 10 ++++++++++ src/Backend/sattranslator.h | 2 ++ 2 files changed, 12 insertions(+) diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index f118e5b..1569b82 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -14,6 +14,16 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* return elemEnc->encodingArray[index]; } +uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){ + uint64_t value=0; + for(int i=elemEnc->numVars-1;i>=0;i--) { + value=value<<1; + if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) + value |= 1; + } + return value; +} + uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){ uint index=0; for(int i=elemEnc->numVars-1;i>=0;i--) { diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h index 64ad37d..52e40a7 100644 --- a/src/Backend/sattranslator.h +++ b/src/Backend/sattranslator.h @@ -11,6 +11,8 @@ #include "classlist.h" bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean); +uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc); +uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc); uint64_t getElementValueSATTranslator(CSolver* This, Element* element); -- 2.34.1