/****** Functions on Files and I/O ***********************/
/* Output                                                */
/*     FILE *OpenFile(integer instance);                 */
/*     void PrintBanner();                               */
/*     void FPrintBanner(FILE *fp);                      */
/* Input                                                 */
/*     void ScanParameters(int argc, char *argv[]);      */
/*********************************************************/


#include <stdio.h>

FILE *OpenFile(integer instance)
{
  char file_name[256];
  FILE *fp;

  sprintf(file_name,"p-%s-%s%s-K%ld-C%ld-V%ld-D%ld.%ld",name,
	  (flag_Kenc? "modK":(flag_S4enc? "modS4":"cnf")),
          (flag_SSSEnc? "SSS" :(flag_LadnerEnc? "Ladn":"")),
	      MaxLiterals,MaxClauses,MaxVariables,MaxDepth,instance);
  fp=fopen(file_name,"w");
  if (fp==NULL) {
    fprintf(stderr,"ERROR - cannot open file - ERROR\n");
    fprintf(stderr,"%s cannot be created (or rewritten)\n",file_name);
    exit(1);
  }
  return fp;
}


void FprintBanner(FILE *fp)
{
  int i;

  fprintf(fp,"%% %s\n",banner[0]);
  fprintf(fp,"%% -clauses %ld -vars %ld -depth %ld -lits %ld %s\n",
                MaxClauses,MaxVariables,MaxDepth,MaxLiterals,
	        (flag_Kenc? "-K":(flag_S4enc? "-S4":"")));
  fprintf(fp,"%% -prneg %lf -prmod %lf\n",
                ProbNegated,ProbModal);
  if (flag_LadnerEnc)
      fprintf(fp,"%% -ladner\n");
  if (flag_SSSEnc)
      fprintf(fp,"%% -sss\n");
  for (i=1;i<MAXBANNER;i++)
    fprintf(fp,"%% %s\n",banner[i]);
  fprintf(fp,"\n\n");
}


void ScanParameters(int argc, char *argv[])
{
  int i;

  i=0;
  while(++i<argc)
    if (strcmp(argv[i],"-clauses")==0) {
      i++;
      MaxClauses=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-vars")==0) {
      i++;
      MaxVariables=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-depth")==0) {
      i++;
      MaxDepth=(integer)atol(argv[i]);
    }
      /* Optional Benchmark Parameters */
    else if (strcmp(argv[i],"-lits")==0) {
      i++;
      MaxLiterals=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-prmod")==0) {
      i++;
      ProbModal=(real)atof(argv[i]);
    }
    else if (strcmp(argv[i],"-prneg")==0) {
      i++;
      ProbNegated=(real)atof(argv[i]);
    }
    else if (strcmp(argv[i],"-K")==0) {
      flag_S4enc=0;
      flag_Kenc=1;
    }
    else if (strcmp(argv[i],"-S4")==0) {
      flag_Kenc=0;
      flag_S4enc=1;
    }
      /* Optional Generator Parameters */
    else if (strcmp(argv[i],"-notest")==0) {
      flag_test=0;
    }
    else if (strcmp(argv[i],"-ladner")==0) {
      flag_LadnerEnc=1;
      flag_SSSEnc=0;
    }
    else if (strcmp(argv[i],"-sss")==0) {
        flag_SSSEnc=1;
        flag_LadnerEnc=0;
    }
    else if (strcmp(argv[i],"-stdio")==0) {
      flag_stdio=1;
    }
    else if (strcmp(argv[i],"-all")==0) {
      flag_all=1;
      i++;
      NthInstance=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-single")==0) {
      i++;
      NthInstance=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-failures")==0) {
      i++;
      MaxFailures=(integer)atol(argv[i]);
    }
    else if (strcmp(argv[i],"-help")==0) {
      fprintf(stderr,"Usage\n");
      fprintf(stderr,"Standard Options: (n integer)\n");
      fprintf(stderr,"  -clauses n\n  -vars n\n  -depth n\n");
      fprintf(stderr,"Additional Options: (n integer and f real)\n");
      fprintf(stderr,"  -lits n\n  -prmod f\n  -prneg f\n");
      fprintf(stderr,"  -K /* Use modal encoding for K */\n");
      fprintf(stderr,"  -S4 /* Use (much harder) modal encoding for S4 */\n");
      fprintf(stderr,"Generator Options:\n");
      fprintf(stderr,"  -ladner /* Use optimized Ladner Encoding for QBF */\n");
      fprintf(stderr,"  -sss /* Use optimized Schmidt-Schauss Smolka Encoding for QBF */\n");
      fprintf(stderr,"  -notest /* Skips tests on benchmark */\n");
      fprintf(stderr,"  -failures n  /* Give up generation after n test failures*/\n");
      fprintf(stderr,"  -all n  /* Generate and output n instances */\n");
      fprintf(stderr,"  -single n  /* Generate n instances and output the nth */\n");
      fprintf(stderr,"  -stdio /* Outputs on standard output rather than file*/\n");
      fprintf(stderr,"  -help  /* This output */\n");
      exit(0);
    }
    else {
      fprintf(stderr,"ERROR - Unknonw Option - ERROR\n Use -help\n");
      exit(1);
    }
}



void PrintBanner()
{
  int i;

  FprintBanner(stdout);

}