Another bug fix

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

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 940500934efcdf1e7560846afa71098de6113cce..d5f4166796809b70dcbfcd5849be89f05208844d 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -1,4 +1,5 @@
 #include "nodeedge.h"
+#include <stdio.h>
 
 int main(int numargs, char ** argv) {
        CNF *cnf=createCNF();
@@ -6,13 +7,26 @@ int main(int numargs, char ** argv) {
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
        Edge nv1=constraintNegate(v1);
+       printCNF(nv1);
+       printf("\n");
        Edge nv2=constraintNegate(v2);
        Edge iff1=constraintIFF(cnf, nv1, v2);
+       printCNF(iff1);
+       printf("\n");
        Edge iff2=constraintIFF(cnf, nv2, v3);
-       //      Edge iff3=constraintIFF(cnf, v3, nv1);
-       //Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
-       Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+       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);
-       solveCNF(cnf);
+       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);
+       } else
+               printf("%d\n",value);
        deleteCNF(cnf);
 }