From 769378ebb26e1c6b091f43620bc5a6346b24c6fb Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 17:07:51 -0700
Subject: [PATCH] Check in bug fix

---
 src/Backend/satfuncencoder.c |  7 ++++---
 src/Test/buildconstraints.c  | 10 ++++------
 src/csolver.c                |  3 ++-
 src/csolver.h                |  2 +-
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 6d43ce1..d28d43d 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -40,7 +40,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
 	}
 	Edge result=constraintOR(This->cnf, size, constraints);
 
-	return generateNegation ? result: constraintNegate(result);
+	return generateNegation ? constraintNegate(result) : result;
 }
 
 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
@@ -117,7 +117,8 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 				Element * elem = getArrayElement(&constraint->inputs, i);
 				carray[i] = getElementValueConstraint(This, elem, vals[i]);
 			}
-			pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray));
+			Edge term=constraintAND(This->cnf, numDomains, carray);
+			pushVectorEdge(clauses, term);
 		}
 		
 		notfinished=false;
@@ -138,7 +139,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 
 	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 	deleteVectorEdge(clauses);
-	return generateNegation ? cor : constraintNegate(cor);
+	return generateNegation ? constraintNegate(cor) : cor;
 }
 
 
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index c4440a7..e47c780 100644
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -11,10 +11,7 @@ int main(int numargs, char ** argv) {
 	Element * inputs[]={e1, e2};
 	Boolean * b=applyPredicate(solver, equals, inputs, 2);
 	addConstraint(solver, b);
-	Order * o=createOrder(solver, TOTAL, s);
-	Boolean * oc=orderConstraint(solver, o, 1, 2);
-	addConstraint(solver, oc);
-		
+
 	uint64_t set2[] = {2, 3};
 	Set* rangef1 = createSet(solver, 1, set2, 2);
 	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
@@ -25,7 +22,7 @@ int main(int numargs, char ** argv) {
 	uint64_t row3[] = {2, 1};
 	uint64_t row4[] = {1, 2};
 	addTableEntry(solver, table, row1, 2, 0);
-	addTableEntry(solver, table, row2, 2, 1);
+	addTableEntry(solver, table, row2, 2, 0);
 	addTableEntry(solver, table, row3, 2, 2);
 	addTableEntry(solver, table, row4, 2, 2);
 	Function * f2 = completeTable(solver, table); //its range would be as same as s
@@ -39,6 +36,7 @@ int main(int numargs, char ** argv) {
 	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
 	addConstraint(solver, pred);
 	
-	startEncoding(solver);
+	if (startEncoding(solver)==1)
+		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
 	deleteSolver(solver);
 }
diff --git a/src/csolver.c b/src/csolver.c
index f9f1e1b..3d062e4 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,7 +174,7 @@ Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t
 	return constraint;
 }
 
-void startEncoding(CSolver* This){
+int startEncoding(CSolver* This){
 	naiveEncodingDecision(This);
 	SATEncoder* satEncoder = This->satEncoder;
 	encodeAllSATEncoder(This, satEncoder);
@@ -184,6 +184,7 @@ void startEncoding(CSolver* This){
 		model_print("%d, ", satEncoder->cnf->solver->solution[i]);
 	}
 	model_print("\n");
+	return result;
 }
 
 uint64_t getElementValue(CSolver* This, Element* element){
diff --git a/src/csolver.h b/src/csolver.h
index 9628f11..1adb679 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -114,7 +114,7 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
 
 /** When everything is done, the client calls this function and then csolver starts to encode*/
-void startEncoding(CSolver*);
+int startEncoding(CSolver*);
 
 /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
 uint64_t getElementValue(CSolver*, Element* element);
-- 
2.34.1