/*********************************************************/
/*                                                       */
/* TABLEAUX NonClassical Systems Comparison (TANCS)      */
/*           Benchmark Generator                         */
/*                                                       */
/*  For information about this program, contact          */
/*      tancs@dis.uniroma1.it 	                         */
/*                                                       */
/* Copyright Fabio Massacci, November 1998               */
/*           Fabio Massacci & Francesco Donini Nov. 1999 */
/*           Universita' di Roma "La Sapienza"           */
/*                                                       */
/*********************************************************/

/*********************************************************/
/* LEGAL STUFF 1: GNU PUBLIC LICENCE                     */
/*********************************************************/
/* Permission is granted to make and distribute verbatim */
/* copies  of this software provided the copyright notice*/
/* this permission notice are preserved on all copies.   */
/*                                                       */ 
/* Permission is granted to copy and distribute modified */
/* versions of this program under the conditions for     */
/* verbatim copying, provided that                       */
/* - modifications and corresponding author(s) are       */
/*   clearly specified in the copyright notice           */
/* - the entire resulting derived work is  distributed   */
/*   under the terms of a permission notice identical to */
/*   this one.                                           */
/* Permission is granted to copy and distribute transla- */
/* tions of this software into another language, under   */
/* the above conditions for modified versions.           */
/*********************************************************/

/*********************************************************/
/* LEGAL STUFF 2: DISCLAIMER                             */
/*********************************************************/
/* The author(s) and the Dipart. of Informatica e Sist,  */
/* of the University of Roma "La Sapienza" disclaim all  */
/* warranties with regard to this program, including all */
/* implied warranties of merchantability and fitness. In */
/* no event shall the author(s) and the Dipart. of       */
/* Informatica e Sist, of the University of Roma "La     */
/* Sapienza" be liable for any special, indirect or      */
/* consequential damages or any damages whatsoever       */
/* resultingi from loss of use, data or profits, whether */
/* in an action of contract, negligence or other tortious*/
/* action, arising out of or in connection with the use  */
/* or performance of this program.                       */
/*********************************************************/

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
/****** DataType CONNECTIVE *******/

typedef short connective;

#define UNKNOWN -1
#define FALSE 0
#define TRUE 1
#define VAR 2
#define NOT 3
#define AND 4
#define OR 5
#define IMP 6
#define XOR 7
#define EQUIV 8
#define BOX 9
#define POS 10
#define REL 11
#define INVERSE 12
#define SEQUENCE 13
#define UNION 14
#define STAR 15
#define TEST 16

#define NUM_SYMBOLS 17

char *symbols_table[NUM_SYMBOLS] = {
   "false",
   "true",
   "v",
   "~",
   "&",
   "|",
   "=>",
   "<~>",
   "<=>",
   "box",
   "pos",
   "r",
   "-",
   "#",
   "U",
   "*",
   "?",
};

/****** DataType INTEGER - BOOL - IDENT *******/

typedef short bool;
typedef long int integer;
typedef double real;
typedef long int ident;

#define ZERO 0
#define ONE 1
#define TWO 2
#define TWO_TO_THE_24 16777216.0 /* 2**24 */

/****** DataType FML - PRG - SEQUENT *******/

struct fml_node;
struct prg_node;

struct sequent_node {
  struct fml_node*     first;
  struct sequent_node* rest;

};

struct pool_node {
  struct prg_node*  first;
  struct pool_node* rest;
};

struct fml_node {
  connective    op;
  ident         name;
  struct pool_node* subprg;
  struct sequent_node* subfml;
};

struct prg_node {
  connective    op;
  ident         name;
  struct sequent_node* subfml;
  struct pool_node* subprg;
};


typedef struct sequent_node *sequent;
typedef struct fml_node *fml;

typedef struct pool_node *pool;
typedef struct prg_node *prg;


#define EMPTY_SEQUENT (sequent)NULL
#define NOT_EXISTS_FML (fml)NULL
#define EMPTY_POOL (pool)NULL
#define NOT_EXISTS_PRG (prg)NULL

/****** Functions on FML, SEQUENTS, PRG, and POOLS *****************/
/* FML Constructors                                                */
     fml False();                                                
     fml True();                                                 
     fml Var(ident);                                        
     fml Not(fml);                                             
     fml And(sequent);                                  
     fml Or(sequent);                                   
     fml Imp(sequent);                                  
     fml Xor(sequent);                                  
     fml Equiv(sequent);                                
     fml Box(prg, fml);                                      
     fml Pos(prg, fml);                                      
/* PRG Constructors */
     prg Rel(ident);                                        
     prg Inverse(prg);                                         
     prg Union(pool);                                   
     prg Sequence(pool);                                
     prg Star(prg);                                            
     prg Test(fml);                                            
/* Destructors  */
     void DeleteFml(fml);                                      
     void DeleteSequent(sequent);                              
     void DeletePrg(prg);                                      
     void DeletePool(pool);                                  
/* Tests */
     ident LitName(fml);                                       
     ident RelName(prg);                                       
     int CmpFml(fml, fml);                                
     bool EqualFml(fml, fml);                                
     bool PrecFml(fml, fml);                                 
     int CmpPrg(prg, prg);
     bool EqualPrg(prg, prg);                                
     bool PrecPrg(prg, prg); 
     bool CompareFml(fml,fml);
     bool ComparePrg(fml,fml);
/* Updates */
     sequent WithFml(fml, sequent);                                  
     sequent AddFml(fml, sequent);                                   
     fml CopyFml(fml);                                         
     pool WithPrg(prg, pool);                                   
     pool AddPrg(prg, pool);                                    
     prg CopyPrg(prg);                                        
