src/Test/orderbm.cc

   1 #include <stdlib.h>
   2 #include "csolver.h"
   3 /**
   4  * TotalOrder(5, 1, 4)
   5  * 5 => 1
   6  * 1 => 4
   7  * Result: O(5,1)=0 O(1,4)=0 O(5,4)=0 O(1,5)=1 O(1111,5)=2
   8  */
   9 int main(int numargs, char **argv) {
  10   if (numargs < 4) {
  11     printf("Requires the following arguments: numpoints numclauses maxclausesize randomseed\n");
  12     return -1;
  13   }
  14   int numpoints = atoi(argv[1]);
  15   int numclauses = atoi(argv[2]);
  16   int maxclause = atoi(argv[3]);
  17   srandom(atoi(argv[4]));
  18
  19   CSolver *solver = new CSolver();
  20   Set *s =solver->createRangeSet(0, 0, numpoints);
  21   Order *order = solver->createOrder(SATC_TOTAL, s);
  22   BooleanEdge be[maxclause];
  23   for(int i = 0; i < numclauses; i++) {
  24     int numterms = (random() % (maxclause -1)) + 1;
  25
  26     for(int j = 0; j < numterms; j++) {
  27       uint src = random() % (numpoints - 1);
  28       uint dst;
  29       do {
  30         dst = random() % numpoints;
  31       } while (src == dst || ((false) && (src > dst)));
  32
  33       be[j] =  solver->orderConstraint(order, src, dst);
  34     }
  35     solver->addConstraint(solver->applyLogicalOperation(SATC_OR, be, numterms));
  36   }
  37   solver->serialize();
  38   if (solver->solve() == 1) {
  39     printf("SAT\n");
  40   } else {
  41     printf("UNSAT\n");
  42   }
  43   delete solver;
  44 }