23882467517

Committed 02 Apr 2026 03:34AM UTC coverage: 66.728% (+0.2%) from 66.539%

Build # 23882467517

Build Type

Pull #611

github

Committed by

web-flow

Commit Message

Merge branch 'master' into mcsat-supplement-cdclt

Pull Request Pull Request #611: Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

Coverage Stats

690 of 1006 new or added lines in 15 files covered. (68.59%)

2 existing lines in 2 files now uncovered.

84087 of 126014 relevant lines covered (66.73%)

1691640.28 hits per line

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

84.0

/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_root_atom(sharing_map_t *map, root_atom_t *c, int32_t p) {
  assert(c == root_atom_for_idx(map->terms, p));
  sharing_map_process_occurrence(map, index_of(c->x), p);
  sharing_map_process_occurrence(map, index_of(c->p), p);
}

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

SRI-CSL / yices2 / 23882467517

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