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 * Test normalization of functions with finite domains
21 */
22
23 #include <inttypes.h>
24 #include <stdio.h>
25 #include <assert.h>
26
27 #include "io/concrete_value_printer.h"
28 #include "io/type_printer.h"
29 #include "model/concrete_values.h"
30 #include "terms/types.h"
31
32 static type_table_t types;
33 static value_table_t vtbl;
34
35
36 /*
37 * Short cuts: type constructors
38 */
pair_type(type_t a,type_t b)39 static type_t pair_type(type_t a, type_t b) {
40 type_t aux[2];
41
42 aux[0] = a;
43 aux[1] = b;
44 return tuple_type(&types, 2, aux);
45 }
46
47 // [a -> b]
fun_type1(type_t a,type_t b)48 static type_t fun_type1(type_t a, type_t b) {
49 return function_type(&types, b, 1, &a);
50 }
51
52 /*
53 * Base types: all finite and small
54 */
55 #define NUM_BASE_TYPES 10
56
57 static type_t base[NUM_BASE_TYPES];
58
init_base_types(void)59 static void init_base_types(void) {
60 base[0] = bool_type(&types); // bool
61 base[1] = bv_type(&types, 5); // bv5
62 base[2] = new_scalar_type(&types, 3); // scalar3
63 base[3] = new_scalar_type(&types, 1); // scalar1
64 base[4] = pair_type(base[0], base[2]); // bool x scalar3
65 base[5] = pair_type(base[3], base[0]); // scalar1 x bool
66 base[6] = fun_type1(base[0], base[2]); // [bool -> scalar3]
67 base[7] = fun_type1(base[0], base[3]); // [bool -> scalar1]
68 base[8] = fun_type1(base[2], base[0]); // [scalar3 -> bool]
69 base[9] = fun_type1(base[3], base[0]); // [scalar1 -> bool]
70 }
71
72
73 /*
74 * Integer objects (range of the functions)
75 */
76 #define NVALS 4
77
78 static value_t val[NVALS];
79
init_val(void)80 static void init_val(void) {
81 int32_t i;
82
83 for (i=0; i<NVALS; i++) {
84 val[i] = vtbl_mk_int32(&vtbl, i);
85 }
86 }
87
88
89 /*
90 * Buffers for building functions
91 */
92 #define BUFFER_SIZE 1024
93
94 static value_t buffer1[BUFFER_SIZE];
95 static value_t buffer2[BUFFER_SIZE];
96
97
98 /*
99 * Mapping element: for function of type [tau[0] x ... x tau[n-1] --> int]
100 * - i = index of an element in the domain
101 * - v = what's mapped to that element
102 */
make_mapping(type_t * tau,uint32_t n,uint32_t i,value_t v)103 static value_t make_mapping(type_t *tau, uint32_t n, uint32_t i, value_t v) {
104 value_t aux[4];
105
106 assert(n <= 4 && good_object(&vtbl, v));
107
108 vtbl_gen_object_tuple(&vtbl, n, tau, i, aux);
109 return vtbl_mk_map(&vtbl, n, aux, v);
110 }
111
112 /*
113 * Build the function defined by tau, n, range, rsize, default
114 * - n = arity
115 * - tau[0 ... n-1] = domain type
116 * - rsize = size of range
117 * - def = default value to use
118 * - all elements in range[0 ... rsize - 1] must be integers
119 *
120 * The function maps element of index i in domain to range[i].
121 */
make_function(type_t * tau,uint32_t n,value_t * range,uint32_t rsize,value_t def)122 static value_t make_function(type_t *tau, uint32_t n,
123 value_t *range, uint32_t rsize, value_t def) {
124 value_t *map;
125 value_t v;
126 uint32_t i, j;
127 type_t ftype;
128
129 assert(n <= 4 && rsize <= BUFFER_SIZE);
130 map = buffer2;
131
132 j = 0;
133 for (i=0; i<rsize; i++) {
134 if (range[i] != def) {
135 map[j] = make_mapping(tau, n, i, range[i]);
136 j ++;
137 }
138 }
139
140 ftype = function_type(&types, int_type(&types), n, tau);
141 v = vtbl_mk_function(&vtbl, ftype, j, map, def);
142
143 return v;
144 }
145
146
147 /*
148 * Test different constructions for the same function
149 * - tau[0...n-1] = domain type
150 * - n = arity
151 * - range = array of size equal to card(domain of tau)
152 * - the function maps x_i to range[i]
153 * where x_i is the i-th tuple in domain of tau
154 */
test_function(type_t * tau,uint32_t n,value_t * range)155 static void test_function(type_t *tau, uint32_t n, value_t *range) {
156 value_t f[NVALS];
157 uint32_t dsize, i;
158 type_t ftype;
159
160 ftype = function_type(&types, int_type(&types), n, tau);
161 dsize = card_of_domain_type(&types, ftype);
162 if (dsize > BUFFER_SIZE) return;
163
164 printf("=== testing function of type ");
165 print_type(stdout, &types, ftype);
166 printf(" ===\n");
167
168 for (i=0; i<NVALS; i++) {
169 f[i] = make_function(tau, n, range, dsize, val[i]);
170 printf("using default: ");
171 vtbl_print_object(stdout, &vtbl, val[i]);
172 printf("\nresult:\n");
173 vtbl_print_object(stdout, &vtbl, f[i]);
174 printf("\n");
175 vtbl_print_queued_functions(stdout, &vtbl, true);
176 printf("\n");
177 }
178
179 for (i=1; i<NVALS; i++) {
180 if (f[0] != f[i]) {
181 fprintf(stderr, "*** BUG: NORMALIZATION FAILED ***\n");
182 fflush(stderr);
183 exit(1);
184 }
185 }
186 }
187
188
189 /*
190 * Test1: all functions from a base type to the range defined by buffer1
191 */
test_base_types(void)192 static void test_base_types(void) {
193 uint32_t i;
194 type_t tau;
195
196 for (i=0; i<NUM_BASE_TYPES; i++) {
197 tau = base[i];
198 test_function(&tau, 1, buffer1);
199 }
200 }
201
202 /*
203 * Test2: take all pairs of base types
204 */
test_pair_types(void)205 static void test_pair_types(void) {
206 uint32_t i, j;
207 type_t tau[2];
208
209 for (i=0; i<NUM_BASE_TYPES; i++) {
210 tau[0] = base[i];
211 for (j=0; j<NUM_BASE_TYPES; j++) {
212 tau[1] = base[j];
213 test_function(tau, 2, buffer1);
214 }
215 }
216 }
217
218
219 /*
220 * Initialize buffer1: cycle through val[0 ... nvals-1]
221 */
init_buffer1(void)222 static void init_buffer1(void) {
223 uint32_t i, j;
224
225 j = 0;
226 for (i=0; i<BUFFER_SIZE; i++) {
227 buffer1[i] = val[j];
228 j ++;
229 if (j > NVALS) j = 0;
230 }
231 }
232
233 /*
234 * remove val[0] from buffer1, replace it by val[2]
235 */
change_buffer1(void)236 static void change_buffer1(void) {
237 uint32_t i;
238
239 for (i=0; i<BUFFER_SIZE; i++) {
240 if (buffer1[i] == val[0]) {
241 buffer1[i] = val[2];
242 }
243 }
244 }
245
246 /*
247 * Store constant value val[1] in buffer1
248 */
constant_buffer1(void)249 static void constant_buffer1(void) {
250 uint32_t i;
251
252 for (i=0; i<BUFFER_SIZE; i++) {
253 buffer1[i] = val[1];
254 }
255 }
256
main(void)257 int main(void) {
258 init_type_table(&types, 10);
259 init_value_table(&vtbl, 0, &types);
260
261 init_base_types();
262 init_val();
263
264 printf("**************************\n"
265 "* TEST1: CYCLIC MAP *\n"
266 "**************************\n\n");
267
268 init_buffer1();
269 test_base_types();
270 test_pair_types();
271
272 printf("**************************\n"
273 "* TEST2: REMOVED ZEROS *\n"
274 "**************************\n\n");
275
276 change_buffer1();
277 test_base_types();
278 test_pair_types();
279
280 printf("**************************\n"
281 "* TEST3: CONSTANT MAP *\n"
282 "**************************\n\n");
283
284 constant_buffer1();
285 test_base_types();
286 test_pair_types();
287
288 delete_value_table(&vtbl);
289 delete_type_table(&types);
290
291 return 0;
292 }
293