9226448713

Committed 24 May 2024 03:34PM UTC coverage: 65.988% (+0.3%) from 65.728%

Build # 9226448713

Build Type

Pull #513

github

Committed by

web-flow

Commit Message

Merge da66d3d5d into f06761440

Pull Request Pull Request #513: Finite Field support

Run Details

2396 of 3347 new or added lines in 66 files covered. (71.59%)

18 existing lines in 12 files now uncovered.

81769 of 123915 relevant lines covered (65.99%)

1493770.28 hits per line

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

86.07

/src/context/shared_terms.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/>.
 */

#include <assert.h>

#include "context/shared_terms.h"

/*
 * Initialization:
 * - intern must be the context's internalization table
 * - the term table is extracted from intern
 */
void init_sharing_map(sharing_map_t *map, intern_tbl_t *intern) { 
  init_int_hmap(&map->hmap, 128);
  map->intern = intern;
  map->terms = intern->terms;
  init_int_queue(&map->queue, 128);
}


/*
 * Delete the whole thing
 */
void delete_sharing_map(sharing_map_t *map) {
  delete_int_hmap(&map->hmap);
  delete_int_queue(&map->queue);
}


/*
 * Reset: emtpty the hmap and the queue
 */
void reset_sharing_map(sharing_map_t *map) {
  int_hmap_reset(&map->hmap);
  int_queue_reset(&map->queue);
}


/*  
 * Process term i
 * - p = a parent of i
 *
 * First replace i but its root in the internalization table
 * If the root is already internalized, we ignore it.
 * If not, we check whether it's in the hmap:
 * - if i is not there, we add it to the hmap with parent = p
 *   we also add i to the queue
 * - if i is already in hmap, it has more than one occurrence so
 *   we set i's paretn to bool_const (as a marker)
 */
static void sharing_map_process_occurrence(sharing_map_t *map, int32_t i, int32_t p) {
  int_hmap_pair_t *r;
  term_t root;

  assert(good_term_idx(map->terms, i) && good_term_idx(map->terms, p));

  root = intern_tbl_get_root(map->intern, pos_term(i));
  if (! intern_tbl_root_is_mapped(map->intern, root)) {
    // root not internalized yet
    i = index_of(root);
    r = int_hmap_get(&map->hmap, i);
    assert(r->key == i);
    if (r->val < 0) {
      // new record so this is the first occurrence of i
      r->val = p;
      int_queue_push(&map->queue, i); // ?? Could skip this if i is atomic
    } else {
      r->val = bool_const;
    }
  }
}



/*
 * Visit non-atomic terms: c = descriptor of a term p
 */
static void sharing_map_visit_composite(sharing_map_t *map, composite_term_t *c, int32_t p) {
  uint32_t i, n;

  assert(c == composite_for_idx(map->terms, p));

  n = c->arity;
  for (i=0; i<n; i++) {
    sharing_map_process_occurrence(map, index_of(c->arg[i]), p);
  }
}

static void sharing_map_visit_select(sharing_map_t *map, select_term_t *c, int32_t p) {
  assert(c == select_for_idx(map->terms, p));
  sharing_map_process_occurrence(map, index_of(c->arg), p);
}

static void sharing_map_visit_pprod(sharing_map_t *map, pprod_t *c, int32_t p) {
  uint32_t i, n;

  assert(c == pprod_for_idx(map->terms, p));

  n = c->len;
  for (i=0; i<n; i++) {
    sharing_map_process_occurrence(map, index_of(c->prod[i].var), p);
  }
}

static void sharing_map_visit_poly(sharing_map_t *map, polynomial_t *c, int32_t p) {
  uint32_t i, n;

  assert(c == polynomial_for_idx(map->terms, p));

  n = c->nterms;
  assert(n > 0);

  i = 0;
  if (c->mono[0].var == const_idx) {
    i ++; // skip the constant
  }
  while (i<n) {
    sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);
    i ++;
  }  
}

static void sharing_map_visit_bvpoly64(sharing_map_t *map, bvpoly64_t *c, int32_t p) {
  uint32_t i, n;

  assert(c == bvpoly64_for_idx(map->terms, p));

  n = c->nterms;
  assert(n > 0);

  i = 0;
  if (c->mono[0].var == const_idx) {
    i ++; // skip the constant
  }
  while (i<n) {
    sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);
    i ++;
  }  
}

