/******* BENCHMARK GENERATION ******/

fml TwoBox(fml A)
{
  return Box(Rel(Random1To(TWO)),Box(Rel(Random1To(TWO)),A));
}

 
fml TwoPos(fml A)
{
  return Pos(Rel(Random1To(TWO)),Pos(Rel(Random1To(TWO)),A));
}


fml NTwoBox(integer n,fml A)
{
  integer i;

  for (i=0;i<n;i++)
    A=TwoBox(A);
  return A;
}
 

sequent GenerateModalFormulae(sequent QBFS)
{
  sequent modS,litS;

  modS=EMPTY_SEQUENT;

  for(; QBFS!=EMPTY_SEQUENT; QBFS=QBFS->rest)
    for(litS=QBFS->first->subfml; litS!=EMPTY_SEQUENT; litS=litS->rest)
      modS=WithFml(NTwoBox(AltDepth-LitName(litS->first)+1,CopyFml(QBFS->first)),
	     modS);

  return modS;
}


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

  altS=EMPTY_SEQUENT;
  
  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);
    }
  
  for (i=1;i<=AltDepth;i++) {
    A=Var(i);
    if (!FindTwinFml(A,varS,EqualFml))
      altS=WithFml(NTwoBox(AltDepth-i,TwoPos(True())),
	   altS);
    DeleteFml(A);
  }
  
  for (S=varS;S!=EMPTY_SEQUENT;S=S->rest) {
    var_name=S->first->name;
    if (Existential(var_name))
      altS=WithFml(NTwoBox(AltDepth-var_name,TwoPos(True())),
	   altS);
    else
      altS=WithFml(NTwoBox(AltDepth-var_name,TwoPos(Var(var_name))),
	   WithFml(NTwoBox(AltDepth-var_name,TwoPos(Not(Var(var_name)))),
	   altS));
    for (i=AltDepth-var_name+1;i<AltDepth;i++)
      altS=WithFml(NTwoBox(i,Or(WithFml(Not(Var(var_name)),
			      WithFml(TwoBox(Var(var_name)),
			      EMPTY_SEQUENT)))),
	   WithFml(NTwoBox(i,Or(WithFml(Var(var_name),
			      WithFml(TwoBox(Not(Var(var_name))),
			      EMPTY_SEQUENT)))),
	    altS));
  }

  DeleteSequent(varS);

  return altS;
}