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

71.43

/src/model/fun_maps.h

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

/*
 * Maps used as models by the function-theory solver
 * - a map is a finite list or pairs [index -> value]
 * - indices and values are represented as particles (see abstract_values.h)
 * - the indices in the list must be pairwise distinct
 * - the domain of a maps is the set of indices in the list
 * - each map may also be given a default value (i.e., what it maps to for
 *   indices outside its domain).
 */

#ifndef __FUN_MAPS_H
#define __FUN_MAPS_H

#include <stdint.h>
#include <assert.h>

#include "model/abstract_values.h"
#include "solvers/egraph/egraph_base_types.h"
#include "utils/int_vectors.h"

/*
 * Map object = array of pairs
 * - size = size of the array
 * - nelems = number of elements in the array
 * - def = default value (null_particle if no default is given)
 * - data = the array proper
 */
typedef struct map_elem_s {
  particle_t index;
  particle_t value;
} map_elem_t;

typedef struct map_s {
  uint32_t size;
  uint32_t nelems;
  particle_t def;
  map_elem_t *data;
} map_t;


#define DEF_MAP_SIZE 10
#define MAX_MAP_SIZE (UINT32_MAX/sizeof(map_elem_t))




/************************
 *  OPERATIONS ON MAPS  *
 ***********************/

/*
 * Create a map object of size n
 * - if n == 0, the default size is used
 * - the map is empty and has no default
 */
extern map_t *new_map(uint32_t n);


/*
 * Delete map
 */
extern void free_map(map_t *map);


/*
 * Set v as default value for map
 * - v must be non null
 */
static inline void set_map_default(map_t *map, particle_t v) {
  assert(v != null_particle);
  map->def = v;
}


/*
 * Add pair [index -> value] to map
 * - index must not occur in the map
 * - index and value must be non_null
 */
extern void add_elem_to_map(map_t *map, particle_t index, particle_t value);


/*
 * Normalize map:
 * - sort elements in increasing index order
 */
extern void normalize_map(map_t *map);


/*
 * Add pair [index -> value] to map and keep map normalized
 * - index must not occur in the map
 * - index and value must be non-null
 * - map must be normalized
 */
extern void add_elem_to_normal_map(map_t *map, particle_t index, particle_t value);



/*
 * Get the default value of map
 * - return null_particle if no default is specified
 */
static inline particle_t map_default_value(map_t *map) {
  return map->def;
}

/*
 * Get the number of pairs [index -> value] in map
 */
static inline uint32_t map_num_elems(map_t *map) {
  return map->nelems;
}


/*
 * Evaluate map at index k
 * - map must be normalized and k must be non-null
 * - if k is an index in map, return the corresponding value
 * - otherwise, if map has a default value return it
 * - otherwise return null_particle
 */
extern particle_t eval_map(map_t *map, particle_t k);



/*
 * Check whether map1 and map2 are equal
 * - the maps are considered equal if they have the same
 *   default value (or both have no default)
 *   and the same set of pairs [idx->value]
 * - both maps must be normalized
 */
extern bool equal_maps(map_t *map1, map_t *map2);


/*
 * Search for a point where map1 and map2 disagree.
 * - both maps must be normalized
 * - search for k in the domain of map1 and map2 such that
 *   eval_map(map1, k) != eval_map(map2, k)
 * - return k if it's found or null_particle otherwise
 */
extern particle_t disagreement_point(map_t *map1, map_t *map2);


/*
 * Search for a point that's in domain of map1 or map2
 * but not in both.
 * - both maps must be normalized
 * - return null_particle if map1 and map2 have the same domain
 */
extern particle_t distinguishing_point(map_t *map1, map_t *map2);


/*
 * Add all indices in the domain of map into vector v
 */
extern void collect_map_indices(map_t *map, ivector_t *v);


/*
 * Check whether index k is in the domain of map
 * - map must be normalized
 * - k must be non-null
 */
extern bool index_in_map_domain(map_t *map, particle_t k);




/*
 * Force maps map[0 ... n-1] to be all distinct by updating them.
 * - pstore = particle store to create fresh indices
 * - f = type descriptor for all the maps in the array
 *
 * Technique used:
 * - create fresh indices i_1,..,i_k in the domain of f
 * - create c values a_1,..., a_c in the range of f
 * such that (c ^ k) >= n.
 * Update map[t] by adding [i_1 -> a_t1, ..., i_k -> a_tk]
 * in such a way that (t1, ...., tk) differ from (u1, ..., uk) when u/=t.
 *
 * Return false if that's not possible (i.e., the number of functions
 * of the type f is finite and smaller than n).
 */
extern bool force_maps_to_differ(pstore_t *store, function_type_t *f, uint32_t n, map_t **map);


