16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Run Details

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

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

24.87

/src/context/assumption_stack.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2018 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/>.
 */

/*
 * STACK TO STORE ASSUMPTIONS IN A CONTEXT
 */

#include <assert.h>
#include <stdbool.h>

#include "context/assumption_stack.h"
#include "utils/hash_functions.h"
#include "utils/memalloc.h"


/*
 * INDEX STRUCTURES
 */

/*
 * Match functions: it takes a key k and an index i and checks whether
 * the assumption at index i in the stack has key k. For the first
 * variant, the key is a literal. For the second variant, the key
 * is a term.
 */
typedef bool (*match_fun_t)(const assumption_elem_t *a, int32_t key, int32_t i);

static bool match_literal(const assumption_elem_t *a, int32_t key, int32_t i) {
  assert(i >= 0);
  return a[i].lit == key;
}

static bool match_term(const assumption_elem_t *a, int32_t key, int32_t i) {
  assert(i >= 0);
  return a[i].term == key;
}

/*
 * Get key functions: takes an index i and either returns the literal or the term.
 */
typedef int32_t (*get_key_fun_t)(const assumption_elem_t *a, int32_t i);

static int32_t key_literal(const assumption_elem_t *a, int32_t i) {
  assert(i >= 0);
  return a[i].lit;
}

static int32_t key_term(const assumption_elem_t *a, int32_t i) {
  assert(i >= 0);
  return a[i].term;
}


/*
 * 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


/*
 * Initialize an index: nothing allocated
 */
static void init_hash_index(hash_index_t *index) {
  index->data = NULL;
  index->size = 0;
  index->nelems = 0;
  index->ndeleted = 0;
  index->resize_threshold = 0;
  index->cleanup_threshold = 0;
}


/*
 * Free memory
 */
static void delete_hash_index(hash_index_t *index) {
  safe_free(index->data);
  index->data = NULL;
}


/*
 * Reset: empty the index
 */
static void reset_hash_index(hash_index_t *index) {
  uint32_t i, n;

  n = index->size;
  for (i=0; i<n; i++) {
    index->data[i] = -1;
  }
  index->nelems = 0;
  index->ndeleted = 0;
}


/*
 * Allocate an array of n elements and initialize all of them to -1
 */
static int32_t *new_index_array(uint32_t n) {  
  int32_t *tmp;
  uint32_t i;

  assert(is_power_of_two(n));
  tmp = (int32_t *) safe_malloc(n * sizeof(int32_t));
  for (i=0; i<n; i++) {
    tmp[i] = -1;
  }
  return tmp;
}

/*
 * Add mapping [key -> x] into array a
 * - x must be non-negative
 * - mask = size of a - 1 (the size of a is a power of 2)
 * - a must not be full
 */
static void clean_array_add(int32_t *a, int32_t key, int32_t x, uint32_t mask) {
  uint32_t i;

  assert(x >= 0);

  i = jenkins_hash_int32(key) & mask;
  while (a[i] >= 0) {
    i ++;
    i &= mask;
  }
  a[i] = x;
}


/*
 * First allocation
 */
static void alloc_hash_index(hash_index_t *index) {
  uint32_t n;

  assert(index->size == 0);

  n = DEF_ASSUMPTION_INDEX_SIZE;
  index->data = new_index_array(n);
  index->size = n;
  index->resize_threshold = (uint32_t)(n * ASSUMPTION_INDEX_RESIZE_RATIO);
  index->cleanup_threshold = (uint32_t)(n * ASSUMPTION_INDEX_CLEANUP_RATIO);
}


/*
 * Double the hash table size and copy its content into a fresh array
 * - key returns the key for element of index i in the stack
 */
