/* select_benchmarks.c
 * Morgan Deters mdeters@cse.wustl.edu, 2007
 * For SMT-COMP'07.  See smtcomp.org
 *
 * Read a file with a count of records, then n lines of the form:
 *
 *    division family category difficulty solution benchmarkid file
 *
 * The fields are delimited by a space.  benchmarkid is a nonnegative
 * integer; the rest are strings (with no embedded spaces).  category is
 * one of "check", "crafted", "industrial", and "random".  "difficulty"
 * is an integer in the range [0,5].  "solution" is one of "sat", "unsat",
 * and "unknown".  "unknown" benchmarks are ineligible for selection; all
 * others are eligible.  This program ignores the file field.
 *
 * The input is expected to be grouped on fields, in left-to-right order.
 * That is, all benchmarks in a common division must be listed together;
 * all benchmarks in a common family and division must be listed together;
 * all such benchmarks with a common difficulty must be listed together;
 * and so on.
 *
 * On stdout, produce a list of distinct benchmarkids, one per line,
 * selected for SMT-COMP'07.  The output is in no guaranteed order.
 * There is never any other output on stdout.  On stderr, produce
 * error messages (if any) or a list of statistics (if benchmark
 * selection is successful).  If there is a fatal error, the exit
 * status is nonzero; there may be a partial benchmarkid list on stdout
 * in such cases.  Only if the exit status is zero should the benchmarkid
 * list be used.
 *
 * This is the breakdown for selection:
 *
 *   1. All eligible benchmarks in category "check" are included.
 *
 *   2. For non-"check" benchmarks, division pools are created.  For each
 *      benchmark family, if the family has <= 200 eligible, non-"check"
 *      benchmarks, all are added to the division pool; otherwise,
 *      200 such benchmarks are added to the pool with the following
 *      distribution:
 *        50 with solution "sat"   and difficulty 0, 1, or 2
 *        50 with solution "sat"   and difficulty 3, 4, or 5
 *        50 with solution "unsat" and difficulty 0, 1, or 2
 *        50 with solution "unsat" and difficulty 3, 4, or 5
 *      If 50 are not available in one of these subdivisions, all available,
 *      eligible, non-"check" benchmarks that are available in the subdivision
 *      are included; to make 200, slots are reallocated to other subdivisions
 *      (for which sufficient benchmarks _are_ available) in equal amounts.
 *      Up to 3 slots can still remain unallocated; these are randomly
 *      reallocated to distinct subdivisions (for which sufficient benchmarks
 *      are available) so far as possible, or non-distinct subdivisions if
 *      sufficient benchmarks aren't available in some subdivisions.
 *
 *   3. For each division, N slots are allocated as follows:
 *        .85N from category "industrial"
 *        .10N from category "crafted"
 *        .05N from category "random"
 *      If there are fewer than .10N (resp. .05N) "crafted" or "random"
 *      benchmarks in the division pool, more "industrial" slots are
 *      allocated to make N total for the division.  If there are too few
 *      "industrial" benchmarks in the division pool, more "crafted" slots
 *      are allocated to make N total for the division.
 *
 *   4. For each category in each division, given that it has n slots
 *      allocated to it, the slot allocation is further subdivided as
 *      follows:
 *        floor(n/4) slots for solution "sat"   with difficulty 0, 1, or 2
 *        floor(n/4) slots for solution "sat"   with difficulty 3, 4, or 5
 *        floor(n/4) slots for solution "unsat" with difficulty 0, 1, or 2
 *        floor(n/4) slots for solution "unsat" with difficulty 3, 4, or 5
 *      If there aren't enough benchmarks in the pool meeting one or more of
 *      the above subdivided requirements for the category, the subdivision
 *      allocation is reduced to the number available in the pool that meet
 *      the requirements.  To make up the full category allotment,
 *      remaining slots are allocated equally to subdivisions with enough
 *      benchmarks in the pool meeting their requirements.  As above, up to
 *      3 slots can remain unallocated, and these are randomly allocated to
 *      distinct subdivisions, so far as possible, for which benchmarks are
 *      available in the pool meeting the necessary requirements; otherwise,
 *      they are randomly allocated to non-distinct subdivisions.
 *
 * In the end, N non-"check" benchmarkids per division are output,
 * together with all the "check" benchmarkids.
 *
 * Originally, N was 100.  However, for SMT-COMP'07 it was decided to
 * increase N to 200.
 */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

