From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 05:53:01 +0000 (-0700)
Subject: bug fixes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=80091e255d2d254ea4eb29809c055d757b146c17;p=satune.git

bug fixes
---

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f836fff..fdc69ce 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -191,7 +191,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 
 	/** De-duplicate array */
 	uint lowindex=0;
-	edges[lowindex++]=edges[initindex++];
+	edges[lowindex]=edges[initindex++];
 
 	for(;initindex<numEdges;initindex++) {
 		Edge e1=edges[lowindex];
@@ -201,8 +201,10 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 				return E_False;
 			}
 		} else
-			edges[lowindex++]=edges[initindex];
+			edges[++lowindex]=edges[initindex];
 	}
+	lowindex++; //Make lowindex look like size
+	
 	if (lowindex==1)
 		return edges[0];
 
@@ -225,7 +227,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 		}
 	}
 	
-	return createNode(cnf, NodeType_AND, numEdges, edges);
+	return createNode(cnf, NodeType_AND, lowindex, edges);
 }
 
 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
@@ -327,12 +329,12 @@ void countPass(CNF *cnf) {
 	deleteVectorEdge(ve);
 }
 
-void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
+void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
 	//Skip constants and variables...
-	if (edgeIsVarConst(e))
+	if (edgeIsVarConst(eroot))
 		return;
 
-	clearVectorEdge(stack);pushVectorEdge(stack, e);
+	clearVectorEdge(stack);pushVectorEdge(stack, eroot);
 
 	bool isMatching=cnf->enableMatching;
 	
@@ -561,7 +563,7 @@ void produceCNF(CNF * cnf, Edge e) {
 
 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
 	if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
-		if (dest == NULL) {
+		if (*dest == NULL) {
 			*dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 		} else if (isProxy(*dest)) {
 			bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 82f926d..9405009 100644
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -9,8 +9,9 @@ int main(int numargs, char ** argv) {
 	Edge nv2=constraintNegate(v2);
 	Edge iff1=constraintIFF(cnf, nv1, v2);
 	Edge iff2=constraintIFF(cnf, nv2, v3);
-	Edge iff3=constraintIFF(cnf, v3, nv1);
-	Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+	//	Edge iff3=constraintIFF(cnf, v3, nv1);
+	//Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+	Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
 	addConstraint(cnf, cand);
 	solveCNF(cnf);
 	deleteCNF(cnf);