Fixing bugs for Unary encoding ...

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index ab597a6a0d032152e64781ca9ad0e896ce7a2f36..ca71c6e9f1905f0c03780bf12273282db70fbc55 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -52,10 +52,12 @@ Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t
 
 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(elem);
-       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
                if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
+                       if(elemEnc->numVars == 0)
+                               return E_True;
                        if (i==0)
                                return constraintNegate(elemEnc->variables[0]);
                        else if ((i+1)==elemEnc->encArraySize)
@@ -64,7 +66,7 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
                                return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
                }
        }
-       return E_BOGUS;
+       return E_False;
 }
 
 Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
@@ -101,8 +103,8 @@ void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 }
 
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { 
-       allocElementConstraintVariables(encoding, getSetSize( getElementSet(encoding->element)));
+void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+       allocElementConstraintVariables(encoding, encoding->encArraySize);
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);        
        for(uint i=0;i<encoding->numVars;i++) {
                for(uint j=i+1;j<encoding->numVars;j++) {

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index d5b88d7027429ef493fa20bfef37621a31c8cb8d..6fe0ac84ce400abc3e7ecbe5eaa5f17d40eed2e1 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -61,7 +61,7 @@ void naiveEncodingPredicate(BooleanPredicate * This) {
 void naiveEncodingElement(Element * This) {
        ElementEncoding * encoding = getElementEncoding(This);
        if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, ONEHOT);
+               setElementEncodingType(encoding, UNARY);
                encodingArrayInitialization(encoding);
        }
        
@@ -77,12 +77,25 @@ void naiveEncodingElement(Element * This) {
        }
 }
 
+uint getSizeEncodingArray(ElementEncoding *This, uint setSize){
+       switch(This->type){
+               case BINARYINDEX:
+                       return NEXTPOW2(setSize);
+               case ONEHOT:
+               case UNARY:
+                       return setSize;
+               default:
+                       ASSERT(0);
+       }
+       return -1;
+}
+
 void encodingArrayInitialization(ElementEncoding *This) {
        Element * element=This->element;
        Set * set= getElementSet(element);
        ASSERT(set->isRange==false);
        uint size=getSizeVectorInt(set->members);
-       uint encSize=NEXTPOW2(size);
+       uint encSize=getSizeEncodingArray(This, size);
        allocEncodingArrayElement(This, encSize);
        allocInUseArrayElement(This, encSize);
        for(uint i=0;i<size;i++) {

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 20f2943ce26a093dd3e22199ad624566f8fb5d73..a4b9ec176b07f117d91774ef81f0ca4f5b163f5c 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -15,5 +15,6 @@ void naiveEncodingLogicOp(BooleanLogic * This);
 void naiveEncodingPredicate(BooleanPredicate * This);
 void naiveEncodingElement(Element * This);
 void encodingArrayInitialization(ElementEncoding *This);
+uint getSizeEncodingArray(ElementEncoding *, uint setSize);
 
 #endif