1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
|
/*-----------------------------------------------------------------------
File : clb_intmap.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Definitions and functions for a data type that maps natural numbers
(including 0) to void* pointers, supporting assignments, retrieval,
deletion, and iteration.
Copyright 2004 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> Sat Dec 18 15:51:13 CET 2004
New
-----------------------------------------------------------------------*/
#ifndef CLB_INTMAP
#define CLB_INTMAP
#include <limits.h>
#include <clb_numtrees.h>
#include <clb_pdrangearrays.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
typedef enum
{
IMEmpty,
IMSingle,
IMArray,
IMTree
}IntMapType;
#define MAX_TREE_DENSITY 8
#define MIN_TREE_DENSITY 4
#define IM_ARRAY_SIZE MAX_TREE_DENSITY
/* This is the main thing - a datatype that keeps key/value pairs and
* allows inserting, updating, deleting, and ordered iteration. I
* expect additons to be frequent and deletions to be rare. Element
* access and iteration are the most frequent operations. We want this
* time- and space efficient for many different key distributions. */
typedef struct intmap_cell
{
IntMapType type;
unsigned long entry_no; /* How many key/value pairs? May be slightly
* larger than the real value, as keys
* associated to NULL are indistinguishable
* from unassociated keys. */
long min_key; /* Smallest key (may be only key). Again, this
* may be an overestimate, as we do not
* always correct this if a key is deleted
* from an array. */
long max_key; /* Largest key (may be only key). Again, this
* may be an overestimate, as we do not
* always correct this if a key is deleted
* from an array. */
union
{
void* value; /* For IMSingle */
PDRangeArr_p array; /* For IMArray */
NumTree_p tree; /* For IMTree */
}values;
}IntMapCell, *IntMap_p;
typedef struct intmap_iter_cell
{
IntMap_p map;
long lower_key;
long upper_key;
union
{
bool seen; /* For IMSingle */
long current; /* For IMArray */
PStack_p tree_iter; /* For IMTree */
}admin_data;
}IntMapIterCell, *IntMapIter_p;
typedef long (*IntMapFreeFunc)(void *junk_node);
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define IntMapCellAlloc() (IntMapCell*)SizeMalloc(sizeof(IntMapCell))
#define IntMapCellFree(junk) SizeFree(junk, sizeof(IntMapCell))
IntMap_p IntMapAlloc(void);
void IntMapFree(IntMap_p map);
void* IntMapGetVal(IntMap_p map, long key);
void** IntMapGetRef(IntMap_p map, long key);
void IntMapAssign(IntMap_p map, long key, void* value);
void* IntMapDelKey(IntMap_p map, long key);
#define IntMapIterCellAlloc() (IntMapIterCell*)SizeMalloc(sizeof(IntMapIterCell))
#define IntMapIterCellFree(junk) SizeFree(junk, sizeof(IntMapIterCell))
#ifdef CONSTANT_MEM_ESTIMATE
#define INTMAPCELL_MEM 20
#else
#define INTMAPCELL_MEM MEMSIZE(IntMapCell)
#endif
#define IntMapDStorage(map) (((map)->type == IMArray)?\
PDArrayStorage((map)->values.array):\
(((map)->type == IMTree)?\
((map)->entry_no*NUMTREECELL_MEM):0))
#define IntMapStorage(map) (INTMAPCELL_MEM+IntMapDStorage(map))
IntMapIter_p IntMapIterAlloc(IntMap_p map, long lower_key, long upper_key);
void IntMapIterFree(IntMapIter_p junk);
static inline void* IntMapIterNext(IntMapIter_p iter, long *key);
void IntMapDebugPrint(FILE* out, IntMap_p map);
/*---------------------------------------------------------------------*/
/* Inline Functions */
/*---------------------------------------------------------------------*/
/*-----------------------------------------------------------------------
//
// Function: IntMapIterNext()
//
// Return the next value/key pair in the map (or NULL/ndef) if the
// iterator is exhausted.
//
// Global Variables: -
//
// Side Effects : -
//
/----------------------------------------------------------------------*/
static inline void* IntMapIterNext(IntMapIter_p iter, long *key)
{
void* res = NULL;
long i;
NumTree_p handle;
assert(iter);
assert(key);
if(!iter->map)
{
return NULL;
}
//printf("IntMapIterNext()...\n");
switch(iter->map->type)
{
case IMEmpty:
break;
case IMSingle:
//printf("Case IMSingle\n");
if(!iter->admin_data.seen)
{
iter->admin_data.seen = true;
*key = iter->map->max_key;
res = iter->map->values.value;
}
break;
case IMArray:
//printf("Case IMArray\n");
for(i=iter->admin_data.current; i<= iter->upper_key; i++)
{
res = PDRangeArrElementP(iter->map->values.array, i);
if(res)
{
*key = i;
break;
}
}
iter->admin_data.current = i+1;
break;
case IMTree:
//printf("Case IMTree\n");
while((handle = NumTreeTraverseNext(iter->admin_data.tree_iter)))
{
if(handle)
{
if(handle->key > iter->upper_key)
{
/* Overrun limit */
break;
}
if(handle->val1.p_val)
{
/* Found real value */
*key = handle->key;
res = handle->val1.p_val;
break;
}
}
}
break;
default:
assert(false && "Unknown IntMap type.");
break;
}
//printf("...IntMapIterNext()\n");
return res;
}
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|