From 449abdd6db336bb0e97d3198a55c4c790342dc19 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 29 Jun 2017 12:52:19 -0700
Subject: [PATCH] getting two of FIXMEs fixed

---
 src/AST/element.c        | 21 +------------------
 src/AST/element.h        |  1 -
 src/Backend/satencoder.c | 45 +++++++++++++++++++++++++++++++++++-----
 src/Backend/satencoder.h |  2 ++
 4 files changed, 43 insertions(+), 26 deletions(-)

diff --git a/src/AST/element.c b/src/AST/element.c
index 8379983..9fc426c 100644
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -33,7 +33,7 @@ Set* getElementSet(Element* This){
 		case ELEMSET:
 			return ((ElementSet*)This)->set;
 		case ELEMFUNCRETURN:
-			;//Nope is needed for label assignment. i.e. next instruction isn't 
+			;//Nope is needed for label assignment. i.e. next instruction isn't a statement 
 			Function* func = ((ElementFunction*)This)->function;
 			switch(GETFUNCTIONTYPE(func)){
 				case TABLEFUNC:
@@ -50,25 +50,6 @@ Set* getElementSet(Element* This){
 	return NULL;
 }
 
-FIXME()!!!!
-
-/** This function belongs in the backend...Elements should not touch
-		binary constraints nor should they touch their encoders... */
-
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
-	ASTNodeType type = GETELEMENTTYPE(This);
-	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
-	ElementEncoding* elemEnc = getElementEncoding(This);
-	for(uint i=0; i<elemEnc->encArraySize; i++){
-		if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
-			return generateBinaryConstraint(elemEnc->numVars,
-				elemEnc->variables, i);
-		}
-	}
-	ASSERT(0);
-	return NULL;
-}
-
 void deleteElement(Element *This) {
 	switch(GETELEMENTTYPE(This)) {
 	case ELEMFUNCRETURN: {
diff --git a/src/AST/element.h b/src/AST/element.h
index 7e4db28..509ee8c 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -51,5 +51,4 @@ static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func
 	return &func->functionencoding;
 }
 
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 #endif
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 24859be..28dd6af 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -27,7 +27,7 @@ void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
 			yet, just do this as you need to during the encodeAllSATEncoder
 			walk.  */
 
-	FIXME!!!!(); // Make sure Hamed sees comment above
+//	FIXME!!!!(); // Make sure Hamed sees comment above
 
 	uint size = getSizeVectorElement(csolver->allElements);
 	for(uint i=0; i<size; i++){
@@ -36,6 +36,44 @@ void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
 	}
 }
 
+
+Constraint * getElementValueConstraint(Element* This, uint64_t value) {
+	switch(getElementEncoding(This)->type){
+		case ONEHOT:
+			ASSERT(0);
+			break;
+		case UNARY:
+			ASSERT(0);
+			break;
+		case BINARYINDEX:
+			ASSERT(0);
+			break;
+		case ONEHOTBINARY:
+			return getElementValueBinaryIndexConstraint(This, value);
+			break;
+		case BINARYVAL:
+			ASSERT(0);
+			break;
+		default:
+			ASSERT(0);
+			break;
+	}
+	return NULL;
+}
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
+	ASTNodeType type = GETELEMENTTYPE(This);
+	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+	ElementEncoding* elemEnc = getElementEncoding(This);
+	for(uint i=0; i<elemEnc->encArraySize; i++){
+		if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
+			return generateBinaryConstraint(elemEnc->numVars,
+				elemEnc->variables, i);
+		}
+	}
+	ASSERT(0);
+	return NULL;
+}
+
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 	VectorBoolean *constraints=csolver->constraints;
 	uint size=getSizeVectorBoolean(constraints);
@@ -181,10 +219,7 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
 		Element* el= getArrayElement(elements, i);
 		Constraint* carray[inputNum];
 		for(uint j=0; j<inputNum; j++){
-			FIXME!!!!();
-			//This next line should not assume a particular encoding type for the element...  just a generic element encoding function that should choose the appropriate encoding...
-			
-			carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[j]);
+			carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
 		}
 		Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 			getElementValueBinaryIndexConstraint((Element*)This, entry->output));
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index b711457..2a3901d 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -19,6 +19,8 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
+Constraint * getElementValueConstraint(Element* This, uint64_t value);
 
 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
-- 
2.34.1