/* Search  */    
     bool FindTwinFml(fml, sequent, bool (*CompareFml)(fml,fml));       
     bool FindTwinPrg(prg, pool, bool (*ComparePrg)(prg,prg));        
/* Output  */
     void PrintFml(fml);                                       
     void PrintSequent(sequent, char *, char *);                               
     void FprintFml(FILE *, fml);                            
     void FprintSequent(FILE *, sequent, char *, char *);                    
     void PrintPrg(prg);                                       
     void FprintPrg(FILE *, prg);
/*******************************************************************/

/****** Constructors *******/


sequent NewSequent()
{
  sequent S;

  S = (sequent)malloc(sizeof(struct sequent_node));
  S -> first = NOT_EXISTS_FML;
  S -> rest = EMPTY_SEQUENT;
  
  return S;
}


fml NewFml()
{
  fml A;

  A = (fml)malloc(sizeof(struct fml_node));
  A->op = UNKNOWN;
  A->name = ZERO;
  A->subfml = EMPTY_SEQUENT;
  A->subprg = EMPTY_POOL;

  return A;
}

pool NewPool()
{
  pool PPP;

  PPP = (pool)malloc(sizeof(struct pool_node));
  PPP -> first = NOT_EXISTS_PRG;
  PPP -> rest = EMPTY_POOL;
  
  return PPP;
}

prg NewPrg()
{
  prg P;

  P = (prg)malloc(sizeof(struct prg_node));
  P->op = UNKNOWN;
  P->name = ZERO;
  P->subprg = EMPTY_POOL;
  P->subfml = EMPTY_SEQUENT;

  return P;
}


/****** Destructors *******/

void DeleteFml(fml A)
{
  DeleteSequent(A->subfml);
  DeletePool(A->subprg);
  free(A);
}

void DeleteSequent(sequent S)
{
  sequent SA;

  while (S!=EMPTY_SEQUENT) {
    SA = S;
    S = S->rest;
    DeleteFml(SA->first);
    free(SA);
  }
}

void DeletePrg(prg P)
{
  DeletePool(P->subprg);
  DeleteSequent(P->subfml);
  free(P);
}

void DeletePool(pool PPP)
{
  pool QQQ;

  while (PPP!=EMPTY_POOL) {
    QQQ = PPP;
    PPP = PPP->rest;
    DeletePrg(QQQ->first);
    free(QQQ);
  }
}

/****** Testing *******/

 
ident LitName(fml A)
{
  if (A->op==VAR)
    return (A->name);
  else if (A->op==NOT && A->subfml->first->op==VAR)
    return (A->subfml->first->name);
  else 
    return ZERO;
}

 
ident RelName(prg P)
{
  if (P->op==REL)
    return (P->name);
  else if (P->op==INVERSE && P->subprg->first->op==REL)
    return (P->subprg->first->name);
  else 
    return ZERO;
}

integer LenghtSequent(sequent S)
{
  integer l;
  
  for (l=0; S!=EMPTY_SEQUENT; S=S->rest)
    ++l;

  return l;

}

integer LenghtPool(pool PPP)
{
  integer l;
  
  for (l=0; PPP!=EMPTY_POOL; PPP=PPP->rest)
    ++l;

  return l;

}


int CmpFml(fml A,fml B)
{
  int compare;

  if (A->op < B->op)
    return -1;
  else if (A->op == B->op && A->name < B-> name )
    return -1;
  else if (A->op == B->op && A->name == B-> name) {
    if ((compare=CmpPool(A->subprg,B->subprg))!=0)
      return compare;
    else
      return CmpSequent(A->subfml,B->subfml);
  }
  else
    return 1;
}

int CmpSequent(sequent Asub, sequent Bsub)
{
  int compare;

  while (Asub!=EMPTY_SEQUENT && Bsub!=EMPTY_SEQUENT && (compare=CmpFml(Asub->first,Bsub->first))==0) {
      Asub = Asub->rest;
      Bsub = Bsub->rest;
    }
    if (Asub!=EMPTY_SEQUENT && Bsub!=EMPTY_SEQUENT)
      return compare;
    else if (Asub==EMPTY_SEQUENT && Bsub!=EMPTY_SEQUENT)
      return -1;
    else if (Asub==EMPTY_SEQUENT && Bsub==EMPTY_SEQUENT)
      return 0;
    else
      return 1;
}

bool PrecFml(fml A,fml B)
{
  return (CmpFml(A,B)==-1);
}


bool EqualFml(fml A, fml B)
{
  return (CmpFml(A,B)==0);
}

bool NegateFml(fml A, fml B)
{

  while (A->op == NOT && B->op == NOT) {
    A=A->subfml->first;
    B=B->subfml->first;
  }

  if (A->op == NOT && B->op != NOT)
    return EqualFml(A->subfml->first,B);
  else if (A->op != NOT && B->op == NOT)
    return EqualFml(A,B->subfml->first);
  else
    return 0;
}

int CmpPrg(prg P, prg Q)
{
  int compare;

  if (P->op < Q->op)
    return -1;
  else if (P->op == Q->op && P->name < Q->name )
    return -1;
  else if (P->op == Q->op && P->name == Q->name ) {
    if ((compare=CmpPool(P->subprg,Q->subprg))!=0)
      return compare;
    else
      return CmpSequent(P->subfml,Q->subfml); 
  }
  else
    return 1;
}

int CmpPool(pool Psub, pool Qsub)
{
  int compare;

  compare=0;
  while (Psub!=EMPTY_POOL && Qsub!=EMPTY_POOL && (compare=CmpPrg(Psub->first,Qsub->first))==0) {
    Psub = Psub->rest;
    Qsub = Qsub->rest;
  }
  if (Psub!=EMPTY_POOL && Qsub!=EMPTY_POOL)
    return compare;
  else if (Psub==EMPTY_POOL && Qsub!=EMPTY_POOL)
    return -1;
  else if (Psub==EMPTY_POOL && Qsub==EMPTY_POOL)
    return 0;
  else
    return 1;
}


bool PrecPrg(prg P,prg Q)
{
  return (CmpPrg(P,Q)==-1);
}


bool EqualPrg(prg P, prg Q)
{
  return (CmpPrg(P,Q)==0);
}

bool InversePrg(prg P, prg Q)
{

  while (P->op == INVERSE && Q->op == INVERSE) {
    P=P->subprg->first;
    Q=Q->subprg->first;
  }

  if (P->op == INVERSE && Q->op != INVERSE)
    return EqualPrg(P->subprg->first,Q);
  else if (P->op != INVERSE && Q->op == INVERSE)
    return EqualPrg(P,Q->subprg->first);
  else
    return 0;
}

/****** Updates *******/


sequent InsertOrdFml(sequent S, fml A,bool (*PrecFml)())
{
  sequent precS,corrS,genS;
  
  genS=NewSequent();
  genS->rest=S;
  precS=genS;
  corrS=precS->rest;

  while (corrS!=EMPTY_SEQUENT && (*PrecFml)(corrS->first,A)) {
    precS=precS->rest;
    corrS=corrS->rest;
  }
  
  precS->rest=NewSequent();
  precS->rest->first=A;
  precS->rest->rest=corrS;
  
  S=genS->rest;
  free(genS);
  
  return S;
}


sequent WithFml(fml A,sequent S)
{
  return InsertOrdFml(S,A,PrecFml);
}


sequent AddFml(fml A,sequent S)
{
  sequent NS;
  
  NS=NewSequent();
  NS->first=A;
  NS->rest=S;
  
  return NS;

}

pool InsertOrdPrg(pool PPP, prg P,bool (*PrecPrg)())
{
  pool precPPP,corrPPP,genPPP;
  
  genPPP=NewPool();
  genPPP->rest=PPP;
  precPPP=genPPP;
  corrPPP=precPPP->rest;

  while (corrPPP!=EMPTY_POOL && (*PrecPrg)(corrPPP->first,P)) {
    precPPP=precPPP->rest;
    corrPPP=corrPPP->rest;
  }
  
  precPPP->rest=NewPool();
  precPPP->rest->first=P;
  precPPP->rest->rest=corrPPP;
  
  PPP=genPPP->rest;
  free(genPPP);
  
  return PPP;
}


pool WithPrg(prg P,pool PPP)
{
  return InsertOrdPrg(PPP,P,PrecPrg);
}


pool AddPrg(prg P,pool PPP)
{
  pool NPPP;
  
  NPPP=NewPool();
  NPPP->first=P;
  NPPP->rest=PPP;
  
  return NPPP;

}


/*************** CONSTRUCTORS *************/

fml False()
{
  fml A=NewFml();

  A->op=FALSE;

  return A;
}


fml True()
{
  fml A=NewFml();

  A->op=TRUE;

  return A;
}


fml Var(ident A_name)
{
  fml A=NewFml();

  A->op=VAR;
  A->name=A_name;

  return A;
}


fml Not(fml A)
{
  fml B=NewFml();

  B->op=NOT;
  B->name=ONE;
  B->subfml=NewSequent();
  B->subfml->first=A;

  return B;
}


fml And(sequent A_subfml)
{
  fml A=NewFml();

  A->op=AND;
  A->name=LenghtSequent(A_subfml);
  A->subfml=A_subfml;

  return A;
}


fml Or(sequent A_subfml)
{
  fml A=NewFml();

  A->op=OR;
  A->name=LenghtSequent(A_subfml);
  A->subfml=A_subfml;

  return A;
}


fml Imp(sequent A_subfml)
{
  fml A=NewFml();

  A->op=IMP;
  A->name=LenghtSequent(A_subfml);
  A->subfml=A_subfml;

  return A;
}


fml Xor(sequent A_subfml)
{
  fml A=NewFml();

  A->op=XOR;
  A->name=LenghtSequent(A_subfml);
  A->subfml=A_subfml;

  return A;
}


fml Equiv(sequent A_subfml)
{
  fml A=NewFml();

  A->op=EQUIV;
  A->name=LenghtSequent(A_subfml);
  A->subfml=A_subfml;

  return A;
}


fml Box(prg P, fml A)
{
  fml B=NewFml();

  B->op=BOX;
  B->name=ONE;
  B->subprg=NewPool();
  B->subprg->first=P;
  B->subfml=NewSequent();
  B->subfml->first=A;

  return B;
}


fml Pos(prg P, fml A)
{
  fml B=NewFml();

  B->op=POS;
  B->name=ONE;
  B->subprg=NewPool();
  B->subprg->first=P;
  B->subfml=NewSequent();
  B->subfml->first=A;

  return B;
}

prg Rel(ident P_name)
{
  prg P=NewPrg();

  P->op=REL;
  P->name=P_name;

  return P;
}


prg Inverse(prg P)
{
  prg Q=NewPrg();

  Q->op=INVERSE;
  Q->name=ONE;
  Q->subprg=NewPool();
  Q->subprg->first=P;

  return Q;
}


