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