From e26cb77b9ed0a2e46b670d2a51c5dbde879b595a Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 30 Jun 2017 16:35:49 -0700
Subject: [PATCH] Starting predicates ...

---
 src/Backend/satencoder.c | 72 +++++++++++++++++++++++++++++++---------
 src/Backend/satencoder.h |  4 +++
 2 files changed, 61 insertions(+), 15 deletions(-)

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 2b631ff..d51a262 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -9,6 +9,7 @@
 #include "tableentry.h"
 #include "table.h"
 #include "order.h"
+#include "predicate.h"
 
 
 SATEncoder * allocSATEncoder() {
@@ -82,19 +83,20 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 		encodeConstraintSATEncoder(This, constraint);
 	}
 	
-	size = getSizeVectorElement(csolver->allElements);
-	for(uint i=0; i<size; i++){
-		Element* element = getVectorElement(csolver->allElements, i);
-		switch(GETELEMENTTYPE(element)){
-			case ELEMFUNCRETURN: 
-				encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
-				break;
-			default:	
-				continue;
-				//ElementSets that aren't used in any constraints/functions
-				//will be eliminated.
-		}
-	}
+//	FIXME: Following line for element!
+//	size = getSizeVectorElement(csolver->allElements);
+//	for(uint i=0; i<size; i++){
+//		Element* element = getVectorElement(csolver->allElements, i);
+//		switch(GETELEMENTTYPE(element)){
+//			case ELEMFUNCRETURN: 
+//				encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
+//				break;
+//			default:	
+//				continue;
+//				//ElementSets that aren't used in any constraints/functions
+//				//will be eliminated.
+//		}
+//	}
 }
 
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
@@ -220,8 +222,48 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
 }
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-	//TO IMPLEMENT
-	
+	switch(GETPREDICATETYPE(constraint) ){
+		case TABLEPRED:
+			return encodeTablePredicateSATEncoder(This, constraint);
+		case OPERATORPRED:
+			return encodeOperatorPredicateSATEncoder(This, constraint);
+		default:
+			ASSERT(0);
+	}
+	return NULL;
+}
+
+Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	switch(constraint->encoding.type){
+		case ENUMERATEIMPLICATIONS:
+			return encodeEnumTablePredicateSATEncoder(This, constraint);
+		case CIRCUIT:
+			ASSERT(0);
+			break;
+		default:
+			ASSERT(0);
+	}
+	return NULL;
+}
+
+Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	TableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
+	uint size = getSizeVectorTableEntry(entries);
+	for(uint i=0; i<size; i++){
+		TableEntry* entry = getVectorTableEntry(entries, i);
+		
+	}
+}
+
+Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	switch(constraint->encoding.type){
+		case ENUMERATEIMPLICATIONS:
+			break;
+		case CIRCUIT:
+			break;
+		default:
+			ASSERT(0);
+	}
 	return NULL;
 }
 
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 32fb6fa..fc79a05 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -22,6 +22,10 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+
 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 Constraint * getElementValueConstraint(Element* This, uint64_t value);
 
-- 
2.34.1