12367760548

Committed 17 Dec 2024 06:41AM UTC coverage: 65.285% (-0.6%) from 65.92%

Build # 12367760548

Build Type

push

github

Committed by

web-flow

Commit Message

Fixes GitHub coverage issue (#544)

* Update action.yml

* Update action.yml

Run Details

81020 of 124102 relevant lines covered (65.29%)

1509382.01 hits per line

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

26.92

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

/*
 * QUERIES TO GET THE VALUE OF ONE OR MORE TERMS IN A MODEL
 */

#include "model/model_eval.h"
#include "model/model_queries.h"
#include "model/model_support.h"
#include "utils/memalloc.h"


/*
 * Get the value of t in mdl
 * - this function first tries a simple lookup in mdl. If that fails,
 *   it computes t's value in mdl (cf. model_eval.h).
 * - t must be a valid term
 *
 * Returns a negative number if t's value can't be computed
 *    -1  means that the value is not known
 *    other values are evaluation errors defined in model_eval.h
 *
 * Returns an index in mdl->vtbl otherwise (concrete value).
 */
value_t model_get_term_value(model_t *mdl, term_t t) {
  evaluator_t evaluator;
  value_t v;

  v = model_find_term_value(mdl, t);
  if (v == null_value) {
    init_evaluator(&evaluator, mdl);
    v = eval_in_model(&evaluator, t);
    delete_evaluator(&evaluator);
  }

  return v;
}


/*
 * Check whether f is true in mdl
 * - f must be a Boolean term
 * - this returns false if the evaluation fails and stores the error code in *code
 */
bool formula_holds_in_model(model_t *mdl, term_t f, int32_t *code) {
  value_t v;
  bool answer;

  assert(is_boolean_term(mdl->terms, f));

  answer = false;
  v = model_get_term_value(mdl, f);
  if (v < 0) {
    // evaluation error
    *code = v;
  } else {
    *code = 0;
    answer = is_true(model_get_vtbl(mdl), v);
  }

  return answer;
}



/*
 * Compute the values of a[0 ... n-1] in mdl
 * - store the result in b[0 ... n-1]
 * - return a negative code if this fails for some a[i]
 * - return 0 otherwise.
 */
int32_t evaluate_term_array(model_t *mdl, uint32_t n, const term_t a[], value_t b[]) {
  evaluator_t evaluator;
  uint32_t i, k;
  value_t v;

  /*
   * First pass: simple eval of all terms.
   * - k = number of terms, for which this fails
   * - if simple eval fails for a[i], we have b[i] = null_value
   */
  k = 0;
  for (i=0; i<n; i++) {
    v = model_find_term_value(mdl, a[i]);
    b[i] = v;
    if (v < 0) {
      assert(v == null_value);
      k ++;
    }
  }

  /*
   * Second pass: if k > 0, use the evaluator to complete array b
   * Stop on the first error if any
   */
  if (k > 0) {
    init_evaluator(&evaluator, mdl);
    for (i=0; i<n; i++) {
      if (b[i] < 0) {
        v = eval_in_model(&evaluator, a[i]);
        b[i] = v;
        if (v < 0) break;
      }
    }
    delete_evaluator(&evaluator);
    if (v < 0) {
      return v;
    }
  }

  return 0;
}


/*
 * Checks whether mdl is a model of a[0 ... n-1]
 * - sets *code to 0 if the evaluation succeeds
 * - returns false if the evaluation fails for some a[i] and stores
 *   the corresponding error code in *code
 */
bool formulas_hold_in_model(model_t *mdl, uint32_t n, const term_t a[], int32_t *code) {
  evaluator_t evaluator;
  value_table_t *vtbl;
  uint32_t i;
  value_t v;
  bool answer;

  answer = true;
  *code = 0;

  vtbl = model_get_vtbl(mdl);
  init_evaluator(&evaluator, mdl);
  for (i=0; i<n; i++) {
    assert(is_boolean_term(mdl->terms, a[i]));
    v = eval_in_model(&evaluator, a[i]);
    if (v < 0) {
      answer = false;
      *code = v;
      break;
    }
    if (! is_true(vtbl, v)) {
      answer = false;
      break;
    }
  }
  delete_evaluator(&evaluator);

  return answer;
}



/*
 * Filter used below:
 * - aux is a term table
 * - t is relevant if it's uninterpreted and has a name
 */
static bool term_is_relevant(void *aux, term_t t) {
  return is_pos_term(t) && term_kind(aux, t) == UNINTERPRETED_TERM && term_name(aux, t) != NULL;
}

/*
 * Get a list of all variables that have a value in the model
 * - these variables are store into vector *v
 */
void model_get_relevant_vars(model_t *mdl, ivector_t *v) {
  evaluator_t eval;

  ivector_reset(v);
  if (mdl->has_alias && mdl->alias_map != NULL) {
    init_evaluator(&eval, mdl);

    /*
     * We use two passes to find all relevant terms:
     * 1) in the first pass, we compute the value of all terms
     *    in the model's alias table.
     * 2) in the second pass, we collect all terms that have
     *    received a value in the first pass.
     *
     * This is necessary in situations like this:
     *   (assert (= x  (.. y ..)))
     * and y does not occur anywhere else.
     * During model construction, we store [x --> (... y ...)]
     * in the model's alias table (so x is known to be relevant).
     * When we compute x's value in phase 1, we also assign a value
     * to y so y is relevant, and its value must be printed.
     *
     * The second pass makes sure that y is found.
     */
    model_collect_terms(mdl, true, mdl->terms, term_is_relevant, v);

    // compute their values
    eval_terms_in_model(&eval, v->data, v->size);

    // second pass: collect all uninterpreted terms that
    // have a value in model or in the evaluator.
    ivector_reset(v);
    model_collect_terms(mdl, false, mdl->terms, term_is_relevant, v);
    evaluator_collect_cached_terms(&eval, mdl->terms, term_is_relevant, v);
    delete_evaluator(&eval);

  } else {
    model_collect_terms(mdl, false, mdl->terms, term_is_relevant, v);
  }
}

/*
 * Copy content of harray_t *s into vector v
 */
static inline void copy_harray_to_vector(const harray_t *s, ivector_t *v) {
  assert(s != NULL);
  ivector_copy(v, s->data, s->nelems);
}

/*
 * Collect the support of term t in model mdl
 * - the variables are added to vector *v
 * - the support of t is a set of variables x_1, ..., x_n
 *   such that the value of t in mdl is determined by the values
 *   of x_1, ..., x_n in mdl.
 */
void model_get_term_support(model_t *mdl, term_t t, ivector_t *v) {
  support_constructor_t sup;
  harray_t *s;

  init_support_constructor(&sup, mdl);
  s = get_term_support(&sup, t);
  copy_harray_to_vector(s, v);
  delete_support_constructor(&sup);
}


/*
 * Collect the support of terms a[0 ... n-1] in model mdl
 * - the variables are added to vector *v
 * - the support of t is a set of variables x_1, ..., x_n
 *   such that the values of a[0], ..., a[n] in mdl are determined by
 *   the value of x_1, ..., x_n in mdl.
 */
void model_get_terms_support(model_t *mdl, uint32_t n, const term_t  a[], ivector_t *v) {
  support_constructor_t sup;
  harray_t *s;

  init_support_constructor(&sup, mdl);
  s = get_term_array_support(&sup, a, n);
  copy_harray_to_vector(s, v);
  delete_support_constructor(&sup);
}

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	* QUERIES TO GET THE VALUE OF ONE OR MORE TERMS IN A MODEL
21	*/
22
23	#include "model/model_eval.h"
24	#include "model/model_queries.h"
25	#include "model/model_support.h"
26	#include "utils/memalloc.h"
27
28
29	/*
30	* Get the value of t in mdl
31	* - this function first tries a simple lookup in mdl. If that fails,
32	* it computes t's value in mdl (cf. model_eval.h).
33	* - t must be a valid term
34	*
35	* Returns a negative number if t's value can't be computed
36	* -1 means that the value is not known
37	* other values are evaluation errors defined in model_eval.h
38	*
39	* Returns an index in mdl->vtbl otherwise (concrete value).
40	*/
41	value_t model_get_term_value(model_t *mdl, term_t t) {	889✔
42	evaluator_t evaluator;
43	value_t v;
44
45	v = model_find_term_value(mdl, t);	889✔
46	if (v == null_value) {	889✔
47	init_evaluator(&evaluator, mdl);	×
48	v = eval_in_model(&evaluator, t);	×
49	delete_evaluator(&evaluator);	×
50	}
51
52	return v;	889✔
53	}
54
55
56	/*
57	* Check whether f is true in mdl
58	* - f must be a Boolean term
59	* - this returns false if the evaluation fails and stores the error code in *code
60	*/
61	bool formula_holds_in_model(model_t mdl, term_t f, int32_t code) {	×
62	value_t v;
63	bool answer;
64
65	assert(is_boolean_term(mdl->terms, f));
66
67	answer = false;	×
68	v = model_get_term_value(mdl, f);	×
69	if (v < 0) {	×
70	// evaluation error
71	*code = v;	×
72	} else {
73	*code = 0;	×
74	answer = is_true(model_get_vtbl(mdl), v);	×
75	}
76
77	return answer;	×
78	}
79
80
81
82	/*
83	* Compute the values of a[0 ... n-1] in mdl
84	* - store the result in b[0 ... n-1]
85	* - return a negative code if this fails for some a[i]
86	* - return 0 otherwise.
87	*/
88	int32_t evaluate_term_array(model_t *mdl, uint32_t n, const term_t a[], value_t b[]) {	30,133✔
89	evaluator_t evaluator;
90	uint32_t i, k;
91	value_t v;
92
93	/*
94	* First pass: simple eval of all terms.
95	* - k = number of terms, for which this fails
96	* - if simple eval fails for a[i], we have b[i] = null_value
97	*/
98	k = 0;	30,133✔
99	for (i=0; i<n; i++) {	124,446✔
100	v = model_find_term_value(mdl, a[i]);	94,313✔
101	b[i] = v;	94,313✔
102	if (v < 0) {	94,313✔
103	assert(v == null_value);
104	k ++;	1,589✔
105	}
106	}
107
108	/*
109	* Second pass: if k > 0, use the evaluator to complete array b
110	* Stop on the first error if any
111	*/
112	if (k > 0) {	30,133✔
113	init_evaluator(&evaluator, mdl);	296✔
114	for (i=0; i<n; i++) {	15,208✔
115	if (b[i] < 0) {	14,912✔
116	v = eval_in_model(&evaluator, a[i]);	1,589✔
117	b[i] = v;	1,589✔
118	if (v < 0) break;	1,589✔
119	}
120	}
121	delete_evaluator(&evaluator);	296✔
122	if (v < 0) {	296✔
123	return v;	×
124	}
125	}
126
127	return 0;	30,133✔
128	}
129
130
131	/*
132	* Checks whether mdl is a model of a[0 ... n-1]
133	* - sets *code to 0 if the evaluation succeeds
134	* - returns false if the evaluation fails for some a[i] and stores
135	* the corresponding error code in *code
136	*/
137	bool formulas_hold_in_model(model_t mdl, uint32_t n, const term_t a[], int32_t code) {	×
138	evaluator_t evaluator;
139	value_table_t *vtbl;
140	uint32_t i;
141	value_t v;
142	bool answer;
143
144	answer = true;	×
145	*code = 0;	×
146
147	vtbl = model_get_vtbl(mdl);	×
148	init_evaluator(&evaluator, mdl);	×
149	for (i=0; i<n; i++) {	×
150	assert(is_boolean_term(mdl->terms, a[i]));
151	v = eval_in_model(&evaluator, a[i]);	×
152	if (v < 0) {	×
153	answer = false;	×
154	*code = v;	×
155	break;	×
156	}
157	if (! is_true(vtbl, v)) {	×
158	answer = false;	×
159	break;	×
160	}
161	}
162	delete_evaluator(&evaluator);	×
163
164	return answer;	×
165	}
166
167
168
169	/*
170	* Filter used below:
171	* - aux is a term table
172	* - t is relevant if it's uninterpreted and has a name
173	*/
174	static bool term_is_relevant(void *aux, term_t t) {	×
175	return is_pos_term(t) && term_kind(aux, t) == UNINTERPRETED_TERM && term_name(aux, t) != NULL;	×
176	}
177
178	/*
179	* Get a list of all variables that have a value in the model
180	* - these variables are store into vector *v
181	*/
182	void model_get_relevant_vars(model_t mdl, ivector_t v) {	×
183	evaluator_t eval;
184
185	ivector_reset(v);	×
186	if (mdl->has_alias && mdl->alias_map != NULL) {	×
187	init_evaluator(&eval, mdl);	×
188
189	/*
190	* We use two passes to find all relevant terms:
191	* 1) in the first pass, we compute the value of all terms
192	* in the model's alias table.
193	* 2) in the second pass, we collect all terms that have
194	* received a value in the first pass.
195	*
196	* This is necessary in situations like this:
197	* (assert (= x (.. y ..)))
198	* and y does not occur anywhere else.
199	* During model construction, we store [x --> (... y ...)]
200	* in the model's alias table (so x is known to be relevant).
201	* When we compute x's value in phase 1, we also assign a value
202	* to y so y is relevant, and its value must be printed.
203	*
204	* The second pass makes sure that y is found.
205	*/
206	model_collect_terms(mdl, true, mdl->terms, term_is_relevant, v);	×
207
208	// compute their values
209	eval_terms_in_model(&eval, v->data, v->size);	×
210
211	// second pass: collect all uninterpreted terms that
212	// have a value in model or in the evaluator.
213	ivector_reset(v);	×
214	model_collect_terms(mdl, false, mdl->terms, term_is_relevant, v);	×
215	evaluator_collect_cached_terms(&eval, mdl->terms, term_is_relevant, v);	×
216	delete_evaluator(&eval);	×
217
218	} else {
219	model_collect_terms(mdl, false, mdl->terms, term_is_relevant, v);	×
220	}
221	}	×
222
223	/*
224	* Copy content of harray_t *s into vector v
225	*/
226	static inline void copy_harray_to_vector(const harray_t s, ivector_t v) {	×
227	assert(s != NULL);
228	ivector_copy(v, s->data, s->nelems);	×
229	}	×
230
231	/*
232	* Collect the support of term t in model mdl
233	* - the variables are added to vector *v
234	* - the support of t is a set of variables x_1, ..., x_n
235	* such that the value of t in mdl is determined by the values
236	* of x_1, ..., x_n in mdl.
237	*/
238	void model_get_term_support(model_t mdl, term_t t, ivector_t v) {	×
239	support_constructor_t sup;
240	harray_t *s;
241
242	init_support_constructor(&sup, mdl);	×
243	s = get_term_support(&sup, t);	×
244	copy_harray_to_vector(s, v);	×
245	delete_support_constructor(&sup);	×
246	}	×
247
248
249	/*
250	* Collect the support of terms a[0 ... n-1] in model mdl
251	* - the variables are added to vector *v
252	* - the support of t is a set of variables x_1, ..., x_n
253	* such that the values of a[0], ..., a[n] in mdl are determined by
254	* the value of x_1, ..., x_n in mdl.
255	*/
256	void model_get_terms_support(model_t mdl, uint32_t n, const term_t a[], ivector_t v) {	×
257	support_constructor_t sup;
258	harray_t *s;
259
260	init_support_constructor(&sup, mdl);	×
261	s = get_term_array_support(&sup, a, n);	×
262	copy_harray_to_vector(s, v);	×
263	delete_support_constructor(&sup);	×
264	}	×

SRI-CSL / yices2 / 12367760548

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