Fix UNARY Encoding issue to use one less variable

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 38d539873d957cd7d223b3a4575c354f2165577a..4f22ba02d59c1bd72403e31df1fad213a9728ab1 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -55,10 +55,12 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
        ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
                if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
-                       if ((i+1)==elemEnc->encArraySize)
-                               return elemEnc->variables[i];
+                       if (i==0)
+                               return constraintNegate(elemEnc->variables[0]);
+                       else if ((i+1)==elemEnc->encArraySize)
+                               return elemEnc->variables[i-1];
                        else
-                               return constraintAND2(This->cnf, elemEnc->variables[i], constraintNegate(elemEnc->variables[i+1]));
+                               return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
                }
        }
        return E_BOGUS;
@@ -107,7 +109,7 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 }
 
 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
-       allocElementConstraintVariables(encoding, encoding->encArraySize);
+       allocElementConstraintVariables(encoding, encoding->encArraySize-1);
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);        
        //Add unary constraint
        for(uint i=1;i<encoding->numVars;i++) {

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 1569b823ad4085317e1fb0f55131f8b4f77b734b..bbf0924e2a59389f4c182ddaa2198d8e082965a6 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -15,6 +15,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 }
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
+       //THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
        uint64_t value=0;
        for(int i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
@@ -35,13 +36,14 @@ uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elem
 }
 
 uint64_t getElementValueUnarySATTranslator(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;
+       uint i;
+       for(i=0;i<elemEnc->numVars;i++) {
+               if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
+                       break;
+               }
        }
-       ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
-       return elemEnc->encodingArray[index];
+
+       return elemEnc->encodingArray[i];
 }
 
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
@@ -71,4 +73,4 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
        int index = getEdgeVar( ((BooleanVar*) boolean)->var );
        return This->satEncoder->cnf->solver->solution[index] == true;
-}
\ No newline at end of file
+}