From 78f6e7822b220424324842e73dcda7b5d8aa29ad Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 13 Jul 2017 14:38:03 -0700
Subject: [PATCH] Fixing the testcase bug

---
 src/Backend/constraint.c      | 5 ++++-
 src/Backend/satencoder.c      | 5 +++--
 src/Backend/satfuncencoder.c  | 8 +++++++-
 src/Backend/satorderencoder.c | 3 +++
 src/config.h                  | 1 +
 5 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index e9f9aa0..e8ef1db 100644
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -210,7 +210,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 			edges[++lowindex]=edges[initindex];
 	}
 	lowindex++; //Make lowindex look like size
-	
+
 	if (lowindex==1)
 		return edges[0];
 
@@ -311,6 +311,9 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
 	pushVectorEdge(&cnf->constraints, constraint);
+	printf("****ADDING NEW Constraint*****\n");
+	printCNF(constraint);
+	printf("\n******************************\n");
 }
 
 Edge constraintNewVar(CNF *cnf) {
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index c34a047..5b2372b 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -30,10 +30,10 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 	VectorBoolean *constraints=csolver->constraints;
 	uint size=getSizeVectorBoolean(constraints);
 	for(uint i=0;i<size;i++) {
+		model_print("Encoding All ...\n\n");
 		Boolean *constraint=getVectorBoolean(constraints, i);
 		Edge c= encodeConstraintSATEncoder(This, constraint);
-		printCNF(c);
-		printf("\n\n");
+		model_print("Returned Constraint in EncodingAll:\n");
 		addConstraintCNF(This->cnf, c);
 	}
 }
@@ -124,6 +124,7 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr
 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
 	switch( GETELEMENTTYPE(This) ){
 		case ELEMFUNCRETURN:
+			generateElementEncoding(encoder, This);
 			encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
 			break;
 		case ELEMSET:
diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index d28d43d..af7c8b3 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -8,7 +8,7 @@
 #include "tableentry.h"
 #include "set.h"
 #include "element.h"
-
+#include "common.h"
 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 	VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
 	FunctionEncodingType encType = constraint->encoding.type;
@@ -144,6 +144,9 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 
 
 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+#ifdef TRACE_DEBUG
+	model_print("Operator Function ...\n");
+#endif
 	FunctionOperator * function = (FunctionOperator *) func->function;
 	uint numDomains=getSizeArrayElement(&func->inputs);
 
@@ -247,6 +250,9 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 }
 
 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
+#ifdef TRACE_DEBUG
+	model_print("Enumeration Table functions ...\n");
+#endif
 	//FIXME: HANDLE UNDEFINED BEHAVIORS
 	ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
 	ArrayElement* elements= &func->inputs;
diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index f04b86e..ff79d76 100644
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -51,6 +51,9 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) {
 
 
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
+#ifdef TRACE_DEBUG
+	model_print("in total order ...\n");
+#endif	
 	ASSERT(order->type == TOTAL);
 	VectorInt* mems = order->set->members;
 	HashTableOrderPair* table = order->orderPairTable;
diff --git a/src/config.h b/src/config.h
index bd998c0..db02014 100644
--- a/src/config.h
+++ b/src/config.h
@@ -17,6 +17,7 @@
 /** Turn on debugging. */
 #ifndef CONFIG_DEBUG
 //#define CONFIG_DEBUG
+#define TRACE_DEBUG
 #endif
 
 #ifndef CONFIG_ASSERT
-- 
2.34.1