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(TOTAL, s);
   8         Boolean *o12 =  solver->orderConstraint(order, 1, 2);
   9         Boolean *o13 =  solver->orderConstraint(order, 1, 3);
  10         Boolean *o24 =  solver->orderConstraint(order, 2, 4);
  11         Boolean *o34 =  solver->orderConstraint(order, 3, 4);
  12         Boolean *o41 =  solver->orderConstraint(order, 4, 1);
  13         Boolean *o57 =  solver->orderConstraint(order, 5, 7);
  14         Boolean *o76 =  solver->orderConstraint(order, 7, 6);
  15         Boolean *o65 =  solver->orderConstraint(order, 6, 5);
  16         Boolean *o58 =  solver->orderConstraint(order, 5, 8);
  17         Boolean *o81 =  solver->orderConstraint(order, 8, 1);
  18         Boolean *in1 [] = {o12, o13, o24, o34};
  19         solver->addConstraint(solver->applyLogicalOperation( L_OR, in1, 4) );
  20         Boolean *in2[] = {o41, o57};
  21         Boolean *b1 = solver->applyLogicalOperation(L_XOR, in2, 2);
  22         Boolean *in3[]= {o34};
  23         Boolean *o34n = solver->applyLogicalOperation(L_NOT,in3 , 1);
  24         Boolean *in4[] = {o24};
  25         Boolean *o24n = solver->applyLogicalOperation(L_NOT, in4, 1);
  26         Boolean *in5[] ={o34n, o24n};
  27         Boolean *b2 = solver->applyLogicalOperation(L_OR, in5, 2);
  28         Boolean *in6[] = {b1, b2};
  29         solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, in6, 2) );
  30         Boolean *in7[] = {o12, o13};
  31         solver->addConstraint(solver->applyLogicalOperation(L_AND, in7, 2) );
  32         Boolean *in8[] = {o76, o65};
  33         solver->addConstraint(solver->applyLogicalOperation(L_OR, in8, 2) );
  34         Boolean *in9[] = {o76, o65};
  35         Boolean* b3= solver->applyLogicalOperation(L_AND, in9, 2) ;
  36         Boolean *in10[] = {o57};
  37         Boolean* o57n= solver->applyLogicalOperation(L_NOT, in10, 1);
  38         Boolean *in11[] = {b3, o57n};
  39         solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, in11, 2) );
  40         Boolean *in12[] = {o58, o81};
  41         solver->addConstraint(solver->applyLogicalOperation(L_AND, in12, 2) );
  42
  43         if (solver->startEncoding() == 1)
  44         printf("SAT\n");
  45         else
  46         printf("UNSAT\n");
  47
  48         delete solver;
  49 }