static void sharing_map_visit_bvpoly(sharing_map_t *map, bvpoly_t *c, int32_t p) {
  uint32_t i, n;

  assert(c == bvpoly_for_idx(map->terms, p));

  n = c->nterms;
  assert(n > 0);

  i = 0;
  if (c->mono[0].var == const_idx) {
    i ++; // skip the constant
  }
  while (i<n) {
    sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);
    i ++;
  }  
}

// visit all subterms of i
static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) {
  switch (kind_for_idx(map->terms, i)) {
  case CONSTANT_TERM:
  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
  case VARIABLE:
  case UNINTERPRETED_TERM:
    // atomic term
    break;

  case ARITH_EQ_ATOM:
  case ARITH_GE_ATOM:
  case ARITH_IS_INT_ATOM:
  case ARITH_FLOOR:
  case ARITH_CEIL:
  case ARITH_ABS:
    sharing_map_process_occurrence(map, index_of(integer_value_for_idx(map->terms, i)), i);
    break;
  case ARITH_ROOT_ATOM:
    assert(false);
    break;

  case ITE_TERM:
  case ITE_SPECIAL:
  case APP_TERM:
  case UPDATE_TERM:
  case TUPLE_TERM:
  case EQ_TERM:
  case DISTINCT_TERM:
  case FORALL_TERM:
  case LAMBDA_TERM:
  case OR_TERM:
  case XOR_TERM:
  case ARITH_BINEQ_ATOM:
  case ARITH_RDIV:
  case ARITH_IDIV:
  case ARITH_MOD:
  case ARITH_DIVIDES_ATOM:
  case BV_ARRAY:
  case BV_DIV:
  case BV_REM:
  case BV_SDIV:
  case BV_SREM:
  case BV_SMOD:
  case BV_SHL:
  case BV_LSHR:
  case BV_ASHR:
  case BV_EQ_ATOM:
  case BV_GE_ATOM:
  case BV_SGE_ATOM:
    sharing_map_visit_composite(map, composite_for_idx(map->terms, i), i);
    break;

  case SELECT_TERM:
  case BIT_TERM:
    sharing_map_visit_select(map, select_for_idx(map->terms, i), i);
    break;

  case POWER_PRODUCT:
    sharing_map_visit_pprod(map, pprod_for_idx(map->terms, i), i);
    break;

  case ARITH_POLY:
    sharing_map_visit_poly(map, polynomial_for_idx(map->terms, i), i);
    break;

  case BV64_POLY:
    sharing_map_visit_bvpoly64(map, bvpoly64_for_idx(map->terms, i), i);
    break;

  case BV_POLY:
    sharing_map_visit_bvpoly(map, bvpoly_for_idx(map->terms, i), i);
    break;

  case ARITH_FF_CONSTANT:
  case ARITH_FF_POLY:
  case ARITH_FF_EQ_ATOM:
  case ARITH_FF_BINEQ_ATOM:
    assert(false);
    break;

  case UNUSED_TERM:
  case RESERVED_TERM:
    assert(false);
    break;
  }
}


/*
 * Process term t:
 * - all subterms of t are visited recursively and added the map
 */
void sharing_map_add_term(sharing_map_t *map, term_t t) {
  int_queue_t *queue;
  int32_t i;

  queue = &map->queue;
  assert(int_queue_is_empty(queue));

  int_queue_push(queue, index_of(t));
  while (! int_queue_is_empty(queue)) {
    i = int_queue_pop(queue);
    sharing_map_visit_subterms(map, i);
  }
}


/*
 * Process all terms in array a
 * - n = size of the array
 */
void sharing_map_add_terms(sharing_map_t *map, term_t *a, uint32_t n) {
  uint32_t i;
  
  for (i=0; i<n; i++) {
    sharing_map_add_term(map, a[i]);
  }
}


/*
 * Check whether t occurs more that once among all the terms visited so far 
 * - this returns false if t is not in the map or if t has been seen only once
 */
bool term_is_shared(sharing_map_t *map, term_t t) {
  int_hmap_pair_t *r;
  int32_t i;

  i = index_of(t);
  assert(good_term_idx(map->terms, i));

  r = int_hmap_find(&map->hmap, i);
  return r != NULL && r->val == bool_const;
}


/*
 * Check whether t occurs once
 * - this returns false if t is not in the map or if t has been visited more than once
 */