static void resize_hash_index(hash_index_t *index, const assumption_elem_t *a, get_key_fun_t key) {
  uint32_t i, n, new_size, mask;
  int32_t x, k;
  int32_t *tmp;

  n = index->size;
  new_size = n << 1;
  if (new_size >= MAX_ASSUMPTION_INDEX_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(new_size));

  tmp = new_index_array(new_size);
  mask = new_size - 1;
  for (i=0; i<n; i++) {
    x = index->data[i];
    if (x >= 0) {
      k = key(a, x);
      clean_array_add(tmp, k, x, mask);
    }
  }

  safe_free(index->data);

  index->data = tmp;
  index->size = new_size;
  index->ndeleted = 0;
  index->resize_threshold = (uint32_t) (new_size * ASSUMPTION_INDEX_RESIZE_RATIO);
  index->cleanup_threshold = (uint32_t) (new_size * ASSUMPTION_INDEX_CLEANUP_RATIO);
}


/*
 * Cleanup the table: remove the deletion marks (i.e., elements set to -2)
 */
static void cleanup_hash_index(hash_index_t *index, const assumption_elem_t *a, get_key_fun_t key) {
  uint32_t i, n, mask;
  int32_t x, k;
  int32_t *tmp;

  n = index->size;
  tmp = new_index_array(n);
  mask = n - 1;
  for (i=0; i<n; i++) {
    x = index->data[i];
    if (x >= 0) {
      k = key(a, x);
      clean_array_add(tmp, k, x, mask);
    }
  }

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


/*
 * Check whether we need to resize/cleanup
 */
static inline bool hash_index_needs_resize(const hash_index_t *index) {
  return index->nelems + index->ndeleted >= index->resize_threshold;
}

static inline bool hash_index_needs_cleanup(const hash_index_t *index) {
  return index->ndeleted >= index->cleanup_threshold && index->ndeleted > 0;
}


/*
 * Search for an entry mapped to k in the index
 * - return -1 if not found
 */
static int32_t find_in_hash_index(const hash_index_t *index, int32_t k, const assumption_elem_t *a, match_fun_t match) {
  uint32_t i, mask;
  int32_t j;

  assert(is_power_of_two(index->size) && index->size > 0);

  mask = index->size - 1;
  i = jenkins_hash_int32(k) & mask;
  for (;;) {
    j = index->data[i];
    if (j == -1 || (j >= 0 && match(a, k, j))) break;
    i ++;
    i &= mask;
  }
  return j;
}


/*
 * Remove entry (k, x) from the index
 * - no change if the entry is not present
 * - note: there's at most one occurrence of x in the index
 */
static void remove_from_hash_index(hash_index_t *index, int32_t k, int32_t x) {
  uint32_t i, mask;
  int32_t j;

  assert(is_power_of_two(index->size) && index->size > 0);
  assert(x >= 0);
  
  mask = index->size - 1;
  i = jenkins_hash_int32(k) & mask;
  for (;;) {
    j = index->data[i];
    if (j == x) break;
    if (j == -1) return;
    i ++;
    i &= mask;
  }

  index->data[i] = -2;
  index->nelems --;
  index->ndeleted ++;
}


/*
 * Add (k, x) to the index
 * - no change if there's already an entry for k
 */
static void add_to_hash_index(hash_index_t *index, int32_t k, int32_t x, const assumption_elem_t *a, match_fun_t match) {
  uint32_t i, mask;
  int32_t j, free;

  assert(is_power_of_two(index->size) && index->size > 0);
  assert(x >= 0);

  free = -1;
  mask = index->size - 1;
  i = jenkins_hash_int32(k) & mask;
  for (;;) {
    j = index->data[i];
    if (j < 0) {
      if (free < 0) free = i; // free slot
      if (j == -1) break;
    } else if (match(a, k, j)) {
      return;
    }
    i ++;
    i &= mask;
  }

  assert(0 <= free && free < (int32_t) index->size && index->data[free] < 0);

  if (index->data[free] == -2) {
    assert(index->ndeleted > 0);
    index->ndeleted --;
  }

  index->data[free] = x;
  index->nelems ++;
}


/*
 * ASSUMPTION STACK
 */

/*
 * Initialize the stack:
 * - nothing is allocated yet
 * - level is 0
 */
void init_assumption_stack(assumption_stack_t *stack) {
  stack->data = NULL;
  stack->size = 0;
  stack->top = 0;
  stack->level = 0;
  init_hash_index(&stack->lit_index);
  init_hash_index(&stack->term_index);
}

/*
 * Free memory
 */
void delete_assumption_stack(assumption_stack_t *stack) {
  safe_free(stack->data);
  stack->data = NULL;
  delete_hash_index(&stack->lit_index);
  delete_hash_index(&stack->term_index);
}

/*
 * Empty the stack
 */
void reset_assumption_stack(assumption_stack_t *stack) {
  stack->top = 0;
  stack->level = 0;
  reset_hash_index(&stack->lit_index);
  reset_hash_index(&stack->term_index);
}


/*
 * Make the stack larger
 */
static void extend_assumption_stack(assumption_stack_t *stack) {
  uint32_t n;

  n = stack->size;
  if (n == 0) {
    // first allocation
    n = DEF_ASSUMPTION_STACK_SIZE;
    assert(n <= MAX_ASSUMPTION_STACK_SIZE);
    stack->data = (assumption_elem_t *) safe_malloc(n * sizeof(assumption_elem_t));
    stack->size = n;
    alloc_hash_index(&stack->lit_index);
    alloc_hash_index(&stack->term_index);

  } else {
    // try to make the stack 50% larger
    n += (n >> 1);
    if (n > MAX_ASSUMPTION_STACK_SIZE) {
      out_of_memory();
    }
    assert(n > stack->size);

    stack->data = (assumption_elem_t *) safe_realloc(stack->data, n * sizeof(assumption_elem_t));
    stack->size = n;
  }
}

/*
 * Close the current level and remove all assumptions added at this
 * level. stack->level must be positive.
 */
void assumption_stack_pop(assumption_stack_t *stack) {
  uint32_t i;

  assert(stack->level > 0);

  i = stack->top;
  while (i>0 && stack->data[i-1].level == stack->level) {
    i --;
    remove_from_hash_index(&stack->lit_index, stack->data[i].lit, i);
    remove_from_hash_index(&stack->term_index, stack->data[i].term, i);
  }

  stack->top = i;
  stack->level --;

  if (hash_index_needs_cleanup(&stack->lit_index)) {
    cleanup_hash_index(&stack->lit_index, stack->data, key_literal);
  }
  if (hash_index_needs_cleanup(&stack->term_index)) {
    cleanup_hash_index(&stack->term_index, stack->data, key_term);
  }
}


/*
 * Add a pair (t, l) on top of the stack: at the current level
 */
void assumption_stack_add(assumption_stack_t *stack, term_t t, literal_t l) {
  uint32_t i;

  i = stack->top;
  if (i == stack->size) {
    extend_assumption_stack(stack);
  }
  assert(i < stack->size);

  stack->data[i].term = t;
  stack->data[i].lit = l;
  stack->data[i].level = stack->level;
  stack->top = i+1;
  
  add_to_hash_index(&stack->lit_index, l, i, stack->data, match_literal);
  add_to_hash_index(&stack->term_index, t, i, stack->data, match_term);

  if (hash_index_needs_resize(&stack->lit_index)) {
    resize_hash_index(&stack->lit_index, stack->data, key_literal);
  }
  if (hash_index_needs_resize(&stack->term_index)) {
    resize_hash_index(&stack->term_index, stack->data, key_term);
  }
}


/*
 * Search for a term t attached to literal l in the stack:
 * - this searches for an element of the form (t, l, k) in the stack
 *   and return t;
 * - if several terms are mapped to l, the function returns the first one
 *   (i.e., with the lowest level k).
 * - if there's no such element, the function returns NULL_TERM (i.e., -1)
 */
term_t assumption_term_for_literal(const assumption_stack_t *stack, literal_t l) {
  int32_t i;
  term_t t;

  t = NULL_TERM;
  if (stack->size > 0) {
    i = find_in_hash_index(&stack->lit_index, l, stack->data, match_literal);
    if (i >= 0) {
      assert(i < stack->size);
      t = stack->data[i].term;
    }
  }

  return t;
}

/*
 * Search for a literal l attached to term t in the stack:
 * - search for a triple (t, l, k) in the stack and return l
 * - return null_literal if there's no such triple
 */
literal_t assumption_literal_for_term(const assumption_stack_t *stack, term_t t) {
  int32_t i;
  literal_t l;

  l = null_literal;
  if (stack->size > 0) {
    i = find_in_hash_index(&stack->term_index, t, stack->data, match_term);
    if (i >= 0) {
      assert(i < stack->size);
      l = stack->data[i].lit;
    }
  }
  return l;
}


1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2018 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	* STACK TO STORE ASSUMPTIONS IN A CONTEXT
21	*/
22
23	#include <assert.h>
24	#include <stdbool.h>
25
26	#include "context/assumption_stack.h"
27	#include "utils/hash_functions.h"
28	#include "utils/memalloc.h"
29
30
31	/*
32	* INDEX STRUCTURES
33	*/
34
35	/*
36	* Match functions: it takes a key k and an index i and checks whether
37	* the assumption at index i in the stack has key k. For the first
38	* variant, the key is a literal. For the second variant, the key
39	* is a term.
40	*/
41	typedef bool (match_fun_t)(const assumption_elem_t a, int32_t key, int32_t i);
42
43	static bool match_literal(const assumption_elem_t *a, int32_t key, int32_t i) {	×
44	assert(i >= 0);
45	return a[i].lit == key;	×
46	}
47
48	static bool match_term(const assumption_elem_t *a, int32_t key, int32_t i) {	×
49	assert(i >= 0);
50	return a[i].term == key;	×
51	}
52
53	/*
54	* Get key functions: takes an index i and either returns the literal or the term.
55	*/
56	typedef int32_t (get_key_fun_t)(const assumption_elem_t a, int32_t i);
57
58	static int32_t key_literal(const assumption_elem_t *a, int32_t i) {	×
59	assert(i >= 0);
60	return a[i].lit;	×
61	}
62
63	static int32_t key_term(const assumption_elem_t *a, int32_t i) {	×
64	assert(i >= 0);
65	return a[i].term;	×
66	}
67
68
69	/*
70	* For debugging: check whether n is 0 or a power of 2
71	*/
72	#ifndef NDEBUG
73	static bool is_power_of_two(uint32_t n) {
74	return (n & (n - 1)) == 0;
75	}
76	#endif
77
78
79	/*
80	* Initialize an index: nothing allocated
81	*/
82	static void init_hash_index(hash_index_t *index) {	16,204✔
83	index->data = NULL;	16,204✔
84	index->size = 0;	16,204✔
85	index->nelems = 0;	16,204✔
86	index->ndeleted = 0;	16,204✔
87	index->resize_threshold = 0;	16,204✔
88	index->cleanup_threshold = 0;	16,204✔
89	}	16,204✔
90
91
92	/*
93	* Free memory
94	*/
95	static void delete_hash_index(hash_index_t *index) {	16,204✔
96	safe_free(index->data);	16,204✔
97	index->data = NULL;	16,204✔
98	}	16,204✔
99
100
101	/*
102	* Reset: empty the index
103	*/
104	static void reset_hash_index(hash_index_t *index) {	2✔
105	uint32_t i, n;
106
107	n = index->size;	2✔
108	for (i=0; i<n; i++) {	2✔
109	index->data[i] = -1;	×
110	}
111	index->nelems = 0;	2✔
112	index->ndeleted = 0;	2✔
113	}	2✔
114
115
116	/*
117	* Allocate an array of n elements and initialize all of them to -1
118	*/
119	static int32_t *new_index_array(uint32_t n) {	×
120	int32_t *tmp;
121	uint32_t i;
122
123	assert(is_power_of_two(n));
124	tmp = (int32_t ) safe_malloc(n sizeof(int32_t));	×
125	for (i=0; i<n; i++) {	×
126	tmp[i] = -1;	×
127	}
128	return tmp;	×
129	}
130
131	/*
132	* Add mapping [key -> x] into array a
133	* - x must be non-negative
134	* - mask = size of a - 1 (the size of a is a power of 2)
135	* - a must not be full
136	*/
137	static void clean_array_add(int32_t *a, int32_t key, int32_t x, uint32_t mask) {	×
138	uint32_t i;
139
140	assert(x >= 0);
141
142	i = jenkins_hash_int32(key) & mask;	×
143	while (a[i] >= 0) {	×
144	i ++;	×
145	i &= mask;	×
146	}
147	a[i] = x;	×
148	}	×
149
150
151	/*
152	* First allocation
153	*/
154	static void alloc_hash_index(hash_index_t *index) {	×
155	uint32_t n;
156
157	assert(index->size == 0);
158
159	n = DEF_ASSUMPTION_INDEX_SIZE;	×
160	index->data = new_index_array(n);	×
161	index->size = n;	×
162	index->resize_threshold = (uint32_t)(n * ASSUMPTION_INDEX_RESIZE_RATIO);	×
163	index->cleanup_threshold = (uint32_t)(n * ASSUMPTION_INDEX_CLEANUP_RATIO);	×
164	}	×
165
166
167	/*
168	* Double the hash table size and copy its content into a fresh array
169	* - key returns the key for element of index i in the stack
170	*/
171	static void resize_hash_index(hash_index_t index, const assumption_elem_t a, get_key_fun_t key) {	×
172	uint32_t i, n, new_size, mask;
173	int32_t x, k;
174	int32_t *tmp;
175
176	n = index->size;	×
177	new_size = n << 1;	×
178	if (new_size >= MAX_ASSUMPTION_INDEX_SIZE) {	×
179	out_of_memory();	×
180	}
181
182	assert(is_power_of_two(new_size));
183
184	tmp = new_index_array(new_size);	×
185	mask = new_size - 1;	×
186	for (i=0; i<n; i++) {	×
187	x = index->data[i];	×
188	if (x >= 0) {	×
189	k = key(a, x);	×
190	clean_array_add(tmp, k, x, mask);	×
191	}
192	}
193
194	safe_free(index->data);	×
195
196	index->data = tmp;	×
197	index->size = new_size;	×
198	index->ndeleted = 0;	×
199	index->resize_threshold = (uint32_t) (new_size * ASSUMPTION_INDEX_RESIZE_RATIO);	×
200	index->cleanup_threshold = (uint32_t) (new_size * ASSUMPTION_INDEX_CLEANUP_RATIO);	×
201	}	×
202
203
204	/*
205	* Cleanup the table: remove the deletion marks (i.e., elements set to -2)
206	*/
207	static void cleanup_hash_index(hash_index_t index, const assumption_elem_t a, get_key_fun_t key) {	×
208	uint32_t i, n, mask;
209	int32_t x, k;
210	int32_t *tmp;
211
212	n = index->size;	×
213	tmp = new_index_array(n);	×
214	mask = n - 1;	×
215	for (i=0; i<n; i++) {	×
216	x = index->data[i];	×
217	if (x >= 0) {	×
218	k = key(a, x);	×
219	clean_array_add(tmp, k, x, mask);	×
220	}
221	}
222
223	safe_free(index->data);	×
224	index->data = tmp;	×
225	index->ndeleted = 0;	×
226	}	×
227
228
229	/*
230	* Check whether we need to resize/cleanup
231	*/
232	static inline bool hash_index_needs_resize(const hash_index_t *index) {	×
233	return index->nelems + index->ndeleted >= index->resize_threshold;	×
234	}
235
236	static inline bool hash_index_needs_cleanup(const hash_index_t *index) {	462✔
237	return index->ndeleted >= index->cleanup_threshold && index->ndeleted > 0;	462✔
238	}
239
240
241	/*
242	* Search for an entry mapped to k in the index
243	* - return -1 if not found
244	*/
245	static int32_t find_in_hash_index(const hash_index_t index, int32_t k, const assumption_elem_t a, match_fun_t match) {	×
246	uint32_t i, mask;
247	int32_t j;
248
249	assert(is_power_of_two(index->size) && index->size > 0);
250
251	mask = index->size - 1;	×
252	i = jenkins_hash_int32(k) & mask;	×
253	for (;;) {
254	j = index->data[i];	×
255	if (j == -1 \|\| (j >= 0 && match(a, k, j))) break;	×
256	i ++;	×
257	i &= mask;	×
258	}
259	return j;	×
260	}
261
262
263	/*
264	* Remove entry (k, x) from the index
265	* - no change if the entry is not present
266	* - note: there's at most one occurrence of x in the index
267	*/
268	static void remove_from_hash_index(hash_index_t *index, int32_t k, int32_t x) {	×
269	uint32_t i, mask;
270	int32_t j;
271
272	assert(is_power_of_two(index->size) && index->size > 0);
273	assert(x >= 0);
274
275	mask = index->size - 1;	×
276	i = jenkins_hash_int32(k) & mask;	×
277	for (;;) {
278	j = index->data[i];	×
279	if (j == x) break;	×
280	if (j == -1) return;	×
281	i ++;	×
282	i &= mask;	×
283	}
284
285	index->data[i] = -2;	×
286	index->nelems --;	×
287	index->ndeleted ++;	×
288	}
289
290
291	/*
292	* Add (k, x) to the index
293	* - no change if there's already an entry for k
294	*/
295	static void add_to_hash_index(hash_index_t index, int32_t k, int32_t x, const assumption_elem_t a, match_fun_t match) {	×
296	uint32_t i, mask;
297	int32_t j, free;
298
299	assert(is_power_of_two(index->size) && index->size > 0);
300	assert(x >= 0);
301
302	free = -1;	×
303	mask = index->size - 1;	×
304	i = jenkins_hash_int32(k) & mask;	×
305	for (;;) {
306	j = index->data[i];	×
307	if (j < 0) {	×
308	if (free < 0) free = i; // free slot	×
309	if (j == -1) break;	×
310	} else if (match(a, k, j)) {	×
311	return;	×
312	}
313	i ++;	×
314	i &= mask;	×
315	}
316
317	assert(0 <= free && free < (int32_t) index->size && index->data[free] < 0);
318
319	if (index->data[free] == -2) {	×
320	assert(index->ndeleted > 0);
321	index->ndeleted --;	×
322	}
323
324	index->data[free] = x;	×
325	index->nelems ++;	×
326	}
327
328
329	/*
330	* ASSUMPTION STACK
331	*/
332
333	/*
334	* Initialize the stack:
335	* - nothing is allocated yet
336	* - level is 0
337	*/
338	void init_assumption_stack(assumption_stack_t *stack) {	8,102✔
339	stack->data = NULL;	8,102✔
340	stack->size = 0;	8,102✔
341	stack->top = 0;	8,102✔
342	stack->level = 0;	8,102✔
343	init_hash_index(&stack->lit_index);	8,102✔
344	init_hash_index(&stack->term_index);	8,102✔
345	}	8,102✔
346
347	/*
348	* Free memory
349	*/
350	void delete_assumption_stack(assumption_stack_t *stack) {	8,102✔
351	safe_free(stack->data);	8,102✔
352	stack->data = NULL;	8,102✔
353	delete_hash_index(&stack->lit_index);	8,102✔
354	delete_hash_index(&stack->term_index);	8,102✔
355	}	8,102✔
356
357	/*
358	* Empty the stack
359	*/
360	void reset_assumption_stack(assumption_stack_t *stack) {	1✔
361	stack->top = 0;	1✔
362	stack->level = 0;	1✔
363	reset_hash_index(&stack->lit_index);	1✔
364	reset_hash_index(&stack->term_index);	1✔
365	}	1✔
366
367
368	/*
369	* Make the stack larger
370	*/
371	static void extend_assumption_stack(assumption_stack_t *stack) {	×
372	uint32_t n;
373
374	n = stack->size;	×
375	if (n == 0) {	×
376	// first allocation
377	n = DEF_ASSUMPTION_STACK_SIZE;	×
378	assert(n <= MAX_ASSUMPTION_STACK_SIZE);
379	stack->data = (assumption_elem_t ) safe_malloc(n sizeof(assumption_elem_t));	×
380	stack->size = n;	×
381	alloc_hash_index(&stack->lit_index);	×
382	alloc_hash_index(&stack->term_index);	×
383
384	} else {
385	// try to make the stack 50% larger
386	n += (n >> 1);	×
387	if (n > MAX_ASSUMPTION_STACK_SIZE) {	×
388	out_of_memory();	×
389	}
390	assert(n > stack->size);
391
392	stack->data = (assumption_elem_t ) safe_realloc(stack->data, n sizeof(assumption_elem_t));	×
393	stack->size = n;	×
394	}
395	}	×
396
397	/*
398	* Close the current level and remove all assumptions added at this
399	* level. stack->level must be positive.
400	*/
401	void assumption_stack_pop(assumption_stack_t *stack) {	231✔
402	uint32_t i;
403
404	assert(stack->level > 0);
405
406	i = stack->top;	231✔
407	while (i>0 && stack->data[i-1].level == stack->level) {	231✔
408	i --;	×
409	remove_from_hash_index(&stack->lit_index, stack->data[i].lit, i);	×
410	remove_from_hash_index(&stack->term_index, stack->data[i].term, i);	×
411	}
412
413	stack->top = i;	231✔
414	stack->level --;	231✔
415
416	if (hash_index_needs_cleanup(&stack->lit_index)) {	231✔
417	cleanup_hash_index(&stack->lit_index, stack->data, key_literal);	×
418	}
419	if (hash_index_needs_cleanup(&stack->term_index)) {	231✔
420	cleanup_hash_index(&stack->term_index, stack->data, key_term);	×
421	}
422	}	231✔
423
424
425	/*
426	* Add a pair (t, l) on top of the stack: at the current level
427	*/
428	void assumption_stack_add(assumption_stack_t *stack, term_t t, literal_t l) {	×
429	uint32_t i;
430
431	i = stack->top;	×
432	if (i == stack->size) {	×
433	extend_assumption_stack(stack);	×
434	}
435	assert(i < stack->size);
436
437	stack->data[i].term = t;	×
438	stack->data[i].lit = l;	×
439	stack->data[i].level = stack->level;	×
440	stack->top = i+1;	×
441
442	add_to_hash_index(&stack->lit_index, l, i, stack->data, match_literal);	×
443	add_to_hash_index(&stack->term_index, t, i, stack->data, match_term);	×
444
445	if (hash_index_needs_resize(&stack->lit_index)) {	×
446	resize_hash_index(&stack->lit_index, stack->data, key_literal);	×
447	}
448	if (hash_index_needs_resize(&stack->term_index)) {	×
449	resize_hash_index(&stack->term_index, stack->data, key_term);	×
450	}
451	}	×
452
453
454	/*
455	* Search for a term t attached to literal l in the stack:
456	* - this searches for an element of the form (t, l, k) in the stack
457	* and return t;
458	* - if several terms are mapped to l, the function returns the first one
459	* (i.e., with the lowest level k).
460	* - if there's no such element, the function returns NULL_TERM (i.e., -1)
461	*/
462	term_t assumption_term_for_literal(const assumption_stack_t *stack, literal_t l) {	×
463	int32_t i;
464	term_t t;
465
466	t = NULL_TERM;	×
467	if (stack->size > 0) {	×
468	i = find_in_hash_index(&stack->lit_index, l, stack->data, match_literal);	×
469	if (i >= 0) {	×
470	assert(i < stack->size);
471	t = stack->data[i].term;	×
472	}
473	}
474
475	return t;	×
476	}
477
478	/*
479	* Search for a literal l attached to term t in the stack:
480	* - search for a triple (t, l, k) in the stack and return l
481	* - return null_literal if there's no such triple
482	*/
483	literal_t assumption_literal_for_term(const assumption_stack_t *stack, term_t t) {	×
484	int32_t i;
485	literal_t l;
486
487	l = null_literal;	×
488	if (stack->size > 0) {	×
489	i = find_in_hash_index(&stack->term_index, t, stack->data, match_term);	×
490	if (i >= 0) {	×
491	assert(i < stack->size);
492	l = stack->data[i].lit;	×
493	}
494	}
495	return l;	×
496	}
497

SRI-CSL / yices2 / 16032530443

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