From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Wed, 9 May 2018 19:18:55 +0000 (-0700)
Subject: Removing extra constraints for the unary encoding
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=f9f7d7f9830b7ca2b85c56bdeaff4ceae29f2128;hp=238830745ba3939323c285b722c9ae512b7baa9b

Removing extra constraints for the unary encoding
---

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index fbf09e6..b80978e 100644
--- 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;
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 115bc31..b67708d 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -62,7 +62,6 @@ private:
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
         void generateAnyValueOneHotEncoding(ElementEncoding *encoding);
-	void generateAnyValueUnaryEncoding(ElementEncoding *encoding);
 	void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
 	void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
 	CNF *cnf;