1 /*-----------------------------------------------------------------------
2 
3 File  : ccl_proofstate.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Proof objects describing the state of a proof attempt (i.e. all
10   information relevant to the calculus, but not information describing
11   control).
12 
13   Copyright 1998-2016 by the author.
14   This code is released under the GNU General Public Licence and
15   the GNU Lesser General Public License.
16   See the file COPYING in the main E directory for details..
17   Run "eprover -h" for contact information.
18 
19 Changes
20 
21 <1> Sat Jul  5 02:28:25 MET DST 1997
22     New
23 <2> Wed Oct 14 22:46:13 MET DST 1998
24     Extracted from CONTROL/cco_proofstate.h
25 
26 -----------------------------------------------------------------------*/
27 
28 #ifndef CTO_PROOFSTATE
29 
30 #define CTO_PROOFSTATE
31 
32 #include <cio_output.h>
33 #include <ccl_def_handling.h>
34 #include <ccl_garbage_coll.h>
35 #include <ccl_global_indices.h>
36 
37 /*---------------------------------------------------------------------*/
38 /*                    Data type declarations                           */
39 /*---------------------------------------------------------------------*/
40 
41 /* Proof state */
42 
43 typedef struct proofstatecell
44 {
45    SortTable_p   sort_table;
46    Sig_p         signature;
47    long          original_symbols;
48    TB_p          terms;
49    TB_p          tmp_terms;
50    VarBank_p     freshvars;
51    GCAdmin_p     gc_terms;
52    FormulaSet_p  f_ax_archive;
53    FormulaSet_p  f_axioms;
54    ClauseSet_p   axioms;
55    ClauseSet_p   ax_archive;
56    ClauseSet_p   processed_pos_rules;
57    ClauseSet_p   processed_pos_eqns;
58    ClauseSet_p   processed_neg_units;
59    ClauseSet_p   processed_non_units;
60    ClauseSet_p   unprocessed;
61    ClauseSet_p   tmp_store;
62    ClauseSet_p   archive;
63    FormulaSet_p  f_archive;
64    PStack_p      extract_roots;
65    GlobalIndices gindices;
66    bool          fvi_initialized; /* Are the feature vector
67                                      indices set up? */
68    FVCollect_p   fvi_cspec;
69    ClauseSet_p   demods[3];       /* Synonyms for
70                                      processed_pos_rules and
71                                      processed_pos_eqns */
72    ClauseSet_p   watchlist;
73    GlobalIndices wlindices;
74    bool          state_is_complete;
75    bool          has_interpreted_symbols;
76    DefStore_p    definition_store;
77    FVCollect_p   def_store_cspec;
78 
79    bool          status_reported;
80    long          answer_count;
81 
82    unsigned long processed_count;
83    unsigned long proc_trivial_count;
84    unsigned long proc_forward_subsumed_count;
85    unsigned long proc_non_trivial_count;
86    unsigned long other_redundant_count; /* Intermediate
87                                            filtering */
88    unsigned long non_redundant_deleted;
89    unsigned long backward_subsumed_count;
90    unsigned long backward_rewritten_count;
91    unsigned long backward_rewritten_lit_count;
92    unsigned long generated_count;
93    unsigned long generated_lit_count;
94    unsigned long non_trivial_generated_count;
95    unsigned long context_sr_count;
96    unsigned long paramod_count;
97    unsigned long factor_count;
98    unsigned long resolv_count;
99 
100    /* The following are only set by ProofStateAnalyse() after
101       DerivationCompute() at the end of the proof search. */
102    unsigned long gc_count;
103    unsigned long gc_used_count;
104 }ProofStateCell, *ProofState_p;
105 
106 typedef enum
107 {
108    TSPrintPos = 1,
109    TSPrintNeg = 2,
110    TSAverageData = 4
111 }TrainingSelector;
112 
113 
114 
115 /*---------------------------------------------------------------------*/
116 /*                Exported Functions and Variables                     */
117 /*---------------------------------------------------------------------*/
118 
119 #define ProofStateCellAlloc() \
120    (ProofStateCell*)SizeMalloc(sizeof(ProofStateCell))
121 #define ProofStateCellFree(junk) \
122    SizeFree(junk, sizeof(ProofStateCell))
123 
124 ProofState_p ProofStateAlloc(FunctionProperties free_symb_prop);
125 void         ProofStateInitWatchlist(ProofState_p state,
126                                      OCB_p ocb,
127                                      char* watchlist_filename,
128                                      IOFormat parse_format);
129 void         ProofStateResetClauseSets(ProofState_p state, bool term_gc);
130 void         ProofStateFree(ProofState_p junk);
131 //void         ProofStateGCMarkTerms(ProofState_p state);
132 //long         ProofStateGCSweepTerms(ProofState_p state);
133 
134 #define      ProofStateStorage(state) \
135    (ClauseSetStorage((state)->unprocessed)+\
136     ClauseSetStorage((state)->processed_pos_rules)+\
137     ClauseSetStorage((state)->processed_pos_eqns)+\
138     ClauseSetStorage((state)->processed_neg_units)+\
139     ClauseSetStorage((state)->processed_non_units)+\
140     ClauseSetStorage((state)->archive)+\
141     TBStorage((state)->terms))
142 
143 
144 void ProofStateAnalyseGC(ProofState_p state);
145 void ProofStatePickTrainingExamples(ProofState_p state,
146                                     PStack_p pos_examples,
147                                     PStack_p neg_examples);
148 void ProofStateTrain(ProofState_p state, bool print_pos, bool print_neg);
149 void ProofStateStatisticsPrint(FILE* out, ProofState_p state);
150 void ProofStatePrint(FILE* out, ProofState_p state);
151 void ProofStatePropDocQuote(FILE* out, int level,
152                             FormulaProperties prop,
153                             ProofState_p state, char* comment);
154 
155 #define ProofStateAxNo(state) (ClauseSetCardinality((state)->axioms)+\
156                                FormulaSetCardinality((state)->f_axioms))
157 
158 #define WATCHLIST_INLINE_STRING "Use inline watchlist type"
159 #define WATCHLIST_INLINE_QSTRING "'" WATCHLIST_INLINE_STRING "'"
160 extern char* UseInlinedWatchList;
161 
162 
163 #endif
164 
165 /*---------------------------------------------------------------------*/
166 /*                        End of File                                  */
167 /*---------------------------------------------------------------------*/
168