From 61769d0df1f175522ba38b165630d73d6993aa40 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Thu, 13 Jul 2017 16:29:15 -0700
Subject: [PATCH] Encoding Bug Fix

---
 src/Backend/constraint.c     | 16 +++++++++++++++-
 src/Backend/satfuncencoder.c | 22 +++++++++-------------
 src/Test/buildconstraints.c  |  7 +++++--
 3 files changed, 29 insertions(+), 16 deletions(-)

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index e8ef1db..4859a93 100644
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -711,8 +711,22 @@ void printCNF(Edge e) {
 		return;
 	}
 	Node *n=getNodePtrFromEdge(e);
-	if (isNeg)
+	if (isNeg) {
+		//Pretty print things that are equivalent to OR's
+		if (getNodeType(e)==NodeType_AND) {
+			printf("or(");
+			for(uint i=0;i<n->numEdges;i++) {
+				Edge e=n->edges[i];
+				if (i!=0)
+					printf(" ");
+				printCNF(constraintNegate(e));
+			}
+			printf(")");
+			return;
+		}
+
 		printf("!");
+	}
 	switch(getNodeType(e)) {
 	case NodeType_AND:
 		printf("and");
diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index af7c8b3..4e1ba3e 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -171,7 +171,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 	
 	bool notfinished=true;
 	while(notfinished) {
-		Edge carray[numDomains+2];
+		Edge carray[numDomains+1];
 
 		uint64_t result=applyFunctionOperator(function, numDomains, vals);
 		bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
@@ -195,30 +195,26 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 			case IGNORE:
 			case NOOVERFLOW:
 			case WRAPAROUND: {
-				clause=constraintAND(This->cnf, numDomains+1, carray);
+				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 				break;
 			}
 			case FLAGFORCESOVERFLOW: {
-				carray[numDomains+1]=constraintNegate(overFlowConstraint);
-				clause=constraintAND(This->cnf, numDomains+2, carray);
+				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				break;
 			}
 			case OVERFLOWSETSFLAG: {
 				if (isInRange) {
-					clause=constraintAND(This->cnf, numDomains+1, carray);
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 				} else {
-					carray[numDomains+1]=overFlowConstraint;
-					clause=constraintAND(This->cnf, numDomains+1, carray);
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
 			case FLAGIFFOVERFLOW: {
 				if (isInRange) {
-				carray[numDomains+1]=constraintNegate(overFlowConstraint);
-					clause=constraintAND(This->cnf, numDomains+2, carray);
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
 				} else {
-					carray[numDomains+1]=overFlowConstraint;
-					clause=constraintAND(This->cnf, numDomains+1, carray);
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
 				}
 				break;
 			}
@@ -244,7 +240,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 		}
 	}
 
-	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 	addConstraintCNF(This->cnf, cor);
 	deleteVectorEdge(clauses);
 }
@@ -271,5 +267,5 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* fu
 		Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
 		constraints[i]=row;
 	}
-	addConstraintCNF(This->cnf, constraintOR(This->cnf, size, constraints));
+	addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
 }
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index e47c780..f30ebd0 100644
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -3,7 +3,10 @@
 int main(int numargs, char ** argv) {
 	CSolver * solver=allocCSolver();
 	uint64_t set1[]={0, 1, 2};
+	uint64_t setbigarray[]={0, 1, 2, 3, 4};
+	
 	Set * s=createSet(solver, 0, set1, 3);
+	Set * setbig=createSet(solver, 0, setbigarray, 5);
 	Element * e1=getElementVar(solver, s);
 	Element * e2=getElementVar(solver, s);
 	Set * domain[]={s, s};
@@ -14,13 +17,13 @@ int main(int numargs, char ** argv) {
 
 	uint64_t set2[] = {2, 3};
 	Set* rangef1 = createSet(solver, 1, set2, 2);
-	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
+	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE);
 	
 	Table* table = createTable(solver, domain, 2, s);
 	uint64_t row1[] = {0, 1};
 	uint64_t row2[] = {1, 1};
 	uint64_t row3[] = {2, 1};
-	uint64_t row4[] = {1, 2};
+	uint64_t row4[] = {2, 2};
 	addTableEntry(solver, table, row1, 2, 0);
 	addTableEntry(solver, table, row2, 2, 0);
 	addTableEntry(solver, table, row3, 2, 2);
-- 
2.34.1