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 }