#endif /* __FUN_MAPS_H */

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	* Maps used as models by the function-theory solver
21	* - a map is a finite list or pairs [index -> value]
22	* - indices and values are represented as particles (see abstract_values.h)
23	* - the indices in the list must be pairwise distinct
24	* - the domain of a maps is the set of indices in the list
25	* - each map may also be given a default value (i.e., what it maps to for
26	* indices outside its domain).
27	*/
28
29	#ifndef __FUN_MAPS_H
30	#define __FUN_MAPS_H
31
32	#include <stdint.h>
33	#include <assert.h>
34
35	#include "model/abstract_values.h"
36	#include "solvers/egraph/egraph_base_types.h"
37	#include "utils/int_vectors.h"
38
39	/*
40	* Map object = array of pairs
41	* - size = size of the array
42	* - nelems = number of elements in the array
43	* - def = default value (null_particle if no default is given)
44	* - data = the array proper
45	*/
46	typedef struct map_elem_s {
47	particle_t index;
48	particle_t value;
49	} map_elem_t;
50
51	typedef struct map_s {
52	uint32_t size;
53	uint32_t nelems;
54	particle_t def;
55	map_elem_t *data;
56	} map_t;
57
58
59	#define DEF_MAP_SIZE 10
60	#define MAX_MAP_SIZE (UINT32_MAX/sizeof(map_elem_t))
61
62
63
64
65	/************************
66	* OPERATIONS ON MAPS *
67	***********************/
68
69	/*
70	* Create a map object of size n
71	* - if n == 0, the default size is used
72	* - the map is empty and has no default
73	*/
74	extern map_t *new_map(uint32_t n);
75
76
77	/*
78	* Delete map
79	*/
80	extern void free_map(map_t *map);
81
82
83	/*
84	* Set v as default value for map
85	* - v must be non null
86	*/
87	static inline void set_map_default(map_t *map, particle_t v) {	2,285✔
88	assert(v != null_particle);
89	map->def = v;	2,285✔
90	}	2,285✔
91
92
93	/*
94	* Add pair [index -> value] to map
95	* - index must not occur in the map
96	* - index and value must be non_null
97	*/
98	extern void add_elem_to_map(map_t *map, particle_t index, particle_t value);
99
100
101	/*
102	* Normalize map:
103	* - sort elements in increasing index order
104	*/
105	extern void normalize_map(map_t *map);
106
107
108	/*
109	* Add pair [index -> value] to map and keep map normalized
110	* - index must not occur in the map
111	* - index and value must be non-null
112	* - map must be normalized
113	*/
114	extern void add_elem_to_normal_map(map_t *map, particle_t index, particle_t value);
115
116
117
118	/*
119	* Get the default value of map
120	* - return null_particle if no default is specified
121	*/
122	static inline particle_t map_default_value(map_t *map) {	1,486✔
123	return map->def;	1,486✔
124	}
125
126	/*
127	* Get the number of pairs [index -> value] in map
128	*/
129	static inline uint32_t map_num_elems(map_t *map) {	×
130	return map->nelems;	×
131	}
132
133
134	/*
135	* Evaluate map at index k
136	* - map must be normalized and k must be non-null
137	* - if k is an index in map, return the corresponding value
138	* - otherwise, if map has a default value return it
139	* - otherwise return null_particle
140	*/
141	extern particle_t eval_map(map_t *map, particle_t k);
142
143
144
145	/*
146	* Check whether map1 and map2 are equal
147	* - the maps are considered equal if they have the same
148	* default value (or both have no default)
149	* and the same set of pairs [idx->value]
150	* - both maps must be normalized
151	*/
152	extern bool equal_maps(map_t map1, map_t map2);
153
154
155	/*
156	* Search for a point where map1 and map2 disagree.
157	* - both maps must be normalized
158	* - search for k in the domain of map1 and map2 such that
159	* eval_map(map1, k) != eval_map(map2, k)
160	* - return k if it's found or null_particle otherwise
161	*/
162	extern particle_t disagreement_point(map_t map1, map_t map2);
163
164
165	/*
166	* Search for a point that's in domain of map1 or map2
167	* but not in both.
168	* - both maps must be normalized
169	* - return null_particle if map1 and map2 have the same domain
170	*/
171	extern particle_t distinguishing_point(map_t map1, map_t map2);
172
173
174	/*
175	* Add all indices in the domain of map into vector v
176	*/
177	extern void collect_map_indices(map_t map, ivector_t v);
178
179
180	/*
181	* Check whether index k is in the domain of map
182	* - map must be normalized
183	* - k must be non-null
184	*/
185	extern bool index_in_map_domain(map_t *map, particle_t k);
186
187
188
189
190	/*
191	* Force maps map[0 ... n-1] to be all distinct by updating them.
192	* - pstore = particle store to create fresh indices
193	* - f = type descriptor for all the maps in the array
194	*
195	* Technique used:
196	* - create fresh indices i_1,..,i_k in the domain of f
197	* - create c values a_1,..., a_c in the range of f
198	* such that (c ^ k) >= n.
199	* Update map[t] by adding [i_1 -> a_t1, ..., i_k -> a_tk]
200	* in such a way that (t1, ...., tk) differ from (u1, ..., uk) when u/=t.
201	*
202	* Return false if that's not possible (i.e., the number of functions
203	* of the type f is finite and smaller than n).
204	*/
205	extern bool force_maps_to_differ(pstore_t store, function_type_t f, uint32_t n, map_t **map);
206
207
208	#endif /* __FUN_MAPS_H */

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