Add Unary Encoding

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 52cd91f316b3a7079e5aca55456122aac4fb4fab..9f3b6ab269f4f35b3c1066b2e1ab2a635b6ef3b8 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -9,8 +9,7 @@ Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value)
                case ONEHOT:
                        return getElementValueOneHotConstraint(This, elem, value);
                case UNARY:
-                       ASSERT(0);
-                       break;
+                       return getElementValueUnaryConstraint(This, elem, value);
                case BINARYINDEX:
                        return getElementValueBinaryIndexConstraint(This, elem, value);
                case ONEHOTBINARY:
@@ -50,6 +49,21 @@ Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t
        return E_BOGUS;
 }
 
+Edge getElementValueUnaryConstraint(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) {
+                       if ((i+1)==elemEnc->encArraySize)
+                               return elemEnc->variables[i];
+                       else
+                               return constraintAND2(This->cnf, elemEnc->variables[i], constraintNegate(elemEnc->variables[i+1]));
+               }
+       }
+       return E_BOGUS;
+}
+
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
        This->numVars = numVars;
        This->variables = ourmalloc(sizeof(Edge) * numVars);
@@ -69,6 +83,16 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
                        addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
                }
        }
+       addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
+}
+
+void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+       allocElementConstraintVariables(encoding, encoding->encArraySize);
+       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);        
+       //Add unary constraint
+       for(uint i=1;i<encoding->numVars;i++) {
+               addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i-1], constraintNegate(encoding->variables[i])));
+       }
 }
 
 void generateElementEncoding(SATEncoder* This, Element * element) {
@@ -83,6 +107,9 @@ void generateElementEncoding(SATEncoder* This, Element * element) {
        case BINARYINDEX:
                generateBinaryIndexEncodingVars(This, encoding);
                return;
+       case UNARY:
+               generateUnaryEncodingVars(This, encoding);
+               return;
        default:
                ASSERT(0);
        }

diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index 78a0ff390f68455e9374ba737b196ddf77307653..ec65cf10f84396583d3721cadfdad4edebd9217c 100644 (file)
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -2,10 +2,12 @@
 #define SATELEMENTENCODER_H
 
 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 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 generateElementEncoding(SATEncoder* This, Element* element);
 #endif