15622981081

Committed 12 Jun 2025 11:37PM UTC coverage: 64.502% (-0.9%) from 65.37%

Build # 15622981081

Build Type

push

github

Committed by

web-flow

Commit Message

L2 o submission merge into smtcomp2025 (#562)

* Add L2O module

* fix bug no vars to hill_climbing

* +l2o TODOs file

* Fixed some code issues.

* Fixed some code issues.

* Fixed code formatting for some files

* Fixed memory leak in hill climbing, removed hill climbing dl list, code improvements

* Removed unused files

* Moved EMPTY_KEY and DELTED_KEY of hmaps in .c files.

* Renamed eval_hash_map to double_hash_map

* +l2o_apply_ls: classical local search cost fx

* assert

* removed redundant code with apply_l2o_ls

* Fixed some breask in l2o_apply

* Added proper conversion from double to mcsat_value

* minor code updates

* Update function signature for l2o

* Portfolio 1

* Portfolio 2

* Portfolio 2 + delayed start

* Portfolio with start L2O

* Start, no portfolio

* Portfolio mod 13

* L2O only at restarts

* Increased initial delay

* No initial delay, cache clear every 2nd l2o run

* Fixed cache memory leak

* Fixed another memory leak

* Fix

* fup

# Conflicts:
#	src/mcsat/l2o/evaluator.c

* baa

* Added l2o_search_state_t and update evaluator.c

* Clean-up evaluator_t

* asserting cache variable comparison

* Update cache

* Cleanup l2o structs

* Cleanup header file

* Cleanup header files and includes

* Variable order sorting by activity in L2O

* Using prio in hill climb

* Using prio in hill climb w/o sorting

* Fixed var selection in hill climbing

* Fixed var selection in hill climbing

* another bugfix

* Update hill_climbing for boolean and bugfix

* enable variable ordering again

* added nra cache statistics

* don't do var order sorting

* L2O always use the cache

* Ever 25th recache, the cache is cleared instead of L2O

* do a % 10 for cache use in l2o

* Clear cache the first time only

* moved L2O call beyond propagation

* l2o after prop with % 2 cache usage

* Reworked hill_climbing.c

* 50/50

* Fixed new hill_climbing.c

* 50/50 %3

* first version of fs_jumping implemented

* Not just base level

* l2o init only ... (continued)

Run Details

231 of 1972 new or added lines in 19 files covered. (11.71%)

5 existing lines in 3 files now uncovered.

81263 of 125986 relevant lines covered (64.5%)

1412845.33 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

10.06

/src/utils/double_hash_map.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * MAPS 32BIT INTEGERS TO DOUBLES (adapted from int_hash_map)
 * Assumes that keys are non-negative
 */

#include <assert.h>
#include <string.h>

#include "utils/memalloc.h"

#include "double_hash_map.h"

/*
 * For debugging: check whether n is 0 or a power of 2
 */
#ifndef NDEBUG
static bool is_power_of_two(uint32_t n) {
  return (n & (n - 1)) == 0;
}
#endif

/*
 * Markers for empty/deleted pairs
 */
enum {
  DELETED_KEY = -2,
  EMPTY_KEY = -1,
};

/*
 * Initialization:
 * - n = initial size, must be a power of 2
 * - if n = 0, the default size is used
 */
void init_double_hmap(double_hmap_t *hmap, uint32_t n) {
  uint32_t i;
  double_hmap_pair_t *tmp;

  if (n == 0) {
    n = DOUBLE_HMAP_DEFAULT_SIZE;
  }

  if (n >= DOUBLE_HMAP_MAX_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(n));

  tmp = (double_hmap_pair_t *) safe_malloc(n * sizeof(double_hmap_pair_t));
  for (i=0; i<n; i++) {
    tmp[i].key = EMPTY_KEY;
  }

  hmap->data = tmp;
  hmap->size = n;
  hmap->nelems = 0;
  hmap->ndeleted = 0;

  hmap->resize_threshold = (uint32_t)(n * DOUBLE_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t) (n * DOUBLE_HMAP_CLEANUP_RATIO);
}


/*
 * Free memory
 */
void delete_double_hmap(double_hmap_t *hmap) {
  safe_free(hmap->data);
  hmap->data = NULL;
}

/*
 * Swap m1 and m2
 */
void double_hmap_swap(double_hmap_t *m1, double_hmap_t *m2) {
  double_hmap_t aux;

  aux = *m1;
  *m1 = *m2;
  *m2 = aux;
}

/*
 * Hash of a key (Jenkins hash)
 */
static uint32_t hash_key(int32_t k) {
  uint32_t x;

  x = (uint32_t) k;
  x = (x + 0x7ed55d16) + (x<<12);
  x = (x ^ 0xc761c23c) ^ (x>>19);
  x = (x + 0x165667b1) + (x<<5);
  x = (x + 0xd3a2646c) ^ (x<<9);
  x = (x + 0xfd7046c5) + (x<<3);
  x = (x ^ 0xb55a4f09) ^ (x>>16);

  return x;
}

/*
 * Make a copy of record d in a clean array data
 * - mask = size of data - 1 (size must be a power of 2)
 */
static void double_hmap_clean_copy(double_hmap_pair_t *data, double_hmap_pair_t *d, uint32_t mask) {
  uint32_t j;

  j = hash_key(d->key) & mask;
  while (data[j].key != EMPTY_KEY) {
    j ++;
    j &= mask;
  }

  data[j].key = d->key;
  data[j].val = d->val;
}


/*
 * Remove deleted records
 */
static void double_hmap_cleanup(double_hmap_t *hmap) {
  double_hmap_pair_t *tmp, *d;
  uint32_t j, n, mask;

  n = hmap->size;
  tmp = (double_hmap_pair_t *) safe_malloc(n * sizeof(double_hmap_pair_t));
  for (j=0; j<n; j++) {
    tmp[j].key = EMPTY_KEY;
  }

  mask = n - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      double_hmap_clean_copy(tmp, d, mask);
    }
    d++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->ndeleted = 0;
}


