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