prg Union(pool P_subprg)
{
  prg P=NewPrg();

  P->op=UNION;
  P->name=LenghtPool(P_subprg);
  P->subprg=P_subprg;

  return P;
}


prg Sequence(pool P_subprg)
{
  prg P;
  P=NewPrg();
  P->op=SEQUENCE;
  P->name=LenghtPool(P_subprg);
  P->subprg=P_subprg;

  return P;
}


prg Star(prg P)
{
  prg Q=NewPrg();

  Q->op=STAR;
  Q->name=ONE;
  Q->subprg=NewPool();
  Q->subprg->first=P;

  return Q;
}

prg Test(fml A)
{
  prg Q=NewPrg();

  Q->op=TEST;
  Q->name=ONE;
  Q->subfml=NewSequent();
  Q->subfml->first=A;

  return Q;
}


fml CopyFml(fml A)
{
  sequent Asub,Bsub;
  fml B;

  if (A==NOT_EXISTS_FML)
    B=NOT_EXISTS_FML;
  else
    switch (A->op) {
    case UNKNOWN:
      B=NewFml();
      break;
    case FALSE:
      B=False();
      break;
    case TRUE:
      B=True();
      break;
    case VAR:
      B=Var(A->name);
      break;
    case NOT:
      B=Not(CopyFml(A->subfml->first));
      break;
    case AND:
      Bsub=EMPTY_SEQUENT;
      for (Asub=A->subfml;Asub!=EMPTY_SEQUENT;Asub=Asub->rest)
	Bsub=WithFml(CopyFml(Asub->first),Bsub);
      B=And(Bsub);
      break;
    case OR:
      Bsub=EMPTY_SEQUENT;
      for (Asub=A->subfml;Asub!=EMPTY_SEQUENT;Asub=Asub->rest)
	Bsub=WithFml(CopyFml(Asub->first),Bsub);
      B=Or(Bsub);
      break;
    case IMP:
      Bsub=EMPTY_SEQUENT;
      for (Asub=A->subfml;Asub!=EMPTY_SEQUENT;Asub=Asub->rest)
	Bsub=WithFml(CopyFml(Asub->first),Bsub);
      B=Imp(Bsub);
      break;
    case XOR:
      Bsub=EMPTY_SEQUENT;
      for (Asub=A->subfml;Asub!=EMPTY_SEQUENT;Asub=Asub->rest)
	Bsub=WithFml(CopyFml(Asub->first),Bsub);
      B=Xor(Bsub);
      break;
    case EQUIV:
      Bsub=EMPTY_SEQUENT;
      for (Asub=A->subfml;Asub!=EMPTY_SEQUENT;Asub=Asub->rest)
	Bsub=WithFml(CopyFml(Asub->first),Bsub);
      B=Equiv(Bsub);
      break;
    case BOX:
      B=Box(CopyPrg(A->subprg->first),CopyFml(A->subfml->first));
      break;
    case POS:
      B=Pos(CopyPrg(A->subprg->first),CopyFml(A->subfml->first));
      break;
    }
  return B;
}


prg CopyPrg(prg P)
{
  pool Psub,Qsub;
  prg Q;

  if (P==NOT_EXISTS_PRG)
    Q=NOT_EXISTS_PRG;
  else
    switch (P->op) {
    case UNKNOWN:
      Q=NewPrg();
      break;
    case REL:
      Q=Rel(P->name);
      break;
    case INVERSE:
      Q=Inverse(CopyPrg(P->subprg->first));
      break;
    case UNION:
      Qsub=EMPTY_POOL;
      for (Psub=P->subprg; Psub!=EMPTY_POOL; Psub=Psub->rest)
	Qsub=WithPrg(CopyPrg(Qsub->first),Qsub);
      Q=Union(Qsub);
      break;
    case SEQUENCE:
      Qsub=EMPTY_POOL;
      for (Psub=P->subprg; Psub!=EMPTY_POOL; Psub=Psub->rest)
	Qsub=WithPrg(CopyPrg(Psub->first),Qsub);
      Q=Sequence(Qsub);
      break;
    case STAR:
      Q=Star(CopyPrg(P->subprg->first));
      break;
    case TEST:
      Q=Test(CopyFml(P->subfml->first));
      break;
    }
  return Q;
}

/****** Search *******/


bool FindTwinFml(fml A, sequent S,bool (*CompareFml)())
{
  while (S != EMPTY_SEQUENT && !((*CompareFml)(A,S->first))) {
    S = S->rest;
  }

  return (S != EMPTY_SEQUENT);
}


bool FindTwinPrg(prg A, pool S,bool (*ComparePrg)())
{
  while (S != EMPTY_POOL && !((*ComparePrg)(A,S->first))) {
    S = S->rest;
  }

  return (S != EMPTY_POOL);
}

/****** Output *******/

void FprintFml(FILE *fp,fml A)
{
  char *op_symbol;
  sequent Asub;

  if (A==NOT_EXISTS_FML) {
    fprintf(stderr,"\nERROR - Formula do not exists - ERROR\n");
    exit(1);
  }
  else {
  op_symbol=symbols_table[A->op];

  switch (A->op) {
  case UNKNOWN:
    fprintf(stderr,"ERROR - ERROR - ERROR\nUNKNOWN FORMULA\n");
    exit(1);
  case FALSE: 
  case TRUE:
    fprintf(fp,"%s",op_symbol);
    break;
  case VAR:
    fprintf(fp,"%s%ld",op_symbol,A->name);
    break;
  case NOT:
    fprintf(fp,"%s",op_symbol);
    FprintFml(fp,A->subfml->first);
    break;
  case AND:
  case OR:
  case XOR:
  case EQUIV:
  case IMP:
    Asub=A->subfml;
    fprintf(fp,"(");
    FprintFml(fp,Asub->first);
    Asub = Asub->rest;
    while (Asub!=EMPTY_SEQUENT) {
      fprintf(fp," %s ",op_symbol);
      FprintFml(fp,Asub->first);
      Asub = Asub->rest;
      }
    fprintf(fp,")");
    break;
  case BOX:
  case POS:
    fprintf(fp,"(");
    fprintf(fp,"%s ",op_symbol);
    FprintPrg(fp,A->subprg->first);
    fprintf(fp," : ");
    FprintFml(fp,A->subfml->first);
    fprintf(fp,")");
    break;
  }
  }
}

