1 /*----------------------------------------------------------------------- 2 3 File : cte_termbanks.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Definitions for term banks - i.e. shared representations of terms as 10 defined in cte_terms.h. Uses the same struct, but adds 11 administrative stuff and functionality for sharing. 12 13 There are two sets of funktions for the manangment of term trees: 14 Funktions operating only on the top cell, and functions descending 15 the term structure. Top level functions implement a conventional splay 16 tree with key f_code.masked_properties.entry_nos_of_args and are 17 implemented in cte_termtrees.[ch] 18 19 Copyright 1998-2011 by the author. 20 This code is released under the GNU General Public Licence and 21 the GNU Lesser General Public License. 22 See the file COPYING in the main E directory for details.. 23 Run "eprover -h" for contact information. 24 25 Changes 26 27 <1> Mon Sep 22 00:15:39 MET DST 1997 28 New 29 <2> Wed Feb 25 18:16:34 MET 1998 30 Adapted for use of new term modules with shared variables 31 <3> Sat Apr 6 21:42:35 CEST 2002 32 Changed for new rewriting 33 34 -----------------------------------------------------------------------*/ 35 36 #ifndef CTE_TERMBANKS 37 38 #define CTE_TERMBANKS 39 40 #include <clb_numtrees.h> 41 #include <cio_basicparser.h> 42 #include <cte_varsets.h> 43 #include <cte_termcellstore.h> 44 45 /*---------------------------------------------------------------------*/ 46 /* Data type declarations */ 47 /*---------------------------------------------------------------------*/ 48 49 typedef struct tbcell 50 { 51 unsigned long in_count; /* How many terms have been inserted? */ 52 unsigned long long insertions;/* How many termtops have been 53 inserted into the term bank? This 54 counts all attempted insertions 55 (as a measure of work done. */ 56 Sig_p sig; /* Store sig info */ 57 VarBank_p vars; /* Information about (shared) variables */ 58 Term_p true_term; /* Pointer to the special term with the 59 $true constant. */ 60 Term_p false_term; /* Pointer to the special term with the 61 $false constant. */ 62 Term_p min_term; /* A small (ideally the minimal 63 possible) term, to be used for RHS 64 instantiation. */ 65 unsigned long rewrite_steps; /* How many calls to TBTermReplace? */ 66 VarSetStore_p freevarsets; /* Associates a term (or Tformula) 67 * with the set of its free 68 * variables. Only initalized for 69 * specific operations and then reset 70 * again */ 71 TermProperties garbage_state; /* For the mark-and sweep garbage 72 collection. This is flipped at 73 each sweep, and all new term cell 74 get the new value, so that marking 75 can be done by flipping in the 76 term cell. */ 77 struct gc_admin_cell *gc; /* Higher level code can register 78 * garbage collection information 79 * here. This is only a convenience 80 * link, memory needs to be managed 81 * elsewhere. */ 82 PDArray_p ext_index; /* Associate _external_ abbreviations (= 83 entry_no's with term nodes, necessary 84 for parsing of term bank terms. For 85 critical cases (full protocolls) this 86 is bound to be densly poulated -> we 87 use an array. Please note that term 88 replacing does not invalidate entries 89 in ext_index 90 (it would be pretty expensive in 91 terms of time and memory), so higher 92 layers have to take care of this if 93 they want to both access terms via 94 references and do replacing! */ 95 TermCellStoreCell term_store; /* Here are the terms */ 96 }TBCell, *TB_p; 97 98 99 100 /*---------------------------------------------------------------------*/ 101 /* Exported Functions and Variables */ 102 /*---------------------------------------------------------------------*/ 103 104 extern bool TBPrintTermsFlat; 105 extern bool TBPrintInternalInfo; 106 extern bool TBPrintDetails; 107 108 #define TBCellAlloc() (TBCell*)SizeMalloc(sizeof(TBCell)) 109 #define TBCellFree(junk) SizeFree(junk, sizeof(TBCell)) 110 111 #define TBSortTable(tb) (tb->vars->sort_table) 112 113 TB_p TBAlloc(Sig_p sig); 114 void TBFree(TB_p junk); 115 116 void TBVarSetStoreFree(TB_p bank); 117 118 long TBTermNodes(TB_p bank); 119 #define TBNonVarTermNodes(bank) TermCellStoreNodes(&(bank)->term_store) 120 #define TBStorage(bank)\ 121 (TERMCELL_DYN_MEM*(bank)->term_store.entries\ 122 +(bank)->term_store.arg_count*TERMP_MEM) 123 124 #define TBCellIdent(term) (TermIsVar(term)?(term)->f_code:term->entry_no) 125 126 #define TermIsTrueTerm(term) ((term)->f_code==SIG_TRUE_CODE) 127 128 #define TBTermIsSubterm(super, term) TermIsSubterm((super),(term),DEREF_NEVER) 129 130 #define TBTermIsTypeTerm(term)\ 131 ((term)->weight==(DEFAULT_VWEIGHT+DEFAULT_FWEIGHT)) 132 #define TBTermIsXTypeTerm(term)\ 133 (term->arity && ((term)->weight==(DEFAULT_FWEIGHT+(term)->arity*DEFAULT_VWEIGHT))) 134 #define TBTermIsGround(t) TermCellQueryProp((t), TPIsGround) 135 136 Term_p TBInsert(TB_p bank, Term_p term, DerefType deref); 137 Term_p TBInsertNoProps(TB_p bank, Term_p term, DerefType deref); 138 Term_p TBInsertRepl(TB_p bank, Term_p term, DerefType deref, Term_p old, Term_p repl); 139 Term_p TBInsertInstantiated(TB_p bank, Term_p term); 140 141 Term_p TBInsertOpt(TB_p bank, Term_p term, DerefType deref); 142 Term_p TBInsertDisjoint(TB_p bank, Term_p term); 143 144 Term_p TBTermTopInsert(TB_p bank, Term_p t); 145 146 Term_p TBAllocNewSkolem(TB_p bank, PStack_p variables, SortType sort); 147 148 Term_p TBFind(TB_p bank, Term_p term); 149 150 void TBPrintBankInOrder(FILE* out, TB_p bank); 151 void TBPrintTermCompact(FILE* out, TB_p bank, Term_p term); 152 #define TBPrintTermFull(out, bank, term) \ 153 TermPrint((out), (term), (bank)->sig, DEREF_NEVER) 154 void TBPrintTerm(FILE* out, TB_p bank, Term_p term, bool fullterms); 155 void TBPrintBankTerms(FILE* out, TB_p bank); 156 Term_p TBTermParseReal(Scanner_p in, TB_p bank, bool check_symb_prop); 157 158 #define TBTermParse(in, bank) TBTermParseReal((in),(bank), true) 159 #define TBRawTermParse(in, bank) TBTermParseReal((in),(bank), false) 160 161 void TBRefSetProp(TB_p bank, TermRef ref, TermProperties prop); 162 void TBRefDelProp(TB_p bank, TermRef ref, TermProperties prop); 163 164 long TBTermDelPropCount(Term_p term, TermProperties prop); 165 166 #define TBTermCellIsMarked(bank, term) \ 167 (GiveProps((term),TPGarbageFlag)!=(bank)->garbage_state) 168 void TBGCMarkTerm(TB_p bank, Term_p term); 169 long TBGCSweep(TB_p bank); 170 Term_p TBCreateMinTerm(TB_p bank, FunCode min_const); 171 172 long TBTermCollectSubterms(Term_p term, PStack_p collector); 173 174 175 /*---------------------------------------------------------------------*/ 176 /* Inline Functions */ 177 /*---------------------------------------------------------------------*/ 178 179 180 #endif 181 182 /*---------------------------------------------------------------------*/ 183 /* End of File */ 184 /*---------------------------------------------------------------------*/ 185