1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
/*-----------------------------------------------------------------------
File : pcl_miniprotocol.h
Author: Stephan Schulz
Contents
Lists of MiniPCL steps
Copyright 1998, 1999, 2002 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> Thu Jul 11 17:37:03 MEST 2002
New (from pcl_rotocol.h
-----------------------------------------------------------------------*/
#ifndef PCL_MINIPROTOCOL
#define PCL_MINIPROTOCOL
#include <pcl_ministeps.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct pclminiprotcell
{
TB_p terms;
long max_ident;
PDArray_p steps; /* indexed by simple-ids */
}PCLMiniProtCell, *PCLMiniProt_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define PCLMiniProtCellAlloc() (PCLMiniProtCell*)SizeMalloc(sizeof(PCLMiniProtCell))
#define PCLMiniProtCellFree(junk) SizeFree(junk, sizeof(PCLMiniProtCell))
PCLMiniProt_p PCLMiniProtAlloc(void);
void PCLMiniProtFree(PCLMiniProt_p junk);
bool PCLMiniProtInsertStep(PCLMiniProt_p prot, PCLMiniStep_p
step);
PCLMiniStep_p PCLMiniProtFindStep(PCLMiniProt_p prot, unsigned long id);
PCLMiniStep_p PCLMiniProtExtractStep(PCLMiniProt_p prot, PCLMiniStep_p
step);
bool PCLMiniProtDeleteStep(PCLMiniProt_p prot, PCLMiniStep_p
step);
long PCLMiniProtParse(Scanner_p in, PCLMiniProt_p prot);
void PCLMiniProtPrint(FILE* out, PCLMiniProt_p prot,
OutputFormatType format);
void PCLMiniExprCollectPreconds(PCLMiniProt_p prot, PCLExpr_p expr,
PTree_p *tree);
bool PCLMiniProtMarkProofClauses(PCLMiniProt_p prot, bool fast);
void PCLMiniProtSetClauseProp(PCLMiniProt_p prot, PCLStepProperties props);
void PCLMiniProtDelClauseProp(PCLMiniProt_p prot, PCLStepProperties props);
void PCLMiniProtPrintProofClauses(FILE* out, PCLMiniProt_p prot,
OutputFormatType format);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
