/*
SAT competition instance shuffler
Copyright (C) 2002 Laurent Simon and Edward Hirsch

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 <string.h>
//#include "my_random.h"

#define MAXLEN 65000 //Lines should be shorter than this

typedef long long int *CLAUSE;

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

long long int my_rand(long long int limit) //should return 0..limit-1 
{
  return ((long long int)random())%limit;
}

void err(int status, char*message) //prints the message on stderr and 
                                   //terminates with the given status
{
  fprintf(stderr,"\nerror %d: %s",status, message);
  exit(status);
}

int sign(long long int lit) //just sign (-1,0,1)
{
  if (lit>0) return 1; else if (lit<0) return -1; else return 0;
}

#define LT(x, y) ((x.key) < (y.key))
#define SWAP(x, y) temp = (x); (x) = (y); (y) = temp

typedef struct KEY_T {
  long long int val;
  long long int key;
} KEY_T;

void  quicksort (KEY_T array[], long long int lower, long long int upper)
{
        long long int    i, m;
        KEY_T  temp, pivot;

        if (lower < upper) {
                SWAP(array[lower], array[(upper+lower)/2]);
                pivot = array[lower];
                m = lower;
                for (i = lower + 1; i <= upper; i++)
                        if (LT(array[i], pivot)) {
                                m++;
                                SWAP(array[m], array[i]);
                        }
                SWAP(array[lower], array[m]);
                quicksort (array, lower, m - 1);
                quicksort (array, m + 1, upper);
        }
}


long long int *randomperm(long long int nobj) //allocates and generates a
                                              //random permutation in S_{nobj}
{
  long long int *perm=(long long int*)malloc((nobj+1)*sizeof(long long int));
  KEY_T * sorted;

  sorted=(KEY_T*)malloc((nobj+1)*sizeof(KEY_T));
  if (!perm) err(-1, "\nNot enough memory.\n\n");
  if (!sorted) err(-1, "\nNot enough memory.\n\n");
  for (long long int i=1; i<=nobj; i++) {
    sorted[i].val = (long long int)i;
    sorted[i].key = (long long int)random();
  }

  quicksort(sorted,1,nobj);
  for (long long int i=1; i<=nobj; i++) {
    //   printf("(%lld,%lld) ",sorted[i].val, sorted[i].key);
    perm[i] = sorted[i].val;
  }

  free(sorted);
  return perm;
}

int *randomsign(long long int nobj) //allocates and generates an
                                    //array of random signs
{
  int *arr=(int*)malloc((nobj+1)*sizeof(int));
  if (!arr) err(-1, "\nNot enough memory.\n\n");
//DEBUG  for (long long int i=1; i<=nobj; i++) arr[i]=-1; //just reverse
  for (long long int i=1; i<=nobj; i++) arr[i]=((my_rand(2)==1)?1:-1);
  return arr;
}

int main(int argc, char** argv)
{   
  FILE *fi, *fo; //input and output streams
  char buffer[MAXLEN]; //input file buffer
  char *cbuffer; //current position in the current string
  long long int clause[MAXLEN]; //current clause buffer
  int pgiven=0; //did we read the "p" line
  long long int nvar, ncla; //...given in the "p" line
  long long int lit; //current literal
  long long int nlit; //current length of current clause
  long long int cla=0; //current clause number (1..ncla)
  CLAUSE *clauses; //our formula
  long long int *permvar; //permutation of variables
  long long int *permcla; //permutation of clauses
  int *permval; //do we flip each variable (-1=yes, 1=no)
  long int seed;
  
  if (argc<3) err(1,"\nUsage: reorder file.cnf seed\n\n");
  srandom(seed=atol(argv[2]));

  //read the formula...
  fi=fopen(argv[1],"rt");
  if (!fi) err(2,"\nCannot open input file.\n\n");
  
  while (!feof(fi))
  {
    fgets(buffer,MAXLEN,fi);
    if (buffer[strlen(buffer)-1]!='\n') if (!feof(fi)) 
    {
      fprintf(stderr,"%s\n",buffer);
      err(4,"\nLine too long.\n\n");
    }
    switch (buffer[0])
    {
      case 'c': if (pgiven) {
         fprintf(stderr,"Error for line '%s'\n",buffer);
	 err(5,"\nComment after the \"p\" line.\n\n");
         }
		break; //drop comments
      case 'p': if (pgiven) err(6,"\nTwo \"p\" lines.\n\n");
		pgiven=1;
		if (2!=sscanf(buffer,"p cnf %lld %lld\n",&nvar,&ncla))
		  err(7,"\nFailed to process the \"p\" line.\n\n");

		permvar=randomperm(nvar);
		permval=randomsign(nvar);
		permcla=randomperm(ncla);

		clauses=(CLAUSE*)malloc(ncla*sizeof(CLAUSE));
		if (!(clauses)) err(-1, "\nNot enough memory.\n\n");
		clauses--; //we are going to number them from 1
		break;
      default:  if (!pgiven) //we don't know the number of vars yet! 
		  err(8, "\nEither \"c\" or \"p\" line was expected.\n\n");
//DEBUG		fprintf(stderr,"[%s]",buffer);
		if (++cla>ncla) //check that the rest of file is empty
		{
		  while (!feof(fi))
		  {
		    char c;
		    if (sscanf(buffer,"%c",&c)>=1) //found a character here!
		      err(9, "\nToo many clauses or garbage before EOF.\n\n");
		    if (!fgets(buffer,MAXLEN,fi)) break;
		  }
		  break;
		}
		cbuffer=buffer;
		while (1)
		{
//DEBUG		  fprintf(stderr,"<%s>",cbuffer);
		  cbuffer=strpbrk(cbuffer,"-0123456789"); // Remove blanks
		  if (!cbuffer)
		    {
		      fprintf(stderr,"%s",buffer);
		      err(110, "\n0-terminated clause line was expected.\n\n");
		    }
		  if (sscanf(cbuffer,"%lld",&lit)!=1) 
		  {
		    fprintf(stderr,"%s",buffer);
		    err(10, "\n0-terminated clause line was expected.\n\n");
		  }
		  if (!lit) //end of clause
		  {
		    clause[nlit++]=0;
		    clauses[cla]=(CLAUSE)malloc(nlit*sizeof(long long int));
		    if (!(clauses[cla])) err(-1, "\nNot enough memory.\n\n");
		    memcpy(clauses[cla],clause,nlit*sizeof(long long int));
		    nlit=0;
		    break;
		  }
		  else 
		  {
		    clause[nlit++]=lit;
		    cbuffer=strpbrk(cbuffer," \t"); //strchr(cbuffer,' ');
		    if (!cbuffer)
		    {
		      fprintf(stderr,"%s",buffer);
		      err(110, "\n0-terminated clause line was expected.\n\n");
		    }
		    else { // forget now all blanks...
		      cbuffer=strpbrk(cbuffer,"-0123456789");
		      if (!cbuffer)
			{
			  fprintf(stderr,"%s",buffer);
			  err(110, "\n0-terminated clause line was expected.\n\n");
			}

		    }
		  }
		} 
    }
  }
  fclose(fi);
  if (cla<ncla) err(12, "\nToo few clauses.\n\n");

  //now print the new formula...
  fo=stdout;
  if (!fo) err(3,"\nCannot open output file.\n\n");

  fprintf(fo,"c A permuted SAT Competition 2002 formula with seed=%ld\n",seed);
  fprintf(fo,"p cnf %lld %lld\n",nvar,ncla); 
  
  for (cla=1; cla<=ncla; cla++)
  {
    long long int *perminc;
    long long int clen, clit;
    CLAUSE cc=clauses[permcla[cla]];
    for (clen=0; cc[clen]!=0; clen++) { ; } //nlit=clause length now
    perminc=randomperm(clen);
    for (clit=1; clit<=clen; clit++)
    {
      nlit=perminc[clit]-1;
      fprintf(fo,"%lld ",
	(long long int)(permval[abs(cc[nlit])]*
			sign(cc[nlit])*
			permvar[abs(cc[nlit])]));
    }
    free(perminc);
    fprintf(fo,"0\n");
  }
 
  fclose(fo); 
  exit(0);
}