One-hot encoding sat solution translator

[satune.git] / src / Backend / sattranslator.c

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a768a4fa61d011cb047d8d0c4650ac548b5463ba..f6827f51e7f931a29bde2bda9675bdf3232b4d48 100644 (file)
--- 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: