// modified by pwn 2001 to take multiple noise parameters as arguments

/************************************************************************/
/**/
/*conv/NB-B  ...Tim Peugniez 11/97*/
/**/
/*  This program takes a file in Non-Boolean WalkSAT format*/
/*     and converts it to standard Boolean WalkSAT format*/
/**/
/*        Input is from stdin and output is to stdout*/
/**/
/************************************************************************/

/************************************************************************/
/**/
/*   NB-PROBLEM INPUT FORMAT: (from stdin)*/
/**/
/*c*/
/*c Comment lines at start of file begin with 'c'*/
/*c*/
/**/
/*nb cnf <numvar> <num_clauses> <domain_size>*/
/**/
/*var_1{V1,V2,...,Vi}  var_2{V1,V2,...,Vj}  ...  var_n{...}  0*/
/**/
/*Each clause is composed of a number of literals and terminated*/
/*by the digit 0.  The literals take the form of the variable*/
/*number, followed by a list of comma separated values*/
/*in parentheses.*/
/**/
/************************************************************************/


/************************************************************************/
/**/
/*   B-PROBLEM OUTPUT FORMAT: (to stdout)*/
/**/
/*c*/
/*c Comment lines at start of file begin with 'c'*/
/*c*/
/**/
/*p cnf <numatom> <num_clauses>*/
/**/
/*lit1 lit2 ... litN 0*/
/**/
/*Each clause is composed of a number of literals and terminated*/
/*by the digit 0.  The literals take the form of atom numbers*/
/*or negated atom numbers, representing atoms and negatedatoms*/
/*respectively.*/
/**/
/************************************************************************/

/*  NOTES : (These should be in a README file, not here!)

Using the UNARY encoding:
=========================

An NB-file with domainsize D, numvar V will translate to a B-file with V*D atoms, each atom
representing 'var[k]==v' for some k and v.  Atoms are shown as atom[k.v] below...

Each NB-clause of the form:

var[k]:={V1,V2,..,Vn}  V  var[l]:!={W1,W2,..,Wm}  V ...

Translates into:

atom[k.V1] V atom[k.V2] V .. V atom[k.Vn]    V    atom[l.W1] V atom[l.W2] V .. V atom [l.Wm]     V ...

... atmostone / atleastone clauses


Using the BINARY encoding:
==========================

An NB-file with domainsize D, numvar V will translate to a B-file with V * Log2 D atoms,
the k'th group of Log2 D atoms representing the bitwise encoding of v, such that var[k]==v

For each NB-clause of the form:

var[k]:={V1,V2, .. Vn}  V  A

Translates into:

atom[k(V1).0]V   A
atom[k(V1).1]V   A
...
atom[k(V1).N-1]V   A


atom[k(V2).0]V   A
atom[k(V2).1]V   A
...
atom[k(V2).N-1]V   A

.
.
.

atom[k(Vn).0]V   A
atom[k(Vn).1]V   A
...
atom[k(Vn).N-1]V   A

Where N is the number of bits required.
Although, in our current experiments, value sets are unlikely to contain more than a single value.

... atleastone clauses for domainsize < 2^pwr


Using the UNARY-BINARY encoding:
================================

Clauses are translated as in the unary encoding

... different atleastone / atmostone clauses

*/

#include <stdio.h>
#include <stdlib.h>
#include <math.h>
#include <sys/time.h>
#include <signal.h>
#include <unistd.h>

#define FALSE0
#define TRUE1

#define UNARY1
#define BINARY2
#define UNARYBINARY3

#define BIN_A1
#define BIN_B2

#define MEMBERS0
#define NONMEMBERS1

#define cube(x)((x)*(x)*(x))
#define extraslot(val) (!oldbin && (val)<(power-domainsize)?1:0)
#define binbase(val) ( oldbin ? (val) : ((val)<=(power-domainsize)?(val)*2:(power-domainsize)+(val)) )

int domainsize;
int log_domainsize;/* = log_2 domainsize */
int power;/* Next power of two after domain size */

int **mapval;/* array of permutations of variable values, for bin and unbin encodings ..
   indexed mapval[var][val]
*/

struct nblit
  {
int var;
int val;
  };
typedef struct nblit nblit_type;

struct clause
  {
int numlit;
int *clause;
struct clause *next;
  };
typedef struct clause clause_type;
typedef clause_type *clause_list;

int space = FALSE;
int verbose = FALSE;
int warnings = TRUE;
int superverbose = FALSE;
int negate = FALSE;
int oldbin = FALSE;
int regular = TRUE;

int encoding = NULL;
int atleastone = FALSE;
int atmostone = FALSE;

