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

Coverage Stats

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

60.87

/src/model/models.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/>.
 */

/*
 * MODELS
 */

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

#include "model/models.h"
#include "utils/memalloc.h"


/*
 * Function to get the name of constant/uninterpreted terms
 * - we check in the term table
 */
static const char *name_of_const(term_table_t *terms, value_unint_t *d) {
  const char *s;
  term_t t;

  s = NULL;
  t = find_constant_term(terms, d->type, d->index);
  if (t != NULL_TERM) {
    s = term_name(terms, t);
  }

  return s;
}


/*
 * Initialize model
 * - terms = attached term table
 * - keep_subst = whether to support alias_map or not
 * - map and vtbl are given default sizes
 * - alias_map is NULL
 */
void init_model(model_t *model, term_table_t *terms, bool keep_subst) {
  init_value_table(&model->vtbl, 0, terms->types);
  value_table_set_namer(&model->vtbl, terms, (unint_namer_fun_t) name_of_const);

  init_int_hmap(&model->map, 0);
  model->alias_map = NULL;
  model->terms = terms;
  model->has_alias = keep_subst;

}


/*
 * Delete model: free all memory
 */
void delete_model(model_t *model) {
  delete_value_table(&model->vtbl);
  delete_int_hmap(&model->map);
  if (model->alias_map != NULL) {
    delete_int_hmap(model->alias_map);
    safe_free(model->alias_map);
    model->alias_map = NULL;
  }
}



/*
 * Find the value of term t in model
 * - return null_value if t is not mapped to anything
 * - return the concrete object mapped to t otherwise
 */
value_t model_find_term_value(model_t *model, term_t t) {
  int_hmap_pair_t *r;

  assert(good_term(model->terms, t));

  r = int_hmap_find(&model->map, t);
  if (r == NULL) {
    return null_value;
  } else {
    return r->val;
  }
}



/*
 * Check whether t is mapped to a term v in the substitution table.
 * - return v if it is
 * - return NULL_TERM otherwise
 */
term_t model_find_term_substitution(model_t *model, term_t t) {
  int_hmap_t *alias;
  int_hmap_pair_t *r;

  assert(good_term(model->terms, t) && model->has_alias);
  alias = model->alias_map;
  if (alias != NULL) {
    r = int_hmap_find(alias, t);
    if (r != NULL) {
      return r->val;
    }
  }

  return NULL_TERM;
}




/*
 * Store the mapping t := v in model
 * - t must not be mapped to anything
 * - v must be a valid object created in model->vtbl.
 *
 * If v is a function object and it has no name, then t's name is
 * given to v.
 */
void model_map_term(model_t *model, term_t t, value_t v) {
  int_hmap_pair_t *r;
  value_table_t *vtbl;
  char *name;

  assert(good_term(model->terms, t));

  r = int_hmap_get(&model->map, t);
  assert(r->val < 0);
  r->val = v;

  // copy t's name if any
  name = term_name(model->terms, t);
  if (name != NULL) {
    vtbl = &model->vtbl;
    if (object_is_function(vtbl, v) && vtbl_function(vtbl, v)->name == NULL) {
      vtbl_set_function_name(vtbl, v, name);
    }
  }
}





/*
 * Store the substitution t --> u in the model
 * - t and u must be valid term indices
 * - t must be an uninterpreted term, not mapped to anything
 */
void model_add_substitution(model_t *model, term_t t, term_t u) {
  int_hmap_t *alias;
  int_hmap_pair_t *r;

  assert(term_kind(model->terms, t) == UNINTERPRETED_TERM &&
         good_term(model->terms, u) && t != u && model->has_alias &&
         int_hmap_find(&model->map, t) == NULL);

  alias = model->alias_map;
  if (alias == NULL) {
    alias = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t));
    init_int_hmap(alias, 0); // default size
    model->alias_map = alias;
  }

  r = int_hmap_get(alias, t);
  assert(r->val < 0);
  r->val = u;
}


/*
 * ITERATOR
 */

