1 /*-----------------------------------------------------------------------
2
3 File : pcl_steps.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Individual PCL steps and related stuff.
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> Thu Mar 30 19:04:05 MET DST 2000
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "pcl_steps.h"
25
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31
32 /* Support PCL without logical content - useful for analysing very
33 * very very large proofs, and faster for Isabelle proofs that don't
34 * need the intermediate results. This can only be set to true in
35 * tools that work only on the proof structure, not contents. */
36 bool SupportShellPCL = false;
37
38 /*---------------------------------------------------------------------*/
39 /* Forward Declarations */
40 /*---------------------------------------------------------------------*/
41
42
43 /*---------------------------------------------------------------------*/
44 /* Internal Functions */
45 /*---------------------------------------------------------------------*/
46
47 /*-----------------------------------------------------------------------
48 //
49 // Function: print_shell_pcl_warning()
50 //
51 // Print a warning that a shell PCL step was encountered where a
52 // normal one was expected.
53 //
54 // Global Variables: -
55 //
56 // Side Effects : Output
57 //
58 /----------------------------------------------------------------------*/
59
print_shell_pcl_warning(FILE * out,PCLStep_p step)60 static void print_shell_pcl_warning(FILE* out, PCLStep_p step)
61 {
62 if(PCLStepIsShell(step))
63 {
64 Warning("Shell PCL step encountered where "
65 "full PCL step was required");
66 fprintf(out, "# Step ");
67 PCLIdPrint(out, step->id);
68 fprintf(out, " omitted (Shell)\n");
69 }
70 }
71
72
73 /*---------------------------------------------------------------------*/
74 /* Exported Functions */
75 /*---------------------------------------------------------------------*/
76
77
78 /*-----------------------------------------------------------------------
79 //
80 // Function: PCLStepFree()
81 //
82 // Free a PCL step.
83 //
84 // Global Variables: -
85 //
86 // Side Effects : Memory operations
87 //
88 /----------------------------------------------------------------------*/
89
PCLStepFree(PCLStep_p junk)90 void PCLStepFree(PCLStep_p junk)
91 {
92 assert(junk && junk->id);
93
94 PCLIdFree(junk->id);
95 if(!PCLStepIsShell(junk))
96 {
97 if(PCLStepIsClausal(junk))
98 {
99 ClauseFree(junk->logic.clause);
100 }
101 else
102 {
103 /* tformula collected by garbage collector */
104 }
105 }
106 PCLExprFree(junk->just);
107 if(junk->extra)
108 {
109 FREE(junk->extra);
110 }
111 PCLStepCellFree(junk);
112 }
113
114 /*-----------------------------------------------------------------------
115 //
116 // Function: PCLParseExternalType()
117 //
118 // Parse a list of type annotations for PCL steps and return a
119 // property word that can be used with SetProp() to set all
120 // necessary properties (the type field and the lemma bit).
121 //
122 // Global Variables: -
123 //
124 // Side Effects : Reads input
125 //
126 /----------------------------------------------------------------------*/
127
PCLParseExternalType(Scanner_p in)128 PCLStepProperties PCLParseExternalType(Scanner_p in)
129 {
130 PCLStepProperties type = PCLTypeAxiom, extra = PCLNoProp;
131
132 while(!TestInpTok(in, Colon))
133 {
134 if(TestInpId(in, "conj"))
135 {
136 type = PCLTypeConjecture;
137 NextToken(in);
138 }
139 else if(TestInpId(in, "que"))
140 {
141 type = PCLTypeQuestion;
142 NextToken(in);
143 }
144 else if(TestInpId(in, "neg"))
145 {
146 type = PCLTypeNegConjecture;
147 NextToken(in);
148 }
149 else if(TestInpId(in, "lemma"))
150 {
151 extra = PCLIsLemma;
152 NextToken(in);
153 }
154 else
155 {
156 CheckInpId(in, "conj|neg|lemma");
157 }
158 if(!TestInpTok(in, Colon))
159 {
160 AcceptInpTok(in, Comma);
161 }
162 }
163 return type | extra;
164 }
165
166 /*-----------------------------------------------------------------------
167 //
168 // Function: PCLStepParse()
169 //
170 // Parse a PCL step.
171 //
172 // Global Variables: -
173 //
174 // Side Effects : Input, memory operations
175 //
176 /----------------------------------------------------------------------*/
177
PCLStepParse(Scanner_p in,TB_p bank)178 PCLStep_p PCLStepParse(Scanner_p in, TB_p bank)
179 {
180 PCLStep_p handle = PCLStepCellAlloc();
181
182 assert(in);
183 assert(bank);
184
185 handle->bank = bank;
186 PCLStepResetTreeData(handle, false);
187 handle->id = PCLIdParse(in);
188 AcceptInpTok(in, Colon);
189 handle->properties = PCLParseExternalType(in);
190 AcceptInpTok(in, Colon);
191 if(SupportShellPCL && TestInpTok(in, Colon))
192 {
193 handle->logic.clause = NULL;
194 PCLStepSetProp(handle, PCLIsShellStep);
195 }
196 else if(TestInpTok(in, OpenSquare))
197 {
198 handle->logic.clause = ClausePCLParse(in, bank);
199 PCLStepDelProp(handle, PCLIsFOFStep);
200 }
201 else
202 {
203 handle->logic.formula = TFormulaTPTPParse(in, bank);
204 PCLStepSetProp(handle, PCLIsFOFStep);
205 }
206 AcceptInpTok(in, Colon);
207 handle->just = PCLFullExprParse(in);
208 if(TestInpTok(in, Colon))
209 {
210 NextToken(in);
211 CheckInpTok(in, SQString|Name|PosInt);
212 handle->extra = DStrCopy(AktToken(in)->literal);
213 NextToken(in);
214 }
215 else
216 {
217 handle->extra = NULL;
218 }
219 PCLStepDelProp(handle, PCLIsProofStep);
220 if(handle->just->op == PCLOpInitial)
221 {
222 PCLStepSetProp(handle, PCLIsInitial);
223 }
224 return handle;
225 }
226
227 /*-----------------------------------------------------------------------
228 //
229 // Function: PCLPrintExternalType()
230 //
231 // Print the type(s) of a PCL step encoded in props.
232 //
233 // Global Variables: -
234 //
235 // Side Effects : Output
236 //
237 /----------------------------------------------------------------------*/
238
PCLPrintExternalType(FILE * out,PCLStepProperties props)239 void PCLPrintExternalType(FILE* out, PCLStepProperties props)
240 {
241 char *prepend="";
242
243 if(props&PCLIsLemma)
244 {
245 fputs("lemma", out);
246 prepend = ",";
247 }
248 props = props & PCLTypeMask;
249 switch(props)
250 {
251 case PCLTypeNegConjecture:
252 fputs(prepend, out);
253 fputs("neg", out);
254 break;
255 case PCLTypeConjecture:
256 fputs(prepend, out);
257 fputs("conj", out);
258 break;
259 case PCLTypeQuestion:
260 fputs(prepend, out);
261 fputs("que", out);
262 break;
263 default:
264 break;
265 }
266 }
267
268
269 /*-----------------------------------------------------------------------
270 //
271 // Function: PCLStepPrintExtra()
272 //
273 // Print a PCL step.
274 //
275 // Global Variables: -
276 //
277 // Side Effects : Output
278 //
279 /----------------------------------------------------------------------*/
280
PCLStepPrintExtra(FILE * out,PCLStep_p step,bool data)281 void PCLStepPrintExtra(FILE* out, PCLStep_p step, bool data)
282 {
283 assert(step);
284
285 PCLIdPrintFormatted(out, step->id, true);
286 fputs(" : ", out);
287 PCLPrintExternalType(out, step->properties);
288 fputs(" : ", out);
289 if(!PCLStepIsShell(step))
290 {
291 if(PCLStepIsFOF(step))
292 {
293 TFormulaTPTPPrint(out, step->bank, step->logic.formula, true, true);
294 }
295 else
296 {
297 ClausePCLPrint(out, step->logic.clause, true);
298 }
299 }
300 fputs(" : ", out);
301 PCLFullExprPrint(out, step->just);
302 if(step->extra)
303 {
304 fputs(" : ", out);
305 fprintf(out, "%s", step->extra);
306 }
307 else if(PCLStepQueryProp(step, PCLIsLemma))
308 {
309 fputs(" : 'lemma'", out);
310 }
311 #ifdef NEVER_DEFINED
312 fprintf(out, "/* %ld -> %f */", step->proof_tree_size, step->lemma_quality);
313 #endif
314 if(data)
315 {
316 #ifdef NEVER_DEFINED
317 fprintf(out, " /* %#8X %6ld %6ld %3ld %3ld %3ld %3ld %4.3f */",
318 step->properties,
319 step->proof_dag_size,
320 step->proof_tree_size,
321 step->active_pm_refs,
322 step->other_generating_refs,
323 step->active_simpl_refs,
324 step->passive_simpl_refs,
325 step->lemma_quality);
326 #endif
327 fprintf(out, " /* %3ld %3ld %3ld %3ld %3ld */",
328 step->contrib_simpl_refs,
329 step->contrib_gen_refs,
330 step->useless_simpl_refs,
331 step->useless_gen_refs,
332 step->proof_distance);
333 }
334 }
335
336
337 /*-----------------------------------------------------------------------
338 //
339 // Function: PCLPropToTSTPType()
340 //
341 // Given PCL properties, return the best string describing the
342 // type.
343 //
344 // Global Variables: -
345 //
346 // Side Effects : -
347 //
348 /----------------------------------------------------------------------*/
349
PCLPropToTSTPType(PCLStepProperties props)350 char * PCLPropToTSTPType(PCLStepProperties props)
351 {
352 switch(props & PCLTypeMask)
353 {
354 case PCLTypeConjecture:
355 return "conjecture";
356 case PCLTypeQuestion:
357 return "question";
358 case PCLTypeNegConjecture:
359 return "negated_conjecture";
360 default:
361 if(props&PCLIsLemma)
362 {
363 return "lemma";
364 }
365 else
366 {
367 if(props&PCLIsInitial)
368 {
369 return "axiom";
370 }
371 else
372 {
373 return "plain";
374 }
375 }
376 }
377 }
378
379
380 /*-----------------------------------------------------------------------
381 //
382 // Function: PCLStepPrintTSTP()
383 //
384 // Print a PCL step in TSTP format.
385 //
386 // Global Variables: -
387 //
388 // Side Effects : Output
389 //
390 /----------------------------------------------------------------------*/
391
PCLStepPrintTSTP(FILE * out,PCLStep_p step)392 void PCLStepPrintTSTP(FILE* out, PCLStep_p step)
393 {
394 assert(step);
395
396 if(PCLStepIsClausal(step))
397 {
398 fprintf(out, "cnf(");
399 PCLIdPrintTSTP(out, step->id);
400 fputc(',', out);
401 fputs(PCLPropToTSTPType(step->properties), out);
402 fputc(',', out);
403 if(PCLStepIsShell(step))
404 {
405 }
406 else
407 {
408 ClauseTSTPCorePrint(out, step->logic.clause, true);
409 }
410 }
411 else
412 {
413 fprintf(out, "fof(");
414 PCLIdPrintTSTP(out, step->id);
415 fputc(',', out);
416 fputs(PCLPropToTSTPType(step->properties), out);
417 fputc(',', out);
418 if(PCLStepIsShell(step))
419 {
420 }
421 else
422 {
423 TFormulaTPTPPrint(out, step->bank, step->logic.formula, true, true);
424 }
425
426 }
427 fputc(',', out);
428 PCLExprPrintTSTP(out, step->just, false);
429 if(step->extra)
430 {
431 fprintf(out, ",[%s]", step->extra);
432 }
433 /* else if(PCLStepQueryProp(step, PCLIsLemma))
434 {
435 fputs(",['lemma']", out);
436 }*/
437 fputs(").", out);
438 }
439
440
441 /*-----------------------------------------------------------------------
442 //
443 // Function: PCLStepPrintTPTP
444 //
445 // Print the logical part of a PCL step as a TPTP-2 clause or
446 // formula.
447 //
448 // Global Variables: -
449 //
450 // Side Effects : Output
451 //
452 /----------------------------------------------------------------------*/
453
PCLStepPrintTPTP(FILE * out,PCLStep_p step)454 void PCLStepPrintTPTP(FILE* out, PCLStep_p step)
455 {
456 assert(step);
457
458 if(PCLStepIsShell(step))
459 {
460 print_shell_pcl_warning(out, step);
461 }
462 else
463 {
464 if(PCLStepIsClausal(step))
465 {
466 ClausePrintTPTPFormat(out, step->logic.clause);
467 }
468 else
469 {
470 fprintf(out, "input_formula(");
471 PCLIdPrintTSTP(out, step->id);
472 fputc(',', out);
473 fputs(PCLPropToTSTPType(step->properties), out);
474 fputc(',', out);
475 TFormulaTPTPPrint(out, step->bank, step->logic.formula, true, true);
476 fputc(')',out);
477 }
478 }
479 }
480
481 /*-----------------------------------------------------------------------
482 //
483 // Function: PCLStepPrintLOP()
484 //
485 // Print the logical part of a PCL step as a LOP clause or formula
486 // (where TPTP core syntax has to stand in for missing LOP syntac).
487 //
488 // Global Variables: -
489 //
490 // Side Effects : Output
491 //
492 /----------------------------------------------------------------------*/
493
PCLStepPrintLOP(FILE * out,PCLStep_p step)494 void PCLStepPrintLOP(FILE* out, PCLStep_p step)
495 {
496 assert(step);
497
498 if(PCLStepIsShell(step))
499 {
500 print_shell_pcl_warning(out, step);
501 }
502 else
503 {
504 if(PCLStepIsClausal(step))
505 {
506 ClausePrintLOPFormat(out, step->logic.clause, true);
507 }
508 else
509 {
510 TFormulaTPTPPrint(out, step->bank, step->logic.formula, true, true);
511 }
512 }
513 }
514
515
516 /*-----------------------------------------------------------------------
517 //
518 // Function: PCLStepPrintFormat()
519 //
520 // Print a PCL step in the requested format.
521 //
522 // Global Variables: -
523 //
524 // Side Effects : Output
525 //
526 /----------------------------------------------------------------------*/
527
PCLStepPrintFormat(FILE * out,PCLStep_p step,bool data,OutputFormatType format)528 void PCLStepPrintFormat(FILE* out, PCLStep_p step, bool data,
529 OutputFormatType format)
530 {
531 switch(format)
532 {
533 case pcl_format:
534 PCLStepPrintExtra(out, step, data);
535 break;
536 case lop_format:
537 PCLStepPrintLOP(out, step);
538 break;
539 case tptp_format:
540 PCLStepPrintTPTP(out, step);
541 break;
542 case tstp_format:
543 PCLStepPrintTSTP(out, step);
544 break;
545 default:
546 assert(false);
547 break;
548 }
549 }
550
551
552 /*-----------------------------------------------------------------------
553 //
554 // Function: PCLStepPrintExampe()
555 //
556 // Print a PCL step in the correct format for an E example file for
557 // pattern-based learning. The format is as follows:
558 // id: (pd, su, sf, gu, gs, ss):clause
559 // where currently id is meaningless (a survivor from the old output
560 // format), pd is the proof distance, su, sf, gu, gs are the
561 // relative number of simplified or generated proof/nonproof
562 // clauses, and ss is 0 (it used to be a subsumption count in the
563 // old format, that information is no longer available in PCL).
564 //
565 // Global Variables: -
566 //
567 // Side Effects : Output
568 //
569 /----------------------------------------------------------------------*/
570
PCLStepPrintExample(FILE * out,PCLStep_p step,long id,long proof_steps,long total_steps)571 void PCLStepPrintExample(FILE* out, PCLStep_p step, long id,
572 long proof_steps, long total_steps)
573 {
574 assert(!PCLStepQueryProp(step,PCLIsFOFStep));
575
576 if(PCLStepIsShell(step))
577 {
578 print_shell_pcl_warning(out, step);
579 }
580 else
581 {
582 fprintf(out, "%4ld:(%ld, %f,%f,%f,%f):",
583 id,
584 step->proof_distance,
585 step->contrib_simpl_refs/(float)(proof_steps+1),
586 step->useless_simpl_refs/(float)(total_steps-proof_steps+1),
587 step->contrib_gen_refs/(float)(proof_steps+1),
588 step->useless_gen_refs/(float)(total_steps-proof_steps+1));
589 ClausePrint(out, step->logic.clause, true);
590 }
591 }
592
593
594 /*-----------------------------------------------------------------------
595 //
596 // Function: PCLStepIdCompare()
597 //
598 // Compare two PCL steps by idents (forPTreeObj-Operations).
599 //
600 // Global Variables: -
601 //
602 // Side Effects : -
603 //
604 /----------------------------------------------------------------------*/
605
PCLStepIdCompare(const void * s1,const void * s2)606 int PCLStepIdCompare(const void* s1, const void* s2)
607 {
608 const PCLStep_p step1 = (const PCLStep_p)s1;
609 const PCLStep_p step2 = (const PCLStep_p)s2;
610
611 return PCLIdCompare(step1->id, step2->id);
612 }
613
614
615 /*-----------------------------------------------------------------------
616 //
617 // Function: PCLStepResetTreeData()
618 //
619 // Reset all counters and size data elements in the step to 0.
620 //
621 // Global Variables: -
622 //
623 // Side Effects : -
624 //
625 /----------------------------------------------------------------------*/
626
PCLStepResetTreeData(PCLStep_p step,bool just_weights)627 void PCLStepResetTreeData(PCLStep_p step, bool just_weights)
628 {
629 step->proof_dag_size = PCLNoWeight;
630 step->proof_tree_size = PCLNoWeight;
631 if(!just_weights)
632 {
633 step->active_pm_refs = 0;
634 step->other_generating_refs = 0;
635 step->active_simpl_refs = 0;
636 step->passive_simpl_refs = 0;
637 step->pure_quote_refs = 0;
638 step->lemma_quality = 0.0;
639 step->contrib_simpl_refs = 0;
640 step->contrib_gen_refs = 0;
641 step->useless_simpl_refs = 0;
642 step->useless_gen_refs = 0;
643 step->proof_distance = PCL_PROOF_DIST_UNKNOWN;
644 PCLStepDelProp(step,PCLIsLemma|PCLIsMarked);
645 }
646 }
647
648 /*---------------------------------------------------------------------*/
649 /* End of File */
650 /*---------------------------------------------------------------------*/
651
652
653