/*----------------------------------------------------------------------- File : ccl_fcvindexing.c Author: Stephan Schulz Contents Algorithms for frequency count vector indexing. Copyright 1998-2011 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:09:10 CEST 2003 New -----------------------------------------------------------------------*/ #include "ccl_fcvindexing.h" /*---------------------------------------------------------------------*/ /* Global Variables */ /*---------------------------------------------------------------------*/ PERF_CTR_DEFINE(FVIndexTimer); FVIndexParmsCell FVIDefaultParameters = { { FVIACFold, false, NULL, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, }, false, /* use_perm_vectors */ false, /* eliminate_uninformative */ FVINDEX_MAX_FEATURES_DEFAULT, FVINDEX_SYMBOL_SLACK_DEFAULT, }; /* { { FVIACFeatures, false, NULL, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, }, true, false, FVINDEX_MAX_FEATURES_DEFAULT, FVINDEX_SYMBOL_SLACK_DEFAULT, }; */ /*---------------------------------------------------------------------*/ /* Forward Declarations */ /*---------------------------------------------------------------------*/ /*---------------------------------------------------------------------*/ /* Internal Functions */ /*---------------------------------------------------------------------*/ /*----------------------------------------------------------------------- // // Function: insert_empty_node() // // Insert an empty node into FVIndex at node node and key key. // // Global Variables: - // // Side Effects : Memory operations, modifies index. // /----------------------------------------------------------------------*/ static FVIndex_p insert_empty_node(FVIndex_p node, FVIAnchor_p anchor, long key) { FVIndex_p handle = FVIndexAlloc(); assert(node); assert(key >= 0); if(!node->u1.successors) { node->u1.successors = IntMapAlloc(); anchor->storage += IntMapStorage(node->u1.successors); } anchor->storage -= IntMapStorage(node->u1.successors); IntMapAssign(node->u1.successors, key, handle); anchor->storage += IntMapStorage(node->u1.successors); anchor->storage += FVINDEX_MEM; return handle; } /*---------------------------------------------------------------------*/ /* Exported Functions */ /*---------------------------------------------------------------------*/ /*----------------------------------------------------------------------- // // Function: FVIndexParmsInit() // // Initialize a FVIndexParmCell with rational values. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ void FVIndexParmsInit(FVIndexParms_p parms) { *parms = FVIDefaultParameters; } /*----------------------------------------------------------------------- // // Function: FVIndexParmsAlloc() // // Allocate an FVIndexParmsCell with rational values. // // Global Variables: - // // Side Effects : Memory operations. // /----------------------------------------------------------------------*/ FVIndexParms_p FVIndexParmsAlloc(void) { FVIndexParms_p handle = FVIndexParmsCellAlloc(); FVIndexParmsInit(handle); return handle; } /*----------------------------------------------------------------------- // // Function: FVIndexAlloc() // // Allocate an empty and initialize FVIndexCell. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ FVIndex_p FVIndexAlloc(void) { FVIndex_p handle = FVIndexCellAlloc(); handle->clause_count = 0; handle->u1.clauses = NULL; handle->u1.successors = NULL; handle->final = false; return handle; } /*----------------------------------------------------------------------- // // Function: FVIndexFree() // // Free a FVIndex - recursively and slightly complex because of the // weird structure... // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ void FVIndexFree(FVIndex_p junk) { IntMapIter_p iter; long i; FVIndex_p succ; if(junk) { if(junk->final) { PTreeFree(junk->u1.clauses); } else if(junk->u1.successors) { iter = IntMapIterAlloc(junk->u1.successors, 0, LONG_MAX); while((succ = IntMapIterNext(iter, &i))) { FVIndexFree(succ); } IntMapIterFree(iter); IntMapFree(junk->u1.successors); } } FVIndexCellFree(junk); } /*----------------------------------------------------------------------- // // Function: FVIAnchorAlloc() // // Allocate an (empty) FV index. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ FVIAnchor_p FVIAnchorAlloc(FVCollect_p cspec, PermVector_p perm) { FVIAnchor_p handle = FVIAnchorCellAlloc(); handle->perm_vector = perm; handle->cspec = cspec; handle->index = FVIndexAlloc(); handle->storage = 0; return handle; } /*----------------------------------------------------------------------- // // Function: FVIAnchorFree() // // Free a FV incex. // // Global Variables: - // // Side Effects : Memory operations // /----------------------------------------------------------------------*/ void FVIAnchorFree(FVIAnchor_p junk) { assert(junk); fprintf(GlobalOut, "# Freeing FVIndex. %ld leaves, %ld empty. Total nodes: %ld. Mem: %ld\n", FVIndexCountNodes(junk->index, true, false), FVIndexCountNodes(junk->index, true, true), FVIndexCountNodes(junk->index, false, false), FVIndexStorage(junk)); FVIndexFree(junk->index); if(junk->perm_vector) { PermVectorFree(junk->perm_vector); } FVIAnchorCellFree(junk); } /*----------------------------------------------------------------------- // // Function: FVIndexGetNextNonEmptyNode() // // Get the next node if it is not empty. Otherwise return NULL. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ FVIndex_p FVIndexGetNextNonEmptyNode(FVIndex_p node, long key) { FVIndex_p handle; assert(!node->final); handle = IntMapGetVal(node->u1.successors, key); if(handle&&handle->clause_count) { return handle; } return NULL; } /*----------------------------------------------------------------------- // // Function: FVIndexInsert() // // Insert a FreqVector (with associated clause) into the index. // // Global Variables: - // // Side Effects : Changes the index. // /----------------------------------------------------------------------*/ void FVIndexInsert(FVIAnchor_p index, FreqVector_p vec_clause) { FVIndex_p handle, newnode = NULL; long i; PERF_CTR_ENTRY(FVIndexTimer); assert(vec_clause); assert(vec_clause->clause); ClauseSubsumeOrderSortLits(vec_clause->clause); handle = index->index; handle->clause_count++; for(i=0; isize; i++) { assert(!handle->final); newnode = IntMapGetVal(handle->u1.successors, vec_clause->array[i]); if(!newnode) { newnode = insert_empty_node(handle, index, vec_clause->array[i]); } handle = newnode; handle->clause_count++; } handle->final = true; PTreeStore(&(handle->u1.clauses), vec_clause->clause); /* ClauseSetProp(vec_clause->clause, CPIsSIndexed); */ PERF_CTR_EXIT(FVIndexTimer); } /*----------------------------------------------------------------------- // // Function: FVIndexDelete() // // Delete a clause from a FVIndex. At the moment, just removes the // clause from the final cell (I expect removals to be rare enough // that it pays to leave the structure intact. Returns true if the // clause was in the index, false otherwise. // // Global Variables: - // // Side Effects : Changes index. // /----------------------------------------------------------------------*/ bool FVIndexDelete(FVIAnchor_p index, Clause_p clause) { FreqVector_p vec; FVIndex_p handle; long i; bool res; vec = OptimizedVarFreqVectorCompute(clause, index->perm_vector, index->cspec); /* FreqVector-Computation is measured independently */ PERF_CTR_ENTRY(FVIndexTimer); handle = index->index; handle->clause_count--; for(i=0; isize; i++) { assert(!handle->final); handle = IntMapGetVal(handle->u1.successors, vec->array[i]); if(!handle) { break; } handle->clause_count--; } FreqVectorFree(vec); /* ClauseDelProp(clause, CPIsSIndexed); */ res = handle?PTreeDeleteEntry(&(handle->u1.clauses), clause):false; PERF_CTR_EXIT(FVIndexTimer); return res; } /*----------------------------------------------------------------------- // // Function: FVIndexCountNodes() // // Count the number of nodes. If empty is true, count empty leaves // only. If leaves it true, count leaves only. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ long FVIndexCountNodes(FVIndex_p index, bool leaves, bool empty) { long res = 0, i; IntMapIter_p iter; FVIndex_p succ; if(index) { if(index->final) { if(!empty || !index->u1.clauses) { res++; } assert(EQUIV(index->clause_count,index->u1.clauses)); } else { if(!(empty||leaves)) { res++; } if(index->u1.successors) { iter = IntMapIterAlloc(index->u1.successors, 0, LONG_MAX); { while((succ = IntMapIterNext(iter, &i))) { res += FVIndexCountNodes(succ, leaves, empty); } } IntMapIterFree(iter); } } } return res; } /*----------------------------------------------------------------------- // // Function: FVIndexPackClause() // // Pack a clause into an apropriate FVPackedClauseStructure for the // index. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ FVPackedClause_p FVIndexPackClause(Clause_p clause, FVIAnchor_p anchor) { if(!anchor) { return FVPackClause(clause, NULL, NULL); } return FVPackClause(clause, anchor->perm_vector, anchor->cspec); } /*---------------------------------------------------------------------*/ /* End of File */ /*---------------------------------------------------------------------*/