From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 06:04:21 +0000 (-0700)
Subject: Add OneHot Encoding
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=97092b7fcacd4d3d27c2550331189547244a76d4;p=satune.git

Add OneHot Encoding
---

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 1644a6b..52cd91f 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -5,18 +5,14 @@
 #include "element.h"
 
 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
-	generateElementEncodingVariables(This, getElementEncoding(elem));
 	switch(getElementEncoding(elem)->type){
 		case ONEHOT:
-			//FIXME
-			ASSERT(0);
-			break;
+			return getElementValueOneHotConstraint(This, elem, value);
 		case UNARY:
 			ASSERT(0);
 			break;
 		case BINARYINDEX:
 			return getElementValueBinaryIndexConstraint(This, elem, value);
-			break;
 		case ONEHOTBINARY:
 			ASSERT(0);
 			break;
@@ -35,10 +31,60 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint
 	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(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
 			return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
 		}
 	}
 	return E_BOGUS;
 }
 
+Edge getElementValueOneHotConstraint(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) {
+			return elemEnc->variables[i];
+		}
+	}
+	return E_BOGUS;
+}
+
+void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
+	This->numVars = numVars;
+	This->variables = ourmalloc(sizeof(Edge) * numVars);
+}
+
+void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+	ASSERT(encoding->type==BINARYINDEX);
+	allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
+	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+}
+
+void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+	allocElementConstraintVariables(encoding, encoding->encArraySize);
+	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);	
+	for(uint i=0;i<encoding->numVars;i++) {
+		for(uint j=0;j<encoding->numVars;j++) {
+			addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
+		}
+	}
+}
+
+void generateElementEncoding(SATEncoder* This, Element * element) {
+	ElementEncoding* encoding = getElementEncoding(element);
+	ASSERT(encoding->type!=ELEM_UNASSIGNED);
+	if(encoding->variables!=NULL)
+		return;
+	switch(encoding->type) {
+	case ONEHOT:
+		generateOneHotEncodingVars(This, encoding);
+		return;
+	case BINARYINDEX:
+		generateBinaryIndexEncodingVars(This, encoding);
+		return;
+	default:
+		ASSERT(0);
+	}
+}
+
diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index 28d50b0..78a0ff3 100644
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -1,7 +1,11 @@
 #ifndef SATELEMENTENCODER_H
 #define SATELEMENTENCODER_H
 
+Edge getElementValueOneHotConstraint(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 generateBinaryIndexEncodingVars(SATEncoder* This, ElementEncoding* encoding);
+void generateElementEncoding(SATEncoder* This, Element* element);
 #endif
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index cd4b234..c34a047 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -127,6 +127,7 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
 			encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
 			break;
 		case ELEMSET:
+			generateElementEncoding(encoder, This);
 			return;
 		default:
 			ASSERT(0);
diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 450ef85..6d43ce1 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -52,7 +52,7 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 		default:
 			ASSERT(0);
 	}
-	return E_BOGUS;
+	exit(-1);
 }
 
 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 2989b3b..2d0b600 100644
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -33,30 +33,7 @@ void allocInUseArrayElement(ElementEncoding *This, uint size) {
 	This->inUseArray=ourcalloc(1, bytes);
 }
 
-void allocElementConstraintVariables(ElementEncoding* This, uint numVars){
-	This->numVars = numVars;
-	This->variables = ourmalloc(sizeof(Edge) * numVars);
-}
-
 void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
 	This->type = type;
 }
 
-void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){
-	ASSERT(This->type==BINARYINDEX);
-	allocElementConstraintVariables(This, NUMBITS(This->encArraySize-1));
-	getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables);
-}
-
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){
-	ASSERT(This->type!=ELEM_UNASSIGNED);
-	if(This->variables!=NULL)
-		return;
-	switch(This->type){
-		case BINARYINDEX:
-			generateBinaryIndexEncodingVars(encoder, This);
-			break;
-		default:
-			ASSERT(0);
-	}
-}
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 72cae3d..d52549d 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -26,8 +26,6 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
-void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
 static inline uint numEncodingVars(ElementEncoding *This) {return This->numVars;}
 
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {