src/Test/buglongclause.cc

   1 #include "csolver.h"
   2
   3 /**
   4  * !b1 AND
   5  * !b2 OR b1 or (!b3 and b4) AND
   6  * b7 OR (!b1 AND (b5 or !b6))
   7  *
   8  */
   9 int main(int numargs, char **argv) {
  10         CSolver *solver = new CSolver();
  11         BooleanEdge b1 = solver->getBooleanVar(0);
  12         BooleanEdge b2 = solver->getBooleanVar(0);
  13         BooleanEdge b3 = solver->getBooleanVar(0);
  14         BooleanEdge b4 = solver->getBooleanVar(0);
  15         BooleanEdge b5 = solver->getBooleanVar(0);
  16         BooleanEdge b6 = solver->getBooleanVar(0);
  17         BooleanEdge b7 = solver->getBooleanVar(0);
  18         //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
  19         BooleanEdge in[] = {b1};
  20         BooleanEdge notb1 = solver->applyLogicalOperation(SATC_NOT, in, 1);
  21         BooleanEdge in2[] = {b2};
  22         BooleanEdge notb2 = solver->applyLogicalOperation(SATC_NOT, in2, 1);
  23         BooleanEdge in3[] = {b3};
  24         BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, in3, 1);
  25         BooleanEdge in4[] = {notb3,b4};
  26         BooleanEdge andnotb3b4 = solver->applyLogicalOperation(SATC_AND, in4, 2);
  27         BooleanEdge in5[] = {notb2, b1, andnotb3b4};
  28         BooleanEdge secondc = solver->applyLogicalOperation(SATC_OR, in5, 3);
  29         BooleanEdge in6[] = {b6};
  30         BooleanEdge notb6 = solver->applyLogicalOperation(SATC_NOT, in6, 1);
  31         BooleanEdge in7[] = {b5,notb6};
  32         BooleanEdge orb5notb6 = solver->applyLogicalOperation(SATC_OR, in7, 2);
  33         BooleanEdge in8[] = {notb1,orb5notb6};
  34         BooleanEdge andnotb1ors = solver->applyLogicalOperation(SATC_AND, in8, 2);
  35         BooleanEdge in9[] = {b7, andnotb1ors};
  36         BooleanEdge third = solver->applyLogicalOperation(SATC_OR, in9, 2);
  37         BooleanEdge in10[] = {secondc, third, notb1};
  38         BooleanEdge final = solver->applyLogicalOperation(SATC_AND, in10, 3);
  39         solver->addConstraint(final);
  40         printf("&&&&&&&&&&&&&&&&&&&&&&&\n");
  41         solver->printConstraints();
  42         if (solver->solve() == 1)
  43                 printf("b1=%d\nb2=%d\nb3=%d\nb4=%d\nb5=%d\nb6=%d\nb7=%d\n",
  44                                          solver->getBooleanValue(b1), solver->getBooleanValue(b2),
  45                                          solver->getBooleanValue(b3), solver->getBooleanValue(b4),
  46                                          solver->getBooleanValue(b5), solver->getBooleanValue(b6),
  47                                          solver->getBooleanValue(b7));
  48         else
  49                 printf("UNSAT\n");
  50         delete solver;
  51 }