X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FTest%2Ftestcnf.c;fp=src%2FTest%2Ftestcnf.c;h=d5f4166796809b70dcbfcd5849be89f05208844d;hb=6120ecdb7144ce0b55fa57352d9cc4e2411bcd08;hp=940500934efcdf1e7560846afa71098de6113cce;hpb=efc2a0e42452b92cee495c7126fa8f5fc137ca76;p=satune.git

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 9405009..d5f4166 100644
--- 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);
 }