bug fixes

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f836fff7a83f16e6245c80fdccaa98ad2c842d31..fdc69ce4a040e01f992dcef5f75787f4bc7fd1d6 100644 (file)
--- 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 82f926de0b4cdfe63bc2f761f6868fa7add3c6d0..940500934efcdf1e7560846afa71098de6113cce 100644 (file)
--- 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);