1 /*----------------------------------------------------------------------- 2 3 File : ccl_freqvectors.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Functions for handling frequency count vectors and permutation 10 vectors. 11 12 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 8 21:48:35 CEST 2003 21 New (separated FreqVector from fcvindexing.*) 22 23 -----------------------------------------------------------------------*/ 24 25 #ifndef CCL_FREQVECTORS 26 27 #define CCL_FREQVECTORS 28 29 #include <clb_pdarrays.h> 30 #include <clb_fixdarrays.h> 31 #include <clb_regmem.h> 32 #include <ccl_clauses.h> 33 34 35 /*---------------------------------------------------------------------*/ 36 /* Data type declarations */ 37 /*---------------------------------------------------------------------*/ 38 39 typedef FixedDArray_p PermVector_p; 40 41 typedef struct tuple3_cell 42 { 43 long pos; 44 long diff; 45 long value; 46 }Tuple3Cell; 47 48 #define FVINDEX_MAX_FEATURES_DEFAULT 17 /* Maximal lenght of feature vector */ 49 #define FVINDEX_SYMBOL_SLACK_DEFAULT 0 /* Reserve symbols for splitting */ 50 51 typedef struct freq_vector_cell 52 { 53 long size; /* How many fields? */ 54 long *array; 55 Clause_p clause; /* Just an unprotected reference */ 56 }FreqVectorCell, *FreqVector_p, *FVPackedClause_p; 57 58 /* Where do the symbol-specific features in classival FV-Vectors 59 * begin? */ 60 #define FV_CLAUSE_FEATURES 2 61 62 typedef enum 63 { 64 FVINoFeatures, 65 FVIACFeatures, 66 FVISSFeatures, 67 FVIAllFeatures, 68 FVIBillFeatures, 69 FVIBillPlusFeatures, 70 FVIACFold, 71 FVIACStagger, 72 FVICollectFeatures, 73 }FVIndexType; 74 75 76 /* Describe how to assemble a feature vector out of a full signature 77 * feature vector. */ 78 79 typedef struct fv_collect_cell 80 { 81 FVIndexType features; 82 bool use_litcount; /* Use pos_lit_no/neg_lit_no */ 83 long* assembly_vector; /* Mapping from full positions to reduced 84 positions */ 85 long ass_vec_len; /* Size of the assembly vector */ 86 long res_vec_len; /* How long is the result? */ 87 /* The rest describe how to handle index values that are larger 88 than ass_vec_len. If _mod is zero, the value is discarded, 89 otherwise it is added to _offset+(f_code%_mod) */ 90 long pos_count_base; 91 long pos_count_offset; 92 long pos_count_mod; 93 long neg_count_base; 94 long neg_count_offset; 95 long neg_count_mod; 96 long pos_depth_base; 97 long pos_depth_offset; 98 long pos_depth_mod; 99 long neg_depth_base; 100 long neg_depth_offset; 101 long neg_depth_mod; 102 /* Legacy parameters for classical implementation. These are not 103 * supported by the allocator and must be overwritten manually. */ 104 long max_symbols; 105 }FVCollectCell, *FVCollect_p; 106 107 108 /*---------------------------------------------------------------------*/ 109 /* Exported Functions and Variables */ 110 /*---------------------------------------------------------------------*/ 111 112 PERF_CTR_DECL(FreqVecTimer); 113 114 #define PermVectorAlloc(size) FixedDArrayAlloc(size) 115 #define PermVectorFree(junk) FixedDArrayFree(junk) 116 #define PermVectorCopy(vec) FixedDArrayCopy(vec) 117 #define PermVectorPrint(out,vec) FixedDArrayPrint((out),(vec)) 118 119 PermVector_p PermVectorComputeInternal(FreqVector_p fmax, FreqVector_p fmin, 120 FreqVector_p sums, 121 long max_len, 122 bool eliminate_uninformative); 123 124 125 #define FreqVectorCellAlloc() (FreqVectorCell*)SizeMalloc(sizeof(FreqVectorCell)) 126 #define FreqVectorCellFree(junk) SizeFree(junk, sizeof(FreqVectorCell)) 127 128 129 #define FVACCompatSize(size) ((size+1)*2+FV_CLAUSE_FEATURES) 130 #define FVSSCompatSize(size) ((size+1)*2) 131 #define FVFullSize(size) ((size+1)*4+FV_CLAUSE_FEATURES) 132 #define FVSize(size, features) (((features)==FVIACFeatures)?FVACCompatSize(size):\ 133 (((features)==FVISSFeatures)?FVSSCompatSize(size):\ 134 FVFullSize(size))) 135 136 137 #define FVCollectCellAlloc() (FVCollectCell*)SizeMalloc(sizeof(FVCollectCell)) 138 #define FVCollectCellFree(junk) SizeFree(junk, sizeof(FVCollectCell)) 139 140 141 142 FreqVector_p FreqVectorAlloc(long size); 143 144 void FreqVectorFreeReal(FreqVector_p junk); 145 #ifndef NDEBUG 146 #define FreqVectorFree(junk) FreqVectorFreeReal(junk);junk=NULL 147 #else 148 #define FreqVectorFree(junk) FreqVectorFreeReal(junk) 149 #endif 150 151 void FreqVectorInitialize(FreqVector_p vec, long value); 152 153 void FreqVectorPrint(FILE* out, FreqVector_p vec); 154 155 void VarFreqVectorAddVals(FreqVector_p vec, long symbols, FVIndexType features, 156 Clause_p clause); 157 FreqVector_p VarFreqVectorCompute(Clause_p clause, FVCollect_p cspec); 158 FreqVector_p OptimizedVarFreqVectorCompute(Clause_p clause, 159 PermVector_p perm, 160 FVCollect_p cspec); 161 162 void FVCollectInit(FVCollect_p handle, 163 FVIndexType features, 164 bool use_litcount, 165 long ass_vec_len, 166 long res_vec_len, 167 long pos_count_base, 168 long pos_count_offset, 169 long pos_count_mod, 170 long neg_count_base, 171 long neg_count_offset, 172 long neg_count_mod, 173 long pos_depth_base, 174 long pos_depth_offset, 175 long pos_depth_mod, 176 long neg_depth_base, 177 long neg_depth_offset, 178 long neg_depth_mod); 179 180 181 FVCollect_p FVCollectAlloc(FVIndexType features, 182 bool use_litcount, 183 long ass_vec_len, 184 long res_vec_len, 185 long pos_count_base, 186 long pos_count_offset, 187 long pos_count_mod, 188 long neg_count_base, 189 long neg_count_offset, 190 long neg_count_mod, 191 long pos_depth_base, 192 long pos_depth_offset, 193 long pos_depth_mod, 194 long neg_depth_base, 195 long neg_depth_offset, 196 long neg_depth_mod); 197 198 void FVCollectFree(FVCollect_p junk); 199 200 FreqVector_p FVCollectFreqVectorCompute(Clause_p clause, FVCollect_p cspec); 201 202 FVCollect_p BillFeaturesCollectAlloc(Sig_p sig, long len); 203 FVCollect_p BillPlusFeaturesCollectAlloc(Sig_p sig, long len); 204 205 206 FVPackedClause_p FVPackClause(Clause_p clause, PermVector_p perm, 207 FVCollect_p cspec); 208 Clause_p FVUnpackClause(FVPackedClause_p pack); 209 210 void FVPackedClauseFreeReal(FVPackedClause_p pack); 211 #ifndef NDEBUG 212 #define FVPackedClauseFree(junk) FVPackedClauseFreeReal(junk);junk=NULL 213 #else 214 #define FVPackedClauseFree(junk) FVPackedClauseFreeReal(junk) 215 #endif 216 217 218 void FreqVectorAdd(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2); 219 void FreqVectorMulAdd(FreqVector_p dest, FreqVector_p s1, long f1, 220 FreqVector_p s2, long f2); 221 #define FreqVectorSub(dest, s1, s2) FreqVectorMulAdd((dest),(s1), 1, (s2), -1) 222 void FreqVectorMax(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2); 223 void FreqVectorMin(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2); 224 225 226 227 228 #ifdef NEVER_DEFINED 229 void StandardFreqVectorAddVals(FreqVector_p vec, long sig_symbols, 230 Clause_p clause); 231 FreqVector_p StandardFreqVectorCompute(Clause_p clause, long sig_symbols); 232 FreqVector_p OptimizedFreqVectorCompute(Clause_p clause, 233 PermVector_p perm, 234 long sig_symbols); 235 #endif 236 237 238 #endif 239 240 /*---------------------------------------------------------------------*/ 241 /* End of File */ 242 /*---------------------------------------------------------------------*/ 243 244 245 246 247 248