void FprintSequent(FILE *fp,sequent S, char *name,char *type)
{
  integer i;

  i=1;
  while (S!=EMPTY_SEQUENT) {
    fprintf(fp,"inputformula(%s%ld,%s,\n",name,i,type);
    fprintf(fp,"    ");
    FprintFml(fp,S->first);
    fprintf(fp,"\n    ).\n\n");
    fflush(fp);
    S = S->rest;
    i++;
  }
}


void FprintPrg(FILE *fp,prg P)
{
  char *op_symbol;
  pool Psub;

  if (P==NOT_EXISTS_PRG) {
    fprintf(stderr,"\nERROR - PROGRAM do not exists - ERROR\n");
    exit(1);
  }
  else {
  op_symbol=symbols_table[P->op];

  switch (P->op) {
  case UNKNOWN:
    fprintf(stderr,"ERROR - ERROR - ERROR\nUNKNOWN FORMULA\n");
    exit(1);
  case REL:
    fprintf(fp,"%s%ld",op_symbol,P->name);
    break;
  case INVERSE:
  case STAR:
    FprintPrg(fp,P->subprg->first);
    fprintf(fp,"%s",op_symbol);
    break;
  case UNION:
  case SEQUENCE:
    Psub=P->subprg;
    fprintf(fp,"(");
    FprintPrg(fp,Psub->first);
    Psub = Psub->rest;
    while (Psub!=EMPTY_POOL) {
      fprintf(fp," %s ",op_symbol);
      FprintPrg(fp,Psub->first);
      Psub = Psub->rest;
      }
    fprintf(fp,")");
    break;
  case TEST:
    FprintFml(fp,P->subfml->first);
    fprintf(fp,"%s",op_symbol);
    break;
  }
  }
}

void PrintFml(fml A)
{
  FprintFml(stdout,A);
}

void PrintSequent(sequent S, char *name,char *type)
{
  FprintSequent(stdout,S,name,type);
}

void PrintPrg(prg P)
{
  FprintPrg(stdout,P);
}





/****************************************/
/* void InitRandom();                   */
/* integer Random1To(integer N);        */
/* integer Random01(real threshold);  */
/****************************************/

/*********************************************************/
/* Creates seeds by using seconds and milliseconds       */
/* Uses only 7 bits of sec == approx 2 minutes           */
/* Uses higher order bits of system function random()    */
/*********************************************************/

#include <sys/time.h>

#define MY_RAND_MAX 2147483647

void InitRandom()
{
  struct timeval tv;
  struct timezone tzp;
  long sec, msec;

  gettimeofday(&tv,&tzp);
  sec = (long) tv.tv_sec;
  msec = (long) tv.tv_usec;

  srandom((unsigned int)(((sec & 0177 ) * 1000000) + msec));
}

integer Random1To(integer n)
{
    return (1+(integer)(((double)n)*random()/(1.0+MY_RAND_MAX)));
}

integer Random01(real threshold)
{
    if ( random()<=(long)(threshold*MY_RAND_MAX) )
      return 1;
    else 
      return 0;
}
#define MAXBANNER 7
char *banner[MAXBANNER+1] = {
  "Unbounded Converse PDL Sat from QBF - Randomly Generated",
  "Original reference Ladner, SIAM J. of Comp., SIAM Press",
  "Smart coding avoid the auxiliary variables of the original paper",
  "Parameter depth=-1 generate a random number of alternations",
  "With K,S4 flag prop variables hidden by modal proposition for K and S4",
  "Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)", 
  "Copyright Fabio Massacci, November 1999"
};

char *name="qbf-cpdl";

/******* BENCHMARK PARAMETERS ******/

integer MaxVariables=2;
integer MaxClauses=20;
integer MaxDepth=2;
integer MaxLiterals=4;
real  ProbModal=0.5;
real  ProbNegated=0.5;
bool flag_Kenc=0;
bool flag_S4enc=0;
bool flag_LadnerEnc=0;
bool flag_SSSEnc=0;

#define AltDepth (MaxVariables*(MaxDepth+1))

/******* OPTIONAL PARAMETERS ******/
bool flag_test=1;
bool flag_stdio=0;
bool flag_all=0;
integer NthInstance=1;
integer MaxFailures=(integer)TWO_TO_THE_24;
/* Quantified Boolean Formula Generation */

fml CodedVar(ident depth)
{
  return(Var(Random1To(MaxVariables)+MaxVariables*depth));
}


fml GenerateUniversalLiteral()
{
  fml L;

  if (MaxDepth%2==0)
    L=CodedVar(2*Random1To(MaxDepth/2)-1);
  else
    L=CodedVar(2*Random1To((MaxDepth+1)/2)-1);
    
  if (Random01(ProbNegated)) 
    L=Not(L);
  
  return L;
}


