src/Test/ordergraphtest.cc

   1 #include "csolver.h"
   2
   3 int main(int numargs, char **argv) {
   4         CSolver *solver = new CSolver();
   5         uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
   6         Set *s = solver->createSet(0, set1, 8);
   7         Order *order = solver->createOrder(SATC_TOTAL, s);
   8         BooleanEdge o12 =  solver->orderConstraint(order, 1, 2);
   9         BooleanEdge o13 =  solver->orderConstraint(order, 1, 3);
  10         BooleanEdge o24 =  solver->orderConstraint(order, 2, 4);
  11         BooleanEdge o34 =  solver->orderConstraint(order, 3, 4);
  12         BooleanEdge o41 =  solver->orderConstraint(order, 4, 1);
  13         BooleanEdge o57 =  solver->orderConstraint(order, 5, 7);
  14         BooleanEdge o76 =  solver->orderConstraint(order, 7, 6);
  15         BooleanEdge o65 =  solver->orderConstraint(order, 6, 5);
  16         BooleanEdge o58 =  solver->orderConstraint(order, 5, 8);
  17         BooleanEdge o81 =  solver->orderConstraint(order, 8, 1);
  18
  19         BooleanEdge array1[] = {o12, o13, o24, o34};
  20         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );
  21         BooleanEdge array2[] = {o41, o57};
  22
  23         BooleanEdge b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
  24         BooleanEdge array3[] = {o34};
  25         BooleanEdge o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
  26         BooleanEdge array4[] = {o24};
  27         BooleanEdge o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
  28         BooleanEdge array5[] = {o34n, o24n};
  29         BooleanEdge b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
  30         BooleanEdge array6[] = {b1, b2};
  31         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
  32
  33         BooleanEdge array7[] = {o12, o13};
  34         solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
  35
  36         BooleanEdge array8[] = {o76, o65};
  37         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
  38
  39         BooleanEdge array9[] = {o76, o65};
  40         BooleanEdge b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
  41         BooleanEdge array10[] = {o57};
  42         BooleanEdge o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
  43         BooleanEdge array11[] = {b3, o57n};
  44         solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
  45
  46         BooleanEdge array12[] = {o58, o81};
  47         solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
  48         solver->serialize();
  49         /*      if (solver->solve() == 1)
  50            printf("SAT\n");
  51            else
  52            printf("UNSAT\n");*/
  53
  54         solver->autoTune(100);
  55         delete solver;
  56 }