Merge branch 'master' into brian

[satune.git] / src / Test / testcnf.c

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index ddad6d7334c4fc048a4aef5206c69ea157814548..ebd79f52f9a788a460d0119e879eec4c8f3a75af 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -1,4 +1,4 @@
-#include "nodeedge.h"
+#include "constraint.h"
 #include <stdio.h>
 
 int main(int numargs, char ** argv) {
@@ -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);