Adding sat solution translator for binary value encoding

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index f118e5bacb7baad56f4daf641b17622a0f1ac912..1569b823ad4085317e1fb0f55131f8b4f77b734b 100644 (file)
--- 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 64ad37ddafc1d524b13de030dda2bf351136524b..52e40a7bcd2854c7590736789b64c3766485ee7c 100644 (file)
--- 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);