src/Test/testcnf.c

   1 #include "nodeedge.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 nv1=constraintNegate(v1);
  10         printCNF(nv1);
  11         printf("\n");
  12         Edge nv2=constraintNegate(v2);
  13         Edge nv3=constraintNegate(v3);
  14         Edge iff1=constraintIFF(cnf, nv1, v2);
  15         printCNF(iff1);
  16         printf("\n");
  17
  18         Edge iff2=constraintOR2(cnf, constraintAND2(cnf, v2, v3), constraintAND2(cnf, nv2, nv3));
  19         printCNF(iff2);
  20         printf("\n");
  21         Edge iff3=constraintIFF(cnf, v3, nv1);
  22         Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
  23
  24         printCNF(cand);
  25         printf("\n");
  26         addConstraint(cnf, cand);
  27         int value=solveCNF(cnf);
  28         if (value==1) {
  29                 bool v1v=getValueCNF(cnf, v1);
  30                 bool v2v=getValueCNF(cnf, v2);
  31                 bool v3v=getValueCNF(cnf, v3);
  32                 printf("%d %u %u %u\n", value, v1v, v2v, v3v);
  33         } else
  34                 printf("%d\n",value);
  35         deleteCNF(cnf);
  36 }