Testing one-hot encoding + fixing bugs ...

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

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a872b62dd4992a6ca034e7bf68a0b08781a5fd08..a9c89fe6c781410b3c7f22702613768a05ecc8c5 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -8,7 +8,7 @@
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=elemEnc->numVars-1;i>=0;i--) {
                index=index<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
@@ -19,7 +19,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint64_t value=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
@@ -36,7 +36,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding*
 
 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=0; i< elemEnc->numVars; i++) {
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
@@ -61,11 +61,9 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
                return getSetElement(getElementSet(element), 0);
        switch(elemEnc->type){
                case ONEHOT:
-                       getElementValueOneHotSATTranslator(This, elemEnc);
-                       break;
+                       return getElementValueOneHotSATTranslator(This, elemEnc);
                case UNARY:
-                       getElementValueUnarySATTranslator(This, elemEnc);
-                       break;
+                       return getElementValueUnarySATTranslator(This, elemEnc);
                case BINARYINDEX:
                        return getElementValueBinaryIndexSATTranslator(This, elemEnc);
                case ONEHOTBINARY: