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