1 /*-----------------------------------------------------------------------
2
3 File : cte_termtypes.h
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Declarations for the basic term type and primitive functions, mainly
10 on single term cells. This module mostly provides only
11 infrastructure for higher level modules.
12
13 Copyright 1998, 1999 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 Created: Tue Feb 24 01:23:24 MET 1998 - Ripped out of the now obsolete
20 cte_terms.h
21
22 -----------------------------------------------------------------------*/
23
24 #ifndef CTE_TERMTYPES
25
26 #define CTE_TERMTYPES
27
28 #include <clb_partial_orderings.h>
29 #include <cte_signature.h>
30 #include <clb_sysdate.h>
31 #include <clb_ptrees.h>
32 #include <clb_properties.h>
33 #include <cte_simplesorts.h>
34
35
36
37 /*---------------------------------------------------------------------*/
38 /* Data type declarations */
39 /*---------------------------------------------------------------------*/
40
41 #define DEFAULT_VWEIGHT 1 /* This has to be an integer > 0! */
42 #define DEFAULT_FWEIGHT 2 /* This has to be >= DEFAULT_VWEIGHT */
43
44 /* POWNRS = Probably obsolete with new rewriting scheme */
45
46 typedef enum
47 {
48 TPIgnoreProps = 0, /* For masking properties out */
49 TPRestricted = 1, /* Rewriting is restricted on this term */
50 TPTopPos = 2, /* This cell is a entry point */
51 TPIsGround = 4, /* Shared term is ground */
52 TPPredPos = 8, /* This is an original predicate
53 position morphed into a term */
54 TPIsRewritable = 16, /* Term is known to be rewritable with
55 respect to a current rule or rule
56 set. Used for removing
57 backward-rewritable clauses. Absence of
58 this flag does not mean that the term
59 is in any kind of normal form! POWNRS */
60 TPIsRRewritable = 32, /* Term is rewritable even if
61 rewriting is restricted to proper
62 instances at the top level.*/
63 TPIsSOSRewritten = 64, /* Term has been rewritten with a SoS
64 clause (at top level) */
65 TPSpecialFlag = 128, /* For internal use with normalizing variables*/
66 TPOpFlag = 256, /* For internal use */
67 TPCheckFlag = 512, /* For internal use */
68 TPOutputFlag = 1024, /* Has this term already been printed (and
69 thus defined)? */
70 TPIsSpecialVar = 2048, /* Is this a meta-variable generated by term
71 top operations and the like? */
72 TPIsRewritten = 4096, /* Term has been rewritten (for the new
73 rewriting scheme) */
74 TPIsRRewritten = 8192, /* Term has been rewritten at a
75 subterm position or with a real
76 instance (for the new rewriting
77 scheme) */
78 TPIsShared = 16384, /* Term is in a term bank */
79 TPGarbageFlag = 32768, /* For the term bank garbage collection */
80 TPIsFreeVar = 65536, /* For Skolemization */
81 TPPotentialParamod = 131072, /* This position needs to be tried for
82 paramodulation */
83 TPPosPolarity = 1<<18, /* In the term encoding of a formula,
84 this occurs with positive polarity. */
85 TPNegPolarity = 1<<19, /* In the term encoding of a formula,
86 this occurs with negative polarity. */
87 }TermProperties;
88
89
90
91 typedef enum /* See CLAUSES/ccl_rewrite.c for more */
92 {
93 NoRewrite = 0, /* Just for completness */
94 RuleRewrite = 1, /* Rewrite with rules only */
95 FullRewrite = 2 /* Rewrite with rules and equations */
96 }RewriteLevel;
97
98 typedef struct
99 {
100 SysDate nf_date[FullRewrite]; /* If term is not rewritten,
101 it is in normal form with
102 respect to the
103 demodulators at this date */
104 struct {
105 struct termcell* replace; /* ...otherwise, it has been
106 rewritten to this term */
107 // long demod_id; /* 0 means subterm! */
108 struct clause_cell *demod; /* NULL means subterm! */
109 }rw_desc;
110 }RewriteState;
111
112
113 typedef struct termcell
114 {
115 FunCode f_code; /* Top symbol of term */
116 TermProperties properties; /* Like basic, lhs, top */
117 int arity; /* Redundant, but saves handing
118 around the signature all the
119 time */
120 struct termcell* *args; /* Pointer to array of arguments */
121 struct termcell* binding; /* For variable bindings,
122 potentially for temporary
123 rewrites - it might be possible
124 to combine the previous two in a
125 union. */
126 long entry_no; /* Counter for terms in a given
127 termbank - needed for
128 administration and external
129 representation */
130 long weight; /* Weight of the term, if term is in term bank */
131 unsigned int v_count; /* Number of variables, if term is in term bank */
132 unsigned int f_count; /* Number of function symbols, if term is in term bank */
133 RewriteState rw_data; /* See above */
134 SortType sort; /* Sort of the term */
135 struct termcell* lson; /* For storing shared term nodes in */
136 struct termcell* rson; /* a splay tree - see
137 cte_termcellstore.[ch] */
138 }TermCell, *Term_p, **TermRef;
139
140
141 typedef uintptr_t DerefType, *DerefType_p;
142
143 #define DEREF_NEVER 0
144 #define DEREF_ONCE 1
145 #define DEREF_ALWAYS 2
146
147 /* The following is an estimate for the memory taken up by a term cell
148 with arguments (the argument array is not counted separately). */
149
150 #ifdef CONSTANT_MEM_ESTIMATE
151 #define TERMCELL_MEM 48
152 #define TERMARG_MEM 4
153 #define TERMP_MEM 4
154 #else
155 #define TERMCELL_MEM MEMSIZE(TermCell)
156 #define TERMARG_MEM sizeof(void*)
157 #define TERMP_MEM sizeof(Term_p)
158 #endif
159
160 #define TERMCELL_DYN_MEM (TERMCELL_MEM+4*TERMARG_MEM)
161
162
163 /*---------------------------------------------------------------------*/
164 /* Exported Functions and Variables */
165 /*---------------------------------------------------------------------*/
166
167 /* Functions which take two terms and return a boolean, i.e. test for
168 equality */
169
170 #define TERMS_INITIAL_ARGS 10
171
172 #define RewriteAdr(level) (assert(level),(level)-1)
173 #define TermIsVar(t) ((t)->f_code < 0)
174 #define TermIsConst(t)(!TermIsVar(t) && ((t)->arity==0))
175
176 #define TermCellSetProp(term, prop) SetProp((term), (prop))
177 #define TermCellDelProp(term, prop) DelProp((term), (prop))
178 #define TermCellAssignProp(term, sel, prop) AssignProp((term),(sel),(prop))
179 /* Are _all_ properties in prop set in term? */
180 #define TermCellQueryProp(term, prop) QueryProp((term), (prop))
181
182 /* Are any properties in prop set in term? */
183 #define TermCellIsAnyPropSet(term, prop) IsAnyPropSet((term), (prop))
184
185 #define TermCellGiveProps(term, props) GiveProps((term),(props))
186 #define TermCellFlipProp(term, props) FlipProp((term),(props))
187
188 #define TermCellAlloc() (TermCell*)SizeMalloc(sizeof(TermCell))
189 #define TermCellFree(junk) SizeFree(junk, sizeof(TermCell))
190 #define TermArgArrayAlloc(arity) ((Term_p*)SizeMalloc((arity)*sizeof(Term_p)))
191 #define TermArgArrayFree(junk, arity) SizeFree((junk),(arity)*sizeof(Term_p))
192
193 #define TermIsRewritten(term) TermCellQueryProp((term), TPIsRewritten)
194 #define TermIsRRewritten(term) TermCellQueryProp((term), TPIsRRewritten)
195 #define TermIsTopRewritten(term) (TermIsRewritten(term)&&TermRWDemodField(term))
196 #define TermIsShared(term) TermCellQueryProp((term), TPIsShared)
197
198 #define TermNFDate(term,i) (TermIsRewritten(term)?\
199 SysDateCreationTime():(term)->rw_data.nf_date[i])
200
201 /* Absolutely get the value of the replace and demod fields */
202 #define TermRWReplaceField(term) ((term)->rw_data.rw_desc.replace)
203 #define TermRWDemodField(term) ((term)->rw_data.rw_desc.demod)
204 #define REWRITE_AT_SUBTERM 0
205
206 /* Get the logical value of the replaced term / demodulator */
207 #define TermRWReplace(term) (TermIsRewritten(term)?TermRWTargetField(term):NULL)
208 #define TermRWDemod(term) (TermIsRewritten(term)?TermRWDemodField(term):NULL)
209
210 static __inline__ Term_p TermDefaultCellAlloc(void);
211 static __inline__ Term_p TermConstCellAlloc(FunCode symbol);
212 static __inline__ Term_p TermTopAlloc(FunCode f_code, int arity);
213 static __inline__ Term_p TermTopCopy(Term_p source);
214 static __inline__ Term_p TermTopCopyWithoutArgs(Term_p source);
215
216 void TermTopFree(Term_p junk);
217 void TermFree(Term_p junk);
218 Term_p TermAllocNewSkolem(Sig_p sig, PStack_p variables, SortType sort);
219
220 void TermSetProp(Term_p term, DerefType deref, TermProperties prop);
221 bool TermSearchProp(Term_p term, DerefType deref, TermProperties prop);
222 bool TermVerifyProp(Term_p term, DerefType deref, TermProperties prop,
223 TermProperties expected);
224 void TermDelProp(Term_p term, DerefType deref, TermProperties prop);
225 void TermDelPropOpt(Term_p term, TermProperties prop);
226 void TermVarSetProp(Term_p term, DerefType deref, TermProperties prop);
227 bool TermVarSearchProp(Term_p term, DerefType deref, TermProperties prop);
228 void TermVarDelProp(Term_p term, DerefType deref, TermProperties prop);
229 bool TermHasInterpretedSymbol(Term_p term);
230
231 static __inline__ Term_p TermDerefAlways(Term_p term);
232 static __inline__ Term_p TermDeref(Term_p term, DerefType_p deref);
233
234 static __inline__ Term_p TermTopCopy(Term_p source);
235
236 void TermStackSetProps(PStack_p stack, TermProperties prop);
237 void TermStackDelProps(PStack_p stack, TermProperties prop);
238
239 /*---------------------------------------------------------------------*/
240 /* Inline functions */
241 /*---------------------------------------------------------------------*/
242
243
244 /*-----------------------------------------------------------------------
245 //
246 // Function: TermDerefAlways()
247 //
248 // Dereference a term as many times as possible.
249 //
250 // Global Variables: -
251 //
252 // Side Effects : -
253 //
254 /----------------------------------------------------------------------*/
255
TermDerefAlways(Term_p term)256 static __inline__ Term_p TermDerefAlways(Term_p term)
257 {
258 assert(TermIsVar(term)||!(term->binding));
259
260 while(term->binding)
261 {
262 term = term->binding;
263 }
264 return term;
265 }
266
267 /*-----------------------------------------------------------------------
268 //
269 // Function: TermDeref()
270 //
271 // Dereference a term. deref* tells us how many derefences to do
272 // at most, it will be decremented for each dereferenciation.
273 //
274 // Global Variables: -
275 //
276 // Side Effects : -
277 //
278 /----------------------------------------------------------------------*/
279
TermDeref(Term_p term,DerefType_p deref)280 static __inline__ Term_p TermDeref(Term_p term, DerefType_p deref)
281 {
282 assert(TermIsVar(term)||!(term->binding));
283
284 if(*deref == DEREF_ALWAYS)
285 {
286 while(term->binding)
287 {
288 term = term->binding;
289 }
290 }
291 else
292 {
293 while(*deref)
294 {
295 if(!term->binding)
296 {
297 break;
298 }
299 term = term->binding;
300 (*deref)--;
301 }
302 }
303 return term;
304 }
305
306
307 /*-----------------------------------------------------------------------
308 //
309 // Function: TermTopCopyWithoutArgs()
310 //
311 // Return a copy of the term node.
312 // Only the top node is duplicated.
313 // Arguments are not initialized.
314 //
315 // Global Variables: -
316 //
317 // Side Effects : Memory operations
318 //
319 /----------------------------------------------------------------------*/
320
TermTopCopyWithoutArgs(restrict Term_p source)321 static __inline__ Term_p TermTopCopyWithoutArgs(restrict Term_p source)
322 {
323 Term_p handle = TermDefaultCellAlloc();
324
325 /* All other properties are tied to the specific term! */
326 handle->properties = (source->properties&TPPredPos);
327 TermCellDelProp(handle, TPOutputFlag); /* As it gets a new id below */
328
329 handle->f_code = source->f_code;
330 handle->sort = source->sort;
331
332 if(source->arity)
333 {
334 handle->arity = source->arity;
335 handle->args = TermArgArrayAlloc(source->arity);
336 }
337
338 return handle;
339 }
340
341
342 /*-----------------------------------------------------------------------
343 //
344 // Function: TermTopCopy()
345 //
346 // Return a copy of the term node (and potential argument
347 // pointers). Only the top node and the pointers are duplicated, the
348 // arguments are shared between source and copy. As this function
349 // operates on nodes, it does not follow bindings! Administrative
350 // stuff (refs etc. will, of course, not be copied but initialized
351 // to rational values for an unshared
352 // term).
353 //
354 // Global Variables: -
355 //
356 // Side Effects : Memory operations
357 //
358 /----------------------------------------------------------------------*/
359
TermTopCopy(restrict Term_p source)360 static __inline__ Term_p TermTopCopy(restrict Term_p source)
361 {
362 Term_p handle = TermTopCopyWithoutArgs(source);
363
364 for(int i=0; i<source->arity; i++)
365 {
366 handle->args[i] = source->args[i];
367 }
368
369 return handle;
370 }
371
372 /*-----------------------------------------------------------------------
373 //
374 // Function: TermDefaultCellAlloc()
375 //
376 // Allocate a term cell with default values.
377 //
378 // Global Variables: -
379 //
380 // Side Effects : Memory operations
381 //
382 /----------------------------------------------------------------------*/
383
TermDefaultCellAlloc(void)384 static __inline__ Term_p TermDefaultCellAlloc(void)
385 {
386 Term_p handle = TermCellAlloc();
387
388 handle->properties = TPIgnoreProps;
389 handle->arity = 0;
390 handle->sort = STNoSort;
391 handle->binding = NULL;
392 handle->args = NULL;
393 handle->rw_data.nf_date[0] = SysDateCreationTime();
394 handle->rw_data.nf_date[1] = SysDateCreationTime();
395 handle->lson = NULL;
396 handle->rson = NULL;
397
398 return handle;
399 }
400
401
402 /*-----------------------------------------------------------------------
403 //
404 // Function: TermConstCellAlloc()
405 //
406 // Allocate a term cell for the constant term with symbol symbol.
407 //
408 // Global Variables: -
409 //
410 // Side Effects : Memory operations
411 //
412 /----------------------------------------------------------------------*/
413
TermConstCellAlloc(FunCode symbol)414 static __inline__ Term_p TermConstCellAlloc(FunCode symbol)
415 {
416 Term_p handle = TermDefaultCellAlloc();
417 handle->f_code = symbol;
418
419 return handle;
420 }
421
422 /*-----------------------------------------------------------------------
423 //
424 // Function: TermTopAlloc()
425 //
426 // Allocate a term top with given f_code and (uninitialized)
427 // argument array.
428 //
429 // Global Variables: -
430 //
431 // Side Effects : -
432 //
433 /----------------------------------------------------------------------*/
434
TermTopAlloc(FunCode f_code,int arity)435 static __inline__ Term_p TermTopAlloc(FunCode f_code, int arity)
436 {
437 Term_p handle = TermDefaultCellAlloc();
438
439 handle->f_code = f_code;
440 handle->arity = arity;
441 if(arity)
442 {
443 handle->args = TermArgArrayAlloc(arity);
444 }
445
446 return handle;
447 }
448
449 #endif
450
451
452 /*---------------------------------------------------------------------*/
453 /* End of File */
454 /*---------------------------------------------------------------------*/
455