bug fix

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 9e85bfc41dd07536f0c019564053fc7300ad3181..9d6e855ef5e89b22a64e3b0371597c58ff9be380 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -167,7 +167,7 @@ Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
        Edge lneg=constraintNegate(left);
        Edge rneg=constraintNegate(right);
-       Edge eand=constraintAND2(cnf, left, right);
+       Edge eand=constraintAND2(cnf, lneg, rneg);
        return constraintNegate(eand);
 }
 

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index d5f4166796809b70dcbfcd5849be89f05208844d..ddad6d7334c4fc048a4aef5206c69ea157814548 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -10,13 +10,17 @@ int main(int numargs, char ** argv) {
        printCNF(nv1);
        printf("\n");
        Edge nv2=constraintNegate(v2);
+       Edge nv3=constraintNegate(v3);
        Edge iff1=constraintIFF(cnf, nv1, v2);
        printCNF(iff1);
        printf("\n");
-       Edge iff2=constraintIFF(cnf, nv2, v3);
+
+       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 cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+
        printCNF(cand);
        printf("\n");
        addConstraint(cnf, cand);