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
|
/*-----------------------------------------------------------------------
File : ccl_fcvindexing.h
Author: Stephan Schulz
Contents
Functions for handling frequency count vector indexing for clause
subsumption.
Copyright 2003 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> Tue Jul 1 13:05:36 CEST 2003
New
<2> Sun Feb 6 02:16:41 CET 2005 (actually 2 weeks or so earlier)
Switched to IntMap
-----------------------------------------------------------------------*/
#ifndef CCL_FCVINDEXING
#define CCL_FCVINDEXING
#include <ccl_freqvectors.h>
#include <clb_intmap.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
PERF_CTR_DECL(FVIndexTimer);
typedef struct fvindex_parms_cell
{
FVCollectCell cspec;
bool use_perm_vectors;
bool eliminate_uninformative;
long max_symbols;
long symbol_slack;
}FVIndexParmsCell, *FVIndexParms_p;
typedef struct fv_index_cell
{
bool final;
long clause_count;
union
{
IntMap_p successors;
PTree_p clauses;
}u1;
}FVIndexCell, *FVIndex_p;
typedef struct fvi_anchor_cell
{
FVCollect_p cspec;
PermVector_p perm_vector;
FVIndex_p index;
long storage;
}FVIAnchorCell, *FVIAnchor_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
/* extern FVIndexParmsCell FVIDefaultParameters; */
#define FVIndexParmsCellAlloc() (FVIndexParmsCell*)SizeMalloc(sizeof(FVIndexParmsCell))
#define FVIndexParmsCellFree(junk) SizeFree(junk, sizeof(FVIndexParmsCell))
void FVIndexParmsInit(FVIndexParms_p parms);
FVIndexParms_p FVIndexParmsAlloc(void);
#define FVIndexParmsFree(junk) FVIndexParmsCellFree(junk)
#define FVIndexCellAlloc() (FVIndexCell*)SizeMalloc(sizeof(FVIndexCell))
#define FVIndexCellFree(junk) SizeFree(junk, sizeof(FVIndexCell))
FVIndex_p FVIndexAlloc(void);
void FVIndexFree(FVIndex_p junk);
#define FVIAnchorCellAlloc() (FVIAnchorCell*)SizeMalloc(sizeof(FVIAnchorCell))
#define FVIAnchorCellFree(junk) SizeFree(junk, sizeof(FVIAnchorCell))
FVIAnchor_p FVIAnchorAlloc(FVCollect_p cspec, PermVector_p perm);
void FVIAnchorFree(FVIAnchor_p junk);
#ifdef CONSTANT_MEM_ESTIMATE
#define FVINDEX_MEM 16
#else
#define FVINDEX_MEM MEMSIZE(FVIndexCell)
#endif
#define FVIndexStorage(index) ((index)?(index)->storage:0)
FVIndex_p FVIndexGetNextNonEmptyNode(FVIndex_p node, long key);
void FVIndexInsert(FVIAnchor_p index, FreqVector_p vec_clause);
bool FVIndexDelete(FVIAnchor_p index, Clause_p clause);
long FVIndexCountNodes(FVIndex_p index, bool leaves, bool empty);
FVPackedClause_p FVIndexPackClause(Clause_p clause, FVIAnchor_p anchor);
void FVIndexPrint(FILE* out, FVIndex_p index, bool fullterms);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|
