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
|
/*-----------------------------------------------------------------------
File : cte_termcellstore.h
Author: Stephan Schulz
Contents
Abstract interface for storing term cells, implemented by a
combination of a hashed array and term cell trees. Use
(term->f_code^term->args[1])&TERM_STORE_HASH_MASK as
hash if args != NULL, otherwise use
term->f_code&TERM_STORE_HASH_MASK.
Copyright 1998, 1999 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
<1> Mon Oct 5 01:09:50 MEST 1998
New
<2> Thu Apr 11 10:08:26 CEST 2002
Support for mark-and-sweep garbage collection (the sweep pass) for
term cells
-----------------------------------------------------------------------*/
#ifndef CTE_TERMCELLSTORE
#define CTE_TERMCELLSTORE
#include <cte_termtrees.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
#define TERM_STORE_HASH_SIZE (8192*4)
#define TERM_STORE_HASH_MASK (TERM_STORE_HASH_SIZE-1)
typedef struct termcellstore
{
long entries;
long arg_count;
Term_p store[TERM_STORE_HASH_SIZE];
}TermCellStoreCell, *TermCellStore_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define tcs_arity0hash(term) ((term)->f_code)
#define tcs_arity1hash(term) (tcs_arity0hash(term)^(((intptr_t)(term)->args[0])>>3))
#define tcs_aritynhash(term) (tcs_arity1hash(term)^(((intptr_t)(term)->args[1])>>4))
#define TermCellHash(term)\
((((term)->arity == 0)?\
tcs_arity0hash(term):\
(((term)->arity == 1)?tcs_arity1hash(term):tcs_aritynhash(term)))\
&TERM_STORE_HASH_MASK)
void TermCellStoreInit(TermCellStore_p store);
void TermCellStoreExit(TermCellStore_p store);
Term_p TermCellStoreFind(TermCellStore_p store, Term_p term);
Term_p TermCellStoreInsert(TermCellStore_p store, Term_p term);
Term_p TermCellStoreExtract(TermCellStore_p store, Term_p term);
bool TermCellStoreDelete(TermCellStore_p store, Term_p term);
void TermCellStoreSetProp(TermCellStore_p store, TermProperties
props);
void TermCellStoreDelProp(TermCellStore_p store, TermProperties
props);
#define TermCellStoreNodes(store) ((store)->entries)
long TermCellStoreCountNodes(TermCellStore_p store);
long TermCellStoreGCSweep(TermCellStore_p store, TermProperties gc_state );
void TermCellStorePrintDistrib(FILE* out, TermCellStore_p store);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
