Binary value encoding ...

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 9f3b6ab269f4f35b3c1066b2e1ab2a635b6ef3b8..facb374f189c7100fe82bbfdc8ba904f52e98b91 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -16,7 +16,7 @@ Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value)
                        ASSERT(0);
                        break;
                case BINARYVAL:
-                       ASSERT(0);
+                       return getElementValueBinaryValueConstraint(This, elem, value);
                        break;
                default:
                        ASSERT(0);
@@ -64,11 +64,31 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
        return E_BOGUS;
 }
 
+Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
+       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 ...
+               }
+       }
+       return E_BOGUS;
+}
+
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
        This->numVars = numVars;
        This->variables = ourmalloc(sizeof(Edge) * numVars);
 }
 
+void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
+       ASSERT(encoding->type==BINARYVAL);
+       allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
+       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+}
+
 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
        ASSERT(encoding->type==BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
@@ -110,6 +130,11 @@ void generateElementEncoding(SATEncoder* This, Element * element) {
        case UNARY:
                generateUnaryEncodingVars(This, encoding);
                return;
+       case ONEHOTBINARY:
+               return;
+       case BINARYVAL:
+               generateBinaryValueEncodingVars(This, encoding);
+               return;
        default:
                ASSERT(0);
        }

diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index ec65cf10f84396583d3721cadfdad4edebd9217c..7ba81cdc2ee4fec060c838cb9df32f177c7443f1 100644 (file)
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -4,10 +4,12 @@
 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
+Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value);
 Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars);
 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding);
 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding);
 void generateBinaryIndexEncodingVars(SATEncoder* This, ElementEncoding* encoding);
+void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding);
 void generateElementEncoding(SATEncoder* This, Element* element);
 #endif

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 2d0b600d6d9f7eaaa7d3ecc78229290438398678..8d01cc79249333407729bc38f232352dfffbdf59 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -37,3 +37,12 @@ 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 d52549d8e98545d49e844f0991695d10238f010b..49a890f321a8fb08377aca5de6b1c29fd2fde429 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -36,4 +36,6 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
        This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
+uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding);
+
 #endif