int cldone = 0;

/* added by PWN */

int tabu = FALSE;/* tabu==true indicates tabu type noise parameters. tabu==false indicates probability type noise parameters */

int palonum = -1;
int pamonum = -1;
int pkernelnum = -1;

int paloden = -1;
int pamoden = -1;
int pkernelden = -1;

int talo=-1;
int tamo=-1;
int tkernel=-1;

/* end */

char str[256];
char tempfile[256]=".tmp_NB-B";
FILE *fp;

void next_nblit(clause_list *Bclauses, nblit_type nblit, int **bit);
void writeoutBclauses(clause_list Bclauses);
clause_type *newclause(int numlit);
void dealloctrans(clause_type **cl);
int newseed(void);

void scanone(int argc, char *argv[], int i, int *varptr)
  {
        if (i>=argc || sscanf(argv[i],"%i",varptr)!=1)
  {
        fprintf(stderr, "Bad argument '%s'\n", i<argc ? argv[i] : argv[argc-1]);
exit(-1);
  }
  } 
  
void handle_sig(int sig)
  {
remove(tempfile);
exit(-1);
  }

void main(int argc,char *argv[])
  {

/* These variables relate to the input Non-Boolean file ... */

int numvar= 0;/* number of vars */
int numNBclause= 0;/* number of clauses */

nblit_type nblit;/* current nb val:var pair */

/* These variables relate to the output Boolean file ... */

int numatom= 0;/* number of atoms */
int numBclause= 0;/* number of clauses */
clause_list Bclauses;/* list of bitwise clauses representing current nb-clause */
clause_type *cl;

/* These variables are just here 'cos they felt like it ... */

int i;/* loop counter */
int j;/* another loop counter */
int k;/* guess what? */

char lastc;
char nextc;

int size;/* size of current NBclause */

int allneg=1;

int lit;/* current variable of lit */
int val;/* current value */
int varbase;/* first atom in group which represents var */
int bitbase;/* first atom in group which represents bitwise encoding of var (using -bitenforce)*/

int mv;/* scratch for mapval */

int **bit;/* array of binary values (using {-1,+1} rather than {0,1}) such that

bit[5][0] =  1 
bit[5][1] = -1 
bit[5][2] =  1 
*/

int typelit;/* Whether each lit is := or :!= */
char *value;/* 'boolean' array of domain values */
int seed;/* random seed */

srandom(newseed());

/* Flags for User Specified Options ... */

        for (i=1; i<argc; i++)
  {
if (strcmp(argv[i],"-v") ==0 )
  verbose = TRUE;
else if (strcmp(argv[i],"-bl") ==0 )
  space = TRUE;
else if (strcmp(argv[i],"-s") ==0 )
  warnings = FALSE;
else if (strcmp(argv[i],"-seed") ==0 )
  if (!(++i<argc && sscanf(argv[i],"%d",&seed)==1))
{
fprintf(stderr,"Bad argument to '-seed' option\n");
exit(-1);
}
  else srandom(seed);
else if (strcmp(argv[i],"-oldbin") ==0 )
  oldbin = TRUE;
else if (strcmp(argv[i],"-negate") ==0 )
  negate = TRUE;
else if (strcmp(argv[i],"-atleastone") ==0 )
  atleastone = TRUE;
else if (strcmp(argv[i],"-atmostone") ==0 )
  atmostone = TRUE;
else if (strcmp(argv[i],"-randomised")==0 || strcmp(argv[i],"-randomized")==0)
  regular = FALSE;
else if (strcmp(argv[i],"-unary") ==0 )
  {
if (encoding==BINARY)
  {
                        fprintf(stderr,"\nError: Binary and unary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }
if (encoding==UNARYBINARY)
  {
                        fprintf(stderr,"\nError: Unary and unary-binary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }

encoding = UNARY;
  }
else if (strcmp(argv[i],"-binary") ==0 )
  {
if (encoding==UNARYBINARY)
  {
                        fprintf(stderr,"\nError: Binary and unary-binary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }
if (encoding==UNARY)
  {
                        fprintf(stderr,"\nError: Unary and binary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }

encoding = BINARY;
  }
else if (strcmp(argv[i],"-unarybinary") ==0 )
  {
if (encoding==BINARY)
  {
                        fprintf(stderr,"\nError: Binary and unary-binary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }
if (encoding==UNARY)
  {
                        fprintf(stderr,"\nError: Unary and unary-binary encodings are mutually exclusive");
                        fprintf(stderr,"\n       Please specify only one of these options\n");
exit(-1);
  }

encoding = UNARYBINARY;
  }
/*added by PWN */
else if (strcmp(argv[i],"-tabu") ==0 )
  {
  tabu=TRUE;
  }
else if (strcmp(argv[i],"-talo") ==0 )
  {
  scanone(argc,argv,++i,&talo);
  }
else if (strcmp(argv[i],"-tamo") ==0 )
  {
  scanone(argc,argv,++i,&tamo);
  }
else if (strcmp(argv[i],"-tkernel") ==0 )
  {
  scanone(argc,argv,++i,&tkernel);
  }
else if (strcmp(argv[i],"-palonum") ==0 )
  {
  scanone(argc,argv,++i,&palonum);
  }
else if (strcmp(argv[i],"-pamonum") ==0 )
  {
  scanone(argc,argv,++i,&pamonum);
  }
else if (strcmp(argv[i],"-pkernelnum") ==0 )
  {
  scanone(argc,argv,++i,&pkernelnum);
  }  
else if (strcmp(argv[i],"-paloden") ==0 )
  {
  scanone(argc,argv,++i,&paloden);
  }
else if (strcmp(argv[i],"-pamoden") ==0 )
  {
  scanone(argc,argv,++i,&pamoden);
  }
else if (strcmp(argv[i],"-pkernelden") ==0 )
  {
  scanone(argc,argv,++i,&pkernelden);
  }
/* end */
else
  {
                        fprintf(stderr,"\nBad argument '%s'\n\n",argv[i]);

                        fprintf(stderr,"Valid arguments to NB-B are :\n\n");

                        fprintf(stderr,"  -vVerbose option: display information about input\n");
                        fprintf(stderr,"                and output files\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -sSuppress warnings\n");
fprintf(stderr,"\n");
                        fprintf(stderr,"  -blAdd blank lines to formulas to improve legibility\n");
fprintf(stderr,"(blank lines cause some solvers to complain)\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -seed Nuse random seed N\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -atleastoneInclude 'at-least-one' clauses\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -atmostoneInclude 'at-most-one' clauses\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -unaryUse a 'unary' encoding (for problems with domain size two)\n");
fprintf(stderr,"By default, problems with domain size two are translated using a binary encoding\n");
fprintf(stderr,"This option forces a unary encoding to be used\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -binaryUse a 'binary' (bitwise) encoding\n");
fprintf(stderr,"Currently this doesn't work well for large clauses\n");
fprintf(stderr,"(The default encoding is unary for problems with domain size greater than two)\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -unarybinaryUse a 'unary-binary' encoding (unary clause translation with\n");
fprintf(stderr,"binary enforcement of singular assignments)\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -oldbinFor binary or unary-binary encodings:  If domain size is not a power of two\n");
fprintf(stderr,"add extra clauses to rule out redundant values (default is to expand mapping to fit)\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -randomisedFor binary and unary-binary encodings using multiple slots (ie. not oldbin) :\n");
fprintf(stderr,"Map the slots differently for each variable (default is to map all variables\n");
fprintf(stderr,"in an identical manner)\n");
fprintf(stderr,"\n");
fprintf(stderr,"  -negateConvert literals to negative form when A:=({D}-x) \n");
fprintf(stderr,"for literal A, domainsize {D} and some value x:={D} \n");
fprintf(stderr,"Default is always to translate to positive formulas\n");
fprintf(stderr,"\n");
exit(-1);
  }
   }

if (encoding==UNARYBINARY && !atleastone && !atmostone)
  {
if (warnings)
  {
fprintf(stderr,"Note: Unary-binary encoding without at-least-one or at-most-one constraints\n");
fprintf(stderr,"      is identical to unary encoding without these constraints\n");
  }

encoding = UNARY;
  }

if (encoding!=BINARY && encoding!=UNARYBINARY && oldbin)
  {
if (warnings)
  {
fprintf(stderr,"Note: The '-oldbin' option is only applicable to binary and unarybinary encodings\n");
fprintf(stderr,"      - I am ignoring it\n");
  }

oldbin=FALSE;
  }

if (oldbin && !regular)
  {
if (warnings)
  {
fprintf(stderr,"Note: The '-randomised' option is not applicable when '-oldbin' is selected\n");
fprintf(stderr,"      - I am ignoring it\n");
  }
regular=TRUE;
  }
/* added by PWN */
if (tabu && (talo<0 || tamo<0 || tkernel<0))
  {
  fprintf(stderr,"Note: The tabu option was selected, but not all of {talo, tamo, tkernel}\n");
fprintf(stderr,"      (the noise parameters) were specified. Exiting.\n");
exit(-1);
  }
if (!tabu && (palonum<0 || pamonum<0 || pkernelnum<0 || paloden<0 || pamoden<0 || pkernelden<0))
  {
  fprintf(stderr,"Note: Not all of {palo, pamo, pkernel}x{num, den} (the noise parameters) were\n");
fprintf(stderr,"      specified. Exiting.\n");
exit(-1);
  }
/* end */
/* open unique tempfile ... */

i=0;j=0;
while(1)
  {
sprintf(str,"%s_%d",tempfile,++i);
while ((fp=fopen(str,"r"))!=NULL)
  {
fclose(fp);
sprintf(str,"%s_%d",tempfile,++i);
  }
if ((fp=fopen(str,"w"))!=NULL)
  {
strcpy(tempfile,str);
break;
  }
else if (++j == 10)
  {
fprintf(stderr,"Can't write temp file '%s' (made %d attempts)\n",str,j);
exit(-1);
  }
  }

signal(SIGINT,handle_sig);
signal(SIGTERM,handle_sig);

/* Write comments through to tempfile ... */

if (verbose) fprintf(stderr,"Writing comments through ...\n");

while ((lastc = getchar()) == 'c')
  {
fprintf(fp,"c > ");
while ((nextc = getchar()) != EOF && nextc != '\n')
  {
fprintf(fp,"%c",nextc);
if (verbose) fprintf(stderr,"%c",nextc);
  }
fprintf(fp,"\n");
if (verbose) fprintf(stderr,"\n");
  }
ungetc(lastc,stdin);



/* Read header ... */

if (verbose) fprintf(stderr,"\nReading header ...\n");

   if (scanf("nb cnf %i %i %i",&numvar,&numNBclause,&domainsize) != 3)
  {
fprintf(stderr,"Bad input file\n");
exit(-1);
  }

if (encoding==NULL)
  {
if (domainsize==2) encoding=BINARY;
else encoding=UNARY;
  }

if (encoding!=UNARY)
  {
log_domainsize=1;
power=2;
while(power<domainsize)
  {
log_domainsize++;
power*=2;/* power = 2^(log_domainsize) */
  }


if ( (bit = (int **) malloc( sizeof(int*) * power )) == 0 )
  {
fprintf(stderr,"Error: Out of memory!\n");
exit(-1);
  }

for (i = 0; i < power; i++)
  {
if ( (bit[i] = (int *) malloc( sizeof(int) * log_domainsize )) == 0 )
  {
fprintf(stderr,"Error: Out of memory!\n");
exit(-1);
  }
for (j = 0; j < log_domainsize; j++)
    bit[i][j] = ((i>>j)&1)*2 - 1;
  }

if ( (mapval = (int **) malloc( sizeof(int*) * numvar )) == 0 )
  {
fprintf(stderr,"Error: Out of memory!\n");
exit(-1);
  }

for(i=1; i<=numvar; i++)
  {
 if ( (mapval[i] = (int *) malloc( sizeof(int) * domainsize )) == 0 )
  {
fprintf(stderr,"Error: Out of memory!\n");
exit(-1);
  }

for(j=0; j<domainsize; j++) mapval[i][j]=j;

if (!regular)
  for(j=0; j<domainsize; j++)
    {
k=j+random()%(domainsize-j);
val=mapval[i][k];
mapval[i][k]=mapval[i][j];
mapval[i][j]=val;
    }

if (superverbose)
  {
fprintf(stderr,"var[%d] : ",i);
for(j=0; j<domainsize; j++)
  {
fprintf(stderr,"%d(%d",mapval[i][j],binbase(mapval[i][j]));
if (extraslot(mapval[i][j])) fprintf(stderr,",%d",binbase(mapval[i][j])+1);
fprintf(stderr,")  ");
  }
fprintf(stderr,"\n");
  }
  }

if (encoding==BINARY && !oldbin && atleastone)
  {
if (warnings)
  {
fprintf(stderr,"\nNote: A binary encoding enforces 'at-least-one' constraints automatically");
fprintf(stderr,"\n      unless the '-oldbin' option is used, so '-atleastone' option is redundant");
fprintf(stderr,"\n      - I am ignoring it\n");
  }

atleastone = FALSE;
  }

if (encoding==BINARY && atleastone && power==domainsize)
  {
if (warnings)
  {
fprintf(stderr,"\nNote: A binary encoding enforces 'at-least-one' constraints automatically");
fprintf(stderr,"\n      when the domain size is a power of two, so '-atleastone' option is redundant");
fprintf(stderr,"\n      - I am ignoring it\n");
  }

atleastone = FALSE;
  }
  }

value = (char *) malloc(domainsize*sizeof(char));
if (value==0)
  {
fprintf(stderr,"Error: Out of memory!\n");
exit(-1);
  }

if (encoding==BINARY && atmostone)
  {
if (warnings)
  {
fprintf(stderr,"\nNote: A binary encoding enforces 'at-most-one' constraints automatically");
fprintf(stderr,"\n      so the '-atmostone' option is redundant - I am ignoring it\n");
  }
atmostone = FALSE;
  }


if (verbose) fprintf(stderr,"Writing bCNF ouput file ...\n\n");

/* Write comments ... */

printf("c\n");
printf("c =========================================================================\n");
printf("c This WalkSAT CNF file is converted from a Non-Boolean WalkSAT file\n");
printf("c The original file had %i variables with domain size %i, and %i clauses\n",
 numvar,domainsize,numNBclause);

switch(encoding)
  {
case UNARY:printf("c A unary encoding is used, with %d atoms per variable\n",domainsize);
break;

case BINARY:printf("c A binary encoding (%s) is used,\n",
(oldbin && power>domainsize)?"with non-surjective mapping":
(regular?"with regular mapping":"with randomised mapping") );
printf("c %d bit%s are used to represent each variable\n",
log_domainsize, log_domainsize==1?"":"s");
break;

case UNARYBINARY:printf("c A unary-binary encoding (%s) is used,\n",
(oldbin && power>domainsize)?"with non-surjective mapping":
(regular?"with regular mapping":"with randomised mapping") );
printf("c %d 'bit atom%s' and %d 'unary atoms' are used to represent each variable\n",
log_domainsize,log_domainsize==1?"":"s",domainsize);
  }

if (encoding!=BINARY)
  {
if (atleastone && atmostone)
  {
printf("c Exactly one value per (non-boolean) variable is enforced\n");
printf("c using 'at-least-one' and 'at-most-one' clauses\n");
  }
else if (atleastone)printf("c At least one value per (non-boolean) variable is enforced\n");
else if (atmostone)printf("c At most one value per (non-boolean) variable is enforced\n");
  }

if (encoding!=UNARY && power>domainsize && atleastone && oldbin)
  {
  printf("c Extra 'at-least-one' clauses are included to limit the domain to {0..%d}\n",domainsize-1);
  }


printf("c =========================================================================\nc\n");



/* Calc header ... */

switch (encoding)
  {
case UNARY:numatom = numvar * domainsize;
numBclause = numNBclause;
if (atleastone)numBclause += numvar;
if (atmostone)numBclause += numvar * (domainsize*(domainsize-1)/2);
break;


case BINARY:numatom = numvar * log_domainsize;
/* don't even bother to calc numNBclause .. just see how many we write! */
break;


case UNARYBINARY:numatom = numvar * (domainsize + log_domainsize);
numBclause = numNBclause;
if (atleastone)
if (oldbin) numBclause += numvar*power;
else numBclause += numvar*domainsize;
if (atmostone)
if (oldbin) numBclause += numvar*domainsize*log_domainsize;
else numBclause += numvar*(domainsize*(log_domainsize+1) - power);
break;
  }

if (space) printf("\n");

/* Write clauses which enforce singular assignments ... */

if (atleastone || atmostone) {

  if (verbose) fprintf(stderr,"Writing clauses to enforce singular assignments ...\n");

  switch(encoding)
    {
case UNARY:

/* Write clauses which specify that each 'variable' must have at MOST and/or at LEAST one value ... */

for (i = 1; i <= numvar; i++)
  {
varbase=(i-1)*domainsize+1;

if (atleastone)
  {
for (j =0; j < domainsize; j++)
  fprintf(fp,"%i ",varbase+j);

/* Modified by PWN */
fprintf(fp,"0 ");
switch(tabu)
  {
  case TRUE:
fprintf(fp,"%d ",talo);
break;
case FALSE:
fprintf(fp,"%d %d ",palonum,paloden);
break;
  }
fprintf(fp,"0\n");
cldone++;
/* end */
  }

if (atmostone)
  {
for (j=0; j<domainsize-1; j++)
  for (k=j+1; k<domainsize; k++)
  {
/* modified by PWN */
fprintf(fp,"-%i -%i 0 ",varbase+j,varbase+k); 
switch(tabu)
    {
  case TRUE:
fprintf(fp,"%d ",tamo);
break;
case FALSE:
fprintf(fp,"%d %d ",pamonum,pamoden);
break;
    }
fprintf(fp,"0\n");
cldone++;
/* end */
  }
if (space) fprintf(fp,"\n");
  }

if (verbose && i%10==0) fprintf(stderr,"\r %3d%% done ",i*100/numvar);
    }
if (!atmostone && space) fprintf(fp,"\n");

if (verbose) fprintf(stderr,"\r 100%% done \n");

break;


case BINARY:

if (oldbin && atleastone)
  {
/* Add clauses to limit the full domain to the required domainsize ... */

for (i = 1; i <= numvar; i++)
  {
bitbase = (log_domainsize*(i-1)+1);

for (j = domainsize; j < power; j++)
  {
for (k = 0; k < log_domainsize; k++)
  fprintf(fp,"%d ",-bit[j][k]*(bitbase+k));
fprintf(fp,"0\n");
cldone++;
  }
if (space && power>domainsize+1 && i<numvar) fprintf(fp,"\n");
  }
if (space) fprintf(fp,"\n");
  }
break;


case UNARYBINARY:

/* Write bitwise mapping clauses ( X_0 <=> ... ~x_2 ^ ~x_1 ^ ~x_0 etc.) ... */

for (i = 1; i <= numvar; i++)
  {
varbase=(i-1)*domainsize+1;
bitbase=numvar*domainsize+1 + (i-1)*log_domainsize;

for (j = 0; j < domainsize; j++)
  {
mv=mapval[i][j];

if (atleastone)
  {
/* Write one clause, stating " X_j <= ... (~)x_2 ^ (~)x_1 ^ (~)x_0 " ... */

for (k = extraslot(mv); k < log_domainsize; k++)
  fprintf(fp,"%d ",-bit[binbase(mv)][k]*(bitbase+k));
fprintf(fp,"%d 0\n",varbase+j);
cldone++;
  }

if (atmostone)
  {
/* Write log_2(domainsize) clauses, stating " X_j => ... (~)x_2 ^ (~)x_1 ^ (~)x_0 " ... */ 

for (k = extraslot(mv); k < log_domainsize; k++)
  {fprintf(fp,"%d %d 0\n",-(varbase+j),bit[binbase(mv)][k]*(bitbase+k)); cldone++;}
  }
  }

if (oldbin && atleastone && power>domainsize)
  {
/* Add clauses to limit the full domain to the required domainsize */

for (j = domainsize; j < power; j++)
  {
for (k = 0; k < log_domainsize; k++)
  fprintf(fp,"%d ",-bit[j][k]*(bitbase+k));
fprintf(fp,"0\n");
cldone++;
  }
  }

if (space) fprintf(fp,"\n");

if (verbose && i%10==0) fprintf(stderr,"\r %3d%% done ",i*100/numvar);
  } 
if (verbose) fprintf(stderr,"\r 100%% done \n");

    }
  }


if (verbose) fprintf(stderr,"\nConverting Non-Boolean clauses into Boolean clauses ...\n");

/* Convert stated clauses into boolean form ... */

for (i = 0; i < numNBclause; i++)
  {
size=0;

if (superverbose) fprintf(stderr,"clause %i :\n",i+1);

if (encoding == BINARY) Bclauses = NULL;/* Empty list of Bclauses representing this clause so far */

do
  {

if (scanf("%i",&lit) != 1)
  {
      fprintf(stderr, "\nBad input file, at clause %i\n",i+1);
      exit(-1);
  }

if (lit!=0)
  {

if(lit > numvar || lit < 0)
  {
fprintf(stderr, "\nBad input file (no such variable),\n (var['%i']) in clause %i\n",lit,i+1);
exit(-1);
  }

if (scanf("%c",&nextc)==1 && nextc=='{')
  typelit=MEMBERS;
else if (nextc=='!' && scanf("%c",&nextc)==1 && nextc=='{')
  typelit=NONMEMBERS;
else
  {
fprintf(stderr, "\nBad input file, at clause %i",i+1);
fprintf(stderr, " (can't determine type of lit %i)\n",size+1);
exit(-1);
  }

size++;

if (superverbose)
  {
if (typelit==MEMBERS)
  fprintf(stderr,"   var[%i]:={",lit);
else
  fprintf(stderr,"   var[%i]:!={",lit);
  }

for (val = 0; val < domainsize; value[val++] = FALSE );

j=0;

do /* THIS LOOP READS LIST OF VALUES IN BRACKETS... */
  {
if (scanf("%i",&val) == 1)
  {
if (val<0 || val>=domainsize)
  {
fprintf(stderr,"\nBad input file (value '%i' outside domain),\n at clause %i, lit%i\n",val,i+1,size);
exit(-1);
  }
else
  {
if (superverbose) { 
  if (j > 0) {fprintf(stderr,",");}
  fprintf(stderr,"%i",val);
}
value[val]=TRUE;
j++;
  }


  }
else
  {
fprintf(stderr,"\nBad input file (bad value list),\n at clause %i, lit%i\n",i+1,size);
exit(-1);
   }
  }
while (scanf("%c",&nextc)==1 && nextc==',');

if (nextc!='}')
  {
fprintf(stderr,"\nBad input file (bad value list),\n at clause %i, lit%i\n",i+1,size);
exit(-1);
  }

if (superverbose) fprintf(stderr,"}\n");

if (typelit==NONMEMBERS)
  {
j=domainsize-j;

for(val=0; val<domainsize; val++)
value[val]=1-value[val];/* Flip all values */
  }

if (encoding == BINARY)
  {
if (negate && j == (domainsize-1) && (Bclauses==NULL || Bclauses->next==NULL))
  {

/* For problems of graph-col form ... Add bitwise literals to single clause */

val=0;
while (value[val]) val++;
mv=mapval[lit][val];

if (Bclauses==NULL)
  {
Bclauses = newclause(log_domainsize - extraslot(mv));
  }
else
  {
cl = newclause(log_domainsize - extraslot(mv) + Bclauses->numlit);
for(k=0; k<(Bclauses->numlit); k++)
cl->clause[k+log_domainsize-extraslot(mv)] = Bclauses->clause[k];
free(Bclauses);
Bclauses = cl;
  }
for(k=extraslot(mv); k<log_domainsize; k++) 
  Bclauses->clause[k-extraslot(mv)] =
-bit[binbase(mv)][k] * (log_domainsize*(lit-1)+k+1);
Bclauses->next = NULL;
  }
else
  {

/* Write a bitwise clause for each lit:val where value[val]=TRUE */

allneg=0;

for (val=0; val<domainsize; val++)
  {
if (value[val])
  {
/* Include this lit:val pair in the set of Bclauses representing the current NBclause .. */

nblit.var = lit;
nblit.val = val;
next_nblit(&Bclauses, nblit, bit);  
  }
  }
  }
  }
else
  {
if (negate && j == (domainsize-1))
  {
for (val = 0; val < domainsize; val++)
  {
if (!value[val])
  {
fprintf(fp,"-%i ",((lit-1)*domainsize + val)+1);
break;
  }
  }
  }
else
  {
for (val = 0; val<domainsize; val++)
  {
if (value[val])
  fprintf(fp,"%i ",((lit-1)*domainsize + val)+1);
  }
  }
  }

  }

  }
while (lit!=0);

if (superverbose) fprintf(stderr,"\n");

if (encoding == BINARY)
  {
writeoutBclauses(Bclauses);
if (space && !allneg) fprintf(fp,"\n");
  }
else
  {
  /* Added by PWN */
switch(tabu)
  {
case TRUE:
fprintf(fp,"0 %d ",tkernel);
break;
case FALSE:
fprintf(fp,"0 %d %d ",pkernelnum,pkernelden);
break;
  }

/* end */
fprintf(fp,"0\n");
cldone++;
  }

if(size==0)
  {
fprintf(stderr,"Bad input file: incorrect problem format or extraneous characters\n");
exit(-1);
  }

if (verbose && i%50==0) fprintf(stderr,"\r %3d%% done ",i*100/numNBclause);

  }
if (verbose) fprintf(stderr,"\r 100%% done \n\n");

if (cldone != numBclause)
  {
    if (encoding == BINARY)
     {
numBclause = cldone;
     }
    else
     {
fprintf(stderr,"Error: Expected to write %d clause%s;  Actually written %d\n", numBclause, (numBclause==1)?"":"s", cldone);
exit(-1);
     }
  }

fclose(fp);
if ((fp=fopen(tempfile,"r"))==NULL)
  {
fprintf(stderr,"Error: Can't read temp file '%s'\n",tempfile);
exit(-1);
  }


/* Write file to output ... */

while (fscanf(fp,"%c",&lastc)==1 && lastc=='c')
  {
printf("c > ");
while (fscanf(fp,"%c",&nextc)==1 && nextc!='\n')
  {
printf("%c",nextc);
  }
printf("\n");
  }
ungetc(lastc,fp);

if (space) printf("\n");
printf("p cnf %i %i\n",numatom,numBclause);
if (space) printf("\n");

while (fscanf(fp,"%c",&nextc)==1) printf("%c",nextc);

fclose(fp);
remove(tempfile);
}

void next_nblit(clause_list *ptrBclauses, nblit_type nblit, int **bit)
  {
int i,j;
clause_list newclauses, clauses;
clause_type *newcl, *cl;
int mv;/* scratch for mapval */

clauses = *ptrBclauses;

mv = mapval[nblit.var][nblit.val];

if (superverbose)
  {
fprintf(stderr,"\nAdd nblit var[%d]=%d to clauses ...\n",nblit.var,nblit.val);
for(cl=clauses; cl!=NULL; cl=cl->next)
  {
fprintf(stderr,"\t ");
for(i=0; i<(cl->numlit); i++) fprintf(stderr,"%d ",cl->clause[i]);
fprintf(stderr,"\n");
  }
if (clauses==NULL) fprintf(stderr,"\t none\n");
fprintf(stderr,"\n");
  }

if (clauses == NULL)/* clause list is empty ? */
  {
/* Create new clause list, containing the literals derived from nblit */

newclauses = newclause(1);
cl = newclauses;
cl->clause[0] = bit[binbase(mv)][extraslot(mv)] * (log_domainsize*(nblit.var-1)+extraslot(mv)+1);

if (superverbose)
  {
fprintf(stderr,"New clause list\n\t ");
for(i=0; i<(cl->numlit); i++) fprintf(stderr,"%d ",cl->clause[i]);
fprintf(stderr,"\n");
  }

for (i=extraslot(mv)+1; i<log_domainsize; i++)
  {
cl->next = newclause(1);
cl = cl->next;
cl->clause[0] = bit[binbase(mv)][i] * (log_domainsize*(nblit.var-1)+i+1);
  }

cl->next = NULL;

if (superverbose)
  {
fprintf(stderr,"\t ");
for(i=0; i<(cl->numlit); i++) fprintf(stderr,"%d ",cl->clause[i]);
fprintf(stderr,"\n");
  }
  }
else
  {
/* Clauselist := cross product of current clauses and new literals */

if (superverbose) fprintf(stderr,"Empty clause list\n");

newclauses = NULL;
newcl = NULL;

for(cl=clauses; cl!=NULL; dealloctrans(&cl))/* transverse list, deleting it as we go ... */
  {

if (superverbose)
  {
fprintf(stderr,"Clause : ");
for(i=0; i<(cl->numlit); i++) fprintf(stderr,"%d ",cl->clause[i]);
fprintf(stderr,"\n");
  }

for(i=extraslot(mv); i<log_domainsize; i++)
  {
if (newcl == NULL)
  {
newclauses = newclause((cl->numlit)+1);
newcl = newclauses;
  }
else
  {
newcl->next = newclause((cl->numlit)+1);
newcl = newcl->next;
  }

newcl->clause[cl->numlit] = bit[binbase(mv)][i] * (log_domainsize*(nblit.var-1)+i+1);
for(j=0; j<(cl->numlit); j++) newcl->clause[j] = cl->clause[j];

if (superverbose)
  {
fprintf(stderr,"\t ... ");
for(j=0; j<(newcl->numlit); j++) fprintf(stderr,"%d ",newcl->clause[j]);
fprintf(stderr,"\n");
  }
  }
  }

  }

*ptrBclauses = newclauses;
  }

void dealloctrans(clause_type **cl)
  {
clause_type *old_cl;

old_cl = *cl;
(*cl) = (*cl)->next;
free(old_cl);
  }

void writeoutBclauses(clause_list Bclauses)
  {
int i;
clause_type *cl;

/* writeout clauses in list, deallocating memory as we go ... */

for(cl=Bclauses; cl!=NULL; dealloctrans(&cl))/* transverse list, deleting it as we go ... */
  {
for(i=0; i<(cl->numlit); i++)
  {
fprintf(fp,"%d ",cl->clause[i]);
  }
fprintf(fp,"0\n");
cldone++;
  }
  }

clause_type *newclause(int numlit)
  {
clause_type *cl;

if ( ( cl = (clause_type *) malloc(sizeof(clause_type)) ) == NULL)
  {
fprintf(stderr,"Out of memory\n");
exit(-1);
  }

if ( (cl->clause = (int *) malloc(sizeof(int)*numlit)) == NULL)
  {
fprintf(stderr,"Out of memory\n");
exit(-1);
  }

cl->numlit = numlit;
cl->next = NULL;

return cl;
  }

int newseed()
  {
int seed;
struct timeval tv;
struct timezone tzp;
unsigned sec, usec; 

gettimeofday(&tv,&tzp); 
usec = (int)tv.tv_usec; 
sec = (int)tv.tv_sec; 
        
seed = (((sec&3)<<20) | (usec<<22) | usec) & 0x7FFFFFFF; 
 
return seed;
  }