Removing extra constraints for the unary encoding

[satune.git] / src / Backend / satelemencoder.cc

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index fbf09e620a097b0573d101ac30412f70f3ce8bf7..b80978ec0c5a620809544b08376171d939729662 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -246,8 +246,6 @@ void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
        for (uint i = 1; i < encoding->numVars; i++) {
                addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
        }
-       if(encoding->anyValue)
-               generateAnyValueUnaryEncoding(encoding);
 }
 
 void SATEncoder::generateElementEncoding(Element *element) {
@@ -288,26 +286,6 @@ void SATEncoder::generateAnyValueOneHotEncoding(ElementEncoding *encoding){
        }
 }
 
-void SATEncoder::generateAnyValueUnaryEncoding(ElementEncoding *encoding){
-       if (encoding->numVars == 0)
-               return;
-       Edge carray[encoding->numVars];
-       int size = 0;
-       for (uint i = 0; i < encoding->encArraySize; i++) {
-               if (encoding->isinUseElement(i)) {
-                       if (i == 0)
-                                carray[size++] = constraintNegate(encoding->variables[0]);
-                       else if ((i + 1) == encoding->encArraySize)
-                               carray[size++] = encoding->variables[i - 1];
-                       else
-                               carray[size++] = constraintAND2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i]));
-               }
-       }
-       if(size > 0){
-               addConstraintCNF(cnf, constraintOR(cnf, size, carray));
-       }
-}
-
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
        if(encoding->numVars == 0)
                return;