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