From 4c14a10504b2532103daf0c1f2d42cfa36864455 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Tue, 11 Jul 2017 17:06:03 -0700
Subject: [PATCH] Make naive encoding follow AST Tree

---
 src/Encoders/elementencoding.h  |  1 +
 src/Encoders/functionencoding.h |  1 +
 src/Encoders/naiveencoder.c     | 84 +++++++++++++++++++++++----------
 src/Encoders/naiveencoder.h     |  5 ++
 4 files changed, 65 insertions(+), 26 deletions(-)

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index af9696f..385f5c2 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -21,6 +21,7 @@ struct ElementEncoding {
 };
 
 void initElementEncoding(ElementEncoding *This, Element *element);
+static inline ElementEncodingType getElementEncodingType(ElementEncoding * This) {return This->type;}
 void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h
index 41d9976..fa8729e 100644
--- a/src/Encoders/functionencoding.h
+++ b/src/Encoders/functionencoding.h
@@ -24,6 +24,7 @@ struct FunctionEncoding {
 void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
 void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
 void setFunctionEncodingType(FunctionEncoding* encoding, FunctionEncodingType type);
+static inline FunctionEncodingType getFunctionEncodingType(FunctionEncoding* This) {return This->type;}
 void deleteFunctionEncoding(FunctionEncoding *This);
 
 #endif
diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 5560526..c3dc425 100644
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -13,34 +13,66 @@
 #include "order.h"
 #include <strings.h>
 
-//BRIAN: MAKE FOLLOW TREE STRUCTURE
-void naiveEncodingDecision(CSolver* csolver){
-	uint size = getSizeVectorElement(csolver->allElements);
-	for(uint i=0; i<size; i++){
-		Element* element = getVectorElement(csolver->allElements, i);
-		//Whether it's a ElementFunction or ElementSet we should do the followings:
-		setElementEncodingType(getElementEncoding(element), BINARYINDEX);
-		baseBinaryIndexElementAssign(getElementEncoding(element));
-		if(GETELEMENTTYPE(element) == ELEMFUNCRETURN){
-			setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
-				ENUMERATEIMPLICATIONS);
-		}
+void naiveEncodingDecision(CSolver* This) {
+	for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
+		naiveEncodingConstraint(getVectorBoolean(This->constraints, i));
+	}
+}
+
+void naiveEncodingConstraint(Boolean * This) {
+	switch(GETBOOLEANTYPE(This)) {
+	case BOOLEANVAR: {
+		return;
+	}
+	case ORDERCONST: {
+		setOrderEncodingType( ((BooleanOrder*)This)->order, PAIRWISE );
+		return;
 	}
+	case LOGICOP: {
+		naiveEncodingLogicOp((BooleanLogic *) This);
+	}
+	case PREDICATEOP: {
+		naiveEncodingPredicate((BooleanPredicate *) This);
+		return;
+	}
+	default:
+		ASSERT(0);
+	}
+}
+
+void naiveEncodingLogicOp(BooleanLogic * This) {
+	for(uint i=0; i < getSizeArrayBoolean(&This->inputs); i++) {
+		naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
+	}
+}
+
+void naiveEncodingPredicate(BooleanPredicate * This) {
+	FunctionEncoding * encoding = getPredicateFunctionEncoding(This);
+	if (getFunctionEncodingType(encoding) != FUNC_UNASSIGNED)
+		return;
+
+	setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
+	for(uint i=0; i < getSizeArrayElement(&This->inputs); i++) {
+		Element * element=getArrayElement(&This->inputs, i);
+		naiveEncodingElement(element);
+	}
+}
+
+void naiveEncodingElement(Element * This) {
+	ElementEncoding * encoding = getElementEncoding(This);
+	if (getElementEncodingType(encoding) != ELEM_UNASSIGNED)
+		return;
 	
-	size = getSizeVectorBoolean(csolver->allBooleans);
-	for(uint i=0; i<size; i++){
-		Boolean* boolean = getVectorBoolean(csolver->allBooleans, i);
-		switch(GETBOOLEANTYPE(boolean)){
-			case PREDICATEOP:
-				setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean),
-					ENUMERATEIMPLICATIONS);
-				break;
-			case ORDERCONST:
-				setOrderEncodingType( ((BooleanOrder*)boolean)->order, PAIRWISE );
-				break;
-			default:
-				continue;
-		} 
+	setElementEncodingType(encoding, BINARYINDEX);
+	baseBinaryIndexElementAssign(encoding);
+	
+	if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
+		ElementFunction *function=(ElementFunction *) This;
+		for(uint i=0; i < getSizeArrayElement(&function->inputs); i++) {
+			Element * element=getArrayElement(&function->inputs, i);
+			naiveEncodingElement(element);
+		}
+		setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
 	}
 }
 
diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 2b9fb87..3d92e12 100644
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -8,7 +8,12 @@
  * @param csolver
  * @param encoder
  */
+
 void naiveEncodingDecision(CSolver* csolver);
+void naiveEncodingConstraint(Boolean * This);
+void naiveEncodingLogicOp(BooleanLogic * This);
+void naiveEncodingPredicate(BooleanPredicate * This);
+void naiveEncodingElement(Element * This);
 void baseBinaryIndexElementAssign(ElementEncoding *This);
 
 #endif
-- 
2.34.1