/* FAMILY_SIZE - the number of benchmarks to include in the division
 * pool from each family */
#define FAMILY_SIZE    200

/* number of non-check benchmarks to include in each division in output */
#define N 200

/* N_POOL_ENTRIES - used to size some arrays; must be at least as
 * large as the total number of eligible non-"check" benchmarks in the
 * largest division */
#define N_POOL_ENTRIES 50000

typedef enum category { INDUSTRIAL, CRAFTED, RANDOM, CHECK } category_t;
typedef enum difficulty { EASY, HARD } difficulty_t;
typedef enum solution { SAT, UNSAT, UNKNOWN } solution_t;

/* whether difficulties are considered easy or hard */
const difficulty_t difficulty_map[] = { EASY, EASY, EASY, HARD, HARD, HARD };

/* # slots available in division selection for each category */
#define CATEGORY_ALLOTMENT { 85*N/100, 10*N/100, 5*N/100 }

/* GCC required */
#define MIN(x,y) \
  ({ unsigned __x = (x); unsigned __y = (y); __x < __y ? __x : __y; })

typedef struct fpool {
  unsigned n;

  struct {
    unsigned n[2][2];     /* [solution][difficulty_map[difficulty]] */
  } solutiondiff;
} fpool_t;

typedef struct dpool {
  unsigned alloc;
  unsigned n;

  struct {
    unsigned first[3][2][2]; /* [category][solution][difficulty_map[difficulty]] */
    unsigned n[3][2][2];     /* [category][solution][difficulty_map[difficulty]] */
    unsigned nc[3];	     /* [category] */
    unsigned next[N_POOL_ENTRIES];
    category_t values[N_POOL_ENTRIES];
  } category;

  struct {
    unsigned first[2][2]; /* [solution][difficulty_map[difficulty]] */
    unsigned n[2][2];     /* [solution][difficulty_map[difficulty]] */
    unsigned next[N_POOL_ENTRIES];
  } solutiondiff;

  unsigned entries[N_POOL_ENTRIES];
} dpool_t;

char *prog;

dpool_t dpool;
fpool_t fpool;

