/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                 PROOF DOCUMENTATION                    * */
/* *                                                        * */
/* *  $Module:   DOCPROOF                                   * */ 
/* *                                                        * */
/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* *                                                        * */
/* $Revision$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

/**************************************************************/
/* Includes                                                   */
/**************************************************************/

#include "doc-proof.h"

/**************************************************************/
/* Global Variables                                           */
/**************************************************************/

int dp_DEPTH;


/**************************************************************/
/* Functions                                                  */
/**************************************************************/

void dp_Init(void)
{
  dp_DEPTH = 0;
}


static void dp_FPrintDFGProof(LIST Clauses, const char *FilePrefix,
			      FLAGSTORE Flags, PRECEDENCE Precedence)
/*********************************************************
  INPUT:   A list of clauses representing a proof, a
           string indicating a file name prefix, a flag
	   store and a precedence.
  RETURNS: void.
  EFFECT:  Outputs the proof in DFG proof format to
           <FilePrefix>.prf
**********************************************************/
{
  FILE   *Output;
  CLAUSE Clause;
  LIST   AxClauses,ConClauses,ProofClauses,Scan;
  char   *name;

  AxClauses = ConClauses = ProofClauses = list_Nil();
  
  name = memory_Malloc(sizeof(char)*(strlen(FilePrefix)+5));
  sprintf(name,"%s.prf", FilePrefix);

  Output = misc_OpenFile(name,"w");

  fputs("begin_problem(Unknown).\n\n", Output);

  fputs("list_of_descriptions.\n", Output);
  fputs("name({*", Output);
  fputs(FilePrefix, Output);
  fputs("*}).\n", Output);
  fputs("author({*SPASS ", Output);
  fputs(misc_VERSION, Output);
  fputs("*}).\n", Output);
  fputs("status(unsatisfiable).\n", Output);
  fputs("description({*File generated by SPASS containing a proof.*}).\n", Output);
  fputs("end_of_list.\n\n", Output);

  fputs("list_of_symbols.\n", Output);
  fol_FPrintDFGSignature(Output);
  fputs("end_of_list.\n\n", Output);

  for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
    Clause = (CLAUSE)list_Car(Scan);
    if (clause_IsFromInput(Clause)) {
      if (clause_GetFlag(Clause, CONCLAUSE))
	ConClauses = list_Cons(Clause, ConClauses);
      else
	AxClauses  = list_Cons(Clause, AxClauses);
    }
    else
      ProofClauses  = list_Cons(Clause, ProofClauses);
  }

  ConClauses   = list_NReverse(ConClauses);
  AxClauses    = list_NReverse(AxClauses);
  ProofClauses = list_NReverse(ProofClauses);
  
  clause_FPrintCnfDFG(Output, FALSE, AxClauses, ConClauses, Flags, Precedence);
  fputs("\nlist_of_proof(SPASS).\n", Output);
  for (Scan=ProofClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
    clause_FPrintDFGStep(Output,list_Car(Scan),TRUE);
  }
  fputs("end_of_list.\n\n", Output);

  fputs("end_problem.\n\n", Output);

  misc_CloseFile(Output, name);
  fputs("\nDFG Proof printed to: ", stdout);
  puts(name);

  list_Delete(ConClauses);
  list_Delete(AxClauses);
  list_Delete(ProofClauses);
  memory_Free(name, sizeof(char)*(strlen(FilePrefix)+5));
}

LIST dp_PrintProof(PROOFSEARCH Search, LIST Clauses, const char *FilePrefix)
/*********************************************************
  INPUT:   A proofsearch object, a list of empty clauses and
           the prefix of the output file name.
  RETURNS: The list of clauses required for the proof.
  MEMORY:  The returned list must be freed.
  EFFECT:  The proof is printed both to standard output and
           to the file <FilePrefix>.prf.
**********************************************************/
{
  LIST ProofClauses,Scan,EmptyClauses,AllClauses, ReducedProof;
  LIST Missing, Incomplete, SplitClauses;

  FLAGSTORE Flags;

  Flags = prfs_Store(Search);

  Missing = pcheck_ConvertParentsInSPASSProof(Search, Clauses);
  
  if (!list_Empty(Missing)) {
    puts("\nNOTE: clauses with following numbers have not been found:");
    for (; !list_Empty(Missing); Missing = list_Pop(Missing))
      printf("%d ", (int)list_Car(Missing)); 
    putchar('\n');
  }

  EmptyClauses = list_Copy(Clauses); 
  ProofClauses = list_Nil();
  AllClauses   = list_Nconc(list_Copy(prfs_DocProofClauses(Search)),
			    list_Nconc(list_Copy(prfs_UsableClauses(Search)),
				       list_Copy(prfs_WorkedOffClauses(Search))));

  /*
   *  collect proof clauses by noodling upward in the 
   *  proof tree, starting from <EmptyClauses>.
   *  Before, add all splitting clauses to avoid gaps in split tree 
   */

  SplitClauses = list_Nil();
  for (Scan = AllClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) 
    if (clause_IsFromSplitting(list_Car(Scan))) 
      SplitClauses = list_Cons(list_Car(Scan), SplitClauses);

  /* mark all needed clauses */
  pcheck_ClauseListRemoveFlag(EmptyClauses, MARKED);
  pcheck_ClauseListRemoveFlag(AllClauses, MARKED);
  pcheck_MarkRecursive(EmptyClauses);
  pcheck_MarkRecursive(SplitClauses);
  
  /* collect all marked clauses */
  ProofClauses = list_Nil();
  for (Scan = AllClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (clause_GetFlag(list_Car(Scan), MARKED))
      ProofClauses = list_Cons(list_Car(Scan), ProofClauses); 
  }

  /* build reduced proof  */
  ProofClauses = list_Nconc(ProofClauses, list_Copy(EmptyClauses));
  ProofClauses = pcheck_ClauseNumberMergeSort(ProofClauses);
  ReducedProof = pcheck_ReduceSPASSProof(ProofClauses); 

  dp_SetProofDepth(pcheck_SeqProofDepth(ReducedProof));
  
  pcheck_ParentPointersToParentNumbers(AllClauses);
  pcheck_ParentPointersToParentNumbers(Clauses);

  /* check reduced proof for clauses whose parents have been marked as
     incomplete (HIDDEN flag) by ConvertParentsInSPASSProof    */

  Incomplete = list_Nil();
  for (Scan = ReducedProof; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (clause_GetFlag(list_Car(Scan), HIDDEN))
      Incomplete = list_Cons(list_Car(Scan), Incomplete);
  }
  if (!list_Empty(Incomplete)) {
    puts("NOTE: Following clauses in reduced proof have incomplete parent sets:");
    for (Scan = Incomplete; !list_Empty(Scan); Scan = list_Cdr(Scan))
      printf("%d ", clause_Number(list_Car(Scan)));
    putchar('\n');
  }

  printf("\n\nHere is a proof with depth %d, length %d :\n",
	 dp_ProofDepth(), list_Length(ReducedProof));
  clause_ListPrint(ReducedProof);

  if (flag_GetFlagValue(Flags, flag_FPDFGPROOF))
    dp_FPrintDFGProof(ReducedProof, FilePrefix, Flags, prfs_Precedence(Search));

  fflush(stdout);

  list_Delete(EmptyClauses);
  list_Delete(AllClauses);
  list_Delete(ProofClauses);
  list_Delete(SplitClauses);
  list_Delete(Incomplete); 

  return ReducedProof;
}