/*
 * Remove deleted records and make the table twice as large
 */
static void double_hmap_extend(double_hmap_t *hmap) {
  double_hmap_pair_t *tmp, *d;
  uint32_t j, n, n2, mask;

  n = hmap->size;
  n2 = n << 1;
  if (n2 >= DOUBLE_HMAP_MAX_SIZE) {
    out_of_memory();
  }

  tmp = (double_hmap_pair_t *) safe_malloc(n2 * sizeof(double_hmap_pair_t));
  for (j=0; j<n2; j++) {
    tmp[j].key = EMPTY_KEY;
  }

  mask = n2 - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      double_hmap_clean_copy(tmp, d, mask);
    }
    d ++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->size = n2;
  hmap->ndeleted = 0;

  hmap->resize_threshold = (uint32_t)(n2 * DOUBLE_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t)(n2 * DOUBLE_HMAP_CLEANUP_RATIO);
}


/*
 * Find record with key k
 * - return NULL if k is not in the table
 */
double_hmap_pair_t *double_hmap_find(const double_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  double_hmap_pair_t *d;

  assert(k >= 0);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key == EMPTY_KEY) return NULL;
    j ++;
    j &= mask;
  }
}


/*
 * Add record with key k after hmap was extended:
 * - initialize val to -1
 * - we know that no record with key k is present
 */
static double_hmap_pair_t *double_hmap_get_clean(double_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  double_hmap_pair_t *d;

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key < 0) {
      hmap->nelems ++;
      d->key = k;
      d->val = -1;
      return d;
    }
    j ++;
    j &= mask;
  }
}


/*
 * Find or add record with key k
 */