fml GenerateExistentialLiteral()
{
  fml L;

  if (MaxDepth%2==0)
    L=CodedVar(2*(Random1To(MaxDepth/2+1)-1));
  else
    L=CodedVar(2*(Random1To((MaxDepth+1)/2)-1));

    
  if (Random01(ProbNegated)) 
    L=Not(L);

  return L;
}


bool Existential(integer var_name)
{
if (var_name%MaxVariables==0)
  return ((var_name/MaxVariables-1)%2==0);
else
  return ((var_name/MaxVariables)%2==0);
}


fml GenerateLiteral()
{
  fml L;

  if (MaxDepth!=0 && Random01(ProbModal))
    L=GenerateUniversalLiteral();
  else
    L=GenerateExistentialLiteral();
  
  return L;
}

fml GenerateQuantifiedClause()
{
  sequent C;
  fml L;
  integer num_literals,failed_literals;

  C=EMPTY_SEQUENT;
  num_literals=0;
  failed_literals=0;
  while (num_literals<MaxLiterals) {
    if (MaxDepth==0 || num_literals==0 || num_literals==2)
      L=GenerateExistentialLiteral();
    else if (num_literals==1|| num_literals ==3)
      L=GenerateUniversalLiteral();
    else
      L=GenerateLiteral();
    if (!flag_test ) {
      num_literals++;
      C=AddFml(L,C);
      failed_literals=0;
    }
    else if (!FindTwinFml(L,C,EqualFml) && !FindTwinFml(L,C,NegateFml)) {
      num_literals++;
      C=WithFml(L,C);
      failed_literals=0;
    }
    else {
      DeleteFml(L);
      failed_literals++;
      if (failed_literals>MaxFailures) {
	fprintf(stderr,"\n WARNING - Too many failures - WARNING \n");
	fprintf(stderr,"There might not be enough different formulae\n");
	fprintf(stderr,"With these parameters\n");
	exit(1);
      }
    }
  }
  return Or(C);
}


sequent GenerateQuantifiedFormulae()
{
  sequent S;
  fml A;  
  integer num_clauses,failed_clauses;

  S=EMPTY_SEQUENT;
  failed_clauses=0;
  num_clauses=0;
  while (num_clauses<MaxClauses) {
    failed_clauses++;
    A=GenerateQuantifiedClause();
    if (!flag_test || !FindTwinFml(A,S,EqualFml)) {
      num_clauses++;
      failed_clauses=0;
      S=WithFml(A,S);
    }
    else {
      failed_clauses++;
      DeleteFml(A);
      if (failed_clauses>MaxFailures) {
	fprintf(stderr,"\n WARNING - Too many failures - WARNING \n");
	fprintf(stderr,"There might not be enough different formulae\n");
	fprintf(stderr,"With these parameters\n");
	exit(1);
      }
    }
  }

  return S;
}


sequent VariablesInQBF(sequent QBFS)
{
  sequent varS, litS;
  fml A;

  varS=EMPTY_SEQUENT;
  for(; QBFS!=EMPTY_SEQUENT; QBFS=QBFS->rest)
    for(litS=QBFS->first->subfml; litS!=EMPTY_SEQUENT; litS=litS->rest) {
	A=Var(LitName(litS->first));
	if (!FindTwinFml(A,varS,EqualFml))
	  varS=AddFml(A,varS);
	else
	  DeleteFml(A);
    }
  return(varS);
}
/******* FORMULAE MODALIZER ******/

prg AltPrg(prg P)
{
  prg Pback,Pforth;

  Pback=Inverse(CopyPrg(P));
  Pforth=CopyPrg(P);

  return Sequence(AddPrg(P,
		  AddPrg(Pback,
		  AddPrg(Pforth,
		  EMPTY_POOL))));

}

fml GenerateModalVariable(ident var)
{
  integer i,j;

  fml A[3],Qi,NQi;

  if (flag_Kenc) {
    Qi=Pos(AltPrg(Rel(ONE)),Var(ONE));
    for (j=1; j<var; j++)
      Qi=Pos(AltPrg(Rel(ONE)),Qi);
    A[2]=Pos(AltPrg(Rel(ONE)),And(WithFml(Not(Var(ONE)),WithFml(Qi,EMPTY_SEQUENT))));
  }
  else {
    for (i=0;i<2;i++) {
      Qi=Pos(AltPrg(Rel(ONE)),Box(AltPrg(Rel(ONE)),Var(ONE)));
      for (j=1; j<var;j++)
	Qi=Pos(AltPrg(Rel(ONE)),And(WithFml(Var(ONE),
			    WithFml(Pos(AltPrg(Rel(ONE)),And(WithFml(Not(Var(ONE)),
					     WithFml(Qi,EMPTY_SEQUENT)))),
			    EMPTY_SEQUENT))));
      NQi=Box(AltPrg(Rel(ONE)),Pos(AltPrg(Rel(ONE)),Not(Var(ONE))));
      for (j=1; j<=var;j++)
	NQi=Box(AltPrg(Rel(ONE)),Or(WithFml(Not(Var(ONE)),
		       WithFml(Box(AltPrg(Rel(ONE)),Or(WithFml(Var(ONE),
				       WithFml(NQi,EMPTY_SEQUENT)))),
		       EMPTY_SEQUENT))));
      A[i]=Pos(AltPrg(Rel(ONE)),And(WithFml(Qi,WithFml(NQi,EMPTY_SEQUENT))));
    }
    A[2]=And(WithFml(Pos(AltPrg(Rel(ONE)),A[0]),
	     WithFml(Box(AltPrg(Rel(ONE)),Or(WithFml(Not(A[1]),
			     WithFml(Pos(AltPrg(Rel(ONE)),Box(AltPrg(Rel(ONE)),Not(Var(ONE)))),
			     EMPTY_SEQUENT)))),
	     EMPTY_SEQUENT)));
  }
  return A[2];
}


prg ModalizePrg(prg);

fml ModalizeFml(fml A)
{
  sequent Asub;
  fml MA;

  if (A==NOT_EXISTS_FML) {
    printf("\nERROR - Formula do not exists - ERROR\n");
    exit(1);
  }

  switch (A->op) {
  case UNKNOWN:
  case FALSE: 
  case TRUE:
    break;
  case VAR:
    MA=GenerateModalVariable(A->name);
    DeleteFml(A);
    A=MA;
    break;
  case NOT:
  case AND:
  case OR:
  case XOR:
  case EQUIV:
  case IMP:
    for (Asub=A->subfml; Asub!=EMPTY_SEQUENT; Asub = Asub->rest)
      Asub->first=ModalizeFml(Asub->first);
    break;
  case BOX:
  case POS:
    A->subprg->first=ModalizePrg(A->subprg->first);
    for (Asub=A->subfml; Asub!=EMPTY_SEQUENT; Asub = Asub->rest)
      Asub->first=ModalizeFml(Asub->first);
    break;
  }
  return A;
}

prg ModalizePrg(prg P)
{
  pool Psub;

  if (P==NOT_EXISTS_PRG) {
    fprintf(stderr,"\nERROR - Program does not exists - ERROR\n");
    exit(1);
  }

  switch (P->op) {
  case UNKNOWN:
  case REL:
    break;
  case INVERSE:
  case UNION:
  case SEQUENCE:
  case STAR:
    for (Psub=P->subprg; Psub!=EMPTY_POOL; Psub = Psub->rest)
      Psub->first=ModalizePrg(Psub->first);
    break;
  case TEST:
    P->subfml->first=ModalizeFml(P->subfml->first);
    break;

  }
  return P;
}

sequent ModalizeFormulae(sequent S)
{
  sequent NS;
  
  for (NS=S;NS!=EMPTY_SEQUENT;NS=NS->rest)
    NS->first=ModalizeFml(NS->first);

  return S;
}
/******* BENCHMARK GENERATION ******/

fml NAltBox(integer n, prg P, fml A)
{
  integer i;

  for (i=0;i<n;i++) {
    A=Box(AltPrg(P),A);
    P=CopyPrg(P);
  }
  if (n>0)
    DeletePrg(P);

  return A;
}


fml NAltPos(integer n, prg P, fml A)
{
  integer i;

  for (i=0;i<n;i++) {
    A=Pos(AltPrg(P),A);
    P=CopyPrg(P);
  }
  if (n>0)
    DeletePrg(P);

  return A;
}
 

sequent GenerateModalFormulae(sequent QBFS)
{
  sequent modS,litS;
  fml A,C;
  integer i;

  modS=EMPTY_SEQUENT;

  if (!flag_SSSEnc)
    for(; QBFS!=EMPTY_SEQUENT; QBFS=QBFS->rest)
      modS=WithFml(Box(Star(AltPrg(Rel(ONE))),CopyFml(QBFS->first)),
                   modS);
  else {
    for(; QBFS!=EMPTY_SEQUENT; QBFS=QBFS->rest) {
      litS=QBFS->first->subfml;
      i=1;
      A=Var(i);
      while(i<=AltDepth && !FindTwinFml(A,litS,EqualFml) &&
            !FindTwinFml(A,litS,NegateFml)) {
        i++;
        DeleteFml(A);
        A=Var(i);
      }

      if (i>AltDepth) {
        C=False();
        DeleteFml(A);
      }
      else {

        if (FindTwinFml(A,litS,EqualFml))
          C=Box(AltPrg(Rel(ONE)),A);
        else
            C=Box(AltPrg(Rel(ONE)),Not(A));

        while(i<AltDepth) {
          i++;
          A=Var(i);
          if (FindTwinFml(A,litS,EqualFml))
            C=Box(AltPrg(Rel(ONE)),Or(WithFml(A,WithFml(C,EMPTY_SEQUENT))));
          else if (FindTwinFml(A,litS,NegateFml))
            C=Box(AltPrg(Rel(ONE)),Or(WithFml(Not(A),WithFml(C,EMPTY_SEQUENT))));
          else {
            C=Box(AltPrg(Rel(ONE)),C);
            DeleteFml(A);
          }
        }
      }
      modS=WithFml(C,modS);
    }
  }
  return modS;
}