/*
 * Iteration: call f(aux, t) for every term t stored in the model
 * - this includes every t in model->map (term mapped to a value)
 * - if all is true, then the iterator is applied to every t in the domain
 *   of model->alias (term mapped to another term)
 * - f must not have side effects on model
 */
void model_term_iterate(model_t *model, bool all, void *aux, model_iterator_t f) {
  int_hmap_t *hmap;
  int_hmap_pair_t *r;

  hmap = &model->map;
  r = int_hmap_first_record(hmap);
  while (r != NULL) {
    f(aux, r->key);
    r = int_hmap_next_record(hmap, r);
  }

  hmap = model->alias_map;
  if (all && hmap != NULL) {
    r = int_hmap_first_record(hmap);
    while (r != NULL) {
      f(aux, r->key);
      r = int_hmap_next_record(hmap, r);
    }
  }
}


/*
 * Collect all terms that satisfy predicate f
 * - add them to vector v
 * - if f(aux, t) returns true, add t to vector v
 * - if all is false, only the terms in model->map are considered
 * - if all is true, the terms in model->map and model->alias are considered
 * - f must not have side effects
 *
 * - v is not reset. All terms collected are added to v
 */
void model_collect_terms(model_t *model, bool all, void *aux, model_filter_t f, ivector_t *v) {
  int_hmap_t *hmap;
  int_hmap_pair_t *r;

  hmap = &model->map;
  r = int_hmap_first_record(hmap);
  while (r != NULL) {
    if (f(aux, r->key)) {
      ivector_push(v, r->key);
    }
    r = int_hmap_next_record(hmap, r);
  }

  hmap = model->alias_map;
  if (all && hmap != NULL) {
    r = int_hmap_first_record(hmap);
    while (r != NULL) {
      if (f(aux, r->key)) {
        ivector_push(v, r->key);
      }
      r = int_hmap_next_record(hmap, r);
    }
  }
}



/*
 * GARBAGE COLLECTION SUPPORT
 */

/*
 * Marker for records in a model's map: every record
 * is a pair <key, value> where key is a term.
 * - aux is the term table where key is defined
 */
static void mdl_mark_map(void *aux, const int_hmap_pair_t *r) {
  term_table_set_gc_mark(aux, index_of(r->key));
}

/*
 * Marker for records in a model's alias_map: every record
 * is a pair <key, value> where both key and value are terms
 * - aux is the term table
 */
static void mdl_mark_alias(void *aux, const int_hmap_pair_t *r) {
  assert(r->val >= 0);
  term_table_set_gc_mark(aux, index_of(r->key));
  term_table_set_gc_mark(aux, index_of(r->val));
}


/*
 * Prepare for garbage collection: mark all the terms present in model
 * - all marked terms will be considered as roots on the next call
 *   to term_table_gc
 */
