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 construction of fresh objects
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/fresh_value_maker.h"
30
31 static type_table_t types;
32 static value_table_t vtbl;
33 static fresh_val_maker_t maker;
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 // [a, b -> c]
fun_type2(type_t a,type_t b,type_t c)53 static type_t fun_type2(type_t a, type_t b, type_t c) {
54 type_t aux[2];
55
56 aux[0] = a;
57 aux[1] = b;
58 return function_type(&types, c, 2, aux);
59 }
60
61
62 /*
63 * Base types
64 */
65 #define NUM_BASE_TYPES 20
66
67 static type_t base[NUM_BASE_TYPES];
68
init_base_types(void)69 static void init_base_types(void) {
70 base[0] = bool_type(&types); // bool
71 base[1] = bv_type(&types, 5); // bv5
72 base[2] = new_scalar_type(&types, 3); // scalar3
73 base[3] = new_scalar_type(&types, 1); // scalar1
74 base[4] = pair_type(base[0], base[2]); // bool x scalar3
75 base[5] = pair_type(base[3], base[0]); // scalar1 x bool
76 base[6] = fun_type1(base[0], base[2]); // [bool -> scalar3]
77 base[7] = fun_type1(base[0], base[3]); // [bool -> scalar1]
78 base[8] = fun_type1(base[2], base[0]); // [scalar3 -> bool]
79 base[9] = fun_type1(base[3], base[0]); // [scalar1 -> bool]
80 base[10] = fun_type1(base[0], base[0]); // [bool -> bool]
81 base[11] = fun_type1(base[10], base[0]); // [[bool -> bool] -> bool]
82
83 // some infinite types
84 base[12] = new_uninterpreted_type(&types);
85 base[13] = real_type(&types);
86 base[14] = int_type(&types);
87 base[15] = fun_type1(base[14], base[0]); // [int -> bool]
88 base[16] = fun_type2(base[0], base[0], base[14]); // [bool, bool -> int]
89
90 // larger finite types
91 base[17] = pair_type(base[1], base[1]); // bv5 x bv5
92 base[18] = bv_type(&types, 40); // bv40
93
94 // infinite domain, unit range
95 base[19] = fun_type1(base[13], base[3]); // [real -> scalar1]
96 }
97
98
99 /*
100 * Test
101 * - create values of type tau
102 * - n: max number of fresh values to try (assumed positive)
103 */
test_type(type_t tau,uint32_t n)104 static void test_type(type_t tau, uint32_t n) {
105 value_t v;
106 uint32_t i;
107
108 printf("==== Test fresh values of type ");
109 print_type(stdout, &types, tau);
110 printf(" ====\n");
111 printf("cardinality: %"PRIu32"\n\n", type_card(&types, tau));
112
113 i = 0;
114 do {
115 v = make_fresh_value(&maker, tau);
116 if (v == null_value) break;
117 i ++;
118 printf("val[%"PRIu32"] = ", i);
119 vtbl_print_object(stdout, &vtbl, v);
120 printf("\n");
121 if (vtbl_queue_is_nonempty(&vtbl)) {
122 vtbl_print_queued_functions(stdout, &vtbl, true);
123 printf("\n");
124 }
125 } while (i <n);
126
127 printf("\n---> got %"PRIu32" fresh values\n\n", i);
128 }
129
130
131 /*
132 * TEST1 : all base types
133 */
test_base_types(void)134 static void test_base_types(void) {
135 uint32_t i;
136
137 printf("*****************\n"
138 "* BASE TYPES *\n"
139 "*****************\n"
140 "\n");
141
142 for (i=0; i<NUM_BASE_TYPES; i++) {
143 test_type(base[i], 100);
144 }
145 }
146
147
main(void)148 int main(void) {
149 init_type_table(&types, 10);
150 init_value_table(&vtbl, 0, &types);
151 init_fresh_val_maker(&maker, &vtbl);
152
153 init_base_types();
154
155 test_base_types();
156
157 delete_fresh_val_maker(&maker);
158 delete_value_table(&vtbl);
159 delete_type_table(&types);
160
161 return 0;
162 }
163