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