1 /*-----------------------------------------------------------------------
2 
3 File  : ccl_fcvindexing.h
4 
5 Author: Stephan Schulz
6 
7 Contents
8 
9   Functions for handling frequency count vector indexing for clause
10   subsumption.
11 
12   Copyright 2003 by the author.
13   This code is released under the GNU General Public Licence and
14   the GNU Lesser General Public License.
15   See the file COPYING in the main E directory for details..
16   Run "eprover -h" for contact information.
17 
18 Changes
19 
20 <1> Tue Jul  1 13:05:36 CEST 2003
21     New
22 <2> Sun Feb  6 02:16:41 CET 2005 (actually 2 weeks or so earlier)
23     Switched to IntMap
24 
25 -----------------------------------------------------------------------*/
26 
27 #ifndef CCL_FCVINDEXING
28 
29 #define CCL_FCVINDEXING
30 
31 #include <ccl_freqvectors.h>
32 #include <clb_intmap.h>
33 
34 /*---------------------------------------------------------------------*/
35 /*                    Data type declarations                           */
36 /*---------------------------------------------------------------------*/
37 
38 
39 PERF_CTR_DECL(FVIndexTimer);
40 
41 
42 typedef struct fvindex_parms_cell
43 {
44    FVCollectCell cspec;
45    bool use_perm_vectors;
46    bool eliminate_uninformative;
47    long max_symbols;
48    long symbol_slack;
49 }FVIndexParmsCell, *FVIndexParms_p;
50 
51 
52 
53 typedef struct fv_index_cell
54 {
55    bool     final;
56    long     clause_count;
57    union
58    {
59       IntMap_p successors;
60       PTree_p  clauses;
61    }u1;
62 }FVIndexCell, *FVIndex_p;
63 
64 typedef struct fvi_anchor_cell
65 {
66    FVCollect_p  cspec;
67    PermVector_p perm_vector;
68    FVIndex_p    index;
69    long         storage;
70 }FVIAnchorCell, *FVIAnchor_p;
71 
72 
73 /*---------------------------------------------------------------------*/
74 /*                Exported Functions and Variables                     */
75 /*---------------------------------------------------------------------*/
76 
77 /* extern FVIndexParmsCell FVIDefaultParameters; */
78 
79 #define FVIndexParmsCellAlloc() (FVIndexParmsCell*)SizeMalloc(sizeof(FVIndexParmsCell))
80 #define FVIndexParmsCellFree(junk) SizeFree(junk, sizeof(FVIndexParmsCell))
81 
82 void           FVIndexParmsInit(FVIndexParms_p parms);
83 FVIndexParms_p FVIndexParmsAlloc(void);
84 #define FVIndexParmsFree(junk) FVIndexParmsCellFree(junk)
85 
86 #define FVIndexCellAlloc()    (FVIndexCell*)SizeMalloc(sizeof(FVIndexCell))
87 #define FVIndexCellFree(junk) SizeFree(junk, sizeof(FVIndexCell))
88 
89 FVIndex_p FVIndexAlloc(void);
90 void      FVIndexFree(FVIndex_p junk);
91 
92 #define FVIAnchorCellAlloc()    (FVIAnchorCell*)SizeMalloc(sizeof(FVIAnchorCell))
93 #define FVIAnchorCellFree(junk) SizeFree(junk, sizeof(FVIAnchorCell))
94 
95 FVIAnchor_p FVIAnchorAlloc(FVCollect_p cspec, PermVector_p perm);
96 void        FVIAnchorFree(FVIAnchor_p junk);
97 
98 #ifdef CONSTANT_MEM_ESTIMATE
99 #define FVINDEX_MEM 16
100 #else
101 #define FVINDEX_MEM MEMSIZE(FVIndexCell)
102 #endif
103 
104 #define FVIndexStorage(index) ((index)?(index)->storage:0)
105 
106 FVIndex_p   FVIndexGetNextNonEmptyNode(FVIndex_p node, long key);
107 void        FVIndexInsert(FVIAnchor_p index, FreqVector_p vec_clause);
108 
109 bool        FVIndexDelete(FVIAnchor_p index, Clause_p clause);
110 
111 long        FVIndexCountNodes(FVIndex_p index, bool leaves, bool empty);
112 
113 FVPackedClause_p FVIndexPackClause(Clause_p clause, FVIAnchor_p anchor);
114 
115 #endif
116 
117 /*---------------------------------------------------------------------*/
118 /*                        End of File                                  */
119 /*---------------------------------------------------------------------*/
120 
121 
122 
123 
124 
125