From 80eabd21d6a90ba33e428f2f9fcf9ec9a2e6c779 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 11 Jul 2017 10:16:17 -0700
Subject: [PATCH] Fixing more bugs in generating constraint and getting sat
 solution

---
 src/Backend/inc_solver.c |  1 +
 src/Backend/satencoder.c | 39 +++++++++++++++++++++++++--------------
 src/csolver.c            |  6 +++++-
 3 files changed, 31 insertions(+), 15 deletions(-)

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 307114e..bb2782a 100644
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -88,6 +88,7 @@ int getSolution(IncrementalSolver * This) {
 			This->solution[0] = 0;
 		}
 		readSolver(This, &This->solution[1], numVars * sizeof(int));
+		This->solutionsize = numVars;
 	}
 	return result;
 }
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index fa1d513..0299740 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -86,8 +86,6 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 		printConstraint(c);
 		model_print("\n\n");
 		addConstraintToSATSolver(c, This->satSolver);
-		//FIXME: When do we want to delete constraints? Should we keep an array of them
-		// and delete them later, or it would be better to just delete them right away?
 	}
 }
 
@@ -425,23 +423,31 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 	ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
 	ASSERT(getSizeArrayElement(&This->inputs)==2 );
-	ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
-	ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
-	Constraint* carray[elem1->encArraySize*elem2->encArraySize];
+	Constraint *elemc1=NULL, *elemc2 = NULL;
+	Element* elem1 = getArrayElement(&This->inputs,0);
+	Element* elem2 = getArrayElement(&This->inputs,1);
+	if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
+		elemc1 = encodeFunctionElementSATEncoder(encoder, (ElementFunction*) elem1);
+	if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
+		elemc2 = encodeFunctionElementSATEncoder(encoder , (ElementFunction*) elem2);
+	
+	ElementEncoding* elemEnc1 = getElementEncoding( elem1 );
+	ElementEncoding* elemEnc2 = getElementEncoding( elem2 );
+	Constraint* carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
 	uint size=0;
 	Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
-	for(uint i=0; i<elem1->encArraySize; i++){
-		if(isinUseElement(elem1, i)){
-			for( uint j=0; j<elem2->encArraySize; j++){
-				if(isinUseElement(elem2, j)){
+	for(uint i=0; i<elemEnc1->encArraySize; i++){
+		if(isinUseElement(elemEnc1, i)){
+			for( uint j=0; j<elemEnc2->encArraySize; j++){
+				if(isinUseElement(elemEnc2, j)){
 					bool isInRange = false;
-					uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
-						elem2->encodingArray[j], &isInRange);
+					uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
+						elemEnc2->encodingArray[j], &isInRange);
 					//FIXME: instead of getElementValueConstraint, it might be useful to have another function
 					// that doesn't iterate over encodingArray and treats more efficient ...
-					Constraint* valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
+					Constraint* valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
 					ASSERT(valConstrIn1 != NULL);
-					Constraint* valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
+					Constraint* valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
 					ASSERT(valConstrIn2 != NULL);
 					Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
 					if(valConstrOut == NULL)
@@ -500,7 +506,12 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element
 			}
 		}
 	}
-	return allocArrayConstraint(AND, size, carray);
+	Constraint* result = allocArrayConstraint(OR, size, carray);
+	if(elemc1 != NULL)
+		result = allocConstraint(AND, result, elemc1);
+	if(elemc2 != NULL)
+		result = allocConstraint(AND, result, elemc2);
+	return result;
 }
 
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
diff --git a/src/csolver.c b/src/csolver.c
index 1d31e42..3e18833 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -177,7 +177,11 @@ void startEncoding(CSolver* solver){
 	encodeAllSATEncoder(solver, satEncoder);
 	finishedClauses(satEncoder->satSolver);
 	int result= solve(satEncoder->satSolver);
-	model_print("sat_solver's result:%d\n", result);
+	model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->satSolver->solutionsize);
+	for(uint i=1; i<=satEncoder->satSolver->solutionsize; i++){
+		model_print("%d, ", satEncoder->satSolver->solution[i]);
+	}
+	model_print("\n");
 	//For now, let's just delete it, and in future for doing queries 
 	//we may need it.
 	deleteSATEncoder(satEncoder);
-- 
2.34.1