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