From 1ed45dd90d8f4df7930473eb1bf6df6f44fd74c8 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 14:11:56 -0700
Subject: [PATCH] Fix UNARY Encoding issue to use one less variable

---
 src/Backend/satelemencoder.c | 10 ++++++----
 src/Backend/sattranslator.c  | 16 +++++++++-------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 38d5398..4f22ba0 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -55,10 +55,12 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
 	ElementEncoding* elemEnc = getElementEncoding(elem);
 	for(uint i=0; i<elemEnc->encArraySize; i++){
 		if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
-			if ((i+1)==elemEnc->encArraySize)
-				return elemEnc->variables[i];
+			if (i==0)
+				return constraintNegate(elemEnc->variables[0]);
+			else if ((i+1)==elemEnc->encArraySize)
+				return elemEnc->variables[i-1];
 			else
-				return constraintAND2(This->cnf, elemEnc->variables[i], constraintNegate(elemEnc->variables[i+1]));
+				return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
 		}
 	}
 	return E_BOGUS;
@@ -107,7 +109,7 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 }
 
 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
-	allocElementConstraintVariables(encoding, encoding->encArraySize);
+	allocElementConstraintVariables(encoding, encoding->encArraySize-1);
 	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);	
 	//Add unary constraint
 	for(uint i=1;i<encoding->numVars;i++) {
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 1569b82..bbf0924 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -15,6 +15,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 }
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
+	//THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
 	uint64_t value=0;
 	for(int i=elemEnc->numVars-1;i>=0;i--) {
 		value=value<<1;
@@ -35,13 +36,14 @@ uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elem
 }
 
 uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
-	uint index=0;
-	for(int i=elemEnc->numVars-1;i>=0;i--) {
-		if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
-			index = i;
+	uint i;
+	for(i=0;i<elemEnc->numVars;i++) {
+		if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
+			break;
+		}
 	}
-	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
-	return elemEnc->encodingArray[index];
+
+	return elemEnc->encodingArray[i];
 }
 
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
@@ -71,4 +73,4 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
 	int index = getEdgeVar( ((BooleanVar*) boolean)->var );
 	return This->satEncoder->cnf->solver->solution[index] == true;
-}
\ No newline at end of file
+}
-- 
2.34.1