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 * BUILD FRESH VALUES OF GIVEN TYPES
21 */
22
23 #ifndef __FRESH_VALUE_MAKER_H
24 #define __FRESH_VALUE_MAKER_H
25
26 #include <stdint.h>
27 #include <stdbool.h>
28
29 #include "model/concrete_values.h"
30
31
32 /*
33 * Data structure to keep track of the number of elements of a finite
34 * type tau[0] x ... x tau[n-1]
35 * - arity = n
36 * - card = cardinal of the product type
37 * - count = enumeration index: it's known that all tuples of index
38 * in [0 ... count-1] exist in the value table
39 * - tau[0 ... n-1] = actual type indices
40 *
41 * We also use this for scalar types (then arity = 1)
42 */
43 typedef struct tuple_counter_s {
44 uint32_t arity;
45 uint32_t card;
46 uint32_t count;
47 type_t tau[0]; // real size = arity
48 } tuple_counter_t;
49
50 #define MAX_TUPLE_COUNTER_ARITY ((UINT32_MAX-sizeof(tuple_counter_t))/sizeof(type_t))
51
52
53 /*
54 * Vector of these counters
55 */
56 typedef struct tup_counter_vector_s {
57 tuple_counter_t **data;
58 uint32_t nelems;
59 uint32_t size; // size of the array data
60 } tup_counter_vector_t;
61
62 #define TUPLE_COUNTER_VECTOR_DEF_SIZE 8
63 #define TUPLE_COUNTER_VECTOR_MAX_SIZE (UINT32_MAX/sizeof(tuple_counter_t *))
64
65
66 /*
67 * Counters for bitvector constants
68 * - bsize = number of bits
69 * - count = enumeration index
70 * - every constant of bsize bits and value < count are known
71 * to be present in vtbl.
72 */
73 typedef struct bv_counter_s {
74 uint32_t bsize;
75 uint32_t count;
76 } bv_counter_t;
77
78
79 /*
80 * Vector of these counters
81 */
82 typedef struct bv_counter_vector_s {
83 bv_counter_t *data;
84 uint32_t nelems;
85 uint32_t size;
86 } bv_counter_vector_t;
87
88 #define BV_COUNTER_VECTOR_DEF_SIZE 8
89 #define BV_COUNTER_VECTOR_MAX_SIZE (UINT32_MAX/sizeof(bv_counter_vector_t))
90
91
92 /*
93 * Fresh-value maker:
94 * - attached to a value_table vtbl and a type_table types
95 * - keep vectors for the counter structures:
96 * - one for tuple (also used for scalar types)
97 * - one for bitvectors
98 * - global counter for the integer constants
99 * + auxiliary buffer for building bitvector constants
100 *
101 * NOTE: we assume that the number of records is small
102 */
103 typedef struct fresh_val_maker_s {
104 value_table_t *vtbl;
105 type_table_t *types;
106 tup_counter_vector_t tuples;
107 bv_counter_vector_t bvs;
108 bvconstant_t aux;
109 int32_t int_count;
110 } fresh_val_maker_t;
111
112
113 /*
114 * Initialize: nothing allocated yet
115 */
116 extern void init_fresh_val_maker(fresh_val_maker_t *maker, value_table_t *vtbl);
117
118 /*
119 * Delete: free all records
120 */
121 extern void delete_fresh_val_maker(fresh_val_maker_t *maker);
122
123
124
125
126 /*
127 * Return a fresh integer:
128 * - this value is different from any other integer already present
129 */
130 extern value_t make_fresh_integer(fresh_val_maker_t *maker);
131
make_fresh_rational(fresh_val_maker_t * maker)132 static inline value_t make_fresh_rational(fresh_val_maker_t *maker) {
133 return make_fresh_integer(maker);
134 }
135
136 /*
137 * Attempt to build a fresh bitvector value of n bits
138 * - if all 2^n values are present in vtbl, return null_value
139 * - otherwise, create a bitvector value distinct from all other values
140 * of the same type and return it.
141 */
142 extern value_t make_fresh_bv(fresh_val_maker_t *maker, uint32_t n);
143
144 /*
145 * Fresh constant of uninterpreted or scalar type
146 * - tau must be an uninterpreted or scalar type
147 * - return null_value if tau is a scalar type and all constants of that
148 * type already occur in vtbl.
149 */
150 extern value_t make_fresh_const(fresh_val_maker_t *maker, type_t tau);
151
152 /*
153 * Fresh tuple of type tau
154 * - tau must be a tuple type
155 * - return null_value if tau is finite and all tuples of that type
156 * already exist
157 */
158 extern value_t make_fresh_tuple(fresh_val_maker_t *maker, type_t tau);
159
160 /*
161 * Fresh function to type tau
162 * - tau must be a function type
163 * - return null_value if tau is finite and all functions of that type
164 * already exist
165 */
166 extern value_t make_fresh_function(fresh_val_maker_t *maker, type_t tau);
167
168 /*
169 * Create a fresh value of type tau:
170 * - return null_value if that fails (i.e., tau is finite and all values
171 * or type tau are already present)
172 */
173 extern value_t make_fresh_value(fresh_val_maker_t *maker, type_t tau);
174
175
176 #endif /* __FRESH_VALUE_MAKER */
177