src/Test/bug_minimal.cc

   1
   2 #include "csolver.h"
   3 /**
   4  * TotalOrder(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
   5  * 0=>1
   6  * 1=>2
   7  * 2=>3
   8  * 1=>4
   9  * 4=>5
  10  * 5=>6
  11  * 1=>7
  12  * 7=>8
  13  * 8=>9
  14  * 9=>2
  15  * 6=>2
  16  *
  17  *
  18  */
  19 int main(int numargs, char **argv) {
  20         CSolver *solver = new CSolver();
  21         uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8, 9};
  22         Set *s = solver->createSet(0, set1, 9);
  23         Order *order = solver->createOrder(SATC_TOTAL, s);
  24         BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
  25         solver->addConstraint(b12);
  26         BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
  27         solver->addConstraint(b23);
  28         BooleanEdge b14 =  solver->orderConstraint(order, 1, 4);
  29         solver->addConstraint(b14);
  30         BooleanEdge b45 =  solver->orderConstraint(order, 4, 5);
  31         solver->addConstraint(b45);
  32         BooleanEdge b56 =  solver->orderConstraint(order, 5, 6);
  33         solver->addConstraint(b56);
  34         BooleanEdge b17 =  solver->orderConstraint(order, 1, 7);
  35         solver->addConstraint(b17);
  36         BooleanEdge b78 =  solver->orderConstraint(order, 7, 8);
  37         solver->addConstraint(b78);
  38         BooleanEdge b89 =  solver->orderConstraint(order, 8, 9);
  39         solver->addConstraint(b89);
  40         BooleanEdge b92 =  solver->orderConstraint(order, 9, 2);
  41         solver->addConstraint(b92);
  42         BooleanEdge b62 =  solver->orderConstraint(order, 6, 2);
  43         solver->addConstraint(b62);
  44
  45         BooleanEdge v6 = solver->getBooleanVar(0);
  46         BooleanEdge v7 = solver->getBooleanVar(0);
  47         BooleanEdge v8 = solver->getBooleanVar(0);
  48         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, solver->applyLogicalOperation(SATC_IFF, v7, v8), v6));
  49         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
  50         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v8));
  51         BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
  52         solver->addConstraint(b48);
  53         BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
  54         solver->addConstraint(b57);
  55
  56
  57         if (solver->solve() == 1) {
  58                 printf("SAT\n");
  59                 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
  60                                          solver->getOrderConstraintValue(order, 5, 1),
  61                                          solver->getOrderConstraintValue(order, 1, 4),
  62                                          solver->getOrderConstraintValue(order, 5, 4),
  63                                          solver->getOrderConstraintValue(order, 1, 5));
  64         } else {
  65                 printf("UNSAT\n");
  66         }
  67         delete solver;
  68 }