1 /*-----------------------------------------------------------------------
2
3 File : pcl_protocol.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Protocols (=trees) of PCL steps, all inclusive ;-)
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Sun Apr 2 01:49:33 GMT 2000
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "pcl_protocol.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32
33 /*---------------------------------------------------------------------*/
34 /* Forward Declarations */
35 /*---------------------------------------------------------------------*/
36
37
38 /*---------------------------------------------------------------------*/
39 /* Internal Functions */
40 /*---------------------------------------------------------------------*/
41
42
43
44 /*---------------------------------------------------------------------*/
45 /* Exported Functions */
46 /*---------------------------------------------------------------------*/
47
48 /*-----------------------------------------------------------------------
49 //
50 // Function: PCLProtAlloc()
51 //
52 // Return an initialized PCL protocol data structure.
53 //
54 // Global Variables: -
55 //
56 // Side Effects : Memory operations
57 //
58 /----------------------------------------------------------------------*/
59
PCLProtAlloc(void)60 PCLProt_p PCLProtAlloc(void)
61 {
62 PCLProt_p handle = PCLProtCellAlloc();
63 SortTable_p sort_table = DefaultSortTableAlloc();
64 Sig_p sig = SigAlloc(sort_table);
65
66 SigInsertInternalCodes(sig);
67 handle->terms = TBAlloc(sig);
68 handle->number = 0;
69 handle->steps = NULL;
70 handle->in_order = PStackAlloc();
71 handle->is_ordered = false;
72
73 return handle;
74 }
75
76
77 /*-----------------------------------------------------------------------
78 //
79 // Function: PCLProtFree()
80 //
81 // Free a PCL protocol
82 //
83 // Global Variables: -
84 //
85 // Side Effects : Memory operations
86 //
87 /----------------------------------------------------------------------*/
88
PCLProtFree(PCLProt_p junk)89 void PCLProtFree(PCLProt_p junk)
90 {
91 PStack_p stack;
92 PTree_p cell;
93 SortTable_p sort_table = junk->terms->sig->sort_table;
94
95 assert(junk && junk->terms);
96
97 stack = PTreeTraverseInit(junk->steps);
98 while((cell=PTreeTraverseNext(stack)))
99 {
100 PCLStepFree(cell->key);
101 }
102 PStackFree(stack);
103 PTreeFree(junk->steps);
104 SigFree(junk->terms->sig);
105 junk->terms->sig = NULL;
106 SortTableFree(sort_table);
107 TBFree(junk->terms);
108 PStackFree(junk->in_order);
109 PCLProtCellFree(junk);
110 }
111
112
113 /*-----------------------------------------------------------------------
114 //
115 // Function: PCLProtExtractStep()
116 //
117 // (Try to) take a step out of the protocol. Return true if it
118 // exists, false otherwise.
119 //
120 // Global Variables: -
121 //
122 // Side Effects : -
123 //
124 /----------------------------------------------------------------------*/
125
PCLProtExtractStep(PCLProt_p prot,PCLStep_p step)126 PCLStep_p PCLProtExtractStep(PCLProt_p prot, PCLStep_p step)
127 {
128 PCLStep_p res;
129
130 res = PTreeObjExtractObject(&(prot->steps), step,
131 PCLStepIdCompare);
132 if(res)
133 {
134 prot->number--;
135 prot->is_ordered = false;
136 }
137 return res;
138 }
139
140
141 /*-----------------------------------------------------------------------
142 //
143 // Function: PCLProtDeleteStep()
144 //
145 // Delete a step from a protocol. Return true if the step existed in
146 // the protocol, false otherwise. In the second case, the step is
147 // _not_ freed.
148 //
149 // Global Variables: -
150 //
151 // Side Effects : -
152 //
153 /----------------------------------------------------------------------*/
154
PCLProtDeleteStep(PCLProt_p prot,PCLStep_p step)155 bool PCLProtDeleteStep(PCLProt_p prot, PCLStep_p step)
156 {
157 PCLStep_p tree_step;
158
159 assert(prot&&step);
160
161 tree_step = PCLProtExtractStep(prot,step);
162 if(tree_step)
163 {
164 assert(step==tree_step);
165 PCLStepFree(tree_step);
166 return true;
167 }
168 return false;
169 }
170
171
172 /*-----------------------------------------------------------------------
173 //
174 // Function: PCLProtFindStep()
175 //
176 // Given a PCL-Identifier, find the matching step in prot.
177 //
178 // Global Variables: -
179 //
180 // Side Effects : May reorganize the tree.
181 //
182 /----------------------------------------------------------------------*/
183
PCLProtFindStep(PCLProt_p prot,PCLId_p id)184 PCLStep_p PCLProtFindStep(PCLProt_p prot, PCLId_p id)
185 {
186 PCLStepCell tmp;
187 PTree_p cell;
188
189 tmp.id = id;
190
191 cell = PTreeObjFind(&(prot->steps), &tmp, PCLStepIdCompare);
192 if(cell)
193 {
194 return cell->key;
195 }
196 return NULL;
197 }
198
199
200
201
202 /*-----------------------------------------------------------------------
203 //
204 // Function: PCLProtSerialize()
205 //
206 // Ensure that prot->in_order is up to date
207 //
208 // Global Variables:
209 //
210 // Side Effects :
211 //
212 /----------------------------------------------------------------------*/
213
PCLProtSerialize(PCLProt_p prot)214 void PCLProtSerialize(PCLProt_p prot)
215 {
216 if(!prot->is_ordered)
217 {
218 PStack_p stack;
219 PTree_p cell;
220 PCLStep_p step;
221
222 PStackReset(prot->in_order);
223 stack = PTreeTraverseInit(prot->steps);
224 while((cell=PTreeTraverseNext(stack)))
225 {
226 step = cell->key;
227 PStackPushP(prot->in_order, step);
228 }
229 PStackFree(stack);
230 prot->is_ordered = true;
231 }
232 }
233
234
235
236 /*-----------------------------------------------------------------------
237 //
238 // Function: PCLProtParse()
239 //
240 // Parse a PCL listing into prot. Return number of steps parsed.
241 //
242 // Global Variables: -
243 //
244 // Side Effects : Memory operations
245 //
246 /----------------------------------------------------------------------*/
247
PCLProtParse(Scanner_p in,PCLProt_p prot)248 long PCLProtParse(Scanner_p in, PCLProt_p prot)
249 {
250 long res = 0;
251 PCLStep_p step;
252 PTree_p cell;
253 DStr_p source_name, errpos;
254 long line, column;
255 StreamType type;
256
257 while(TestInpTok(in, PosInt))
258 {
259 if(!in->ignore_comments)
260 {
261 fprintf(GlobalOut, "%s", DStrView(AktToken(in)->comment));
262 DStrReset(AktToken(in)->comment);
263 }
264 line = AktToken(in)->line;
265 column = AktToken(in)->column;
266 source_name = DStrGetRef(AktToken(in)->source);
267 type = AktToken(in)->stream_type;
268
269 step = PCLStepParse(in, prot->terms);
270 cell = PCLProtInsertStep(prot, step);
271 if(cell)
272 {
273 errpos = DStrAlloc();
274
275 DStrAppendStr(errpos, PosRep(type, source_name, line, column));
276 DStrAppendStr(errpos, " duplicate PCL identifier");
277 Error(DStrView(errpos), SYNTAX_ERROR);
278 DStrFree(errpos);
279 }
280 DStrReleaseRef(source_name);
281 res++;
282 }
283 if(!in->ignore_comments)
284 {
285 fprintf(GlobalOut, "%s", DStrView(AktToken(in)->comment));
286 DStrReset(AktToken(in)->comment);
287 }
288 return res;
289 }
290
291
292 /*-----------------------------------------------------------------------
293 //
294 // Function: PCLProtPrintExtra()
295 //
296 // Print a PCL protocol.
297 //
298 // Global Variables: -
299 //
300 // Side Effects : Output, some memory operations
301 //
302 /----------------------------------------------------------------------*/
303
PCLProtPrintExtra(FILE * out,PCLProt_p prot,bool data,OutputFormatType format)304 void PCLProtPrintExtra(FILE* out, PCLProt_p prot, bool data,
305 OutputFormatType format)
306 {
307 PCLStep_p step;
308 PStackPointer i;
309
310 PCLProtSerialize(prot);
311
312 for(i=0; i<PStackGetSP(prot->in_order); i++)
313 {
314 step = PStackElementP(prot->in_order, i);
315 PCLStepPrintFormat(out, step, data, format);
316 fputc('\n',out);
317 }
318 }
319
320
321 /*-----------------------------------------------------------------------
322 //
323 // Function: PCLStepHasFOFParent()
324 //
325 // Return true if one of the parents of step is a FOF step, false
326 // otherwise.
327 //
328 // Global Variables: -
329 //
330 // Side Effects : Memory operations
331 //
332 /----------------------------------------------------------------------*/
333
PCLStepHasFOFParent(PCLProt_p prot,PCLStep_p step)334 bool PCLStepHasFOFParent(PCLProt_p prot, PCLStep_p step)
335 {
336 PTree_p parents = NULL, cell;
337 PCLStep_p parent;
338 PStack_p iter_stack;
339 bool res = false;
340
341 PCLStepCollectPreconds(prot, step, &parents);
342
343 iter_stack = PTreeTraverseInit(parents);
344 while((cell = PTreeTraverseNext(iter_stack)))
345 {
346 parent = cell->key;
347 if(PCLStepQueryProp(parent, PCLIsFOFStep))
348 {
349 res = true;
350 break;
351 }
352 }
353 PTreeTraverseExit(iter_stack);
354 PTreeFree(parents);
355 return res;
356 }
357
358
359 /*-----------------------------------------------------------------------
360 //
361 // Function: PCLProtStripFOF()
362 //
363 // Remove all FOF steps from protocol. Make steps referencing a FOF
364 // step into initials and rewrite the justification
365 // accordingly. Expensive if there are FOF steps, reasonably cheap
366 // otherwise...
367 //
368 // Global Variables: -
369 //
370 // Side Effects : Changes prot, memory operations.
371 //
372 /----------------------------------------------------------------------*/
373
PCLProtStripFOF(PCLProt_p prot)374 long PCLProtStripFOF(PCLProt_p prot)
375 {
376 PCLStep_p step;
377 PStackPointer i;
378 long res;
379 PStack_p fof_steps = PStackAlloc();
380
381 PCLProtCollectPropSteps(prot, PCLIsFOFStep, fof_steps);
382 res = PStackGetSP(fof_steps);
383
384 if(res)
385 {
386 PCLProtSerialize(prot); /* Should be serialized, but let's play
387 * it safe */
388 for(i=0; i<PStackGetSP(prot->in_order); i++)
389 {
390 step = PStackElementP(prot->in_order, i);
391 if(!PCLStepQueryProp(step,PCLIsFOFStep)
392 &&
393 PCLStepHasFOFParent(prot, step))
394 {
395 PCLExprFree(step->just);
396 step->just = PCLExprAlloc();
397 step->just->arg_no = 0;
398 step->just->op = PCLOpInitial;
399 }
400 }
401 }
402 while(!PStackEmpty(fof_steps))
403 {
404 bool check;
405
406 step = PStackPopP(fof_steps);
407 check = PCLProtDeleteStep(prot, step);
408 UNUSED(check); assert(check);
409 }
410 PStackFree(fof_steps);
411 return res;
412 }
413
414
415 /*-----------------------------------------------------------------------
416 //
417 // Function: PCLProtResetTreeData()
418 //
419 // Reset the tree data counters in all steps in the protocol.
420 //
421 // Global Variables: -
422 //
423 // Side Effects : As described
424 //
425 /----------------------------------------------------------------------*/
426
PCLProtResetTreeData(PCLProt_p prot,bool just_weights)427 void PCLProtResetTreeData(PCLProt_p prot, bool just_weights)
428 {
429 PCLStep_p step;
430 PStackPointer i;
431
432 PCLProtSerialize(prot);
433
434 for(i=0; i<PStackGetSP(prot->in_order); i++)
435 {
436 step = PStackElementP(prot->in_order, i);
437 PCLStepResetTreeData(step, just_weights);
438 }
439
440 }
441
442
443 /*-----------------------------------------------------------------------
444 //
445 // Function: PCLExprCollectPreconds()
446 //
447 // Collect all PCL steps referenced in expr into tree.
448 //
449 // Global Variables: -
450 //
451 // Side Effects : -
452 //
453 /----------------------------------------------------------------------*/
454
PCLExprCollectPreconds(PCLProt_p prot,PCLExpr_p expr,PTree_p * tree)455 void PCLExprCollectPreconds(PCLProt_p prot, PCLExpr_p expr, PTree_p *tree)
456 {
457 PCLStep_p step;
458 int i;
459
460 assert(prot && expr);
461
462 switch(expr->op)
463 {
464 case PCLOpNoOp:
465 assert(false);
466 break;
467 case PCLOpInitial:
468 break;
469 case PCLOpQuote:
470 step = PCLProtFindStep(prot,PCLExprArg(expr,0));
471 PTreeStore(tree, step);
472 break;
473 default:
474 for(i=0; i<expr->arg_no; i++)
475 {
476 PCLExprCollectPreconds(prot, PCLExprArg(expr,i), tree);
477 }
478 break;
479 }
480 }
481
482
483 /*-----------------------------------------------------------------------
484 //
485 // Function: PCLExprGetQuotedArg()
486 //
487 // If the designated arg is a quote expression, retrieve and return
488 // the quoted step. Otherwise return NULL.
489 //
490 // Global Variables: -
491 //
492 // Side Effects : -
493 //
494 /----------------------------------------------------------------------*/
495
PCLExprGetQuotedArg(PCLProt_p prot,PCLExpr_p expr,int arg)496 PCLStep_p PCLExprGetQuotedArg(PCLProt_p prot, PCLExpr_p expr, int arg)
497 {
498 PCLExpr_p argexpr;
499
500 assert(arg < expr->arg_no);
501
502 /* printf("pcl_expr_get_quoted_arg(%p, %p, %d)...\n", prot, expr,
503 arg); */
504 argexpr = PCLExprArg(expr,arg);
505 if(argexpr->op == PCLOpQuote)
506 {
507 return PCLProtFindStep(prot,PCLExprArg(argexpr,0));
508 }
509 return NULL;
510 }
511
512
513 /*-----------------------------------------------------------------------
514 //
515 // Function: PCLProtMarkProofClauses()
516 //
517 // Mark all proof steps in protocol with PCLIsProofStep. Return
518 // true if protocol describes a proof (i.e. contains the empty
519 // clause).
520 // otherwise.
521 //
522 // Global Variables: -
523 //
524 // Side Effects : -
525 //
526 /----------------------------------------------------------------------*/
527
PCLProtMarkProofClauses(PCLProt_p prot)528 bool PCLProtMarkProofClauses(PCLProt_p prot)
529 {
530 bool res = false;
531 PStack_p to_proc = PStackAlloc();
532 PTree_p root = NULL;
533 PCLStep_p step;
534 PStackPointer i;
535
536 PCLProtSerialize(prot);
537
538 for(i=0; i<PStackGetSP(prot->in_order); i++)
539 {
540 step = PStackElementP(prot->in_order, i);
541 if((PCLStepIsShell(step)
542 &&step->extra
543 &&(strcmp(step->extra, "'proof'")==0))
544 ||
545 (!PCLStepIsShell(step)&&
546 !PCLStepIsFOF(step)&&
547 ClauseIsEmpty(step->logic.clause)))
548 {
549 res = true;
550 }
551 if(PCLStepExtract(step->extra))
552 {
553 PStackPushP(to_proc, step);
554 }
555 }
556 while(!PStackEmpty(to_proc))
557 {
558 step = PStackPopP(to_proc);
559 if(!PCLStepQueryProp(step,PCLIsProofStep))
560 {
561 PCLStepSetProp(step,PCLIsProofStep);
562 PCLExprCollectPreconds(prot, step->just, &root);
563 while(root)
564 {
565 step = PTreeExtractRootKey(&root);
566 PStackPushP(to_proc, step);
567 }
568 }
569 }
570 PStackFree(to_proc);
571 return res;
572 }
573
574
575
576 /*-----------------------------------------------------------------------
577 //
578 // Function: PCLProtSetProp()
579 //
580 // Set props in all clauses in the protocol.
581 //
582 // Global Variables: -
583 //
584 // Side Effects : May sort the protocol.
585 //
586 /----------------------------------------------------------------------*/
587
PCLProtSetProp(PCLProt_p prot,PCLStepProperties props)588 void PCLProtSetProp(PCLProt_p prot, PCLStepProperties props)
589 {
590 PCLStep_p step;
591 PStackPointer i;
592
593 PCLProtSerialize(prot);
594
595 for(i=0; i<PStackGetSP(prot->in_order); i++)
596 {
597 step = PStackElementP(prot->in_order, i);
598 PCLStepSetProp(step,props);
599 }
600 }
601
602
603 /*-----------------------------------------------------------------------
604 //
605 // Function: PCLProtDelProp()
606 //
607 // Set props in all clauses in the protocol.
608 //
609 // Global Variables: -
610 //
611 // Side Effects : May sort the protocol.
612 //
613 /----------------------------------------------------------------------*/
614
PCLProtDelProp(PCLProt_p prot,PCLStepProperties props)615 void PCLProtDelProp(PCLProt_p prot, PCLStepProperties props)
616 {
617 PCLStep_p step;
618 PStackPointer i;
619
620 PCLProtSerialize(prot);
621
622 for(i=0; i<PStackGetSP(prot->in_order); i++)
623 {
624 step = PStackElementP(prot->in_order, i);
625 PCLStepDelProp(step,props);
626 }
627 }
628
629
630 /*-----------------------------------------------------------------------
631 //
632 // Function: PCLProtCountProp()
633 //
634 // Return the number of steps with all properties in props set.
635 //
636 // Global Variables: -
637 //
638 // Side Effects : May sort the protocol
639 //
640 /----------------------------------------------------------------------*/
641
PCLProtCountProp(PCLProt_p prot,PCLStepProperties props)642 long PCLProtCountProp(PCLProt_p prot, PCLStepProperties props)
643 {
644 PCLStep_p step;
645 PStackPointer i;
646 long res = 0;
647
648 PCLProtSerialize(prot);
649
650 for(i=0; i<PStackGetSP(prot->in_order); i++)
651 {
652 step = PStackElementP(prot->in_order, i);
653 if(PCLStepQueryProp(step,props))
654 {
655 res++;
656 }
657 }
658 return res;
659 }
660
661
662 /*-----------------------------------------------------------------------
663 //
664 // Function: PCLProtCollectPropSteps()
665 //
666 // Push all steps in prot with properties props set onto stack.
667 //
668 // Global Variables:
669 //
670 // Side Effects :
671 //
672 /----------------------------------------------------------------------*/
673
PCLProtCollectPropSteps(PCLProt_p prot,PCLStepProperties props,PStack_p steps)674 long PCLProtCollectPropSteps(PCLProt_p prot, PCLStepProperties props,
675 PStack_p steps)
676 {
677 PCLStep_p step;
678 PStackPointer i;
679
680 PCLProtSerialize(prot);
681
682 for(i=0; i<PStackGetSP(prot->in_order); i++)
683 {
684 step = PStackElementP(prot->in_order, i);
685 if(PCLStepQueryProp(step,props))
686 {
687 PStackPushP(steps, step);
688 }
689 }
690 return PStackGetSP(steps);
691 }
692
693 /*-----------------------------------------------------------------------
694 //
695 // Function: PCLProtPrintPropClauses()
696 //
697 // Print all steps with prop set.
698 //
699 // Global Variables: -
700 //
701 // Side Effects : Output, some memory operations
702 //
703 /----------------------------------------------------------------------*/
704
PCLProtPrintPropClauses(FILE * out,PCLProt_p prot,PCLStepProperties prop,OutputFormatType format)705 void PCLProtPrintPropClauses(FILE* out, PCLProt_p prot,
706 PCLStepProperties prop,
707 OutputFormatType format)
708 {
709 PCLStep_p step;
710 PStackPointer i;
711
712 PCLProtSerialize(prot);
713
714 for(i=0; i<PStackGetSP(prot->in_order); i++)
715 {
716 step = PStackElementP(prot->in_order, i);
717 if(PCLStepQueryProp(step,prop))
718 {
719 PCLStepPrintFormat(out, step, false, format);
720 fputc('\n',out);
721 }
722 }
723 }
724
725
726 /*-----------------------------------------------------------------------
727 //
728 // Function: PCLProtPrintExamples()
729 //
730 // Print all PCL steps that are marked as examples in example
731 // format.
732 //
733 // Global Variables: -
734 //
735 // Side Effects : Output
736 //
737 /----------------------------------------------------------------------*/
738
PCLProtPrintExamples(FILE * out,PCLProt_p prot)739 void PCLProtPrintExamples(FILE* out, PCLProt_p prot)
740 {
741 long proof_steps;
742 PCLStep_p step;
743 PStackPointer i;
744
745 proof_steps = PCLProtCountProp(prot, PCLIsProofStep);
746 /* The above also serializes the protocol! */
747 assert(prot->is_ordered);
748
749 for(i=0; i<PStackGetSP(prot->in_order); i++)
750 {
751 step = PStackElementP(prot->in_order, i);
752 if(PCLStepQueryProp(step,PCLIsExample))
753 {
754 PCLStepPrintExample(out, step, i, proof_steps, prot->number);
755 fputc('\n', out);
756 }
757 }
758 }
759
760
761 /*---------------------------------------------------------------------*/
762 /* End of File */
763 /*---------------------------------------------------------------------*/
764
765
766
767
768