double_hmap_pair_t *double_hmap_get(double_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  double_hmap_pair_t *d, *aux;

  assert(k >= 0);
  assert(hmap->size > hmap->ndeleted + hmap->nelems);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;

  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key < 0) break;
    j ++;
    j &= mask;
  }

  aux = d; // new record, if needed, will be aux
  while (d->key != EMPTY_KEY) {
    j ++;
    j &= mask;
    d = hmap->data + j;
    if (d->key == k) return d;
  }

  if (aux->key == DELETED_KEY) {
    assert(hmap->ndeleted > 0);
    hmap->ndeleted --;
  }

  if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
    double_hmap_extend(hmap);
    aux = double_hmap_get_clean(hmap, k);
  } else {
    hmap->nelems ++;
    aux->key = k;
    aux->val = -1;
  }

  return aux;
}


/*
 * Add record [k -> v ] to hmap
 * - there must not be a record with the same key
 */
void double_hmap_add(double_hmap_t *hmap, int32_t k, double v) {
  uint32_t i, mask;

  assert(k >= 0 && hmap->nelems + hmap->ndeleted < hmap->size);

  mask = hmap->size - 1;
  i = hash_key(k) & mask;
  while (hmap->data[i].key >= 0) {
    assert(hmap->data[i].key != k);
    i ++;
    i &= mask;
  }

  // store the new record in data[i]
  if (hmap->data[i].key == DELETED_KEY) {
    assert(hmap->ndeleted > 0);
    hmap->ndeleted --;
  }
  hmap->data[i].key = k;
  hmap->data[i].val = v;
  hmap->nelems ++;

  if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
    double_hmap_extend(hmap);
  }
}


/*
 * Add record [k -> v ] to hmap
 * - if there is a record with the same key, it is replaced by the new record
 */
void double_hmap_add_replace(double_hmap_t *hmap, int32_t k, double v) {
  double_hmap_pair_t* record = double_hmap_find(hmap, k);
  if (record != NULL){
    double_hmap_erase(hmap, record);
  }
  double_hmap_add(hmap, k, v);
}

/*
 * Add record [k -> v ] to hmap
 * - if there is a record with the same key, it does not replace it (but does not throw an error)
 */
void double_hmap_add_not_replace(double_hmap_t *hmap, int32_t k, double v) {
  double_hmap_pair_t* record = double_hmap_find(hmap, k);
  if (record == NULL){
    double_hmap_add(hmap, k, v);
  }
}


/*
 * Erase record r
 */
void double_hmap_erase(double_hmap_t *hmap, double_hmap_pair_t *r) {
  assert(double_hmap_find(hmap, r->key) == r);

  r->key = DELETED_KEY;
  hmap->nelems --;
  hmap->ndeleted ++;
  if (hmap->ndeleted >= hmap->cleanup_threshold) {
    double_hmap_cleanup(hmap);
  }
}

/*
 * Deep copy one map to another
 */
extern void double_hmap_copy(double_hmap_t *hmap_to, const double_hmap_t *hmap_from) {
  hmap_to->size = hmap_from->size;
  hmap_to->nelems = hmap_from->nelems;
  hmap_to->ndeleted = hmap_from->ndeleted;
  hmap_to->resize_threshold = hmap_from->resize_threshold;
  hmap_to->cleanup_threshold = hmap_from->cleanup_threshold;
  hmap_to->data = safe_realloc(hmap_to->data, hmap_from->size * sizeof(double_hmap_pair_t));
  memcpy(hmap_to->data, hmap_from->data, hmap_from->size * sizeof(double_hmap_pair_t));
}


/*
 * Empty the map
 */
void double_hmap_reset(double_hmap_t *hmap) {
  uint32_t i, n;
  double_hmap_pair_t *d;

  n = hmap->size;
  d = hmap->data;
  for (i=0; i<n; i++) {
    d->key = EMPTY_KEY;
    d ++;
  }

  hmap->nelems = 0;
  hmap->ndeleted = 0;
}



/*
 * First non-empty record in the table, starting from p
 */
static const double_hmap_pair_t *double_hmap_get_next(const double_hmap_t *hmap, const double_hmap_pair_t *p) {
  double_hmap_pair_t *end;

  end = hmap->data + hmap->size;
  while (p < end) {
    if (p->key != EMPTY_KEY) return p;
    p ++;
  }

  return NULL;
}


/*
 * Get the first non-empty record or NULL if the table is empty
 */