sequent GenerateAltFormulae(sequent QBFS)
{
  sequent altS,S,litS,varS;
  fml A, Alt;
  integer i,j, curr_depth;

  altS=EMPTY_SEQUENT;

  varS=VariablesInQBF(QBFS);

  if (flag_SSSEnc || flag_LadnerEnc) {

    i=1;
    A=Var(i);
    while(i<=AltDepth && !FindTwinFml(A,varS,EqualFml) &&
          !FindTwinFml(A,varS,NegateFml)) {
      i++;
      DeleteFml(A);
      A=Var(i);
    }
    DeleteFml(A);

    if (i>AltDepth)
      Alt=True();
    else {
      curr_depth=i;

      if ( Existential(i))
        Alt=Pos(Rel(ONE),True());
      else
        Alt=Pos(Rel(ONE),And(WithFml(Var(i),
                             WithFml(Pos(Inverse(Rel(ONE)),Pos(Rel(ONE),Not(Var(i)))),
                             EMPTY_SEQUENT))));

      while(i<AltDepth) {
        i++;
        A=Var(i);
        if (!FindTwinFml(A,varS,EqualFml) || Existential(i)) {
          Alt=And(WithFml(Pos(Rel(ONE),True()),
                  WithFml(Box(AltPrg(Rel(ONE)),Alt),
                  EMPTY_SEQUENT)));
        }
        else {
          Alt=And(WithFml(Pos(Rel(ONE),And(WithFml(Var(i),
                                           WithFml(Pos(Inverse(Rel(ONE)),Pos(Rel(ONE),Not(Var(i)))),
                                           EMPTY_SEQUENT)))),
                  WithFml(Box(AltPrg(Rel(ONE)),Alt),
                  EMPTY_SEQUENT)));
        }
        DeleteFml(A);
      }
    }

    altS=WithFml(Alt,altS);

    if (flag_LadnerEnc) {
      for (j=curr_depth+1;j<=AltDepth;j++) {
        A=Var(j);
        if (FindTwinFml(A,varS,EqualFml)) {
          Alt=NAltBox(AltDepth-j+1,Rel(ONE),Imp(WithFml(CopyFml(A),
                                                WithFml(Box(Star(AltPrg(Rel(ONE))),CopyFml(A)),
                                                EMPTY_SEQUENT))));
          altS=WithFml(Alt,altS);

          A=Not(A);
          Alt=NAltBox(AltDepth-j+1,Rel(ONE),Imp(WithFml(CopyFml(A),
                                                WithFml(Box(Star(AltPrg(Rel(ONE))),CopyFml(A)),
                                                EMPTY_SEQUENT))));
          altS=WithFml(Alt,altS);
        }
        DeleteFml(A);
      }
    }
  }
  else {

    for (i=1;i<=AltDepth;i++) {
      A=Var(i);
      if (!FindTwinFml(A,varS,EqualFml))
        altS=WithFml(NAltBox(AltDepth-i,Rel(ONE),Pos(Rel(ONE),True())),
                     altS);
      DeleteFml(A);
    }

    for (S=varS;S!=EMPTY_SEQUENT;S=S->rest) {
      j=S->first->name;
      if (Existential(j))
        altS=WithFml(NAltBox(AltDepth-j,Rel(ONE),Pos(Rel(ONE),True())),
                     altS);
      else
        altS=WithFml(NAltBox(AltDepth-j,Rel(ONE),
                             Pos(Rel(ONE),And(WithFml(Var(j),
                                                      WithFml(Pos(Inverse(Rel(ONE)),
                                                                  Pos(Rel(ONE),Not(Var(j)))),
                                                              EMPTY_SEQUENT))))),
                     altS);
      altS=WithFml(NAltBox(AltDepth-j+1,Rel(ONE),
                           Imp(WithFml(Var(j),
                                      WithFml(Box(Star(AltPrg(Rel(ONE))),Var(j)),
                                              EMPTY_SEQUENT)))),
                   WithFml(NAltBox(AltDepth-j+1,Rel(ONE),
                                   Imp(WithFml(Not(Var(j)),
                                              WithFml(Box(Star(AltPrg(Rel(ONE))),Not(Var(j))),
                                                      EMPTY_SEQUENT)))),
                           altS));
    }
  }
  DeleteSequent(varS);

  return altS;
}


integer FindWorkableDepth(integer depth, integer vars)
{
  integer power,big_power;

  big_power=0;
  power=1;
  while (big_power<power) {
    big_power=power;
    power*=2;
  }
  
  if (depth==-1)
    return (Random1To(big_power/vars));
  else if (depth>big_power/vars) {
    fprintf(stderr,"ERROR - Alternation depth too big - ERROR\n");
    fprintf(stderr,"Approv Max for these var numbers = %ld\n",big_power/vars);
    exit(1);
  }
  else
    return depth;
}



/****** 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);

}
/******* MAIN FILE ******/

int main(int argc, char *argv[])
{
  sequent QBFS,ModS,AltS,Sgoal;
  integer instance;
  int i;
  FILE *fp;

  ScanParameters(argc,argv);

  InitRandom();

  Sgoal=WithFml(False(),EMPTY_SEQUENT);

  MaxDepth=FindWorkableDepth(MaxDepth,MaxVariables);
    
  QBFS=EMPTY_SEQUENT;
  ModS=EMPTY_SEQUENT;
  AltS=EMPTY_SEQUENT;
  for(instance=1; instance<=NthInstance; instance++) {
    DeleteSequent(QBFS);
    DeleteSequent(ModS);
    DeleteSequent(AltS);

    QBFS=GenerateQuantifiedFormulae();
    ModS=GenerateModalFormulae(QBFS);
    AltS=GenerateAltFormulae(QBFS);

    if (flag_Kenc || flag_S4enc) {
      ModS=ModalizeFormulae(ModS);
      AltS=ModalizeFormulae(AltS);
    }
    if (flag_all || instance==NthInstance) {
      if (flag_stdio) {
	PrintBanner();
	PrintSequent(ModS,"mod","hypothesis");
	PrintSequent(AltS,"alt","hypothesis");
	PrintSequent(Sgoal,"result","conjecture");
      }
      else {
	fp=OpenFile(instance);
	FprintBanner(fp);
	FprintSequent(fp,ModS,"mod","hypothesis");
	FprintSequent(fp,AltS,"alt","hypothesis");
	FprintSequent(fp,Sgoal,"result","conjecture");
	fclose(fp);
      }
    }
  }


  DeleteSequent(QBFS);
  DeleteSequent(ModS);
  DeleteSequent(AltS);
  DeleteSequent(Sgoal);

  return 0;
}