/*----------------------------------------------------------------------- File : pcl_protocol.c Author: Stephan Schulz Contents Protocols (=trees) of PCL steps, all inclusive ;-) Copyright 1998, 1999 by the author. This code is released under the GNU General Public Licence and the GNU Lesser General Public License. See the file COPYING in the main E directory for details.. Run "eprover -h" for contact information. Changes <1> Sun Apr 2 01:49:33 GMT 2000 New -----------------------------------------------------------------------*/ #include "pcl_protocol.h" /*---------------------------------------------------------------------*/ /* Global Variables */ /*---------------------------------------------------------------------*/ /*---------------------------------------------------------------------*/ /* Forward Declarations */ /*---------------------------------------------------------------------*/ /*---------------------------------------------------------------------*/ /* Internal Functions */ /*---------------------------------------------------------------------*/ /*---------------------------------------------------------------------*/ /* Exported Functions */ /*---------------------------------------------------------------------*/ /*----------------------------------------------------------------------- // // Function: PCLProtAlloc() // // Return an initialized PCL protocol data structure. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ PCLProt_p PCLProtAlloc(void) { PCLProt_p handle = PCLProtCellAlloc(); Sig_p sig = SigAlloc(); SigInsertInternalCodes(sig); handle->terms = TBAlloc(sig); handle->number = 0; handle->steps = NULL; handle->in_order = PStackAlloc(); handle->is_ordered = false; return handle; } /*----------------------------------------------------------------------- // // Function: PCLProtFree() // // Free a PCL protocol // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ void PCLProtFree(PCLProt_p junk) { PStack_p stack; PTree_p cell; assert(junk && junk->terms); stack = PTreeTraverseInit(junk->steps); while((cell=PTreeTraverseNext(stack))) { PCLStepFree(cell->key); } PStackFree(stack); PTreeFree(junk->steps); SigFree(junk->terms->sig); junk->terms->sig = NULL; TBFree(junk->terms); PStackFree(junk->in_order); PCLProtCellFree(junk); } /*----------------------------------------------------------------------- // // Function: PCLProtExtractStep() // // (Try to) take a step out of the protocol. Return true if it // exists, false otherwise. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ PCLStep_p PCLProtExtractStep(PCLProt_p prot, PCLStep_p step) { PCLStep_p res; res = PTreeObjExtractObject(&(prot->steps), step, PCLStepIdCompare); if(res) { prot->number--; prot->is_ordered = false; } return res; } /*----------------------------------------------------------------------- // // Function: PCLProtDeleteStep() // // Delete a step from a protocol. Return true if the step existed in // the protocol, false otherwise. In the second case, the step is // _not_ freed. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ bool PCLProtDeleteStep(PCLProt_p prot, PCLStep_p step) { PCLStep_p tree_step; assert(prot&&step); tree_step = PCLProtExtractStep(prot,step); if(tree_step) { assert(step==tree_step); PCLStepFree(tree_step); return true; } return false; } /*----------------------------------------------------------------------- // // Function: PCLProtFindStep() // // Given a PCL-Identifier, find the matching step in prot. // // Global Variables: - // // Side Effects : May reorganize the tree. // /----------------------------------------------------------------------*/ PCLStep_p PCLProtFindStep(PCLProt_p prot, PCLId_p id) { PCLStepCell tmp; PTree_p cell; tmp.id = id; cell = PTreeObjFind(&(prot->steps), &tmp, PCLStepIdCompare); if(cell) { return cell->key; } return NULL; } /*----------------------------------------------------------------------- // // Function: PCLProtSerialize() // // Ensure that prot->in_order is up to date // // Global Variables: // // Side Effects : // /----------------------------------------------------------------------*/ void PCLProtSerialize(PCLProt_p prot) { if(!prot->is_ordered) { PStack_p stack; PTree_p cell; PCLStep_p step; PStackReset(prot->in_order); stack = PTreeTraverseInit(prot->steps); while((cell=PTreeTraverseNext(stack))) { step = cell->key; PStackPushP(prot->in_order, step); } PStackFree(stack); prot->is_ordered = true; } } /*----------------------------------------------------------------------- // // Function: PCLProtParse() // // Parse a PCL listing into prot. Return number of steps parsed. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ long PCLProtParse(Scanner_p in, PCLProt_p prot) { long res = 0; PCLStep_p step; PTree_p cell; DStr_p source_name, errpos; long line, column; StreamType type; while(TestInpTok(in, PosInt)) { if(!in->ignore_comments) { fprintf(GlobalOut, "%s", DStrView(AktToken(in)->comment)); DStrReset(AktToken(in)->comment); } line = AktToken(in)->line; column = AktToken(in)->column; source_name = DStrGetRef(AktToken(in)->source); type = AktToken(in)->stream_type; step = PCLStepParse(in, prot->terms); cell = PCLProtInsertStep(prot, step); if(cell) { errpos = DStrAlloc(); DStrAppendStr(errpos, PosRep(type, source_name, line, column)); DStrAppendStr(errpos, " duplicate PCL identifier"); Error(DStrView(errpos), SYNTAX_ERROR); DStrFree(errpos); } DStrReleaseRef(source_name); res++; } if(!in->ignore_comments) { fprintf(GlobalOut, "%s", DStrView(AktToken(in)->comment)); DStrReset(AktToken(in)->comment); } return res; } /*----------------------------------------------------------------------- // // Function: PCLProtPrintExtra() // // Print a PCL protocol. // // Global Variables: - // // Side Effects : Output, some memory operations // /----------------------------------------------------------------------*/ void PCLProtPrintExtra(FILE* out, PCLProt_p prot, bool data, OutputFormatType format) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); PCLStepPrintFormat(out, step, data, format); fputc('\n',out); } } /*----------------------------------------------------------------------- // // Function: PCLStepHasFOFParent() // // Return true if one of the parents of step is a FOF step, false // otherwise. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ bool PCLStepHasFOFParent(PCLProt_p prot, PCLStep_p step) { PTree_p parents = NULL, cell; PCLStep_p parent; PStack_p iter_stack; bool res = false; PCLStepCollectPreconds(prot, step, &parents); iter_stack = PTreeTraverseInit(parents); while((cell = PTreeTraverseNext(iter_stack))) { parent = cell->key; if(PCLStepQueryProp(parent, PCLIsFOFStep)) { res = true; break; } } PTreeTraverseExit(iter_stack); PTreeFree(parents); return res; } /*----------------------------------------------------------------------- // // Function: PCLProtStripFOF() // // Remove all FOF steps from protocol. Make steps referencing a FOF // step into initials and rewrite the justification // accordingly. Expensive if there are FOF steps, reasonably cheap // otherwise... // // Global Variables: - // // Side Effects : Changes prot, memory operations. // /----------------------------------------------------------------------*/ long PCLProtStripFOF(PCLProt_p prot) { PCLStep_p step; PStackPointer i; long res; PStack_p fof_steps = PStackAlloc(); PCLProtCollectPropSteps(prot, PCLIsFOFStep, fof_steps); res = PStackGetSP(fof_steps); if(res) { PCLProtSerialize(prot); /* Should be serialized, but let's play * it safe */ for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(!PCLStepQueryProp(step,PCLIsFOFStep) && PCLStepHasFOFParent(prot, step)) { PCLExprFree(step->just); step->just = PCLExprAlloc(); step->just->arg_no = 0; step->just->op = PCLOpInitial; } } } while(!PStackEmpty(fof_steps)) { bool check; step = PStackPopP(fof_steps); check = PCLProtDeleteStep(prot, step); assert(check); } PStackFree(fof_steps); return res; } /*----------------------------------------------------------------------- // // Function: PCLProtResetTreeData() // // Reset the tree data counters in all steps in the protocol. // // Global Variables: - // // Side Effects : As described // /----------------------------------------------------------------------*/ void PCLProtResetTreeData(PCLProt_p prot, bool just_weights) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); PCLStepResetTreeData(step, just_weights); } } /*----------------------------------------------------------------------- // // Function: PCLExprCollectPreconds() // // Collect all PCL steps referenced in expr into tree. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ void PCLExprCollectPreconds(PCLProt_p prot, PCLExpr_p expr, PTree_p *tree) { PCLStep_p step; int i; assert(prot && expr); switch(expr->op) { case PCLOpNoOp: assert(false); break; case PCLOpInitial: break; case PCLOpQuote: step = PCLProtFindStep(prot,PCLExprArg(expr,0)); PTreeStore(tree, step); break; default: for(i=0; iarg_no; i++) { PCLExprCollectPreconds(prot, PCLExprArg(expr,i), tree); } break; } } /*----------------------------------------------------------------------- // // Function: PCLExprGetQuotedArg() // // If the designated arg is a quote expression, retrieve and return // the quoted step. Otherwise return NULL. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ PCLStep_p PCLExprGetQuotedArg(PCLProt_p prot, PCLExpr_p expr, int arg) { PCLExpr_p argexpr; assert(arg < expr->arg_no); /* printf("pcl_expr_get_quoted_arg(%p, %p, %d)...\n", prot, expr, arg); */ argexpr = PCLExprArg(expr,arg); if(argexpr->op == PCLOpQuote) { return PCLProtFindStep(prot,PCLExprArg(argexpr,0)); } return NULL; } /*----------------------------------------------------------------------- // // Function: PCLProtMarkProofClauses() // // Mark all proof steps in protocol with CPIsProofClause. Return // true if protocol describes a proof (i.e. contains the empty // clause). // otherwise. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ bool PCLProtMarkProofClauses(PCLProt_p prot) { bool res = false; PStack_p to_proc = PStackAlloc(); PTree_p root = NULL; PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(!PCLStepQueryProp(step, PCLIsFOFStep)&& ClauseIsEmpty(step->logic.clause)) { res = true; } if(PCLStepExtract(step->extra)) { PStackPushP(to_proc, step); } } while(!PStackEmpty(to_proc)) { step = PStackPopP(to_proc); if(!PCLStepQueryProp(step,PCLIsProofStep)) { PCLStepSetProp(step,PCLIsProofStep); PCLExprCollectPreconds(prot, step->just, &root); while(root) { step = PTreeExtractRootKey(&root); PStackPushP(to_proc, step); } } } PStackFree(to_proc); return res; } /*----------------------------------------------------------------------- // // Function: PCLProtSetProp() // // Set props in all clauses in the protocol. // // Global Variables: - // // Side Effects : May sort the protocol. // /----------------------------------------------------------------------*/ void PCLProtSetProp(PCLProt_p prot, PCLStepProperties props) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); PCLStepSetProp(step,props); } } /*----------------------------------------------------------------------- // // Function: PCLProtDelProp() // // Set props in all clauses in the protocol. // // Global Variables: - // // Side Effects : May sort the protocol. // /----------------------------------------------------------------------*/ void PCLProtDelProp(PCLProt_p prot, PCLStepProperties props) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); PCLStepDelProp(step,props); } } /*----------------------------------------------------------------------- // // Function: PCLProtCountProp() // // Return the number of steps with all properties in props set. // // Global Variables: - // // Side Effects : May sort the protocol // /----------------------------------------------------------------------*/ long PCLProtCountProp(PCLProt_p prot, PCLStepProperties props) { PCLStep_p step; PStackPointer i; long res = 0; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(PCLStepQueryProp(step,props)) { res++; } } return res; } /*----------------------------------------------------------------------- // // Function: PCLProtCollectPropSteps() // // Push all steps in prot with properties props set onto stack. // // Global Variables: // // Side Effects : // /----------------------------------------------------------------------*/ long PCLProtCollectPropSteps(PCLProt_p prot, PCLStepProperties props, PStack_p steps) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(PCLStepQueryProp(step,props)) { PStackPushP(steps, step); } } return PStackGetSP(steps); } /*----------------------------------------------------------------------- // // Function: PCLProtPrintPropClauses() // // Print all steps with prop set. // // Global Variables: - // // Side Effects : Output, some memory operations // /----------------------------------------------------------------------*/ void PCLProtPrintPropClauses(FILE* out, PCLProt_p prot, PCLStepProperties prop, OutputFormatType format) { PCLStep_p step; PStackPointer i; PCLProtSerialize(prot); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(PCLStepQueryProp(step,prop)) { PCLStepPrintFormat(out, step, false, format); fputc('\n',out); } } } /*----------------------------------------------------------------------- // // Function: PCLProtPrintExamples() // // Print all PCL steps that are marked as examples in example // format. // // Global Variables: - // // Side Effects : Output // /----------------------------------------------------------------------*/ void PCLProtPrintExamples(FILE* out, PCLProt_p prot) { long proof_steps; PCLStep_p step; PStackPointer i; proof_steps = PCLProtCountProp(prot, PCLIsProofStep); /* The above also serializes the protocol! */ assert(prot->is_ordered); for(i=0; iin_order); i++) { step = PStackElementP(prot->in_order, i); if(PCLStepQueryProp(step,PCLIsExample)) { PCLStepPrintExample(out, step, i, proof_steps, prot->number); fputc('\n', out); } } } /*---------------------------------------------------------------------*/ /* End of File */ /*---------------------------------------------------------------------*/