From 367a97c32557460dae585719efd5f748266f38ad Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 24 Jul 2018 13:53:34 -0700
Subject: [PATCH] remove redundant constraint

---
 src/Backend/satelemencoder.cc | 18 +-----------------
 src/Backend/satencoder.h      |  1 -
 2 files changed, 1 insertion(+), 18 deletions(-)

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3266f1c..0efe7a1 100644
--- 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, 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;
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index b67708d..7fb889c 100644
--- 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);
-        void generateAnyValueOneHotEncoding(ElementEncoding *encoding);
 	void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
 	void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
 	CNF *cnf;
-- 
2.34.1