remove redundant constraint

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3266f1ca9e5f3be1d9473c3a3be1ffa969d88400..0efe7a138a1da5edfd310fc9784e6c751ee76286 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -234,9 +234,8 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }

-       addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));

        if(encoding->anyValue)
        if(encoding->anyValue)

-               generateAnyValueOneHotEncoding(encoding);
+               addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));

 }
 
 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
 }
 
 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {


@@ -271,21 +270,6 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
        }
 }
 

-void SATEncoder::generateAnyValueOneHotEncoding(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)){
-                       carray[size++] = encoding->variables[i];
-               }
-       }
-       if(size > 0){
-               addConstraintCNF(cnf, constraintOR(cnf, size, carray));
-       }
-}
-

 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
        if(encoding->numVars == 0)
                return;
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
        if(encoding->numVars == 0)
                return;

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index b67708da00a749dbe0d9b9473c68d97f06f79e0a..7fb889c9b92e06697f53093410af2fbb40d1351b 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -61,7 +61,6 @@ private:
        Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
        Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
        void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
        void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);

-        void generateAnyValueOneHotEncoding(ElementEncoding *encoding);

        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;
        void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
        void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
        CNF *cnf;