From f73199bcd272bfa10aa58f514827454cd986d067 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 22:43:23 -0700
Subject: [PATCH] Bug fix

---
 src/Backend/constraint.c    | 17 ++++++++++-------
 src/Test/buildconstraints.c |  4 ++--
 src/Test/testcnf.c          | 27 +++++++++++++--------------
 3 files changed, 25 insertions(+), 23 deletions(-)

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 6065e5f..7f65364 100644
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -232,7 +232,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 			return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 		}
 	}
-	
+
 	return createNode(cnf, NodeType_AND, lowindex, edges);
 }
 
@@ -397,8 +397,8 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
 				n->intAnnot[polarity]=1;
 				for (uint i=0;i<n->numEdges;i++) {
 					Edge succ=n->edges[i];
-					succ=constraintNegateIf(succ, polarity);
 					if(!edgeIsVarConst(succ)) {
+						succ=constraintNegateIf(succ, polarity);
 						pushVectorEdge(stack, succ);
 					}
 				}
@@ -605,7 +605,7 @@ void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
 	if (exp->litSize == 1) {
 		Literal l = getLiteralLitVector(&exp->singletons, 0);
 		deleteCNFExpr(exp);
-		n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+		n->ptrAnnot[sign] = (void*) ((((intptr_t) l) << 1) | 1);
 	} else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
 		introProxy(cnf, e, exp, sign);
 	} else {
@@ -625,7 +625,7 @@ void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
 	for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 		Literal l=getLiteralLitVector(&expr->singletons,i);
 		Literal clause[] = {-lcond, l};
-		addArrayClauseLiteral(cnf->solver, 1, clause);
+		addArrayClauseLiteral(cnf->solver, 2, clause);
 	}
 	for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 		LitVector *lv=getVectorLitVector(&expr->clauses,i);
@@ -654,7 +654,8 @@ CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
 	Node *n=getNodePtrFromEdge(e);
 	int i = n->numEdges;
 	while (i != 0) {
-		Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+		Edge arg = n->edges[--i];
+		arg=constraintNegateIf(arg, isNeg);
 		Node * narg = getNodePtrFromEdge(arg);
 		
 		if (edgeIsVarConst(arg)) {
@@ -734,7 +735,8 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 	Edge largestEdge;
 	
 	CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
-	if (accum == NULL) accum = allocCNFExprBool(true);
+	if (accum == NULL)
+		accum = allocCNFExprBool(true);
 	
 	int i = getSizeVectorEdge(&cnf->args);
 	while (i != 0) {
@@ -750,7 +752,8 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 				conjoinCNFLit(accum, getProxy(argExp));
 			} else {
 				conjoinCNFExpr(accum, argExp, destroy);
-				if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+				if (destroy)
+					narg->ptrAnnot[isNegEdge(arg)] = NULL;
 			}
 		}
 	}
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 23d943c..222d4a1 100644
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -14,7 +14,7 @@ int main(int numargs, char ** argv) {
 	Order * o=createOrder(solver, TOTAL, s);
 	Boolean * oc=orderConstraint(solver, o, 1, 2);
 	addBoolean(solver, oc);
-	/*	
+		
 	uint64_t set2[] = {2, 3};
 	Set* rangef1 = createSet(solver, 1, set2, 2);
 	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
@@ -38,7 +38,7 @@ int main(int numargs, char ** argv) {
 	Element* inputs2 [] = {e4, e3};
 	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
 	addBoolean(solver, pred);
-	*/
+	
 	startEncoding(solver);
 	deleteSolver(solver);
 }
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 06b83bb..ebd79f5 100644
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -6,30 +6,29 @@ int main(int numargs, char ** argv) {
 	Edge v1=constraintNewVar(cnf);
 	Edge v2=constraintNewVar(cnf);
 	Edge v3=constraintNewVar(cnf);
+	Edge v4=constraintNewVar(cnf);
+	Edge v5=constraintNewVar(cnf);
+
 	Edge nv1=constraintNegate(v1);
-	printCNF(nv1);
-	printf("\n");
 	Edge nv2=constraintNegate(v2);
 	Edge nv3=constraintNegate(v3);
-	Edge iff1=constraintIFF(cnf, nv1, v2);
-	printCNF(iff1);
-	printf("\n");
-
-	Edge iff2=constraintOR2(cnf, constraintAND2(cnf, v2, v3), constraintAND2(cnf, nv2, nv3));
-	printCNF(iff2);
-	printf("\n");
-	Edge iff3=constraintIFF(cnf, v3, nv1);
-	Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+	Edge nv4=constraintNegate(v4);
 
-	printCNF(cand);
+	Edge c1=constraintAND2(cnf, v1, nv2);
+	Edge c2=constraintAND2(cnf, v3, nv4);
+	Edge c3=constraintAND2(cnf, nv1, v2);
+	Edge c4=constraintAND2(cnf, nv3, v4);
+	Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+	printCNF(cor);
 	printf("\n");
-	addConstraint(cnf, cand);
+	addConstraint(cnf, cor);
 	int value=solveCNF(cnf);
 	if (value==1) {
 		bool v1v=getValueCNF(cnf, v1);
 		bool v2v=getValueCNF(cnf, v2);
 		bool v3v=getValueCNF(cnf, v3);
-		printf("%d %u %u %u\n", value, v1v, v2v, v3v);
+		bool v4v=getValueCNF(cnf, v4);
+		printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
 	} else
 		printf("%d\n",value);
 	deleteCNF(cnf);
-- 
2.34.1