src/Test/cnftest.cc

   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
  11         Edge nv1 = constraintNegate(v1);
  12         Edge nv2 = constraintNegate(v2);
  13         Edge nv3 = constraintNegate(v3);
  14         Edge nv4 = constraintNegate(v4);
  15
  16         Edge c1 = constraintAND2(cnf, v1, nv2);
  17         Edge c2 = constraintAND2(cnf, v3, nv4);
  18         Edge c3 = constraintAND2(cnf, nv1, v2);
  19         Edge c4 = constraintAND2(cnf, nv3, v4);
  20         Edge cor = constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4));
  21         printCNF(cor);
  22         printf("\n");
  23         addConstraintCNF(cnf, cor);
  24         int value = solveCNF(cnf);
  25         if (value == 1) {
  26                 bool v1v = getValueCNF(cnf, v1);
  27                 bool v2v = getValueCNF(cnf, v2);
  28                 bool v3v = getValueCNF(cnf, v3);
  29                 bool v4v = getValueCNF(cnf, v4);
  30                 printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
  31         } else
  32                 printf("%d\n",value);
  33         deleteCNF(cnf);
  34 }