int main(int argc, char *argv[]) {
  char last_division[256] = "", last_family[256] = "";
  char first = 1;
  unsigned lines = 1, nlines;
  unsigned seed;
  unsigned long l;
  char buf[1024];
  char *end;
  FILE *fp;

  /* get the basename of argv[0], for error messages */
  prog = strrchr(argv[0], '/');
  prog = prog ? prog + 1 : argv[0];

  if(argc != 3 && argc != 4) {
    fprintf(stderr, "usage: %s random-seed benchmarks-file\n", prog);
    exit(1);
  }

  l = strtoul(argv[1], &end, 0);
  if(*end) {
    fprintf(stderr, "%s: improper random seed `%s'\n", prog, argv[1]);
    exit(1);
  }
  if(l >= (1 << 30)) {
    fprintf(stderr, "%s: random seed must be in the range [0,2^30)\n", prog);
    exit(1);
  }

  seed = (unsigned) l;
  fprintf(stderr, "seeding with %u\n", seed);
  srandom(seed);

  if(!(fp = fopen(argv[2], "r"))) {
    fprintf(stderr, "%s: cannot open benchmarks file `%s'\n", prog, argv[2]);
    exit(1);
  }

  if(!fgets(buf, sizeof(buf), fp)) {
    fprintf(stderr, "%s: error reading file `%s' at line 1\n", prog, argv[2]);
    exit(1);
  }
  nlines = (unsigned) strtoul(buf, &end, 10);

  while(fgets(buf, sizeof(buf), fp)) {
    char *division, *family, *s_category, *s_difficulty;
    char *s_solution, *s_benchmarkid, *file;
    unsigned difficulty, benchmarkid;
    solution_t solution;
    category_t category;

    ++lines;
    size_t len = strlen(buf);
    if(buf[len - 1] != '\n') {
      fprintf(stderr, "%s: `%s' line %u too long (max len %d characters)\n",
	      prog, argv[2], lines, sizeof(buf) - 2);
      exit(1);
    }

    if( !(division      = buf) ||
	!(family        = strchr(division,          ' ')) ||
	!(s_category    = strchr(family + 1,        ' ')) || 
	!(s_difficulty  = strchr(s_category + 1,    ' ')) ||
	!(s_solution    = strchr(s_difficulty + 1,  ' ')) ||
	!(s_benchmarkid = strchr(s_solution + 1,    ' ')) ||
	!(file          = strchr(s_benchmarkid + 1, ' ')) ) {
      fprintf(stderr, "%s: `%s' line %u malformed\n", prog, argv[2], lines);
      exit(1);
    }

    /* these things are pointing to the spaces _before_ their fields;
     * fix them */
    *family++ = 0;
    *s_category++ = 0;
    *s_difficulty++ = 0;
    *s_solution++ = 0;
    *s_benchmarkid++ = 0;
    *file++ = 0;

    difficulty = (unsigned) strtoul(s_difficulty, &end, 10);

    benchmarkid = (unsigned) strtoul(s_benchmarkid, &end, 10);
    if(*end) {
      fprintf(stderr, "%s: `%s' line %u: bad benchmarkid `%s'\n",
	      prog, argv[2], lines, s_benchmarkid);
      exit(1);
    }

    if(!strcmp(s_solution, "sat"))
      solution = SAT;
    else if(!strcmp(s_solution, "unsat"))
      solution = UNSAT;
    else if(!strcmp(s_solution, "unknown"))
      solution = UNKNOWN;
    else {
      fprintf(stderr, "%s: `%s' line %u: bad solution `%s'\n",
	      prog, argv[2], lines, s_solution);
      exit(1);
    }

    if((*end || difficulty > 5) && solution != UNKNOWN) {
      fprintf(stderr, "%s: `%s' line %u: bad difficulty `%s'\n",
	      prog, argv[2], lines, s_difficulty);
      exit(1);
    }

    if(!strcmp(s_category, "check")) {
      category = CHECK;
    } else if(!strcmp(s_category, "industrial"))
      category = INDUSTRIAL;
    else if(!strcmp(s_category, "crafted"))
      category = CRAFTED;
    else if(!strcmp(s_category, "random"))
      category = RANDOM;
    else {
      fprintf(stderr, "%s: `%s' line %u: bad category `%s'\n",
	      prog, argv[2], lines, s_category);
      exit(1);
    }

    if(category == CHECK) {
      puts(s_benchmarkid);
      continue;
    }
    if(solution == UNKNOWN)
      continue;

    if(first) {
      strcpy(last_family, family);
      strcpy(last_division, division);
    } else if(strcmp(family, last_family) ||strcmp(division, last_division)) {
      /* end of family; add last_family contribution to division pool */
      unsigned i, j;

      fprintf(stderr, "family %s\n  %u benchmarks", last_family, fpool.n);

      if(fpool.n > FAMILY_SIZE) {
	/* do selection to get down to FAMILY_SIZE */
	unsigned slots[2][2];
	unsigned total = 0;
	unsigned limited = 0;

	fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [eligible non-check]",
		fpool.solutiondiff.n[SAT][EASY],
		fpool.solutiondiff.n[SAT][HARD],
		fpool.solutiondiff.n[UNSAT][EASY],
		fpool.solutiondiff.n[UNSAT][HARD]);

	for(i = 0; i < 2; ++i)
	  for(j = 0; j < 2; ++j)
	    if(fpool.solutiondiff.n[i][j] <= FAMILY_SIZE / 4) {
	      total += slots[i][j] = fpool.solutiondiff.n[i][j];
	      ++limited;
	    } else total += slots[i][j] = FAMILY_SIZE / 4;

	while(total < FAMILY_SIZE) {
	  unsigned each = (FAMILY_SIZE - total) / (4 - limited);
	  if(each == 0)
	    break;
	  for(i = 0; i < 2; ++i)
	    for(j = 0; j < 2; ++j)
	      if(slots[i][j] < fpool.solutiondiff.n[i][j]) {
		if(slots[i][j] + each > fpool.solutiondiff.n[i][j]) {
		  total -= slots[i][j];
		  total += slots[i][j] = fpool.solutiondiff.n[i][j];
		  ++limited;
		} else {
		  slots[i][j] += each;
		  total += each;
		  if(slots[i][j] == fpool.solutiondiff.n[i][j])
		    ++limited;
		}
	      }
	}

	while(total < FAMILY_SIZE) {
	  long n1, n2 = -1, n3 = -1;
	  n1 = random() % (4 - limited);
	  if(total < FAMILY_SIZE - 1 && limited <= 2) {
	    n2 = random() % (3 - limited);
	    if(n2 == n1) ++n2;
	  }
	  if(total < FAMILY_SIZE - 2 && limited <= 1) {
	    n3 = random() % (2 - limited);
	    if(n3 == n1 || n3 == n2) ++n3;
	    if(n3 == n1 || n3 == n2) ++n3;
	  }

	  for(i = 0; i < 2; ++i)
	    for(j = 0; j < 2; ++j)
	      if(slots[i][j] < fpool.solutiondiff.n[i][j] &&
		 (n1-- == 0 || n2-- == 0 || n3-- == 0)) {
		++total;
		if(++slots[i][j] == fpool.solutiondiff.n[i][j])
		  ++limited;
	      }
	}

	fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [to division pool]\n",
		slots[SAT][EASY],
		slots[SAT][HARD],
		slots[UNSAT][EASY],
		slots[UNSAT][HARD]);

	for(i = 0; i < 2; ++i)
	  for(j = 0; j < 2; ++j) {
            /*fprintf(stderr,"beforeward:[%u][%u] %u slots, fpool has %u, dpool has %u\n", i, j, slots[i][j], fpool.solutiondiff.n[i][j], dpool.solutiondiff.n[i][j]);
	    fprintf(stderr,"\nhave [n=%u]:\n", dpool.solutiondiff.n[i][j]);
	    if(dpool.solutiondiff.n[i][j]) {
	      unsigned x = dpool.solutiondiff.first[i][j];
	      int k = 0;
	      do {
	        fprintf(stderr, "%3u[%u][%u] :: %3u %5u\n", k, i, j, x, dpool.entries[x]);
	        x = dpool.solutiondiff.next[x];
	      } while(++k < dpool.solutiondiff.n[i][j]);
	    }*/

	    while(slots[i][j] < fpool.solutiondiff.n[i][j]) {
	      long n = random() % fpool.solutiondiff.n[i][j];
	      unsigned *x = &dpool.solutiondiff.first[i][j];
	      while(n--)
		x = &dpool.solutiondiff.next[*x];

              //fprintf(stderr,"cutting %3u %5u [%u][%u], next=%3u %5u\n",*x,dpool.entries[*x],i,j,dpool.solutiondiff.next[*x],dpool.entries[dpool.solutiondiff.next[*x]]);

	      /*dpool.category.values[*x] = -1;*/

	      *x = dpool.solutiondiff.next[*x];
	      --fpool.solutiondiff.n[i][j];
	      --dpool.solutiondiff.n[i][j];
	      --fpool.n;
	      --dpool.n;
	    }
            /*fprintf(stderr,"afterward: [%u][%u] %u slots, fpool has %u, dpool has %u\n", i, j, slots[i][j], fpool.solutiondiff.n[i][j], dpool.solutiondiff.n[i][j]);
	    fprintf(stderr,"\nhave [n=%u]:\n", dpool.solutiondiff.n[i][j]);
	    if(dpool.solutiondiff.n[i][j]) {
	      unsigned x = dpool.solutiondiff.first[i][j];
	      int k = 0;
	      do {
	        fprintf(stderr, "%3u[%u][%u] :: %3u %5u\n", k, i, j, x, dpool.entries[x]);
	        x = dpool.solutiondiff.next[x];
	      } while(++k < dpool.solutiondiff.n[i][j]);
	    }*/
          }
      } else {
	fprintf(stderr, ", all go to division pool\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [to division pool]\n",
		fpool.solutiondiff.n[SAT][EASY],
		fpool.solutiondiff.n[SAT][HARD],
		fpool.solutiondiff.n[UNSAT][EASY],
		fpool.solutiondiff.n[UNSAT][HARD]);
      }
      /*fprintf(stderr, "\nafter, in dpool:\n  %u easySAT,\n  %u hardSAT,\n  %u easyUNSAT\n  %u hardUNSAT\n\n", dpool.solutiondiff.n[SAT][EASY], dpool.solutiondiff.n[SAT][HARD], dpool.solutiondiff.n[UNSAT][EASY], dpool.solutiondiff.n[UNSAT][HARD]);
      for(i = 0; i < 2; ++i)
	for(j = 0; j < 2; ++j) {
	  fprintf(stderr,"\nhave [n=%u]:\n", dpool.solutiondiff.n[i][j]);
	  if(dpool.solutiondiff.n[i][j]) {
	    unsigned x = dpool.solutiondiff.first[i][j];
	    int k = 0;
	    do {
	      fprintf(stderr, "%3u[%u][%u] :: %3u %5u\n", k, i, j, x, dpool.entries[x]);
	      x = dpool.solutiondiff.next[x];
	    } while(++k < dpool.solutiondiff.n[i][j]);
	  }
	}*/

      /* reset family counters */
      fpool.n = 0;
      memset(fpool.solutiondiff.n, 0, sizeof(fpool.solutiondiff.n));

      strcpy(last_family, family);
    }
    if(!first && strcmp(division, last_division)) {
      /* end of division; select from division pool */
      unsigned i, j, x, c;

      fprintf(stderr, "division %s, %u benchmarks in pool", last_division, dpool.n);
      fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [pool totals]",
	      dpool.solutiondiff.n[SAT][EASY],
	      dpool.solutiondiff.n[SAT][HARD],
	      dpool.solutiondiff.n[UNSAT][EASY],
	      dpool.solutiondiff.n[UNSAT][HARD]);

      /* generate category reverse map */
      dpool.category.nc[INDUSTRIAL] = 0;
      dpool.category.nc[CRAFTED] = 0;
      dpool.category.nc[RANDOM] = 0;
      for(i = 0; i < 2; ++i)
	for(j = 0; j < 2; ++j) {
	  /*fprintf(stderr,"\nhave [n=%u]:\n", dpool.solutiondiff.n[i][j]);
	  if(dpool.solutiondiff.n[i][j]) {
	    unsigned x = dpool.solutiondiff.first[i][j];
	    int k = 0;
	    do {
	      fprintf(stderr, "%3u[%u][%u] :: %3u %5u\n", k, i, j, x, dpool.entries[x]);
	      x = dpool.solutiondiff.next[x];
	    } while(++k < dpool.solutiondiff.n[i][j]);
	  }*/

	  dpool.category.n[INDUSTRIAL][i][j] = 0;
	  dpool.category.n[CRAFTED][i][j] = 0;
	  dpool.category.n[RANDOM][i][j] = 0;
	  if(dpool.solutiondiff.n[i][j]) {
	    int k = 1;
	    x = dpool.solutiondiff.first[i][j];
	    do {
	      category_t cat = dpool.category.values[x];
	      assert(cat >= 0 && cat <= 2);
	      ++dpool.category.n[cat][i][j];
	      ++dpool.category.nc[cat];
	      dpool.category.next[x] = dpool.category.first[cat][i][j];
	      dpool.category.first[cat][i][j] = x;
	      x = dpool.solutiondiff.next[x];
	    } while(++k <= dpool.solutiondiff.n[i][j]);
	  }
	}

      fprintf(stderr, "\n %4u industr,%4u crafted,%4u random                   [pool totals]",
	      dpool.category.nc[INDUSTRIAL],
	      dpool.category.nc[CRAFTED],
	      dpool.category.nc[RANDOM]);
      fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [industrial]",
	      dpool.category.n[INDUSTRIAL][SAT][EASY],
	      dpool.category.n[INDUSTRIAL][SAT][HARD],
	      dpool.category.n[INDUSTRIAL][UNSAT][EASY],
	      dpool.category.n[INDUSTRIAL][UNSAT][HARD]);
      fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [crafted]",
	      dpool.category.n[CRAFTED][SAT][EASY],
	      dpool.category.n[CRAFTED][SAT][HARD],
	      dpool.category.n[CRAFTED][UNSAT][EASY],
	      dpool.category.n[CRAFTED][UNSAT][HARD]);
      fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [random]",
	      dpool.category.n[RANDOM][SAT][EASY],
	      dpool.category.n[RANDOM][SAT][HARD],
	      dpool.category.n[RANDOM][UNSAT][EASY],
	      dpool.category.n[RANDOM][UNSAT][HARD]);

      unsigned cslots[3] = CATEGORY_ALLOTMENT;
      if(dpool.category.nc[RANDOM] < cslots[RANDOM]) {
	cslots[INDUSTRIAL] += cslots[RANDOM] - dpool.category.nc[RANDOM];
	cslots[RANDOM] = dpool.category.nc[RANDOM];
      }
      if(dpool.category.nc[CRAFTED] < cslots[CRAFTED]) {
	cslots[INDUSTRIAL] += cslots[CRAFTED] - dpool.category.nc[CRAFTED];
	cslots[CRAFTED] = dpool.category.nc[CRAFTED];
	if(dpool.category.nc[INDUSTRIAL] < cslots[INDUSTRIAL]) {
	  cslots[RANDOM] += cslots[INDUSTRIAL] - dpool.category.nc[INDUSTRIAL];
	  cslots[INDUSTRIAL] = dpool.category.nc[INDUSTRIAL];
	}
      } else if(dpool.category.nc[INDUSTRIAL] < cslots[INDUSTRIAL]) {
	cslots[CRAFTED] += cslots[INDUSTRIAL] - dpool.category.nc[INDUSTRIAL];
	cslots[INDUSTRIAL] = dpool.category.nc[INDUSTRIAL];
      }

      fprintf(stderr, "\n %4u industr,%4u crafted,%4u random                   [slot allotments]\n",
	      cslots[INDUSTRIAL],
	      cslots[CRAFTED],
	      cslots[RANDOM]);

      assert(cslots[INDUSTRIAL] + cslots[CRAFTED] + cslots[RANDOM] == N);
      if(dpool.category.nc[INDUSTRIAL] < cslots[INDUSTRIAL] ||
         dpool.category.nc[CRAFTED] < cslots[CRAFTED]) {
	fprintf(stderr,"CANNOT DO THIS DIVISION - NOT ENOUGH BENCHMARKS\n");
	fprintf(stderr,"industrial in dpool: %u\nslots for industrial: %u\n",dpool.category.nc[INDUSTRIAL],cslots[INDUSTRIAL]);
	fprintf(stderr,"crafted in dpool: %u\nslots for crafted: %u\n",dpool.category.nc[CRAFTED],cslots[CRAFTED]);
	fprintf(stderr,"random in dpool: %u\nslots for random: %u\n",dpool.category.nc[RANDOM],cslots[RANDOM]);
	cslots[INDUSTRIAL] = dpool.category.nc[INDUSTRIAL];
	cslots[CRAFTED] = dpool.category.nc[CRAFTED];
      }
      assert(dpool.category.nc[INDUSTRIAL] >= cslots[INDUSTRIAL]);
      assert(dpool.category.nc[CRAFTED] >= cslots[CRAFTED]);
      assert(dpool.category.nc[RANDOM] >= cslots[RANDOM]);

      for(c = 0; c < 3; ++c) {
	unsigned slots[2][2];
	unsigned total = 0;
	unsigned limited = 0;

	fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [cat %d avail]",
		dpool.category.n[c][SAT][EASY],
		dpool.category.n[c][SAT][HARD],
		dpool.category.n[c][UNSAT][EASY],
		dpool.category.n[c][UNSAT][HARD],
		c);

	for(i = 0; i < 2; ++i)
	  for(j = 0; j < 2; ++j)
	    if(dpool.category.n[c][i][j] <= cslots[c] / 4) {
	      total += slots[i][j] = dpool.category.n[c][i][j];
	      ++limited;
	    } else total += slots[i][j] = cslots[c] / 4;

	while(total < cslots[c]) {
	  unsigned each = (cslots[c] - total) / (4 - limited);
	  if(each == 0)
	    break;
	  for(i = 0; i < 2; ++i)
	    for(j = 0; j < 2; ++j)
	      if(slots[i][j] < dpool.category.n[c][i][j]) {
		if(slots[i][j] + each > dpool.category.n[c][i][j]) {
		  total -= slots[i][j];
		  total += slots[i][j] = dpool.category.n[c][i][j];
		  ++limited;
		} else {
		  slots[i][j] += each;
		  total += each;
		  if(slots[i][j] == dpool.category.n[c][i][j])
		    ++limited;
		}
	      }
	}

	while(total < cslots[c]) {
	fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [cat %d allotmentx]",
		slots[SAT][EASY],
		slots[SAT][HARD],
		slots[UNSAT][EASY],
		slots[UNSAT][HARD],
		c);
	  long n1, n2 = -1, n3 = -1;
	  n1 = random() % (4 - limited);
	  if(total < cslots[c] - 1 && limited <= 2) {
	    n2 = random() % (3 - limited);
	    if(n2 == n1) ++n2;
	  }
	  if(total < cslots[c] - 2 && limited <= 1) {
	    n3 = random() % (2 - limited);
	    if(n3 == n1 || n3 == n2) ++n3;
	    if(n3 == n1 || n3 == n2) ++n3;
	  }

	  for(i = 0; i < 2; ++i)
	    for(j = 0; j < 2; ++j)
	      if(slots[i][j] < dpool.category.n[c][i][j] &&
		 (n1-- == 0 || n2-- == 0 || n3-- == 0)) {
		++total;
		if(++slots[i][j] == dpool.category.n[c][i][j])
		  ++limited;
	      }
	}

	fprintf(stderr, "\n %4u easySAT,%4u hardSAT,%4u easyUNSAT,%4u hardUNSAT [cat %d allotment]\n",
		slots[SAT][EASY],
		slots[SAT][HARD],
		slots[UNSAT][EASY],
		slots[UNSAT][HARD],
		c);

	for(i = 0; i < 2; ++i)
	  for(j = 0; j < 2; ++j) {
	    /*if(dpool.category.n[c][i][j]) {
	      unsigned x = dpool.category.first[c][i][j];
	      int k = 0;
	      do {
		fprintf(stderr, "%3u[%u][%u][%u] :: %5u\n", k, c, i, j, dpool.entries[x]);
		x = dpool.category.next[x];
	      } while(++k < dpool.category.n[c][i][j]);
	    }*/

	    while(slots[i][j]--) {
	      long n = random() % dpool.category.n[c][i][j];
	      unsigned *x = &dpool.category.first[c][i][j];
	      //printf("%5u ", n);
	      //fprintf(stderr,"%5u ", n);
	      while(n--)
		x = &dpool.category.next[*x];

	      //printf("%u %u %u %u\n", c, i, j, dpool.entries[*x]);
	      //fprintf(stderr,"%u %u %u %u\n", c, i, j, dpool.entries[*x]);
	      printf("%u\n", dpool.entries[*x]);

	      *x = dpool.category.next[*x];
	      --dpool.category.n[c][i][j];
	    }
	  }
      }
      fflush(stderr);
      fflush(stdout);

      /* reset division counters */
      dpool.n = 0;
      dpool.alloc = 0;
      memset(dpool.solutiondiff.n, 0, sizeof(dpool.solutiondiff.n));

      strcpy(last_division, division);
    }
    first = 0;

    assert(dpool.alloc < N_POOL_ENTRIES);
    dpool.category.values[dpool.alloc] = category;
    ++fpool.solutiondiff.n[solution][difficulty_map[difficulty]];
    ++dpool.solutiondiff.n[solution][difficulty_map[difficulty]];
    dpool.solutiondiff.next[dpool.alloc] =
      dpool.solutiondiff.first[solution][difficulty_map[difficulty]];
    dpool.solutiondiff.first[solution][difficulty_map[difficulty]] = dpool.alloc;
    dpool.entries[dpool.alloc++] = benchmarkid;
    ++dpool.n;
    ++fpool.n;

    //fprintf(stderr,"added %3u %5u [%u][%u], next=%3u %5u\n",dpool.alloc-1,benchmarkid,solution,difficulty_map[difficulty],dpool.solutiondiff.next[dpool.alloc-1],dpool.entries[dpool.solutiondiff.next[dpool.alloc-1]]);

    /*
    fprintf(stderr,"added : %5u\n", benchmarkid);
    if(dpool.solutiondiff.n[solution][difficulty_map[difficulty]]) {
      unsigned x = dpool.solutiondiff.first[solution][difficulty_map[difficulty]];
      int k = 0;
      do {
	fprintf(stderr, "%3u[%u][%u] :: %5u\n", k, solution, difficulty_map[difficulty], dpool.entries[x]);
	x = dpool.solutiondiff.next[x];
      } while(++k < dpool.solutiondiff.n[solution][difficulty_map[difficulty]]);
    }
    */
  }

  if(!feof(fp)) {
    fprintf(stderr, "%s: error reading file `%s' at line %u/%u\n",
	    prog, argv[1], lines, nlines);
    exit(1);
  }

  fclose(fp);

  return 0;
}