/*
SAT competition Random 3CNF generator
Copyright (C) 2002 Laurent Simon

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*/

#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <unistd.h>
#include "my_random.h"

#define LENGTH 3

int devrandom=1;
int verbose=0;

int **tabclauses;

int getrand(int max) {
 return(1+(int) ((double) max * my_rand()/(RAND_MAX+1.0)));
} 

int main(int argc, char** argv)
{   int nbc, nbv;
  int graine;
  FILE  *fin, *fout;
  int i,j;
  int a,b;
  int checkedclause, checkedlit;
  int k, i2, newlit;
  int j2, nblitcommon;

  if (argc<3) {
    fprintf(stderr,"Usage: genAlea nbc nbv\n3CNF uniform random generation.\n");
    exit(1);
  }
  
  nbc = atoi(argv[1]);
  nbv = atoi(argv[2]);

  // Initialisation soigneuse de la graine aléatoire...
  if (argc>3) 
    graine = atoi(argv[3]);
  else {
    graine = ((int)(time((time_t*)NULL))) + ((int)clock());
    graine += getpid() + getppid()*256;
    if(devrandom) {
      if (verbose)
	fprintf(stderr,"Opening /dev/urandom...");fflush(stderr);
      fin = fopen("/dev/urandom","r");
      if (fin>0) {
	if (verbose)
	  fprintf(stderr,"Reading 4 bytes...");fflush(stderr);
	graine += ((fgetc(fin)) << 24) + ((fgetc(fin))<<16) + 
	  (fgetc(fin) << 8) + 
	  fgetc(fin);
	if (verbose)
	  fprintf(stderr,"Closed.\n",a,b);
	fclose(fin);
      }
  }
  }
  if (graine<0) graine = -graine;

  my_srand(graine);
 
  if (verbose)
    fprintf(stderr,"Initializing random seed to %d.\n",graine);

 fout = stdout;  
 
 fprintf(fout,"c genAlea with seed %d\n",graine);
 fprintf(fout,"p cnf %d %d\n",nbv,nbc);

 tabclauses = (int **) malloc(sizeof(int)*nbc);
 for(i=0;i<nbc;i++) {
  tabclauses[i] = (int*)malloc(sizeof(int)*3);
  checkedclause = 1;
  while (checkedclause) {
    for(j=0;j<LENGTH;j++) {
      checkedlit = 1;
      while (checkedlit) {
	checkedlit = 0;
	newlit = (my_rand()%2?(-1):1) * (getrand(nbv));
	for(k=0;k<j;k++)
	  if (abs(newlit) == abs(tabclauses[i][k])) 
	    checkedlit = 1;
      }
      tabclauses[i][j] = newlit;
    }

    // Check if the clause already exists.
    // To speed-up generation, I could use hash-tables to check
    // uniqueness of triplet 
    // but I'm lazy today...
    checkedclause = 0;
    for(i2=0;i2<i;i2++) {
      nblitcommon=0;
      for(j2=0;j2<3;j2++) {
	if ((tabclauses[i][j2] == tabclauses[i2][0]) ||
	    (tabclauses[i][j2] == tabclauses[i2][1]) ||
	    (tabclauses[i][j2] == tabclauses[i2][2])) 
	  nblitcommon++;
      }
      if (nblitcommon == 3) {
	checkedclause = 1;
	break;
      }
    }
  }
 }
 


 for(i=0;i<nbc;i++) {
  for(j=0;j<LENGTH;j++)
    fprintf(stdout,"%d ",tabclauses[i][j]);
  fprintf(stdout,"0\n");
 }

 return(0);
}