From ad85c42cdbc545a5dff8010f08978b2dbc607f08 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 11 Jul 2017 23:39:28 -0700
Subject: [PATCH] Add Unary Encoding

---
 src/Backend/satelemencoder.c | 31 +++++++++++++++++++++++++++++--
 src/Backend/satelemencoder.h |  2 ++
 2 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 52cd91f..9f3b6ab 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -9,8 +9,7 @@ Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value)
 		case ONEHOT:
 			return getElementValueOneHotConstraint(This, elem, value);
 		case UNARY:
-			ASSERT(0);
-			break;
+			return getElementValueUnaryConstraint(This, elem, value);
 		case BINARYINDEX:
 			return getElementValueBinaryIndexConstraint(This, elem, value);
 		case ONEHOTBINARY:
@@ -50,6 +49,21 @@ Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t
 	return E_BOGUS;
 }
 
+Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
+	ASTNodeType type = GETELEMENTTYPE(elem);
+	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+	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];
+			else
+				return constraintAND2(This->cnf, elemEnc->variables[i], constraintNegate(elemEnc->variables[i+1]));
+		}
+	}
+	return E_BOGUS;
+}
+
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
 	This->numVars = numVars;
 	This->variables = ourmalloc(sizeof(Edge) * numVars);
@@ -69,6 +83,16 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 			addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
 		}
 	}
+	addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
+}
+
+void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+	allocElementConstraintVariables(encoding, encoding->encArraySize);
+	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);	
+	//Add unary constraint
+	for(uint i=1;i<encoding->numVars;i++) {
+		addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i-1], constraintNegate(encoding->variables[i])));
+	}
 }
 
 void generateElementEncoding(SATEncoder* This, Element * element) {
@@ -83,6 +107,9 @@ void generateElementEncoding(SATEncoder* This, Element * element) {
 	case BINARYINDEX:
 		generateBinaryIndexEncodingVars(This, encoding);
 		return;
+	case UNARY:
+		generateUnaryEncodingVars(This, encoding);
+		return;
 	default:
 		ASSERT(0);
 	}
diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index 78a0ff3..ec65cf1 100644
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -2,10 +2,12 @@
 #define SATELEMENTENCODER_H
 
 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value);
+Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
 Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars);
 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding);
+void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding);
 void generateBinaryIndexEncodingVars(SATEncoder* This, ElementEncoding* encoding);
 void generateElementEncoding(SATEncoder* This, Element* element);
 #endif
-- 
2.34.1