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 finite type enumerators in concrete_values.c
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 * Base types: all finite and small
38 */
39 #define NUM_BASE_TYPES 10
40
41 static type_t base[NUM_BASE_TYPES];
42
pair_type(type_t a,type_t b)43 static type_t pair_type(type_t a, type_t b) {
44 type_t aux[2];
45
46 aux[0] = a;
47 aux[1] = b;
48 return tuple_type(&types, 2, aux);
49 }
50
triple_type(type_t a,type_t b,type_t c)51 static type_t triple_type(type_t a, type_t b, type_t c) {
52 type_t aux[3];
53
54 aux[0] = a;
55 aux[1] = b;
56 aux[2] = c;
57 return tuple_type(&types, 3, aux);
58 }
59
60 // [a -> b]
fun_type1(type_t a,type_t b)61 static type_t fun_type1(type_t a, type_t b) {
62 return function_type(&types, b, 1, &a);
63 }
64
65 // [a, b -> c]
fun_type2(type_t a,type_t b,type_t c)66 static type_t fun_type2(type_t a, type_t b, type_t c) {
67 type_t aux[2];
68
69 aux[0] = a;
70 aux[1] = b;
71 return function_type(&types, c, 2, aux);
72 }
73
init_base_types(void)74 static void init_base_types(void) {
75 base[0] = bool_type(&types); // bool
76 base[1] = bv_type(&types, 5); // bv5
77 base[2] = new_scalar_type(&types, 3); // scalar3
78 base[3] = new_scalar_type(&types, 1); // scalar1
79 base[4] = pair_type(base[0], base[2]); // bool x scalar3
80 base[5] = pair_type(base[3], base[0]); // scalar1 x bool
81 base[6] = fun_type1(base[0], base[2]); // [bool -> scalar3]
82 base[7] = fun_type1(base[0], base[3]); // [bool -> scalar1]
83 base[8] = fun_type1(base[2], base[0]); // [scalar3 -> bool]
84 base[9] = fun_type1(base[3], base[0]); // [scalar1 -> bool]
85 }
86
test_enum_type(type_t tau)87 static void test_enum_type(type_t tau) {
88 uint32_t i, n;
89 value_t x;
90
91 assert(is_finite_type(&types, tau) && type_card_is_exact(&types, tau));
92
93 n = type_card(&types, tau);
94 printf("==== Enumerating elements of type ");
95 print_type(stdout, &types, tau);
96 printf(" ====\n");
97 printf("cardinality: %"PRIu32"\n", n);
98 for (i=0; i<n; i++) {
99 x = vtbl_gen_object(&vtbl, tau, i);
100 printf("elem[%"PRIu32"] = ", i);
101 vtbl_print_object(stdout, &vtbl, x);
102 printf("\n");
103 if (vtbl_queue_is_nonempty(&vtbl)) {
104 vtbl_print_queued_functions(stdout, &vtbl, true);
105 printf("\n");
106 }
107 }
108 printf("\n");
109 }
110
111
112 /*
113 * TEST1: all base types
114 */
test_base_types(void)115 static void test_base_types(void) {
116 uint32_t i;
117
118 printf("*****************\n"
119 "* BASE TYPES *\n"
120 "*****************\n"
121 "\n");
122
123 for (i=0; i<NUM_BASE_TYPES; i++) {
124 test_enum_type(base[i]);
125 }
126 }
127
128 /*
129 * TEST2: pairs of base types
130 * - skip any pair type of cardinaly >= threshold
131 */
test_pairs(uint32_t threshold)132 static void test_pairs(uint32_t threshold) {
133 uint32_t i, j;
134 type_t tau;
135
136 printf("*****************\n"
137 "* PAIR TYPES *\n"
138 "*****************\n"
139 "\n");
140
141 for (i=0; i<NUM_BASE_TYPES; i++) {
142 for (j=0; j<NUM_BASE_TYPES; j++) {
143 tau = pair_type(base[i], base[j]);
144 if (type_card(&types, tau) < threshold) {
145 test_enum_type(tau);
146 }
147 }
148 }
149 }
150
151 /*
152 * TEST3: triples
153 */
test_triples(uint32_t threshold)154 static void test_triples(uint32_t threshold) {
155 uint32_t i, j, k;
156 type_t tau;
157
158 printf("*******************\n"
159 "* TRIPLE TYPES *\n"
160 "*******************\n"
161 "\n");
162
163 for (i=0; i<NUM_BASE_TYPES; i++) {
164 for (j=0; j<NUM_BASE_TYPES; j++) {
165 for (k=0; k<NUM_BASE_TYPES; k++) {
166 tau = triple_type(base[i], base[j], base[k]);
167 if (type_card(&types, tau) < threshold) {
168 test_enum_type(tau);
169 }
170 }
171 }
172 }
173 }
174
175 /*
176 * TEST4: unary functions
177 */
test_unary_functions(uint32_t threshold)178 static void test_unary_functions(uint32_t threshold) {
179 uint32_t i, j;
180 type_t tau;
181
182 printf("***************************\n"
183 "* UNARY FUNCTION TYPES *\n"
184 "***************************\n"
185 "\n");
186
187 for (i=0; i<NUM_BASE_TYPES; i++) {
188 for (j=0; j<NUM_BASE_TYPES; j++) {
189 tau = fun_type1(base[i], base[j]);
190 if (type_card(&types, tau) < threshold) {
191 test_enum_type(tau);
192 }
193 }
194 }
195 }
196
197
198 /*
199 * TEST 5: binary functions
200 */
test_bin_functions(uint32_t threshold)201 static void test_bin_functions(uint32_t threshold) {
202 uint32_t i, j, k;
203 type_t tau;
204
205 printf("****************************\n"
206 "* BINARY FUNCTION TYPES *\n"
207 "****************************\n"
208 "\n");
209
210 for (i=0; i<NUM_BASE_TYPES; i++) {
211 for (j=0; j<NUM_BASE_TYPES; j++) {
212 for (k=0; k<NUM_BASE_TYPES; k++) {
213 tau = fun_type2(base[i], base[j], base[k]);
214 if (type_card(&types, tau) < threshold) {
215 test_enum_type(tau);
216 }
217 }
218 }
219 }
220 }
221
222
223 /*
224 * TEST6: (-> (-> (-> bool bool) bool) bool)
225 */
test_deep_type(void)226 static void test_deep_type(void) {
227 type_t b, tau;
228
229 b = bool_type(&types);
230 tau = fun_type1(b, b); // (-> bool bool)
231 tau = fun_type1(tau, b); // (-> (-> bool bool) bool)
232 tau = fun_type1(tau, b); // (-> (-> (-> bool bool) bool) bool)
233
234 printf("*****************************\n"
235 "* NESTED FUNCTION TYPE *\n"
236 "*****************************\n"
237 "\n");
238
239 test_enum_type(tau);
240 }
241
242
main(void)243 int main(void) {
244 init_type_table(&types, 10);
245 init_value_table(&vtbl, 0, &types);
246
247 init_base_types();
248 test_base_types();
249 test_pairs(1000);
250 test_triples(1000);
251 test_unary_functions(1000);
252 test_bin_functions(1000);
253 test_deep_type();
254
255 delete_value_table(&vtbl);
256 delete_type_table(&types);
257
258 return 0;
259 }
260