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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
/*-----------------------------------------------------------------------
File : pcl_protocol.h
Author: Stephan Schulz
Contents
Lists of PCL steps
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> Sat Apr 1 22:17:54 GMT 2000
New
-----------------------------------------------------------------------*/
#ifndef PCL_PROTOCOL
#define PCL_PROTOCOL
#include <pcl_steps.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef struct pclprotcell
{
TB_p terms;
long number;
PTree_p steps; /* Ordered by PCL-Id's */
PStack_p in_order; /* Steps in increasing order of ids. */
bool is_ordered; /* True if previous is true ;-) */
}PCLProtCell, *PCLProt_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define PCLProtCellAlloc() (PCLProtCell*)SizeMalloc(sizeof(PCLProtCell))
#define PCLProtCellFree(junk) SizeFree(junk, sizeof(PCLProtCell))
PCLProt_p PCLProtAlloc(void);
void PCLProtFree(PCLProt_p junk);
#define PCLProtInsertStep(prot, step) \
(((prot)->is_ordered = false),\
((prot)->number++),\
(PTreeObjStore(&((prot)->steps), (step),\
(ComparisonFunctionType)PCLStepIdCompare)))
PCLStep_p PCLProtExtractStep(PCLProt_p prot, PCLStep_p step);
bool PCLProtDeleteStep(PCLProt_p prot, PCLStep_p step);
#define PCLProtStepNo(prot) ((prot->number))
PCLStep_p PCLProtFindStep(PCLProt_p prot, PCLId_p id);
void PCLProtSerialize(PCLProt_p prot);
long PCLProtParse(Scanner_p in, PCLProt_p prot);
void PCLProtPrintExtra(FILE* out, PCLProt_p prot, bool data,
OutputFormatType format);
#define PCLProtPrint(out, prot, format) PCLProtPrintExtra((out),\
(prot),\
false, \
(format))
bool PCLStepHasFOFParent(PCLProt_p prot, PCLStep_p step);
long PCLProtStripFOF(PCLProt_p prot);
void PCLProtResetTreeData(PCLProt_p prot, bool just_weights);
void PCLExprCollectPreconds(PCLProt_p prot, PCLExpr_p expr,
PTree_p *tree);
#define PCLStepCollectPreconds(prot, step, tree)\
PCLExprCollectPreconds((prot), (step)->just, (tree))
PCLStep_p PCLExprGetQuotedArg(PCLProt_p prot, PCLExpr_p expr, int arg);
bool PCLProtMarkProofClauses(PCLProt_p prot);
void PCLProtSetProp(PCLProt_p prot, PCLStepProperties props);
void PCLProtDelProp(PCLProt_p prot, PCLStepProperties props);
long PCLProtCountProp(PCLProt_p prot, PCLStepProperties props);
long PCLProtCollectPropSteps(PCLProt_p prot, PCLStepProperties props,
PStack_p steps);
void PCLProtPrintPropClauses(FILE* out, PCLProt_p prot,
PCLStepProperties prop,
OutputFormatType format);
#define PCLProtPrintProofClauses(out, prot, format)\
PCLProtPrintPropClauses((out), (prot), PCLIsProofStep, format)
void PCLProtPrintExamples(FILE* out, PCLProt_p prot);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
