remove redundant constraint
authorbdemsky <bdemsky@uci.edu>
Tue, 24 Jul 2018 20:53:34 +0000 (13:53 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 24 Jul 2018 20:53:34 +0000 (13:53 -0700)
src/Backend/satelemencoder.cc
src/Backend/satencoder.h

index 3266f1c..0efe7a1 100644 (file)
@@ -234,9 +234,8 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
-       addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
        if(encoding->anyValue)
-               generateAnyValueOneHotEncoding(encoding);
+               addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 
 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;
index b67708d..7fb889c 100644 (file)
@@ -61,7 +61,6 @@ private:
        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;