1 /*-----------------------------------------------------------------------
2 
3 File  : pcl_steps.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   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> Thu Mar 30 17:52:53 MET DST 2000
20     New
21 
22 -----------------------------------------------------------------------*/
23 
24 #ifndef PCL_STEPS
25 
26 #define PCL_STEPS
27 
28 #include <pcl_expressions.h>
29 
30 /*---------------------------------------------------------------------*/
31 /*                    Data type declarations                           */
32 /*---------------------------------------------------------------------*/
33 
34 #define PCL_PROOF_DIST_INFINITY LONG_MAX /* It's magic */
35 #define PCL_PROOF_DIST_DEFAULT  10 /* Default for non-proofs */
36 #define PCL_PROOF_DIST_UNKNOWN  -1 /* Not yet computed */
37 
38 
39 typedef enum
40 {
41    PCLNoProp         =  0,
42    PCLIsLemma        =  1,
43    PCLIsInitial      =  2,
44    PCLIsFinal        =  4,
45    PCLIsMarked       =  8,
46    PCLIsProofStep    = 16,
47    PCLIsExample      = 32, /* Selected for learning */
48    PCLIsFOFStep      = 64, /* Otherwise its a clause */
49    PCLIsShellStep    = 128,
50    PCLType1          = CPType1, /* 256 */
51    PCLType2          = CPType2,
52    PCLType3          = CPType3,
53    PCLTypeMask       = CPTypeMask,
54    PCLTypeUnknown    = 0,                /* Also used as wildcard */
55    PCLTypeAxiom      = CPTypeAxiom,      /* Formula is Axiom */
56    PCLTypeHypothesis = CPTypeHypothesis, /* Formula is Hypothesis */
57    PCLTypeConjecture = CPTypeConjecture, /* Formula is Conjecture */
58    /* No Lemma type, in PLC that is independent of step type! */
59    PCLTypeNegConjecture = CPTypeNegConjecture, /* Formula is NegConjecture */
60    PCLTypeQuestion      = CPTypeQuestion, /* It's a question */
61 
62 }PCLStepProperties;
63 
64 
65 typedef struct pclstepcell
66 {
67    TB_p              bank;
68    PCLId_p           id;
69    union
70    {
71       Clause_p          clause;
72       TFormula_p        formula;
73    }logic;
74    PCLExpr_p         just;
75    char*             extra;
76    PCLStepProperties properties;
77    /* The following data is collected for lemma evaluation */
78    long              proof_dag_size;
79    long              proof_tree_size;
80    long              active_pm_refs;
81    long              other_generating_refs;
82    long              active_simpl_refs;
83    long              passive_simpl_refs;
84    long              pure_quote_refs;
85    float             lemma_quality;
86    /* The following data is collected for pattern-based learning */
87    long              contrib_simpl_refs; /* Simplification of proof
88                                           * clauses -- counts active
89                                           * use only! */
90    long              contrib_gen_refs;   /* Generation of proof clauses */
91    long              useless_simpl_refs; /* Simplification of
92                                           * superfluous c.-- counts
93                                           * active use only! */
94    long              useless_gen_refs;   /* Generation of superfluous c. */
95    long              proof_distance;
96 }PCLStepCell, *PCLStep_p;
97 
98 #define PCLNoWeight -1
99 
100 
101 /*---------------------------------------------------------------------*/
102 /*                Exported Functions and Variables                     */
103 /*---------------------------------------------------------------------*/
104 
105 extern bool SupportShellPCL;
106 
107 #define PCLStepCellAlloc() (PCLStepCell*)SizeMalloc(sizeof(PCLStepCell))
108 #define PCLStepCellFree(junk)         SizeFree(junk, sizeof(PCLStepCell))
109 
110 #define PCLStepSetProp(clause, prop) SetProp((clause), (prop))
111 #define PCLStepDelProp(clause, prop) DelProp((clause), (prop))
112 #define PCLStepGiveProps(clause, prop) GiveProps((clause), (prop))
113 #define PCLStepQueryProp(clause, prop) QueryProp((clause), (prop))
114 #define PCLStepIsAnyPropSet(clause, prop) IsAnyPropSet((clause), (prop))
115 
116 #define PCLStepIsFOF(step) PCLStepQueryProp((step), PCLIsFOFStep)
117 #define PCLStepIsShell(step) PCLStepQueryProp((step), PCLIsShellStep)
118 #define PCLStepIsClausal(step) (!PCLStepIsFOF(step))
119 
120 void      PCLStepFree(PCLStep_p junk);
121 
122 PCLStepProperties PCLParseExternalType(Scanner_p in);
123 PCLStep_p PCLStepParse(Scanner_p in, TB_p bank);
124 void      PCLPrintExternalType(FILE* out, PCLStepProperties props);
125 void      PCLStepPrintExtra(FILE* out, PCLStep_p step, bool data);
126 #define   PCLStepPrint(out, step) PCLStepPrintExtra((out),(step),false)
127 char *    PCLPropToTSTPType(PCLStepProperties props);
128 void      PCLStepPrintTSTP(FILE* out, PCLStep_p step);
129 void      PCLStepPrintTPTP(FILE* out, PCLStep_p step);
130 void      PCLStepPrintLOP(FILE* out, PCLStep_p step);
131 void      PCLStepPrintFormat(FILE* out, PCLStep_p step, bool data,
132               OutputFormatType format);
133 void      PCLStepPrintExample(FILE* out, PCLStep_p step, long id,
134                               long proof_steps, long total_steps);
135 int       PCLStepIdCompare(const void* s1, const void* s2);
136 void      PCLStepResetTreeData(PCLStep_p step, bool just_weights);
137 
138 #endif
139 
140 /*---------------------------------------------------------------------*/
141 /*                        End of File                                  */
142 /*---------------------------------------------------------------------*/
143 
144 
145 
146 
147 
148