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
  19         /* Not Valid c++...Let Hamed fix...
  20            addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
  21            Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
  22            Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
  23            Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
  24            Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
  25            addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
  26            addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
  27            addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
  28            Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
  29            Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
  30            addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
  31            addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
  32
  33            if (solver->startEncoding() == 1)
  34            printf("SAT\n");
  35            else
  36            printf("UNSAT\n");
  37          */
  38         delete solver;
  39 }