void model_gc_mark(model_t *model) {
  int_hmap_iterate(&model->map, model->terms, mdl_mark_map);
  if (model->alias_map != NULL) {
    int_hmap_iterate(model->alias_map, model->terms, mdl_mark_alias);
  }
}




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	* MODELS
21	*/
22
23	#include <assert.h>
24	#include <inttypes.h>
25	#include <string.h>
26
27	#include "model/models.h"
28	#include "utils/memalloc.h"
29
30
31	/*
32	* Function to get the name of constant/uninterpreted terms
33	* - we check in the term table
34	*/
35	static const char name_of_const(term_table_t terms, value_unint_t *d) {	×
36	const char *s;
37	term_t t;
38
39	s = NULL;	×
40	t = find_constant_term(terms, d->type, d->index);	×
41	if (t != NULL_TERM) {	×
42	s = term_name(terms, t);	×
43	}
44
45	return s;	×
46	}
47
48
49	/*
50	* Initialize model
51	* - terms = attached term table
52	* - keep_subst = whether to support alias_map or not
53	* - map and vtbl are given default sizes
54	* - alias_map is NULL
55	*/
56	void init_model(model_t model, term_table_t terms, bool keep_subst) {	30,883✔
57	init_value_table(&model->vtbl, 0, terms->types);	30,883✔
58	value_table_set_namer(&model->vtbl, terms, (unint_namer_fun_t) name_of_const);	30,883✔
59
60	init_int_hmap(&model->map, 0);	30,883✔
61	model->alias_map = NULL;	30,883✔
62	model->terms = terms;	30,883✔
63	model->has_alias = keep_subst;	30,883✔
64
65	}	30,883✔
66
67
68	/*
69	* Delete model: free all memory
70	*/
71	void delete_model(model_t *model) {	30,883✔
72	delete_value_table(&model->vtbl);	30,883✔
73	delete_int_hmap(&model->map);	30,883✔
74	if (model->alias_map != NULL) {	30,883✔
75	delete_int_hmap(model->alias_map);	18✔
76	safe_free(model->alias_map);	18✔
77	model->alias_map = NULL;	18✔
78	}
79	}	30,883✔
80
81
82
83	/*
84	* Find the value of term t in model
85	* - return null_value if t is not mapped to anything
86	* - return the concrete object mapped to t otherwise
87	*/
88	value_t model_find_term_value(model_t *model, term_t t) {	3,496,558✔
89	int_hmap_pair_t *r;
90
91	assert(good_term(model->terms, t));
92
93	r = int_hmap_find(&model->map, t);	3,496,558✔
94	if (r == NULL) {	3,496,558✔
95	return null_value;	2,526,331✔
96	} else {
97	return r->val;	970,227✔
98	}
99	}
100
101
102
103	/*
104	* Check whether t is mapped to a term v in the substitution table.
105	* - return v if it is
106	* - return NULL_TERM otherwise
107	*/
108	term_t model_find_term_substitution(model_t *model, term_t t) {	17,004✔
109	int_hmap_t *alias;
110	int_hmap_pair_t *r;
111
112	assert(good_term(model->terms, t) && model->has_alias);
113	alias = model->alias_map;	17,004✔
114	if (alias != NULL) {	17,004✔
115	r = int_hmap_find(alias, t);	749✔
116	if (r != NULL) {	749✔
117	return r->val;	725✔
118	}
119	}
120
121	return NULL_TERM;	16,279✔
122	}
123
124
125
126
127	/*
128	* Store the mapping t := v in model
129	* - t must not be mapped to anything
130	* - v must be a valid object created in model->vtbl.
131	*
132	* If v is a function object and it has no name, then t's name is
133	* given to v.
134	*/
135	void model_map_term(model_t *model, term_t t, value_t v) {	198,622✔
136	int_hmap_pair_t *r;
137	value_table_t *vtbl;
138	char *name;
139
140	assert(good_term(model->terms, t));
141
142	r = int_hmap_get(&model->map, t);	198,622✔
143	assert(r->val < 0);
144	r->val = v;	198,622✔
145
146	// copy t's name if any
147	name = term_name(model->terms, t);	198,622✔
148	if (name != NULL) {	198,622✔
149	vtbl = &model->vtbl;	198,622✔
150	if (object_is_function(vtbl, v) && vtbl_function(vtbl, v)->name == NULL) {	198,622✔
151	vtbl_set_function_name(vtbl, v, name);	931✔
152	}
153	}
154	}	198,622✔
155
156
157
158
159
160	/*
161	* Store the substitution t --> u in the model
162	* - t and u must be valid term indices
163	* - t must be an uninterpreted term, not mapped to anything
164	*/
165	void model_add_substitution(model_t *model, term_t t, term_t u) {	648✔
166	int_hmap_t *alias;
167	int_hmap_pair_t *r;
168
169	assert(term_kind(model->terms, t) == UNINTERPRETED_TERM &&
170	good_term(model->terms, u) && t != u && model->has_alias &&
171	int_hmap_find(&model->map, t) == NULL);
172
173	alias = model->alias_map;	648✔
174	if (alias == NULL) {	648✔
175	alias = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t));	18✔
176	init_int_hmap(alias, 0); // default size	18✔
177	model->alias_map = alias;	18✔
178	}
179
180	r = int_hmap_get(alias, t);	648✔
181	assert(r->val < 0);
182	r->val = u;	648✔
183	}	648✔
184
185
186	/*
187	* ITERATOR
188	*/
189
190	/*
191	* Iteration: call f(aux, t) for every term t stored in the model
192	* - this includes every t in model->map (term mapped to a value)
193	* - if all is true, then the iterator is applied to every t in the domain
194	* of model->alias (term mapped to another term)
195	* - f must not have side effects on model
196	*/
197	void model_term_iterate(model_t model, bool all, void aux, model_iterator_t f) {	×
198	int_hmap_t *hmap;
199	int_hmap_pair_t *r;
200
201	hmap = &model->map;	×
202	r = int_hmap_first_record(hmap);	×
203	while (r != NULL) {	×
204	f(aux, r->key);	×
205	r = int_hmap_next_record(hmap, r);	×
206	}
207
208	hmap = model->alias_map;	×
209	if (all && hmap != NULL) {	×
210	r = int_hmap_first_record(hmap);	×
211	while (r != NULL) {	×
212	f(aux, r->key);	×
213	r = int_hmap_next_record(hmap, r);	×
214	}
215	}
216	}	×
217
218
219	/*
220	* Collect all terms that satisfy predicate f
221	* - add them to vector v
222	* - if f(aux, t) returns true, add t to vector v
223	* - if all is false, only the terms in model->map are considered
224	* - if all is true, the terms in model->map and model->alias are considered
225	* - f must not have side effects
226	*
227	* - v is not reset. All terms collected are added to v
228	*/
229	void model_collect_terms(model_t model, bool all, void aux, model_filter_t f, ivector_t *v) {	2✔
230	int_hmap_t *hmap;
231	int_hmap_pair_t *r;
232
233	hmap = &model->map;	2✔
234	r = int_hmap_first_record(hmap);	2✔
235	while (r != NULL) {	6✔
236	if (f(aux, r->key)) {	4✔
237	ivector_push(v, r->key);	4✔
238	}
239	r = int_hmap_next_record(hmap, r);	4✔
240	}
241
242	hmap = model->alias_map;	2✔
243	if (all && hmap != NULL) {	2✔
244	r = int_hmap_first_record(hmap);	×
245	while (r != NULL) {	×
246	if (f(aux, r->key)) {	×
247	ivector_push(v, r->key);	×
248	}
249	r = int_hmap_next_record(hmap, r);	×
250	}
251	}
252	}	2✔
253
254
255
256	/*
257	* GARBAGE COLLECTION SUPPORT
258	*/
259
260	/*
261	* Marker for records in a model's map: every record
262	* is a pair <key, value> where key is a term.
263	* - aux is the term table where key is defined
264	*/
265	static void mdl_mark_map(void aux, const int_hmap_pair_t r) {	×
266	term_table_set_gc_mark(aux, index_of(r->key));	×
267	}	×
268
269	/*
270	* Marker for records in a model's alias_map: every record
271	* is a pair <key, value> where both key and value are terms
272	* - aux is the term table
273	*/
274	static void mdl_mark_alias(void aux, const int_hmap_pair_t r) {	×
275	assert(r->val >= 0);
276	term_table_set_gc_mark(aux, index_of(r->key));	×
277	term_table_set_gc_mark(aux, index_of(r->val));	×
278	}	×
279
280
281	/*
282	* Prepare for garbage collection: mark all the terms present in model
283	* - all marked terms will be considered as roots on the next call
284	* to term_table_gc
285	*/
286	void model_gc_mark(model_t *model) {	×
287	int_hmap_iterate(&model->map, model->terms, mdl_mark_map);	×
288	if (model->alias_map != NULL) {	×
289	int_hmap_iterate(model->alias_map, model->terms, mdl_mark_alias);	×
290	}
291	}	×
292
293
294

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