bool term_is_not_shared(sharing_map_t *map, term_t t) {
  int_hmap_pair_t *r;
  int32_t i;

  i = index_of(t);
  assert(good_term_idx(map->terms, i));

  r = int_hmap_find(&map->hmap, i);
  return r != NULL && r->val != bool_const;
}


/*
 * Get the unique parent of t
 * - if t has been seen only once, this returns t's parent as stored in map->hamp
 * - if t has not been seen at all, this returns NULL_TERM
 * - if t has more than once occurrences, this returns true_term (as a marker).
 */
term_t unique_parent(sharing_map_t *map, term_t t) {
  int_hmap_pair_t *r;
  int32_t i;
  term_t parent;

  i = index_of(t);
  assert(good_term_idx(map->terms, i));

  parent = NULL_TERM;
  r = int_hmap_find(&map->hmap, i);
  if (r != NULL) {
    assert(r->key == i);
    parent = pos_term(r->val);
  }

  return parent;
}


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	#include <assert.h>
20
21	#include "context/shared_terms.h"
22
23	/*
24	* Initialization:
25	* - intern must be the context's internalization table
26	* - the term table is extracted from intern
27	*/
28	void init_sharing_map(sharing_map_t map, intern_tbl_t intern) {	13,174✔
29	init_int_hmap(&map->hmap, 128);	13,174✔
30	map->intern = intern;	13,174✔
31	map->terms = intern->terms;	13,174✔
32	init_int_queue(&map->queue, 128);	13,174✔
33	}	13,174✔
34
35
36	/*
37	* Delete the whole thing
38	*/
39	void delete_sharing_map(sharing_map_t *map) {	13,174✔
40	delete_int_hmap(&map->hmap);	13,174✔
41	delete_int_queue(&map->queue);	13,174✔
42	}	13,174✔
43
44
45	/*
46	* Reset: emtpty the hmap and the queue
47	*/
48	void reset_sharing_map(sharing_map_t *map) {	43,574✔
49	int_hmap_reset(&map->hmap);	43,574✔
50	int_queue_reset(&map->queue);	43,574✔
51	}	43,574✔
52
53
54	/*
55	* Process term i
56	* - p = a parent of i
57	*
58	* First replace i but its root in the internalization table
59	* If the root is already internalized, we ignore it.
60	* If not, we check whether it's in the hmap:
61	* - if i is not there, we add it to the hmap with parent = p
62	* we also add i to the queue
63	* - if i is already in hmap, it has more than one occurrence so
64	* we set i's paretn to bool_const (as a marker)
65	*/
66	static void sharing_map_process_occurrence(sharing_map_t *map, int32_t i, int32_t p) {	1,708,261✔
67	int_hmap_pair_t *r;
68	term_t root;
69
70	assert(good_term_idx(map->terms, i) && good_term_idx(map->terms, p));
71
72	root = intern_tbl_get_root(map->intern, pos_term(i));	1,708,261✔
73	if (! intern_tbl_root_is_mapped(map->intern, root)) {	1,708,261✔
74	// root not internalized yet
75	i = index_of(root);	1,282,984✔
76	r = int_hmap_get(&map->hmap, i);	1,282,984✔
77	assert(r->key == i);
78	if (r->val < 0) {	1,282,984✔
79	// new record so this is the first occurrence of i
80	r->val = p;	609,295✔
81	int_queue_push(&map->queue, i); // ?? Could skip this if i is atomic	609,295✔
82	} else {
83	r->val = bool_const;	673,689✔
84	}
85	}
86	}	1,708,261✔
87
88
89
90	/*
91	* Visit non-atomic terms: c = descriptor of a term p
92	*/
93	static void sharing_map_visit_composite(sharing_map_t map, composite_term_t c, int32_t p) {	272,168✔
94	uint32_t i, n;
95
96	assert(c == composite_for_idx(map->terms, p));
97
98	n = c->arity;	272,168✔
99	for (i=0; i<n; i++) {	1,571,848✔
100	sharing_map_process_occurrence(map, index_of(c->arg[i]), p);	1,299,680✔
101	}
102	}	272,168✔
103
104	static void sharing_map_visit_select(sharing_map_t map, select_term_t c, int32_t p) {	325,963✔
105	assert(c == select_for_idx(map->terms, p));
106	sharing_map_process_occurrence(map, index_of(c->arg), p);	325,963✔
107	}	325,963✔
108
109	static void sharing_map_visit_pprod(sharing_map_t map, pprod_t c, int32_t p) {	593✔
110	uint32_t i, n;
111
112	assert(c == pprod_for_idx(map->terms, p));
113
114	n = c->len;	593✔
115	for (i=0; i<n; i++) {	1,749✔
116	sharing_map_process_occurrence(map, index_of(c->prod[i].var), p);	1,156✔
117	}
118	}	593✔
119
120	static void sharing_map_visit_poly(sharing_map_t map, polynomial_t c, int32_t p) {	19,601✔
121	uint32_t i, n;
122
123	assert(c == polynomial_for_idx(map->terms, p));
124
125	n = c->nterms;	19,601✔
126	assert(n > 0);
127
128	i = 0;	19,601✔
129	if (c->mono[0].var == const_idx) {	19,601✔
130	i ++; // skip the constant	11,414✔
131	}
132	while (i<n) {	62,196✔
133	sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);	42,595✔
134	i ++;	42,595✔
135	}
136	}	19,601✔
137
138	static void sharing_map_visit_bvpoly64(sharing_map_t map, bvpoly64_t c, int32_t p) {	12,108✔
139	uint32_t i, n;
140
141	assert(c == bvpoly64_for_idx(map->terms, p));
142
143	n = c->nterms;	12,108✔
144	assert(n > 0);
145
146	i = 0;	12,108✔
147	if (c->mono[0].var == const_idx) {	12,108✔
148	i ++; // skip the constant	3,093✔
149	}
150	while (i<n) {	27,942✔
151	sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);	15,834✔
152	i ++;	15,834✔
153	}
154	}	12,108✔
155
156	static void sharing_map_visit_bvpoly(sharing_map_t map, bvpoly_t c, int32_t p) {	610✔
157	uint32_t i, n;
158
159	assert(c == bvpoly_for_idx(map->terms, p));
160
161	n = c->nterms;	610✔
162	assert(n > 0);
163
164	i = 0;	610✔
165	if (c->mono[0].var == const_idx) {	610✔
166	i ++; // skip the constant	539✔
167	}
168	while (i<n) {	1,276✔
169	sharing_map_process_occurrence(map, index_of(c->mono[i].var), p);	666✔
170	i ++;	666✔
171	}
172	}	610✔
173
174	// visit all subterms of i
175	static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) {	704,230✔
176	switch (kind_for_idx(map->terms, i)) {	704,230✔
177	case CONSTANT_TERM:	50,820✔
178	case ARITH_CONSTANT:
179	case BV64_CONSTANT:
180	case BV_CONSTANT:
181	case VARIABLE:
182	case UNINTERPRETED_TERM:
183	// atomic term
184	break;	50,820✔
185
186	case ARITH_EQ_ATOM:	22,367✔
187	case ARITH_GE_ATOM:
188	case ARITH_IS_INT_ATOM:
189	case ARITH_FLOOR:
190	case ARITH_CEIL:
191	case ARITH_ABS:
192	sharing_map_process_occurrence(map, index_of(integer_value_for_idx(map->terms, i)), i);	22,367✔
193	break;	22,367✔
194	case ARITH_ROOT_ATOM:	×
195	assert(false);
196	break;	×
197
198	case ITE_TERM:	272,168✔
199	case ITE_SPECIAL:
200	case APP_TERM:
201	case UPDATE_TERM:
202	case TUPLE_TERM:
203	case EQ_TERM:
204	case DISTINCT_TERM:
205	case FORALL_TERM:
206	case LAMBDA_TERM:
207	case OR_TERM:
208	case XOR_TERM:
209	case ARITH_BINEQ_ATOM:
210	case ARITH_RDIV:
211	case ARITH_IDIV:
212	case ARITH_MOD:
213	case ARITH_DIVIDES_ATOM:
214	case BV_ARRAY:
215	case BV_DIV:
216	case BV_REM:
217	case BV_SDIV:
218	case BV_SREM:
219	case BV_SMOD:
220	case BV_SHL:
221	case BV_LSHR:
222	case BV_ASHR:
223	case BV_EQ_ATOM:
224	case BV_GE_ATOM:
225	case BV_SGE_ATOM:
226	sharing_map_visit_composite(map, composite_for_idx(map->terms, i), i);	272,168✔
227	break;	272,168✔
228
229	case SELECT_TERM:	325,963✔
230	case BIT_TERM:
231	sharing_map_visit_select(map, select_for_idx(map->terms, i), i);	325,963✔
232	break;	325,963✔
233
234	case POWER_PRODUCT:	593✔
235	sharing_map_visit_pprod(map, pprod_for_idx(map->terms, i), i);	593✔
236	break;	593✔
237
238	case ARITH_POLY:	19,601✔
239	sharing_map_visit_poly(map, polynomial_for_idx(map->terms, i), i);	19,601✔
240	break;	19,601✔
241
242	case BV64_POLY:	12,108✔
243	sharing_map_visit_bvpoly64(map, bvpoly64_for_idx(map->terms, i), i);	12,108✔
244	break;	12,108✔
245
246	case BV_POLY:	610✔
247	sharing_map_visit_bvpoly(map, bvpoly_for_idx(map->terms, i), i);	610✔
248	break;	610✔
249
NEW 250	case ARITH_FF_CONSTANT:	×
251	case ARITH_FF_POLY:
252	case ARITH_FF_EQ_ATOM:
253	case ARITH_FF_BINEQ_ATOM:
254	assert(false);
NEW 255	break;	×
256
UNCOV 257	case UNUSED_TERM:	×
258	case RESERVED_TERM:
259	assert(false);
260	break;	×
261	}
262	}	704,230✔
263
264
265	/*
266	* Process term t:
267	* - all subterms of t are visited recursively and added the map
268	*/
269	void sharing_map_add_term(sharing_map_t *map, term_t t) {	94,935✔
270	int_queue_t *queue;
271	int32_t i;
272
273	queue = &map->queue;	94,935✔
274	assert(int_queue_is_empty(queue));
275
276	int_queue_push(queue, index_of(t));	94,935✔
277	while (! int_queue_is_empty(queue)) {	799,165✔
278	i = int_queue_pop(queue);	704,230✔
279	sharing_map_visit_subterms(map, i);	704,230✔
280	}
281	}	94,935✔
282
283
284	/*
285	* Process all terms in array a
286	* - n = size of the array
287	*/
288	void sharing_map_add_terms(sharing_map_t map, term_t a, uint32_t n) {	130,713✔
289	uint32_t i;
290
291	for (i=0; i<n; i++) {	225,648✔
292	sharing_map_add_term(map, a[i]);	94,935✔
293	}
294	}	130,713✔
295
296
297	/*
298	* Check whether t occurs more that once among all the terms visited so far
299	* - this returns false if t is not in the map or if t has been seen only once
300	*/
301	bool term_is_shared(sharing_map_t *map, term_t t) {	×
302	int_hmap_pair_t *r;
303	int32_t i;
304
305	i = index_of(t);	×
306	assert(good_term_idx(map->terms, i));
307
308	r = int_hmap_find(&map->hmap, i);	×
309	return r != NULL && r->val == bool_const;	×
310	}
311
312
313	/*
314	* Check whether t occurs once
315	* - this returns false if t is not in the map or if t has been visited more than once
316	*/
317	bool term_is_not_shared(sharing_map_t *map, term_t t) {	2,030✔
318	int_hmap_pair_t *r;
319	int32_t i;
320
321	i = index_of(t);	2,030✔
322	assert(good_term_idx(map->terms, i));
323
324	r = int_hmap_find(&map->hmap, i);	2,030✔
325	return r != NULL && r->val != bool_const;	2,030✔
326	}
327
328
329	/*
330	* Get the unique parent of t
331	* - if t has been seen only once, this returns t's parent as stored in map->hamp
332	* - if t has not been seen at all, this returns NULL_TERM
333	* - if t has more than once occurrences, this returns true_term (as a marker).
334	*/
335	term_t unique_parent(sharing_map_t *map, term_t t) {	×
336	int_hmap_pair_t *r;
337	int32_t i;
338	term_t parent;
339
340	i = index_of(t);	×
341	assert(good_term_idx(map->terms, i));
342
343	parent = NULL_TERM;	×
344	r = int_hmap_find(&map->hmap, i);	×
345	if (r != NULL) {	×
346	assert(r->key == i);
347	parent = pos_term(r->val);	×
348	}
349
350	return parent;	×
351	}
352

SRI-CSL / yices2 / 9226448713

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