Add OneHot Encoding

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 1644a6becb55d42d6d8406395b0e4fbdc8264f5f..52cd91f316b3a7079e5aca55456122aac4fb4fab 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -5,18 +5,14 @@
 #include "element.h"
 
 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
-       generateElementEncodingVariables(This, getElementEncoding(elem));
        switch(getElementEncoding(elem)->type){
                case ONEHOT:
-                       //FIXME
-                       ASSERT(0);
-                       break;
+                       return getElementValueOneHotConstraint(This, elem, value);
                case UNARY:
                        ASSERT(0);
                        break;
                case BINARYINDEX:
                        return getElementValueBinaryIndexConstraint(This, elem, value);
-                       break;
                case ONEHOTBINARY:
                        ASSERT(0);
                        break;
@@ -35,10 +31,60 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
        ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
-               if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
+               if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
                        return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
                }
        }
        return E_BOGUS;
 }
 
+Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {
+       ASTNodeType type = GETELEMENTTYPE(elem);
+       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+       ElementEncoding* elemEnc = getElementEncoding(elem);
+       for(uint i=0; i<elemEnc->encArraySize; i++){
+               if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
+                       return elemEnc->variables[i];
+               }
+       }
+       return E_BOGUS;
+}
+
+void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
+       This->numVars = numVars;
+       This->variables = ourmalloc(sizeof(Edge) * numVars);
+}
+
+void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+       ASSERT(encoding->type==BINARYINDEX);
+       allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
+       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+}
+
+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=0;j<encoding->numVars;j++) {
+                       addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
+               }
+       }
+}
+
+void generateElementEncoding(SATEncoder* This, Element * element) {
+       ElementEncoding* encoding = getElementEncoding(element);
+       ASSERT(encoding->type!=ELEM_UNASSIGNED);
+       if(encoding->variables!=NULL)
+               return;
+       switch(encoding->type) {
+       case ONEHOT:
+               generateOneHotEncodingVars(This, encoding);
+               return;
+       case BINARYINDEX:
+               generateBinaryIndexEncodingVars(This, encoding);
+               return;
+       default:
+               ASSERT(0);
+       }
+}
+

diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index 28d50b02985d65cc28b831746ca18a354bca09ec..78a0ff390f68455e9374ba737b196ddf77307653 100644 (file)
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -1,7 +1,11 @@
 #ifndef SATELEMENTENCODER_H
 #define SATELEMENTENCODER_H
 
+Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueBinaryIndexConstraint(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 generateBinaryIndexEncodingVars(SATEncoder* This, ElementEncoding* encoding);
+void generateElementEncoding(SATEncoder* This, Element* element);
 #endif

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index cd4b234c2c10325ed2ab366ca4f6b0888130a4c1..c34a04729d5038679d41d0504498d06b913e3422 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -127,6 +127,7 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
                        encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
                        break;
                case ELEMSET:
+                       generateElementEncoding(encoder, This);
                        return;
                default:
                        ASSERT(0);

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 450ef8527cf5d0d4d3af5694d8fe6f6b29bc9ede..6d43ce1b2a8f25a10c4aa2f3ad77d2edf0c81862 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -52,7 +52,7 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
                default:
                        ASSERT(0);
        }
-       return E_BOGUS;
+       exit(-1);
 }
 
 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 2989b3b8abb48daf408e7382ea1c19e448a6c7e9..2d0b600d6d9f7eaaa7d3ecc78229290438398678 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -33,30 +33,7 @@ void allocInUseArrayElement(ElementEncoding *This, uint size) {
        This->inUseArray=ourcalloc(1, bytes);
 }
 
-void allocElementConstraintVariables(ElementEncoding* This, uint numVars){
-       This->numVars = numVars;
-       This->variables = ourmalloc(sizeof(Edge) * numVars);
-}
-
 void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
        This->type = type;
 }
 
-void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){
-       ASSERT(This->type==BINARYINDEX);
-       allocElementConstraintVariables(This, NUMBITS(This->encArraySize-1));
-       getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables);
-}
-
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){
-       ASSERT(This->type!=ELEM_UNASSIGNED);
-       if(This->variables!=NULL)
-               return;
-       switch(This->type){
-               case BINARYINDEX:
-                       generateBinaryIndexEncodingVars(encoder, This);
-                       break;
-               default:
-                       ASSERT(0);
-       }
-}

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 72cae3d21d70ff2f9b73f5a540bf3468ce421ba6..d52549d8e98545d49e844f0991695d10238f010b 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -26,8 +26,6 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
-void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
 static inline uint numEncodingVars(ElementEncoding *This) {return This->numVars;}
 
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {