Include encoding for values

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 80e14898d843e179827367c615eed4f33ddc3cf3..87d19b4ae31b5747cdfe46b45876beca6eb8e8b5 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -70,14 +70,17 @@ Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, u
        ASTNodeType type = GETELEMENTTYPE(element);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
        ElementEncoding* elemEnc = getElementEncoding(element);
-       for(uint i=0; i<elemEnc->encArraySize; i++){
-               if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
-                       return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, value);
-                       // This constraint can be generated right away without iterating over encodingArray
-                       // but we need to make sure that element with that value is in use ...
-               }
+       if (elemEnc->low <= elemEnc->high) {
+               if (value < elemEnc->low || value > elemEnc->high)
+                       return E_False;
+       } else {
+               //Range wraps around 0
+               if (value < elemEnc->low && value > elemEnc->high)
+                       return E_False;
        }
-       return E_BOGUS;
+       
+       uint64_t valueminusoffset=value-elemEnc->offset;
+       return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
 }
 
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
@@ -87,7 +90,7 @@ void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
 
 void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
        ASSERT(encoding->type==BINARYVAL);
-       allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
+       allocElementConstraintVariables(encoding, encoding->numBits);
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 }
 

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 01cb65a2845a4b29cbf84c015d0923847e08b133..19d3111c05357e4867a22e9d36aac5acf6393055 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -16,13 +16,19 @@ 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;
                if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
                        value |= 1;
        }
+       if (elemEnc->isBinaryValSigned &&
+                       This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+               //Do sign extension of negative number
+               uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+               value+=highbits;
+       }
+       value+=elemEnc->offset;
        return value;
 }
 

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 8d01cc79249333407729bc38f232352dfffbdf59..47c6ea0fef0f52f917ce7b69e4e09786b3d92e92 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -37,12 +37,4 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
        This->type = type;
 }
 
-uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding) {
-       uint64_t max = 0;
-       for(uint i=0; i< encoding->encArraySize; i++){
-               if(encoding->encodingArray[i]>max)
-                       max = encoding->encodingArray[i];
-       }
-       return NUMBITS(max-1);
-}
 

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 49a890f321a8fb08377aca5de6b1c29fd2fde429..61bdb3e88af8dfb783bcdf5c94f4b0e8ee213ded 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -14,9 +14,20 @@ struct ElementEncoding {
        ElementEncodingType type;
        Element * element;
        Edge * variables;/* List Variables Used To Encode Element */
-       uint64_t * encodingArray;       /* List the Variables in the appropriate order */
-       uint64_t * inUseArray;/* Bitmap to track variables in use */
-       uint encArraySize;
+       union {
+               struct {
+                       uint64_t * encodingArray;       /* List the Variables in the appropriate order */
+                       uint64_t * inUseArray;/* Bitmap to track variables in use */
+                       uint encArraySize;
+               };
+               struct {
+                       uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */
+                       uint64_t low;/* Lowest value to encode */
+                       uint64_t high;/* High value to encode.   If low > high, we assume wrap around to include 0. */
+                       uint numBits;
+                       bool isBinaryValSigned;
+               };
+       };
        uint numVars;   /* Number of variables */
 };
 
@@ -36,6 +47,4 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
        This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
-uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding);
-
 #endif