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 * Concrete values = constants of different types.
21 * This is used to build models: a model is a mapping from terms to concrete values.
22 *
23 * The table is divided into two parts:
24 * - permanent objects = objects that must be kept in the model
25 * - temporary objects = objects created when evaluating the value of a non-atomic term.
26 * The temporary objects can be deleted.
27 *
28 * The implementation works in two modes:
29 * - default mode: create permanent objects
30 * - tmp mode: all objects created are temporary and are deleted when
31 * tmp_mode is exited.
32 *
33 * We attempt to ensure that different objects in the table actually
34 * represent different values. But this is hard to ensure for
35 * functions. So we attach a "canonical flag" to each object:
36 * - if the bit is 1 for object i then i is in a canonical representation.
37 * An object j with a different descriptor cannot be equal to i.
38 * - if the bit is 0, then i is not in a canonical form.
39 *
40 *
41 * For printing/pretty printing, we keep track of function objects
42 * whose map must be printed. We store them in a queue + add a mark.
43 */
44
45 #ifndef __CONCRETE_VALUES_H
46 #define __CONCRETE_VALUES_H
47
48 #include <stdint.h>
49 #include <stdbool.h>
50 #include <stdio.h>
51 #include <assert.h>
52
53 #include "terms/bv_constants.h"
54 #include "terms/rationals.h"
55 #include "terms/types.h"
56 #include "utils/bitvectors.h"
57 #include "utils/int_hash_tables.h"
58 #include "utils/int_queues.h"
59 #include "utils/int_vectors.h"
60
61
62 /*
63 * Each concrete value is identified by an integer index.
64 * A type and descriptor for each value is stored in a table.
65 * We use hash consing.
66 *
67 * The concrete types are
68 * UNKNOWN_VALUE
69 * BOOLEAN_VALUE
70 * RATIONAL_VALUE
71 * ALGEBRAIC_VALUE
72 * BITVECTOR_VALUE
73 * TUPLE_VALUE
74 * UNINTERPRETED_VALUE
75 * FUNCTION_VALUE
76 * FUNCTION_UPDATE
77 *
78 * A function value is a finite set of mappings + a default value.
79 * The mappings are stored as MAP_VALUE objects in the table.
80 * A mapping is of the form [a_0 ... a_{n-1} -> val].
81 * If such a mapping belongs to f then (f a_0 ... a_{n-1}) = val.
82 * To save memory, we also allow functions to be constructed as
83 * updates of the form (update f_0 k) where k is a mapping and f_0
84 * is another function.
85 *
86 * An algebraic value is an algebraic number (imported from the
87 * libpoly library).
88 */
89
90 /*
91 * Value indices = signed integers
92 */
93 typedef int32_t value_t;
94
95
96 /*
97 * null_value means no value assigned yet.
98 * This is different from UNKNOWN_VALUE.
99 */
100 enum {
101 null_value = -1,
102 };
103
104
105 /*
106 * Types
107 */
108 typedef enum {
109 UNKNOWN_VALUE,
110 BOOLEAN_VALUE,
111 RATIONAL_VALUE,
112 ALGEBRAIC_VALUE,
113 BITVECTOR_VALUE,
114 TUPLE_VALUE,
115 UNINTERPRETED_VALUE,
116 FUNCTION_VALUE,
117 MAP_VALUE,
118 UPDATE_VALUE,
119 } value_kind_t;
120
121 #define NUM_VALUE_KIND ((uint32_t) (UPDATE_VALUE + 1))
122
123
124 /*
125 * Value stored in the table:
126 * - either an integer or a rational or a pointer to an object descriptor
127 */
128 typedef union value_desc_u {
129 int32_t integer;
130 rational_t rational;
131 void *ptr;
132 } value_desc_t;
133
134
135 /*
136 * Descriptors: encode the actual value
137 */
138 // bitvector constant
139 typedef struct value_bv_s {
140 uint32_t nbits;
141 uint32_t width; // size in words = ceil(nbits/32)
142 uint32_t data[0]; // real size = width
143 } value_bv_t;
144
145 // tuple = array of values
146 typedef struct value_tuple_s {
147 uint32_t nelems;
148 value_t elem[0]; // real size = arity
149 } value_tuple_t;
150
151 // uninterpreted constant
152 typedef struct value_unint_s {
153 type_t type;
154 int32_t index; // id = same as in constant_terms in term table
155 char *name;
156 } value_unint_t;
157
158 // mapping object: arg[0] ... arg[n-1] |-> val
159 typedef struct value_map_s {
160 uint32_t arity;
161 value_t val;
162 value_t arg[0]; // real size = arity
163 } value_map_t;
164
165 // function: default value + an array of mapping objects
166 typedef struct value_fun_s {
167 char *name;
168 type_t type; // function type
169 uint32_t arity; // number of parameters
170 value_t def; // default value
171 uint32_t map_size; // size of array map
172 value_t map[0]; // array of mapping object of size = map_size
173 } value_fun_t;
174
175
176 // function update = (update fun map)
177 typedef struct value_update_s {
178 uint32_t arity;
179 value_t fun; // function
180 value_t map; // mapping
181 } value_update_t;
182
183
184 // Limits on the size of maps and tuple that can be represented
185 #define VTBL_MAX_MAP_SIZE ((UINT32_MAX-sizeof(value_fun_t))/sizeof(value_t))
186 #define VTBL_MAX_TUPLE_SIZE ((UINT32_MAX-sizeof(value_tuple_t))/sizeof(value_t))
187 #define VTBL_MAX_MAP_ARITY ((UINT32_MAX-sizeof(value_map_t))/sizeof(value_t))
188
189
190 /*
191 * To accelerate function evaluation, we store pairs
192 * <function, map> into an auxiliary hash table.
193 * - function is a function object (not an update)
194 * - map must be a mapping object that belongs to function
195 */
196 typedef struct map_pair_s {
197 value_t function;
198 value_t map;
199 } map_pair_t;
200
201 typedef struct map_htbl_s {
202 map_pair_t *data; // hash table proper
203 uint32_t size; // its size (must be a power of 2)
204 uint32_t nelems;
205 uint32_t resize_threshold;
206 } map_htbl_t;
207
208
209 /*
210 * Default initial size of a map table + maximal size
211 */
212 #define MAP_HTBL_DEFAULT_SIZE 64
213 #define MAP_HTBL_MAX_SIZE (UINT32_MAX/sizeof(map_pair_t))
214
215 /*
216 * Resize ratio: the table size is doubled when nelems >= size * resize ratio
217 */
218 #define MAP_HTBL_RESIZE_RATIO 0.7
219
220
221
222 /*
223 * Hash set used to compute the normal form of update objects
224 * - a function is represented as a finite set of mapping objects
225 * - normalizing an update object converts it to a finite set of
226 * mappings.
227 * This set is represented as a hash-set
228 */
229 typedef struct map_hset_s {
230 value_t *data; // set elements
231 uint32_t size; // size of the data array
232 uint32_t nelems; // number of elements in the array
233 uint32_t resize_threshold;
234 } map_hset_t;
235
236
237 /*
238 * Default initial size + maximal size of an hset
239 */
240 #define MAP_HSET_DEFAULT_SIZE 32
241 #define MAP_HSET_MAX_SIZE (UINT32_MAX/sizeof(value_t))
242
243
244 /*
245 * Resize ratio
246 */
247 #define MAP_HSET_RESIZE_RATIO 0.7
248
249
250 /*
251 * Reduce threshold: in reset, if the hset size is more than this
252 * threshold then the data array is reduced to the default size.
253 */
254 #define MAP_HSET_REDUCE_THRESHOLD 256
255
256
257 /*
258 * Queue + bitvector for functions whose map must be printed.
259 */
260 typedef struct vtbl_queue_s {
261 int_queue_t queue;
262 byte_t *mark;
263 uint32_t size; // size of the mark vector
264 } vtbl_queue_t;
265
266 #define DEF_VTBL_QUEUE_SIZE 2048
267
268
269 /*
270 * Optional function to name uninterpreted constants
271 * - the table contains a pointer to a function 'unint_namer'
272 * + an opaque pointer aux_namer.
273 * - when an uninterpreted value is printed, the value's name
274 * (stored in the value_unint_t descriptor d) is used.
275 * - if d->name is NULL and name_of_unint is non NULL, then
276 * unint_namer(aux, d) is called
277 * if this function returns a non-NULL string, that's used
278 * as the name.
279 * - otherwise, the modules uses a name 'const!k' for some k
280 */
281 typedef const char *(*unint_namer_fun_t)(void *aux, value_unint_t *d);
282
283
284 /*
285 * Table of concrete objects
286 * - valid objects have indices between 0 and nobjects - 1
287 * - for each object,
288 * kind[i] = its type
289 * desc[i] = its descriptor
290 * canonical[i] = one bit: 1 means i is in a canonical form
291 * 0 means it's not
292 * - other components:
293 * type_table = pointer to an associated type table
294 * htbl = hash table for hash consing
295 * buffer for building bitvector constants
296 * auxiliary vector
297 * mtbl = hash table of pairs (fun, map)
298 * hset1, hset2 = hash sets allocated on demand (used in
299 * hash consing of update objects)
300 * - unknown_value = index of the unknown value
301 * - true_value, false_value = indices of true/false values
302 *
303 * Three special values to give an interpretation of division by zero.
304 * All three should be assigned to a function value (or null_value).
305 * - rdiv_by_zero: (real division)
306 * - idiv_by_zero: (integer division)
307 * - mod_by_zero: (integer modulo)
308 * To be consistent with the Yices semantics of idiv/mod, the expected
309 * types should be:
310 * rdiv_by_zero: [ real -> real ]
311 * idiv_by_zero: [ real -> int ]
312 * imod_by_zero: [ real -> real ]
313 *
314 * But, we don't enforce this here. Any function that maps an
315 * arithmetic type to an arithmetic type is accepted.
316 *
317 * - first_tmp = index of the first temporary object
318 * if first_tmp = -1 then all objects are permanent.
319 * if first_tmp >= 0, then objects in [0 .. first_tmp -1] are permanent
320 * and objects in [first_tmp .. nobjects - 1] are temporary.
321 *
322 * - pointer for getting names of uninterpreted constants
323 */
324 typedef struct value_table_s {
325 uint32_t size;
326 uint32_t nobjects;
327 uint8_t *kind;
328 value_desc_t *desc;
329 byte_t *canonical; // bitvector
330
331 type_table_t *type_table;
332 int_htbl_t htbl;
333 bvconstant_t buffer;
334 ivector_t aux_vector;
335 map_htbl_t mtbl;
336 vtbl_queue_t queue;
337 map_hset_t *hset1;
338 map_hset_t *hset2;
339
340 int32_t unknown_value;
341 int32_t true_value;
342 int32_t false_value;
343
344 int32_t zero_rdiv_fun;
345 int32_t zero_idiv_fun;
346 int32_t zero_mod_fun;
347
348 int32_t first_tmp;
349
350 void *aux_namer;
351 unint_namer_fun_t unint_namer;
352 } value_table_t;
353
354
355 #define DEF_VALUE_TABLE_SIZE 200
356 #define MAX_VALUE_TABLE_SIZE (UINT32_MAX/sizeof(value_desc_t))
357
358
359
360
361 /*
362 * INITIALIZATION
363 */
364
365 /*
366 * Initialize a table;
367 * - n = initial size. If n is zero, the default size is used.
368 * - ttbl = attached type table.
369 */
370 extern void init_value_table(value_table_t *table, uint32_t n, type_table_t *ttbl);
371
372 /*
373 * Delete table: free all memory
374 */
375 extern void delete_value_table(value_table_t *table);
376
377 /*
378 * Reset: empty the table
379 */
380 extern void reset_value_table(value_table_t *table);
381
382
383 /*
384 * Assign aux and namer for dealing with uninterpreted values whose name is missing
385 */
value_table_set_namer(value_table_t * table,void * aux,unint_namer_fun_t f)386 static inline void value_table_set_namer(value_table_t *table, void *aux, unint_namer_fun_t f) {
387 assert(f != NULL);
388 table->aux_namer = aux;
389 table->unint_namer = f;
390 }
391
392
393 /*
394 * OBJECT CONSTRUCTORS
395 */
396
397 /*
398 * Undefined value
399 */
400 extern value_t vtbl_mk_unknown(value_table_t *table);
401
402 /*
403 * Boolean constant: val = 0 means false, val != 0 means true
404 */
405 extern value_t vtbl_mk_bool(value_table_t *table, int32_t val);
406 extern value_t vtbl_mk_true(value_table_t *table);
407 extern value_t vtbl_mk_false(value_table_t *table);
408
409 /*
410 * Negate v (v must be either true or false)
411 */
412 extern value_t vtbl_mk_not(value_table_t *table, value_t v);
413
414
415 /*
416 * Rational (or integer) constant (make a copy)
417 */
418 extern value_t vtbl_mk_rational(value_table_t *table, rational_t *v);
419 extern value_t vtbl_mk_int32(value_table_t *table, int32_t x);
420
421
422 /*
423 * Algebraic number (make a copy).
424 */
425 extern value_t vtbl_mk_algebraic(value_table_t *table, void *a);
426
427 /*
428 * Bit-vector constant: input is an array of n integers
429 * - bit i is 0 if a[i] == 0
430 * - bit i is 1 if a[i] != 0
431 * So a[0] = low order bit, a[n-1] = high order bit
432 */
433 extern value_t vtbl_mk_bv(value_table_t *table, uint32_t n, int32_t *a);
434
435 /*
436 * Variant: the input is an array of 32bit words
437 * - n = number of bits
438 * - a = array of w words where w = ceil(n/32)
439 */
440 extern value_t vtbl_mk_bv_from_bv(value_table_t *table, uint32_t n, uint32_t *a);
441
442 /*
443 * Variant: input is a bvconstant object
444 * - b->bitsize = number of bits
445 * - b->data = bits (stored as an array of uint32_t integers)
446 */
447 extern value_t vtbl_mk_bv_from_constant(value_table_t *table, bvconstant_t *b);
448
449 /*
450 * Variant: input is a 64bit unsigned integer
451 * - n = number of bits to use (n <= 64)
452 * - c = integer constant
453 */
454 extern value_t vtbl_mk_bv_from_bv64(value_table_t *table, uint32_t n, uint64_t c);
455
456 /*
457 * Variants:
458 * - bitvector 0b0000...00 of n bits
459 * - bitvector 0b0000...01 of n bits
460 */
461 extern value_t vtbl_mk_bv_zero(value_table_t *table, uint32_t n);
462 extern value_t vtbl_mk_bv_one(value_table_t *table, uint32_t n);
463
464
465 /*
466 * Tuple:
467 * - n = arity
468 * - e[0] ... e[n-1] = components
469 * all components must be valid elements in table
470 * n must be less than MAX_TERM_ARITY
471 */
472 extern value_t vtbl_mk_tuple(value_table_t *table, uint32_t n, value_t *e);
473
474
475 /*
476 * Uninterpreted constant of index id
477 * - tau = its type (must be UNINTERPRETED or SCALAR type)
478 * - name = optional name (NULL if no name is given)
479 * - id = index (must be non-negative)
480 *
481 * If the constant already exists and has a name, it keeps
482 * its current name. Otherwise, if name != NULL, then the constant
483 * is given that name.
484 */
485 extern value_t vtbl_mk_const(value_table_t *table, type_t tau, int32_t id, char *name);
486
487
488 /*
489 * Mapping a[0 ... n-1] := v
490 * - return a mapping object
491 */
492 extern value_t vtbl_mk_map(value_table_t *table, uint32_t n, value_t *a, value_t v);
493
494
495 /*
496 * Function defined by the array a[0...n] and default value def
497 * - tau = its type
498 * - a = array of n mapping objects.
499 * The array must not contain conflicting mappings and all elements in a
500 * must have the right arity (same as defined by type tau). It's allowed
501 * to have duplicate elements in a.
502 * - def = default value (must be unknown if no default is given).
503 *
504 * NOTE: array a is modified.
505 */
506 extern value_t vtbl_mk_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t def);
507
508
509 /*
510 * Create (update f (a[0] ... a[n-1]) v)
511 * - f must be a function of arity n (either a function object or another update)
512 */
513 extern value_t vtbl_mk_update(value_table_t *table, value_t f, uint32_t n, value_t *a, value_t v);
514
515
516 /*
517 * DIVISIONS BY ZERO
518 */
519
520 /*
521 * Give a value to the divide-by-zero function:
522 * - f must be a value in table of type [real -> real]
523 * - f can be either a function or an update object
524 */
525 extern void vtbl_set_zero_rdiv(value_table_t *table, value_t f);
526
527 /*
528 * Same thing for the integer divide-by-zero and modulo
529 */
530 extern void vtbl_set_zero_idiv(value_table_t *table, value_t f);
531 extern void vtbl_set_zero_mod(value_table_t *table, value_t f);
532
533
534
535 /*
536 * DEFAULT VALUES
537 */
538
539 /*
540 * Return an arbitrary value of type tau:
541 * - this is deterministic: the same value is returned every time the function is called
542 * with the same type.
543 * - tau must be a valid ground type defined in table->type_table
544 */
545 extern value_t vtbl_make_object(value_table_t *table, type_t tau);
546
547
548 /*
549 * Attempt to construct two distinct objects of type tau.
550 * - return false if tau is a singleton type
551 * - otherwise store the two objects in a[0] and a[1] and return true
552 */
553 extern bool vtbl_make_two_objects(value_table_t *vtbl, type_t tau, value_t a[2]);
554
555
556
557
558 /*
559 * CHECK WHETHER OBJECTS ARE PRESENT
560 */
561
562 /*
563 * All functions below check whether an object exists in table
564 * - they return the object id (value_t) if it exists
565 * - they return null_value otherwise (and don't construct anything
566 * in table).
567 */
568
569 // rationals
570 extern value_t vtbl_find_rational(value_table_t *table, rational_t *v);
571 extern value_t vtbl_find_int32(value_table_t *table, int32_t x);
572
573 // algebraic
574 extern value_t vtbl_find_algebraic(value_table_t *table, void* a);
575
576 // constants of scalar or uninterpreted type
577 extern value_t vtbl_find_const(value_table_t *table, type_t tau, int32_t id);
578
579 // tuple e[0] ... e[n-1]
580 extern value_t vtbl_find_tuple(value_table_t *table, uint32_t n, value_t *e);
581
582 // bitvector defined by a[0 ... n-1]
583 extern value_t vtbl_find_bv(value_table_t *table, uint32_t n, int32_t *a);
584
585 // bitvector defined by c. n = number of bits (must be <= 64)
586 extern value_t vtbl_find_bv64(value_table_t *table, uint32_t n, uint64_t c);
587
588 // bitvector defined by a bvconstant b
589 extern value_t vtbl_find_bvconstant(value_table_t *table, bvconstant_t *b);
590
591 // map object: a[0 ... n-1] := v
592 extern value_t vtbl_find_map(value_table_t *table, uint32_t n, value_t *a, value_t v);
593
594 // function defined by array of n maps + the default value
595 // array a is modified
596 extern value_t vtbl_find_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t def);
597
598
599 /*
600 * TEST EXISTENCE
601 */
vtbl_test_rational(value_table_t * table,rational_t * v)602 static inline bool vtbl_test_rational(value_table_t *table, rational_t *v) {
603 return vtbl_find_rational(table, v) >= 0;
604 }
605
vtbl_test_int32(value_table_t * table,int32_t x)606 static inline bool vtbl_test_int32(value_table_t *table, int32_t x) {
607 return vtbl_find_int32(table, x) >= 0;
608 }
609
vtbl_test_const(value_table_t * table,type_t tau,int32_t id)610 static inline bool vtbl_test_const(value_table_t *table, type_t tau, int32_t id) {
611 return vtbl_find_const(table, tau, id) >= 0;
612 }
613
vtbl_test_tuple(value_table_t * table,uint32_t n,value_t * e)614 static inline bool vtbl_test_tuple(value_table_t *table, uint32_t n, value_t *e) {
615 return vtbl_find_tuple(table, n, e) >= 0;
616 }
617
vtbl_test_bv(value_table_t * table,uint32_t n,int32_t * a)618 static inline bool vtbl_test_bv(value_table_t *table, uint32_t n, int32_t *a) {
619 return vtbl_find_bv(table, n, a) >= 0;
620 }
621
vtbl_test_bv64(value_table_t * table,uint32_t n,uint64_t c)622 static inline bool vtbl_test_bv64(value_table_t *table, uint32_t n, uint64_t c) {
623 return vtbl_find_bv64(table, n, c) >= 0;
624 }
625
vtbl_test_bvconstant(value_table_t * table,bvconstant_t * b)626 static inline bool vtbl_test_bvconstant(value_table_t *table, bvconstant_t *b) {
627 return vtbl_find_bvconstant(table, b) >= 0;
628 }
629
vtbl_test_map(value_table_t * table,uint32_t n,value_t * a,value_t v)630 static inline bool vtbl_test_map(value_table_t *table, uint32_t n, value_t *a, value_t v) {
631 return vtbl_find_map(table, n, a, v) >= 0;
632 }
633
634 // warning: a is modified
vtbl_test_function(value_table_t * table,type_t tau,uint32_t n,value_t * a,value_t def)635 static inline bool vtbl_test_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t def) {
636 return vtbl_find_function(table, tau, n, a, def) >= 0;
637 }
638
639
640
641
642 /*
643 * OBJECTS OF FINITE TYPE
644 */
645
646 /*
647 * If tau is a finite type, then we can enumerate its elements from
648 * 0 to card(tau) - 1. The following function constructs an element
649 * of finite type tau given an enumeration index i.
650 * - tau must be finite
651 * - i must be smaller than card(tau)
652 */
653 extern value_t vtbl_gen_object(value_table_t *table, type_t tau, uint32_t i);
654
655 /*
656 * Same thing for tuples:
657 * - tau[0 ... n-1] must be n finite types
658 * - i must be an index between 0 and card(tau[0]) x ... x card(tau[n-1])
659 * - a must be large enough to store n elements
660 * - this stores n objects in a[0 ... n-1] where a[k] has type tau[k]
661 * - different indices i generate different tuples of n objects
662 */
663 extern void vtbl_gen_object_tuple(value_table_t *table, uint32_t n, type_t *tau, uint32_t i, value_t *a);
664
665 /*
666 * Same thing for a finite function type tau:
667 * - the domain must be finite
668 * - let D = cardinality of tau's domain and R = cardinality of tau's range
669 * - a function of type tau is defined by D values a[0 ... D-1] where each a[k] is an
670 * object of tau's range.
671 * - this function builds a[0 ... D-1] given an index i between 0 and R^D.
672 * - a must be large enough to store D elements
673 */
674 extern void vtbl_gen_function_map(value_table_t *table, type_t tau, uint32_t i, value_t *a);
675
676
677 /*
678 * Check whether object of index i is present in the table
679 * - tau must be finite
680 * - i must be smaller than card(tau)
681 * - if the object exists, it's returned
682 * - otherwise, the function returns null_value
683 */
684 extern value_t vtbl_find_object(value_table_t *table, type_t tau, uint32_t i);
685
vtbl_test_object(value_table_t * table,type_t tau,uint32_t i)686 static inline bool vtbl_test_object(value_table_t *table, type_t tau, uint32_t i) {
687 return vtbl_find_object(table, tau, i) >= 0;
688 }
689
690
691 /*
692 * Search for object tuple of index i and type tau[0] x ... x tau[n-1]
693 * - return null_value if it's not present
694 */
695 extern value_t vtbl_find_object_tuple(value_table_t *table, uint32_t n, type_t *tau, uint32_t i);
696
vtbl_test_object_tuple(value_table_t * table,uint32_t n,type_t * tau,uint32_t i)697 static inline bool vtbl_test_object_tuple(value_table_t *table, uint32_t n, type_t *tau, uint32_t i) {
698 return vtbl_find_object_tuple(table, n, tau, i) >= 0;
699 }
700
701
702 /*
703 * NAMES
704 */
705
706 /*
707 * Set or change the name of function f
708 * - overwrite the current name if any
709 * - make an internal copy of the string if name != NULL
710 * - if name = NULL, this clears the name of f
711 */
712 extern void vtbl_set_function_name(value_table_t *table, value_t f, char *name);
713
714
715 /*
716 * Set or change the name of constant c
717 * - same effect as the previous function
718 */
719 extern void vtbl_set_constant_name(value_table_t *table, value_t c, char *name);
720
721
722
723
724 /*
725 * TEMPORARY OBJECTS
726 */
727
728 /*
729 * Switch to temporary mode:
730 * - all objects currently in the table are considered permanent.
731 * - all terms created after this function is called are temporary.
732 * - the table must not be in temporary mode already.
733 *
734 * Side effect: creates the unknown, true, and false values if they
735 * don't exist already. These are always permanent terms.
736 *
737 * Warning: the permanent terms must not be modified after this.
738 * So add_map and set_function_default should not be called with a permanent f.
739 */
740 extern void value_table_start_tmp(value_table_t *table);
741
742
743 /*
744 * Delete all temporary objects and return to permanent mode.
745 * Do nothing if the table is not in temporary mode.
746 */
747 extern void value_table_end_tmp(value_table_t *table);
748
749
750
751
752
753 /*
754 * EVALUATION
755 */
756
757 /*
758 * Check whether a and b are equal
759 * - return unknown if we can't tell
760 */
761 extern value_t vtbl_eval_eq(value_table_t *table, value_t a, value_t b);
762
763
764 /*
765 * Check whether arrays a[0 ... n-1] and b[0 ... n-1] are equal
766 * - return unknown if we can't tell
767 */
768 extern value_t vtbl_eval_array_eq(value_table_t *table, value_t *a, value_t *b, uint32_t n);
769
770
771 /*
772 * Evaluate (f a[0] ... a[n-1])
773 * - f must be a function or update object of arity n
774 * - a[0] ... a[n-1] must be non-null values
775 * Return unknown if the map is not defined for a[0 ... n-1]
776 */
777 extern value_t vtbl_eval_application(value_table_t *table, value_t f, uint32_t n, value_t *a);
778
779
780 /*
781 * Evaluate (/ v 0) by a lookup in table->rdiv_by_zero.
782 * - v should be an arithmetic object (but we don't check)
783 * - return unknown if either rdiv_by_zero is null or if the mapping to v is not defined.
784 */
785 extern value_t vtbl_eval_rdiv_by_zero(value_table_t *table, value_t v);
786
787 /*
788 * Same thing for integer division: use table->idiv_by_zero
789 */
790 extern value_t vtbl_eval_idiv_by_zero(value_table_t *table, value_t v);
791
792 /*
793 * Same thing for modulo: use table->mod_by_zero
794 */
795 extern value_t vtbl_eval_mod_by_zero(value_table_t *table, value_t v);
796
797
798
799 /*
800 * ACCESS TO OBJECT REPRESENTATION
801 */
good_object(value_table_t * table,value_t v)802 static inline bool good_object(value_table_t *table, value_t v) {
803 return 0 <= v && v < table->nobjects;
804 }
805
object_kind(value_table_t * table,value_t v)806 static inline value_kind_t object_kind(value_table_t *table, value_t v) {
807 assert(good_object(table, v));
808 return (value_kind_t) table->kind[v];
809 }
810
811 // check the type of v
object_is_unknown(value_table_t * table,value_t v)812 static inline bool object_is_unknown(value_table_t *table, value_t v) {
813 return object_kind(table, v) == UNKNOWN_VALUE;
814 }
815
object_is_boolean(value_table_t * table,value_t v)816 static inline bool object_is_boolean(value_table_t *table, value_t v) {
817 return object_kind(table, v) == BOOLEAN_VALUE;
818 }
819
object_is_rational(value_table_t * table,value_t v)820 static inline bool object_is_rational(value_table_t *table, value_t v) {
821 return object_kind(table, v) == RATIONAL_VALUE;
822 }
823
object_is_algebraic(value_table_t * table,value_t v)824 static inline bool object_is_algebraic(value_table_t *table, value_t v) {
825 return object_kind(table, v) == ALGEBRAIC_VALUE;
826 }
827
object_is_integer(value_table_t * table,value_t v)828 static inline bool object_is_integer(value_table_t *table, value_t v) {
829 return object_is_rational(table, v) && q_is_integer(&table->desc[v].rational);
830 }
831
object_is_bitvector(value_table_t * table,value_t v)832 static inline bool object_is_bitvector(value_table_t *table, value_t v) {
833 return object_kind(table, v) == BITVECTOR_VALUE;
834 }
835
object_is_tuple(value_table_t * table,value_t v)836 static inline bool object_is_tuple(value_table_t *table, value_t v) {
837 return object_kind(table, v) == TUPLE_VALUE;
838 }
839
object_is_unint(value_table_t * table,value_t v)840 static inline bool object_is_unint(value_table_t *table, value_t v) {
841 return object_kind(table, v) == UNINTERPRETED_VALUE;
842 }
843
object_is_function(value_table_t * table,value_t v)844 static inline bool object_is_function(value_table_t *table, value_t v) {
845 return object_kind(table, v) == FUNCTION_VALUE;
846 }
847
object_is_map(value_table_t * table,value_t v)848 static inline bool object_is_map(value_table_t *table, value_t v) {
849 return object_kind(table, v) == MAP_VALUE;
850 }
851
object_is_update(value_table_t * table,value_t v)852 static inline bool object_is_update(value_table_t *table, value_t v) {
853 return object_kind(table, v) == UPDATE_VALUE;
854 }
855
856
857 /*
858 * Check the canonical bit
859 */
object_is_canonical(value_table_t * table,value_t v)860 static inline bool object_is_canonical(value_table_t *table, value_t v) {
861 assert(good_object(table, v));
862 return tst_bit(table->canonical, v);
863 }
864
865
866 // check value of v
is_unknown(value_table_t * table,value_t v)867 static inline bool is_unknown(value_table_t *table, value_t v) {
868 assert(good_object(table, v));
869 return v == table->unknown_value;
870 }
871
is_true(value_table_t * table,value_t v)872 static inline bool is_true(value_table_t *table, value_t v) {
873 assert(good_object(table, v));
874 return v == table->true_value;
875 }
876
is_false(value_table_t * table,value_t v)877 static inline bool is_false(value_table_t *table, value_t v) {
878 assert(good_object(table, v));
879 return v == table->false_value;
880 }
881
boolobj_value(value_table_t * table,value_t v)882 static inline bool boolobj_value(value_table_t *table, value_t v) {
883 assert(object_is_boolean(table, v));
884 return (bool) table->desc[v].integer;
885 }
886
887
888 // get descriptor of v
vtbl_rational(value_table_t * table,value_t v)889 static inline rational_t *vtbl_rational(value_table_t *table, value_t v) {
890 assert(object_is_rational(table, v));
891 return &table->desc[v].rational;
892 }
893
vtbl_algebraic_number(value_table_t * table,value_t v)894 static inline void *vtbl_algebraic_number(value_table_t *table, value_t v) {
895 assert(object_is_algebraic(table, v));
896 return table->desc[v].ptr;
897 }
898
vtbl_bitvector(value_table_t * table,value_t v)899 static inline value_bv_t *vtbl_bitvector(value_table_t *table, value_t v) {
900 assert(object_is_bitvector(table, v));
901 return (value_bv_t *) table->desc[v].ptr;
902 }
903
vtbl_tuple(value_table_t * table,value_t v)904 static inline value_tuple_t *vtbl_tuple(value_table_t *table, value_t v) {
905 assert(object_is_tuple(table, v));
906 return (value_tuple_t *) table->desc[v].ptr;
907 }
908
vtbl_unint(value_table_t * table,value_t v)909 static inline value_unint_t *vtbl_unint(value_table_t *table, value_t v) {
910 assert(object_is_unint(table, v));
911 return (value_unint_t *) table->desc[v].ptr;
912 }
913
vtbl_function(value_table_t * table,value_t v)914 static inline value_fun_t *vtbl_function(value_table_t *table, value_t v) {
915 assert(object_is_function(table, v));
916 return (value_fun_t *) table->desc[v].ptr;
917 }
918
vtbl_map(value_table_t * table,value_t v)919 static inline value_map_t *vtbl_map(value_table_t *table, value_t v) {
920 assert(object_is_map(table, v));
921 return (value_map_t *) table->desc[v].ptr;
922 }
923
vtbl_map_result(value_table_t * table,value_t v)924 static inline value_t vtbl_map_result(value_table_t *table, value_t v) {
925 return vtbl_map(table, v)->val;
926 }
927
vtbl_update(value_table_t * table,value_t v)928 static inline value_update_t *vtbl_update(value_table_t *table, value_t v) {
929 assert(object_is_update(table, v));
930 return (value_update_t *) table->desc[v].ptr;
931 }
932
933
934 /*
935 * Check whether v is zero:
936 * - v must be a good object
937 * - return true if v is a rational equal to zero
938 */
939 extern bool is_zero(value_table_t *table, value_t v);
940
941 /*
942 * Check whether v is one
943 * - v must be a good object
944 * - return true if v is a rational equal to 1
945 */
946 extern bool is_one(value_table_t *table, value_t v);
947
948 /*
949 * Check whether v is +1 or -1
950 * - v must be a good object
951 */
952 extern bool is_unit(value_table_t *table, value_t v);
953
954 /*
955 * Check whether v is 0b00000...
956 * - v must be a good object
957 * - return true if v is a bitvector constant of the form 0b0....0
958 */
959 extern bool is_bvzero(value_table_t *table, value_t v);
960
961
962 /*
963 * UTILITIES
964 */
965
966 /*
967 * Normalize an update object i
968 * - this computes a set of mapping for object i
969 * - the default value for i is stored in *def
970 * - the type of i is stored in *tau (this is a function type)
971 *
972 * The set of mappings is stored in the internal hset1 table:
973 * - hset1->data contains the set of mapping objects for i (without duplicates)
974 * - hset1->nelems = number of mappings in hset1->data
975 */
976 extern void vtbl_expand_update(value_table_t *table, value_t i, value_t *def, type_t *tau);
977
978 /*
979 * Get the type of a function or update object i
980 */
981 extern type_t vtbl_function_type(value_table_t *table, value_t i);
982
983
984 /*
985 * Push v into the internal queue
986 * - v must be a valid object
987 * - do nothing if v is already in the queue
988 */
989 extern void vtbl_push_object(value_table_t *table, value_t v);
990
991
992 /*
993 * Check whether the queue is empty
994 */
995 extern bool vtbl_queue_is_empty(value_table_t *table);
996
vtbl_queue_is_nonempty(value_table_t * table)997 static inline bool vtbl_queue_is_nonempty(value_table_t *table) {
998 return !vtbl_queue_is_empty(table);
999 }
1000
1001 /*
1002 * Empty the internal queue
1003 */
1004 extern void vtbl_empty_queue(value_table_t *table);
1005
1006
1007 #endif /* __CONCRETE_VALUES_H */
1008