src/Test/testcnf.c

   1 #include "constraint.h"
   2 #include <stdio.h>
   3
   4 int main(int numargs, char ** argv) {
   5         CNF *cnf=createCNF();
   6         Edge v1=constraintNewVar(cnf);
   7         Edge v2=constraintNewVar(cnf);
   8         Edge v3=constraintNewVar(cnf);
   9         Edge v4=constraintNewVar(cnf);
  10         Edge v5=constraintNewVar(cnf);
  11
  12         Edge nv1=constraintNegate(v1);
  13         Edge nv2=constraintNegate(v2);
  14         Edge nv3=constraintNegate(v3);
  15         Edge nv4=constraintNegate(v4);
  16
  17         Edge c1=constraintAND2(cnf, v1, nv2);
  18         Edge c2=constraintAND2(cnf, v3, nv4);
  19         Edge c3=constraintAND2(cnf, nv1, v2);
  20         Edge c4=constraintAND2(cnf, nv3, v4);
  21         Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
  22         printCNF(cor);
  23         printf("\n");
  24         addConstraint(cnf, cor);
  25         int value=solveCNF(cnf);
  26         if (value==1) {
  27                 bool v1v=getValueCNF(cnf, v1);
  28                 bool v2v=getValueCNF(cnf, v2);
  29                 bool v3v=getValueCNF(cnf, v3);
  30                 bool v4v=getValueCNF(cnf, v4);
  31                 printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
  32         } else
  33                 printf("%d\n",value);
  34         deleteCNF(cnf);
  35 }