1 /*-----------------------------------------------------------------------
2 
3 File  : pcl_protocol.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Lists of PCL steps
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> Sat Apr  1 22:17:54 GMT 2000
20     New
21 
22 -----------------------------------------------------------------------*/
23 
24 #ifndef PCL_PROTOCOL
25 
26 #define PCL_PROTOCOL
27 
28 #include <pcl_steps.h>
29 
30 /*---------------------------------------------------------------------*/
31 /*                    Data type declarations                           */
32 /*---------------------------------------------------------------------*/
33 
34 typedef struct pclprotcell
35 {
36    TB_p     terms;
37    long     number;
38    PTree_p  steps;      /* Ordered by PCL-Id's */
39    PStack_p in_order;   /* Steps in increasing order of ids. */
40    bool     is_ordered; /* True if previous is true ;-) */
41 }PCLProtCell, *PCLProt_p;
42 
43 
44 /*---------------------------------------------------------------------*/
45 /*                Exported Functions and Variables                     */
46 /*---------------------------------------------------------------------*/
47 
48 #define PCLProtCellAlloc() (PCLProtCell*)SizeMalloc(sizeof(PCLProtCell))
49 #define PCLProtCellFree(junk)         SizeFree(junk, sizeof(PCLProtCell))
50 
51 PCLProt_p PCLProtAlloc(void);
52 void      PCLProtFree(PCLProt_p junk);
53 
54 #define PCLProtInsertStep(prot, step) \
55         (((prot)->is_ordered = false),\
56          ((prot)->number++),\
57         (PTreeObjStore(&((prot)->steps), (step),\
58         (ComparisonFunctionType)PCLStepIdCompare)))
59 
60 PCLStep_p PCLProtExtractStep(PCLProt_p prot, PCLStep_p step);
61 bool      PCLProtDeleteStep(PCLProt_p prot, PCLStep_p step);
62 
63 #define   PCLProtStepNo(prot) ((prot->number))
64 PCLStep_p PCLProtFindStep(PCLProt_p prot, PCLId_p id);
65 
66 void      PCLProtSerialize(PCLProt_p prot);
67 
68 long      PCLProtParse(Scanner_p in, PCLProt_p prot);
69 void      PCLProtPrintExtra(FILE* out, PCLProt_p prot, bool data,
70              OutputFormatType format);
71 #define   PCLProtPrint(out, prot, format) PCLProtPrintExtra((out),\
72                          (prot),\
73                          false, \
74                          (format))
75 bool      PCLStepHasFOFParent(PCLProt_p prot, PCLStep_p step);
76 long      PCLProtStripFOF(PCLProt_p prot);
77 
78 void      PCLProtResetTreeData(PCLProt_p prot, bool just_weights);
79 
80 void      PCLExprCollectPreconds(PCLProt_p prot, PCLExpr_p expr,
81              PTree_p *tree);
82 #define   PCLStepCollectPreconds(prot, step, tree)\
83           PCLExprCollectPreconds((prot), (step)->just, (tree))
84 PCLStep_p PCLExprGetQuotedArg(PCLProt_p prot, PCLExpr_p expr, int arg);
85 
86 bool      PCLProtMarkProofClauses(PCLProt_p prot);
87 void      PCLProtSetProp(PCLProt_p prot, PCLStepProperties props);
88 void      PCLProtDelProp(PCLProt_p prot, PCLStepProperties props);
89 long      PCLProtCountProp(PCLProt_p prot, PCLStepProperties props);
90 long      PCLProtCollectPropSteps(PCLProt_p prot, PCLStepProperties props,
91                                   PStack_p steps);
92 void      PCLProtPrintPropClauses(FILE* out, PCLProt_p prot,
93               PCLStepProperties prop,
94               OutputFormatType format);
95 
96 #define PCLProtPrintProofClauses(out, prot, format)\
97         PCLProtPrintPropClauses((out), (prot), PCLIsProofStep, format)
98 void    PCLProtPrintExamples(FILE* out, PCLProt_p prot);
99 
100 
101 #endif
102 
103 /*---------------------------------------------------------------------*/
104 /*                        End of File                                  */
105 /*---------------------------------------------------------------------*/
106 
107 
108 
109 
110 
111