extern double_hmap_pair_t *double_hmap_first_record(const double_hmap_t *hmap) {
  return (double_hmap_pair_t *) double_hmap_get_next(hmap, hmap->data);
}


/*
 * Next record after p or NULL
 */
extern double_hmap_pair_t *double_hmap_next_record(const double_hmap_t *hmap, const double_hmap_pair_t *p) {
  assert(p != NULL && p<hmap->data + hmap->size && p->key != EMPTY_KEY);
  return (double_hmap_pair_t *) double_hmap_get_next(hmap, p + 1);
}


1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* MAPS 32BIT INTEGERS TO DOUBLES (adapted from int_hash_map)
21	* Assumes that keys are non-negative
22	*/
23
24	#include <assert.h>
25	#include <string.h>
26
27	#include "utils/memalloc.h"
28
29	#include "double_hash_map.h"
30
31	/*
32	* For debugging: check whether n is 0 or a power of 2
33	*/
34	#ifndef NDEBUG
35	static bool is_power_of_two(uint32_t n) {
36	return (n & (n - 1)) == 0;
37	}
38	#endif
39
40	/*
41	* Markers for empty/deleted pairs
42	*/
43	enum {
44	DELETED_KEY = -2,
45	EMPTY_KEY = -1,
46	};
47
48	/*
49	* Initialization:
50	* - n = initial size, must be a power of 2
51	* - if n = 0, the default size is used
52	*/
53	void init_double_hmap(double_hmap_t *hmap, uint32_t n) {	1,268✔
54	uint32_t i;
55	double_hmap_pair_t *tmp;
56
57	if (n == 0) {	1,268✔
58	n = DOUBLE_HMAP_DEFAULT_SIZE;	1,268✔
59	}
60
61	if (n >= DOUBLE_HMAP_MAX_SIZE) {	1,268✔
NEW 62	out_of_memory();	×
63	}
64
65	assert(is_power_of_two(n));
66
67	tmp = (double_hmap_pair_t ) safe_malloc(n sizeof(double_hmap_pair_t));	1,268✔
68	for (i=0; i<n; i++) {	41,844✔
69	tmp[i].key = EMPTY_KEY;	40,576✔
70	}
71
72	hmap->data = tmp;	1,268✔
73	hmap->size = n;	1,268✔
74	hmap->nelems = 0;	1,268✔
75	hmap->ndeleted = 0;	1,268✔
76
77	hmap->resize_threshold = (uint32_t)(n * DOUBLE_HMAP_RESIZE_RATIO);	1,268✔
78	hmap->cleanup_threshold = (uint32_t) (n * DOUBLE_HMAP_CLEANUP_RATIO);	1,268✔
79	}	1,268✔
80
81
82	/*
83	* Free memory
84	*/
85	void delete_double_hmap(double_hmap_t *hmap) {	1,268✔
86	safe_free(hmap->data);	1,268✔
87	hmap->data = NULL;	1,268✔
88	}	1,268✔
89
90	/*
91	* Swap m1 and m2
92	*/
NEW 93	void double_hmap_swap(double_hmap_t m1, double_hmap_t m2) {	×
94	double_hmap_t aux;
95
NEW 96	aux = *m1;	×
NEW 97	m1 = m2;	×
NEW 98	*m2 = aux;	×
NEW 99	}	×
100
101	/*
102	* Hash of a key (Jenkins hash)
103	*/
NEW 104	static uint32_t hash_key(int32_t k) {	×
105	uint32_t x;
106
NEW 107	x = (uint32_t) k;	×
NEW 108	x = (x + 0x7ed55d16) + (x<<12);	×
NEW 109	x = (x ^ 0xc761c23c) ^ (x>>19);	×
NEW 110	x = (x + 0x165667b1) + (x<<5);	×
NEW 111	x = (x + 0xd3a2646c) ^ (x<<9);	×
NEW 112	x = (x + 0xfd7046c5) + (x<<3);	×
NEW 113	x = (x ^ 0xb55a4f09) ^ (x>>16);	×
114
NEW 115	return x;	×
116	}
117
118	/*
119	* Make a copy of record d in a clean array data
120	* - mask = size of data - 1 (size must be a power of 2)
121	*/
NEW 122	static void double_hmap_clean_copy(double_hmap_pair_t data, double_hmap_pair_t d, uint32_t mask) {	×
123	uint32_t j;
124
NEW 125	j = hash_key(d->key) & mask;	×
NEW 126	while (data[j].key != EMPTY_KEY) {	×
NEW 127	j ++;	×
NEW 128	j &= mask;	×
129	}
130
NEW 131	data[j].key = d->key;	×
NEW 132	data[j].val = d->val;	×
NEW 133	}	×
134
135
136	/*
137	* Remove deleted records
138	*/
NEW 139	static void double_hmap_cleanup(double_hmap_t *hmap) {	×
140	double_hmap_pair_t tmp, d;
141	uint32_t j, n, mask;
142
NEW 143	n = hmap->size;	×
NEW 144	tmp = (double_hmap_pair_t ) safe_malloc(n sizeof(double_hmap_pair_t));	×
NEW 145	for (j=0; j<n; j++) {	×
NEW 146	tmp[j].key = EMPTY_KEY;	×
147	}
148
NEW 149	mask = n - 1;	×
NEW 150	d = hmap->data;	×
NEW 151	for (j=0; j<n; j++) {	×
NEW 152	if (d->key >= 0) {	×
NEW 153	double_hmap_clean_copy(tmp, d, mask);	×
154	}
NEW 155	d++;	×
156	}
157
NEW 158	safe_free(hmap->data);	×
NEW 159	hmap->data = tmp;	×
NEW 160	hmap->ndeleted = 0;	×
NEW 161	}	×
162
163
164	/*
165	* Remove deleted records and make the table twice as large
166	*/
NEW 167	static void double_hmap_extend(double_hmap_t *hmap) {	×
168	double_hmap_pair_t tmp, d;
169	uint32_t j, n, n2, mask;
170
NEW 171	n = hmap->size;	×
NEW 172	n2 = n << 1;	×
NEW 173	if (n2 >= DOUBLE_HMAP_MAX_SIZE) {	×
NEW 174	out_of_memory();	×
175	}
176
NEW 177	tmp = (double_hmap_pair_t ) safe_malloc(n2 sizeof(double_hmap_pair_t));	×
NEW 178	for (j=0; j<n2; j++) {	×
NEW 179	tmp[j].key = EMPTY_KEY;	×
180	}
181
NEW 182	mask = n2 - 1;	×
NEW 183	d = hmap->data;	×
NEW 184	for (j=0; j<n; j++) {	×
NEW 185	if (d->key >= 0) {	×
NEW 186	double_hmap_clean_copy(tmp, d, mask);	×
187	}
NEW 188	d ++;	×
189	}
190
NEW 191	safe_free(hmap->data);	×
NEW 192	hmap->data = tmp;	×
NEW 193	hmap->size = n2;	×
NEW 194	hmap->ndeleted = 0;	×
195
NEW 196	hmap->resize_threshold = (uint32_t)(n2 * DOUBLE_HMAP_RESIZE_RATIO);	×
NEW 197	hmap->cleanup_threshold = (uint32_t)(n2 * DOUBLE_HMAP_CLEANUP_RATIO);	×
NEW 198	}	×
199
200
201	/*
202	* Find record with key k
203	* - return NULL if k is not in the table
204	*/
NEW 205	double_hmap_pair_t double_hmap_find(const double_hmap_t hmap, int32_t k) {	×
206	uint32_t mask, j;
207	double_hmap_pair_t *d;
208
209	assert(k >= 0);
210
NEW 211	mask = hmap->size - 1;	×
NEW 212	j = hash_key(k) & mask;	×
213	for (;;) {
NEW 214	d = hmap->data + j;	×
NEW 215	if (d->key == k) return d;	×
NEW 216	if (d->key == EMPTY_KEY) return NULL;	×
NEW 217	j ++;	×
NEW 218	j &= mask;	×
219	}
220	}
221
222
223	/*
224	* Add record with key k after hmap was extended:
225	* - initialize val to -1
226	* - we know that no record with key k is present
227	*/
NEW 228	static double_hmap_pair_t double_hmap_get_clean(double_hmap_t hmap, int32_t k) {	×
229	uint32_t mask, j;
230	double_hmap_pair_t *d;
231
NEW 232	mask = hmap->size - 1;	×
NEW 233	j = hash_key(k) & mask;	×
234	for (;;) {
NEW 235	d = hmap->data + j;	×
NEW 236	if (d->key < 0) {	×
NEW 237	hmap->nelems ++;	×
NEW 238	d->key = k;	×
NEW 239	d->val = -1;	×
NEW 240	return d;	×
241	}
NEW 242	j ++;	×
NEW 243	j &= mask;	×
244	}
245	}
246
247
248	/*
249	* Find or add record with key k
250	*/
NEW 251	double_hmap_pair_t double_hmap_get(double_hmap_t hmap, int32_t k) {	×
252	uint32_t mask, j;
253	double_hmap_pair_t d, aux;
254
255	assert(k >= 0);
256	assert(hmap->size > hmap->ndeleted + hmap->nelems);
257
NEW 258	mask = hmap->size - 1;	×
NEW 259	j = hash_key(k) & mask;	×
260
261	for (;;) {
NEW 262	d = hmap->data + j;	×
NEW 263	if (d->key == k) return d;	×
NEW 264	if (d->key < 0) break;	×
NEW 265	j ++;	×
NEW 266	j &= mask;	×
267	}
268
NEW 269	aux = d; // new record, if needed, will be aux	×
NEW 270	while (d->key != EMPTY_KEY) {	×
NEW 271	j ++;	×
NEW 272	j &= mask;	×
NEW 273	d = hmap->data + j;	×
NEW 274	if (d->key == k) return d;	×
275	}
276
NEW 277	if (aux->key == DELETED_KEY) {	×
278	assert(hmap->ndeleted > 0);
NEW 279	hmap->ndeleted --;	×
280	}
281
NEW 282	if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {	×
NEW 283	double_hmap_extend(hmap);	×
NEW 284	aux = double_hmap_get_clean(hmap, k);	×
285	} else {
NEW 286	hmap->nelems ++;	×
NEW 287	aux->key = k;	×
NEW 288	aux->val = -1;	×
289	}
290
NEW 291	return aux;	×
292	}
293
294
295	/*
296	* Add record [k -> v ] to hmap
297	* - there must not be a record with the same key
298	*/
NEW 299	void double_hmap_add(double_hmap_t *hmap, int32_t k, double v) {	×
300	uint32_t i, mask;
301
302	assert(k >= 0 && hmap->nelems + hmap->ndeleted < hmap->size);
303
NEW 304	mask = hmap->size - 1;	×
NEW 305	i = hash_key(k) & mask;	×
NEW 306	while (hmap->data[i].key >= 0) {	×
307	assert(hmap->data[i].key != k);
NEW 308	i ++;	×
NEW 309	i &= mask;	×
310	}
311
312	// store the new record in data[i]
NEW 313	if (hmap->data[i].key == DELETED_KEY) {	×
314	assert(hmap->ndeleted > 0);
NEW 315	hmap->ndeleted --;	×
316	}
NEW 317	hmap->data[i].key = k;	×
NEW 318	hmap->data[i].val = v;	×
NEW 319	hmap->nelems ++;	×
320
NEW 321	if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {	×
NEW 322	double_hmap_extend(hmap);	×
323	}
NEW 324	}	×
325
326
327	/*
328	* Add record [k -> v ] to hmap
329	* - if there is a record with the same key, it is replaced by the new record
330	*/
NEW 331	void double_hmap_add_replace(double_hmap_t *hmap, int32_t k, double v) {	×
NEW 332	double_hmap_pair_t* record = double_hmap_find(hmap, k);	×
NEW 333	if (record != NULL){	×
NEW 334	double_hmap_erase(hmap, record);	×
335	}
NEW 336	double_hmap_add(hmap, k, v);	×
NEW 337	}	×
338
339	/*
340	* Add record [k -> v ] to hmap
341	* - if there is a record with the same key, it does not replace it (but does not throw an error)
342	*/
NEW 343	void double_hmap_add_not_replace(double_hmap_t *hmap, int32_t k, double v) {	×
NEW 344	double_hmap_pair_t* record = double_hmap_find(hmap, k);	×
NEW 345	if (record == NULL){	×
NEW 346	double_hmap_add(hmap, k, v);	×
347	}
NEW 348	}	×
349
350
351	/*
352	* Erase record r
353	*/
NEW 354	void double_hmap_erase(double_hmap_t hmap, double_hmap_pair_t r) {	×
355	assert(double_hmap_find(hmap, r->key) == r);
356
NEW 357	r->key = DELETED_KEY;	×
NEW 358	hmap->nelems --;	×
NEW 359	hmap->ndeleted ++;	×
NEW 360	if (hmap->ndeleted >= hmap->cleanup_threshold) {	×
NEW 361	double_hmap_cleanup(hmap);	×
362	}
NEW 363	}	×
364
365	/*
366	* Deep copy one map to another
367	*/
NEW 368	extern void double_hmap_copy(double_hmap_t hmap_to, const double_hmap_t hmap_from) {	×
NEW 369	hmap_to->size = hmap_from->size;	×
NEW 370	hmap_to->nelems = hmap_from->nelems;	×
NEW 371	hmap_to->ndeleted = hmap_from->ndeleted;	×
NEW 372	hmap_to->resize_threshold = hmap_from->resize_threshold;	×
NEW 373	hmap_to->cleanup_threshold = hmap_from->cleanup_threshold;	×
NEW 374	hmap_to->data = safe_realloc(hmap_to->data, hmap_from->size * sizeof(double_hmap_pair_t));	×
NEW 375	memcpy(hmap_to->data, hmap_from->data, hmap_from->size * sizeof(double_hmap_pair_t));	×
NEW 376	}	×
377
378
379	/*
380	* Empty the map
381	*/
NEW 382	void double_hmap_reset(double_hmap_t *hmap) {	×
383	uint32_t i, n;
384	double_hmap_pair_t *d;
385
NEW 386	n = hmap->size;	×
NEW 387	d = hmap->data;	×
NEW 388	for (i=0; i<n; i++) {	×
NEW 389	d->key = EMPTY_KEY;	×
NEW 390	d ++;	×
391	}
392
NEW 393	hmap->nelems = 0;	×
NEW 394	hmap->ndeleted = 0;	×
NEW 395	}	×
396
397
398
399	/*
400	* First non-empty record in the table, starting from p
401	*/
NEW 402	static const double_hmap_pair_t double_hmap_get_next(const double_hmap_t hmap, const double_hmap_pair_t *p) {	×
403	double_hmap_pair_t *end;
404
NEW 405	end = hmap->data + hmap->size;	×
NEW 406	while (p < end) {	×
NEW 407	if (p->key != EMPTY_KEY) return p;	×
NEW 408	p ++;	×
409	}
410
NEW 411	return NULL;	×
412	}
413
414
415	/*
416	* Get the first non-empty record or NULL if the table is empty
417	*/
NEW 418	extern double_hmap_pair_t double_hmap_first_record(const double_hmap_t hmap) {	×
NEW 419	return (double_hmap_pair_t *) double_hmap_get_next(hmap, hmap->data);	×
420	}
421
422
423	/*
424	* Next record after p or NULL
425	*/
NEW 426	extern double_hmap_pair_t double_hmap_next_record(const double_hmap_t hmap, const double_hmap_pair_t *p) {	×
427	assert(p != NULL && p<hmap->data + hmap->size && p->key != EMPTY_KEY);
NEW 428	return (double_hmap_pair_t *) double_hmap_get_next(hmap, p + 1);	×
429	}
430

SRI-CSL / yices2 / 15622981081

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous