1 /*-----------------------------------------------------------------------
2
3 File : ccl_fcvindexing.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Algorithms for frequency count vector indexing.
10
11 Copyright 1998-2011 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Tue Jul 1 13:09:10 CEST 2003
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "ccl_fcvindexing.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32 PERF_CTR_DEFINE(FVIndexTimer);
33
34 FVIndexParmsCell FVIDefaultParameters =
35 {
36 {
37 FVIACFold,
38 false,
39 NULL,
40 0,
41 0,
42 0,
43 0,
44 0,
45 0,
46 0,
47 0,
48 0,
49 0,
50 0,
51 0,
52 0,
53 0,
54 0,
55 },
56 false, /* use_perm_vectors */
57 false, /* eliminate_uninformative */
58 FVINDEX_MAX_FEATURES_DEFAULT,
59 FVINDEX_SYMBOL_SLACK_DEFAULT,
60 };
61
62 /*---------------------------------------------------------------------*/
63 /* Forward Declarations */
64 /*---------------------------------------------------------------------*/
65
66
67 /*---------------------------------------------------------------------*/
68 /* Internal Functions */
69 /*---------------------------------------------------------------------*/
70
71 /*-----------------------------------------------------------------------
72 //
73 // Function: insert_empty_node()
74 //
75 // Insert an empty node into FVIndex at node node and key key.
76 //
77 // Global Variables: -
78 //
79 // Side Effects : Memory operations, modifies index.
80 //
81 /----------------------------------------------------------------------*/
82
insert_empty_node(FVIndex_p node,FVIAnchor_p anchor,long key)83 static FVIndex_p insert_empty_node(FVIndex_p node, FVIAnchor_p anchor, long key)
84 {
85 FVIndex_p handle = FVIndexAlloc();
86
87 assert(node);
88 assert(key >= 0);
89
90 if(!node->u1.successors)
91 {
92 node->u1.successors = IntMapAlloc();
93 anchor->storage += IntMapStorage(node->u1.successors);
94 }
95
96 anchor->storage -= IntMapStorage(node->u1.successors);
97 IntMapAssign(node->u1.successors, key, handle);
98 anchor->storage += IntMapStorage(node->u1.successors);
99 anchor->storage += FVINDEX_MEM;
100
101 return handle;
102 }
103
104
105 /*---------------------------------------------------------------------*/
106 /* Exported Functions */
107 /*---------------------------------------------------------------------*/
108
109
110 /*-----------------------------------------------------------------------
111 //
112 // Function: FVIndexParmsInit()
113 //
114 // Initialize a FVIndexParmCell with rational values.
115 //
116 // Global Variables: -
117 //
118 // Side Effects : -
119 //
120 /----------------------------------------------------------------------*/
121
FVIndexParmsInit(FVIndexParms_p parms)122 void FVIndexParmsInit(FVIndexParms_p parms)
123 {
124 *parms = FVIDefaultParameters;
125 }
126
127 /*-----------------------------------------------------------------------
128 //
129 // Function: FVIndexParmsAlloc()
130 //
131 // Allocate an FVIndexParmsCell with rational values.
132 //
133 // Global Variables: -
134 //
135 // Side Effects : Memory operations.
136 //
137 /----------------------------------------------------------------------*/
138
FVIndexParmsAlloc(void)139 FVIndexParms_p FVIndexParmsAlloc(void)
140 {
141 FVIndexParms_p handle = FVIndexParmsCellAlloc();
142
143 FVIndexParmsInit(handle);
144
145 return handle;
146 }
147
148
149 /*-----------------------------------------------------------------------
150 //
151 // Function: FVIndexAlloc()
152 //
153 // Allocate an empty and initialize FVIndexCell.
154 //
155 // Global Variables: -
156 //
157 // Side Effects : Memory operations
158 //
159 /----------------------------------------------------------------------*/
160
FVIndexAlloc(void)161 FVIndex_p FVIndexAlloc(void)
162 {
163 FVIndex_p handle = FVIndexCellAlloc();
164
165 handle->clause_count = 0;
166 handle->u1.clauses = NULL;
167 handle->u1.successors = NULL;
168 handle->final = false;
169
170 return handle;
171 }
172
173 /*-----------------------------------------------------------------------
174 //
175 // Function: FVIndexFree()
176 //
177 // Free a FVIndex - recursively and slightly complex because of the
178 // weird structure...
179 //
180 // Global Variables: -
181 //
182 // Side Effects : Memory operations
183 //
184 /----------------------------------------------------------------------*/
185
186
FVIndexFree(FVIndex_p junk)187 void FVIndexFree(FVIndex_p junk)
188 {
189 IntMapIter_p iter;
190 long i;
191 FVIndex_p succ;
192
193 if(junk)
194 {
195 if(junk->final)
196 {
197 PTreeFree(junk->u1.clauses);
198 }
199 else if(junk->u1.successors)
200 {
201 iter = IntMapIterAlloc(junk->u1.successors, 0, LONG_MAX);
202 while((succ = IntMapIterNext(iter, &i)))
203 {
204 FVIndexFree(succ);
205 }
206 IntMapIterFree(iter);
207 IntMapFree(junk->u1.successors);
208 }
209 }
210 FVIndexCellFree(junk);
211 }
212
213
214 /*-----------------------------------------------------------------------
215 //
216 // Function: FVIAnchorAlloc()
217 //
218 // Allocate an (empty) FV index.
219 //
220 // Global Variables: -
221 //
222 // Side Effects : Memory operations
223 //
224 /----------------------------------------------------------------------*/
225
FVIAnchorAlloc(FVCollect_p cspec,PermVector_p perm)226 FVIAnchor_p FVIAnchorAlloc(FVCollect_p cspec, PermVector_p perm)
227 {
228 FVIAnchor_p handle = FVIAnchorCellAlloc();
229
230 handle->perm_vector = perm;
231 handle->cspec = cspec;
232 handle->index = FVIndexAlloc();
233 handle->storage = 0;
234
235 return handle;
236 }
237
238
239
240 /*-----------------------------------------------------------------------
241 //
242 // Function: FVIAnchorFree()
243 //
244 // Free a FV incex.
245 //
246 // Global Variables: -
247 //
248 // Side Effects : Memory operations
249 //
250 /----------------------------------------------------------------------*/
251
FVIAnchorFree(FVIAnchor_p junk)252 void FVIAnchorFree(FVIAnchor_p junk)
253 {
254 assert(junk);
255
256 fprintf(GlobalOut,
257 "# Freeing FVIndex. %ld leaves, %ld empty. Total nodes: %ld. Mem: %ld\n",
258 FVIndexCountNodes(junk->index, true, false),
259 FVIndexCountNodes(junk->index, true, true),
260 FVIndexCountNodes(junk->index, false, false),
261 FVIndexStorage(junk));
262
263 FVIndexFree(junk->index);
264 if(junk->perm_vector)
265 {
266 PermVectorFree(junk->perm_vector);
267 }
268 FVIAnchorCellFree(junk);
269 }
270
271
272 /*-----------------------------------------------------------------------
273 //
274 // Function: FVIndexGetNextNonEmptyNode()
275 //
276 // Get the next node if it is not empty. Otherwise return NULL.
277 //
278 // Global Variables: -
279 //
280 // Side Effects : -
281 //
282 /----------------------------------------------------------------------*/
283
FVIndexGetNextNonEmptyNode(FVIndex_p node,long key)284 FVIndex_p FVIndexGetNextNonEmptyNode(FVIndex_p node, long key)
285 {
286 FVIndex_p handle;
287
288 assert(!node->final);
289
290 handle = IntMapGetVal(node->u1.successors, key);
291 if(handle&&handle->clause_count)
292 {
293 return handle;
294 }
295 return NULL;
296 }
297
298
299
300 /*-----------------------------------------------------------------------
301 //
302 // Function: FVIndexInsert()
303 //
304 // Insert a FreqVector (with associated clause) into the index.
305 //
306 // Global Variables: -
307 //
308 // Side Effects : Changes the index.
309 //
310 /----------------------------------------------------------------------*/
311
FVIndexInsert(FVIAnchor_p index,FreqVector_p vec_clause)312 void FVIndexInsert(FVIAnchor_p index, FreqVector_p vec_clause)
313 {
314 FVIndex_p handle, newnode = NULL;
315 long i;
316
317 PERF_CTR_ENTRY(FVIndexTimer);
318
319 assert(vec_clause);
320 assert(vec_clause->clause);
321
322 ClauseSubsumeOrderSortLits(vec_clause->clause);
323
324 handle = index->index;
325 handle->clause_count++;
326
327 for(i=0; i<vec_clause->size; i++)
328 {
329 assert(!handle->final);
330
331 newnode = IntMapGetVal(handle->u1.successors, vec_clause->array[i]);
332 if(!newnode)
333 {
334 newnode = insert_empty_node(handle,
335 index,
336 vec_clause->array[i]);
337 }
338 handle = newnode;
339 handle->clause_count++;
340 }
341 handle->final = true;
342 PTreeStore(&(handle->u1.clauses), vec_clause->clause);
343 /* ClauseSetProp(vec_clause->clause, CPIsSIndexed); */
344 PERF_CTR_EXIT(FVIndexTimer);
345 }
346
347
348 /*-----------------------------------------------------------------------
349 //
350 // Function: FVIndexDelete()
351 //
352 // Delete a clause from a FVIndex. At the moment, just removes the
353 // clause from the final cell (I expect removals to be rare enough
354 // that it pays to leave the structure intact. Returns true if the
355 // clause was in the index, false otherwise.
356 //
357 // Global Variables: -
358 //
359 // Side Effects : Changes index.
360 //
361 /----------------------------------------------------------------------*/
362
FVIndexDelete(FVIAnchor_p index,Clause_p clause)363 bool FVIndexDelete(FVIAnchor_p index, Clause_p clause)
364 {
365 FreqVector_p vec;
366 FVIndex_p handle;
367 long i;
368 bool res;
369
370 vec = OptimizedVarFreqVectorCompute(clause, index->perm_vector,
371 index->cspec);
372 /* FreqVector-Computation is measured independently */
373 PERF_CTR_ENTRY(FVIndexTimer);
374 handle = index->index;
375 handle->clause_count--;
376
377 for(i=0; i<vec->size; i++)
378 {
379 assert(!handle->final);
380 handle = IntMapGetVal(handle->u1.successors, vec->array[i]);
381 if(!handle)
382 {
383 break;
384 }
385 handle->clause_count--;
386 }
387 FreqVectorFree(vec);
388 /* ClauseDelProp(clause, CPIsSIndexed); */
389 res = handle?PTreeDeleteEntry(&(handle->u1.clauses), clause):false;
390 PERF_CTR_EXIT(FVIndexTimer);
391 return res;
392 }
393
394 /*-----------------------------------------------------------------------
395 //
396 // Function: FVIndexCountNodes()
397 //
398 // Count the number of nodes. If empty is true, count empty leaves
399 // only. If leaves it true, count leaves only.
400 //
401 // Global Variables: -
402 //
403 // Side Effects : -
404 //
405 /----------------------------------------------------------------------*/
406
FVIndexCountNodes(FVIndex_p index,bool leaves,bool empty)407 long FVIndexCountNodes(FVIndex_p index, bool leaves, bool empty)
408 {
409 long res = 0, i;
410 IntMapIter_p iter;
411 FVIndex_p succ;
412
413 if(index)
414 {
415 if(index->final)
416 {
417 if(!empty || !index->u1.clauses)
418 {
419 res++;
420 }
421 assert(EQUIV(index->clause_count,index->u1.clauses));
422 }
423 else
424 {
425 if(!(empty||leaves))
426 {
427 res++;
428 }
429 if(index->u1.successors)
430 {
431 iter = IntMapIterAlloc(index->u1.successors, 0, LONG_MAX);
432 {
433 while((succ = IntMapIterNext(iter, &i)))
434 {
435 res += FVIndexCountNodes(succ, leaves, empty);
436 }
437 }
438 IntMapIterFree(iter);
439 }
440 }
441 }
442 return res;
443 }
444
445 /*-----------------------------------------------------------------------
446 //
447 // Function: FVIndexPackClause()
448 //
449 // Pack a clause into an apropriate FVPackedClauseStructure for the
450 // index.
451 //
452 // Global Variables: -
453 //
454 // Side Effects : -
455 //
456 /----------------------------------------------------------------------*/
457
FVIndexPackClause(Clause_p clause,FVIAnchor_p anchor)458 FVPackedClause_p FVIndexPackClause(Clause_p clause, FVIAnchor_p anchor)
459 {
460 if(!anchor)
461 {
462 return FVPackClause(clause, NULL, NULL);
463 }
464 return FVPackClause(clause, anchor->perm_vector,
465 anchor->cspec);
466 }
467
468
469 /*---------------------------------------------------------------------*/
470 /* End of File */
471 /*---------------------------------------------------------------------*/
472
473
474