/*********************************************************/
/*                                                       */
/* 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 10
char *banner[MAXBANNER+1] = {
 "Unbounded Modal Sat from QBF - Randomly Generated",
  "Original reference Ladner, SIAM JOC, 1977, SIAM Press",
  "Smart coding avoid the auxiliary variables of the original paper",
  "With ladner flag encoding further optimized",
  "With sss flag encoding by Schimdt-Schauss Smolka, AIJ 1991, Elsevier",
  "With K,S4 flag prop variables hidden by modal proposition for K and S4",
  "(formulae are no longer in CNF) due to Halpern, AIJ 95, Elsevier",
  "Parameter depth=-1 generate a random number of alternations",
  "Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)",
  "Copyright Fabio Massacci, November 1998"
};

char *name="qbf";

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


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

  fml A[3],Qi,NQi;

  if (flag_Kenc) {
    Qi=Pos(Rel(ONE),Var(ONE));
    for (j=1; j<var; j++)
      Qi=Pos(Rel(ONE),Qi);
    A[2]=Pos(Rel(ONE),And(WithFml(Not(Var(ONE)),WithFml(Qi,EMPTY_SEQUENT))));
  }
  else {
    for (i=0;i<2;i++) {
      Qi=Pos(Rel(ONE),Box(Rel(ONE),Var(ONE)));
      for (j=1; j<var;j++)
	Qi=Pos(Rel(ONE),And(WithFml(Var(ONE),
			    WithFml(Pos(Rel(ONE),And(WithFml(Not(Var(ONE)),
					     WithFml(Qi,EMPTY_SEQUENT)))),
			    EMPTY_SEQUENT))));
      NQi=Box(Rel(ONE),Pos(Rel(ONE),Not(Var(ONE))));
      for (j=1; j<=var;j++)
	NQi=Box(Rel(ONE),Or(WithFml(Not(Var(ONE)),
		       WithFml(Box(Rel(ONE),Or(WithFml(Var(ONE),
				       WithFml(NQi,EMPTY_SEQUENT)))),
		       EMPTY_SEQUENT))));
      A[i]=Pos(Rel(ONE),And(WithFml(Qi,WithFml(NQi,EMPTY_SEQUENT))));
    }
    A[2]=And(WithFml(Pos(Rel(ONE),A[0]),
	     WithFml(Box(Rel(ONE),Or(WithFml(Not(A[1]),
			     WithFml(Pos(Rel(ONE),Box(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 NBox(integer n, prg P, fml A)
{
  integer i;

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

  return A;
}


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

  for (i=0;i<n;i++) {
    A=Pos(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)
      for(litS=QBFS->first->subfml; litS!=EMPTY_SEQUENT; litS=litS->rest)
        modS=WithFml(NBox(AltDepth-LitName(litS->first)+1,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(Rel(ONE),A);
        else
            C=Box(Rel(ONE),Not(A));

        while(i<AltDepth) {
          i++;
          A=Var(i);
          if (FindTwinFml(A,litS,EqualFml))
            C=Box(Rel(ONE),Or(WithFml(A,WithFml(C,EMPTY_SEQUENT))));
          else if (FindTwinFml(A,litS,NegateFml))
            C=Box(Rel(ONE),Or(WithFml(Not(A),WithFml(C,EMPTY_SEQUENT))));
          else {
            C=Box(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=And(WithFml(Pos(Rel(ONE),Var(i)),
                WithFml(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(Rel(ONE),Alt),EMPTY_SEQUENT)));
        }
        else {
          Alt=And(WithFml(Pos(Rel(ONE),Var(i)),
                          WithFml(Pos(Rel(ONE),Not(Var(i))),
                                  WithFml(Box(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=CopyFml(A);
          for (i=1;i<j-curr_depth;i++)
            Alt=And(WithFml(CopyFml(A),
                    WithFml(Box(Rel(ONE),Alt),
                        EMPTY_SEQUENT)));
          Alt=NBox(AltDepth-j+1,Rel(ONE),Imp(WithFml(CopyFml(A),
                                                  WithFml(Box(Rel(ONE),Alt),
                                                          EMPTY_SEQUENT))));
          altS=WithFml(Alt,altS);

          A=Not(A);
          Alt=CopyFml(A);
          for (i=1;i<j-curr_depth;i++)
            Alt=And(WithFml(CopyFml(A),
                    WithFml(Box(Rel(ONE),Alt),
                        EMPTY_SEQUENT)));
          Alt=NBox(AltDepth-j+1,Rel(ONE),Imp(WithFml(CopyFml(A),
                                                  WithFml(Box(Rel(ONE),Alt),
                                                          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(NBox(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(NBox(AltDepth-j,Rel(ONE),Pos(Rel(ONE),True())),
                   altS);
      else
        altS=WithFml(NBox(AltDepth-j,Rel(ONE),Pos(Rel(ONE),Var(j))),
	   WithFml(NBox(AltDepth-j,Rel(ONE),Pos(Rel(ONE),Not(Var(j)))),
                   altS));
      for (i=AltDepth-j+1;i<AltDepth;i++)
      altS=WithFml(NBox(i,Rel(ONE),Or(WithFml(Not(Var(j)),
                                              WithFml(Box(Rel(ONE),Var(j)),
                                                      EMPTY_SEQUENT)))),
	   WithFml(NBox(i,Rel(ONE),Or(WithFml(Var(j),
                                              WithFml(Box(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;
}