Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...

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

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index ebd79f52f9a788a460d0119e879eec4c8f3a75af..6740543ffaeef71821e83a5f0721310e1866295c 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -7,7 +7,6 @@ int main(int numargs, char ** argv) {
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
        Edge v4=constraintNewVar(cnf);
-       Edge v5=constraintNewVar(cnf);
 
        Edge nv1=constraintNegate(v1);
        Edge nv2=constraintNegate(v2);
@@ -18,10 +17,10 @@ int main(int numargs, char ** argv) {
        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);
+       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4));
        printCNF(cor);
        printf("\n");
-       addConstraint(cnf, cor);
+       addConstraintCNF(cnf, cor);
        int value=solveCNF(cnf);
        if (value==1) {
                bool v1v=getValueCNF(cnf, v1);