1 /* Boolector: Satisfiability Modulo Theories (SMT) solver. 2 * 3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file. 4 * 5 * This file is part of Boolector. 6 * See COPYING for more information on using this software. 7 */ 8 9 #ifndef BTORSORT_H_INCLUDED 10 #define BTORSORT_H_INCLUDED 11 12 #include "btortypes.h" 13 #include "utils/btormem.h" 14 #include "utils/btorstack.h" 15 16 #include <stdbool.h> 17 #include <stdint.h> 18 19 typedef uint32_t BtorSortId; 20 // typedef struct btorsortanon btorsortanon; // debug 21 // typedef btorsortanon* BtorSortId; 22 23 enum BtorSortKind 24 { 25 BTOR_INVALID_SORT = 0, 26 BTOR_BOOL_SORT = 1, 27 BTOR_BV_SORT = 2, 28 BTOR_ARRAY_SORT = 3, 29 BTOR_LST_SORT = 4, 30 BTOR_FUN_SORT = 5, 31 BTOR_TUPLE_SORT = 6 32 }; 33 34 typedef enum BtorSortKind BtorSortKind; 35 36 typedef struct BtorSort BtorSort; 37 typedef struct BtorBitVecSort BtorBitVecSort; 38 typedef struct BtorArraySort BtorArraySort; 39 typedef struct BtorLstSort BtorLstSort; 40 typedef struct BtorFunSort BtorFunSort; 41 typedef struct BtorTupleSort BtorTupleSort; 42 43 struct BtorBitVecSort 44 { 45 uint32_t width; 46 }; 47 48 struct BtorArraySort 49 { 50 BtorSort *index; 51 BtorSort *element; 52 }; 53 54 struct BtorLstSort 55 { 56 BtorSort *head; 57 BtorSort *tail; 58 }; 59 60 struct BtorFunSort 61 { 62 bool is_array; 63 uint32_t arity; 64 BtorSort *domain; 65 BtorSort *codomain; 66 }; 67 68 struct BtorTupleSort 69 { 70 uint32_t num_elements; 71 BtorSort **elements; 72 }; 73 74 typedef struct BtorSortUniqueTable BtorSortUniqueTable; 75 76 struct BtorSort 77 { 78 BtorSortKind kind; 79 BtorSortId id; 80 uint32_t refs; /* reference counter */ 81 uint32_t ext_refs; /* reference counter for API references */ 82 BtorSort *next; /* collision chain for unique table */ 83 BtorSortUniqueTable *table; 84 #ifndef NDEBUG 85 Btor *btor; 86 uint32_t parents; 87 #endif 88 union 89 { 90 BtorBitVecSort bitvec; 91 BtorArraySort array; 92 BtorLstSort lst; 93 BtorFunSort fun; 94 BtorTupleSort tuple; 95 }; 96 }; 97 98 BTOR_DECLARE_STACK (BtorSortPtr, BtorSort *); 99 BTOR_DECLARE_STACK (BtorSortId, BtorSortId); 100 101 struct BtorSortUniqueTable 102 { 103 uint32_t size; 104 uint32_t num_elements; 105 BtorSort **chains; 106 BtorMemMgr *mm; 107 BtorSortPtrStack id2sort; 108 }; 109 110 BtorSortId btor_sort_bool (Btor *btor); 111 112 BtorSortId btor_sort_bv (Btor *btor, uint32_t width); 113 114 BtorSortId btor_sort_array (Btor *btor, 115 BtorSortId index_id, 116 BtorSortId element_id); 117 118 #if 0 119 BtorSortId btor_sort_lst (Btor * btor, 120 BtorSortId head_id, 121 BtorSortId tail_id); 122 #endif 123 124 BtorSortId btor_sort_fun (Btor *btor, 125 BtorSortId domain_id, 126 BtorSortId codomain_id); 127 128 BtorSortId btor_sort_tuple (Btor *btor, 129 BtorSortId *element_ids, 130 size_t num_elements); 131 132 BtorSortId btor_sort_copy (Btor *btor, BtorSortId id); 133 134 void btor_sort_release (Btor *btor, BtorSortId id); 135 136 BtorSort *btor_sort_get_by_id (Btor *btor, BtorSortId id); 137 138 uint32_t btor_sort_bv_get_width (Btor *btor, BtorSortId id); 139 140 uint32_t btor_sort_fun_get_arity (Btor *btor, BtorSortId id); 141 uint32_t btor_sort_tuple_get_arity (Btor *btor, BtorSortId id); 142 143 BtorSortId btor_sort_fun_get_codomain (Btor *btor, BtorSortId id); 144 BtorSortId btor_sort_fun_get_domain (Btor *btor, BtorSortId id); 145 146 BtorSortId btor_sort_array_get_index (Btor *btor, BtorSortId id); 147 BtorSortId btor_sort_array_get_element (Btor *btor, BtorSortId id); 148 149 bool btor_sort_is_valid (Btor *btor, BtorSortId id); 150 151 bool btor_sort_is_bool (Btor *btor, BtorSortId id); 152 153 bool btor_sort_is_bv (Btor *btor, BtorSortId id); 154 155 bool btor_sort_is_array (Btor *btor, BtorSortId id); 156 157 bool btor_sort_is_tuple (Btor *btor, BtorSortId id); 158 159 bool btor_sort_is_fun (Btor *btor, BtorSortId id); 160 161 struct BtorTupleSortIterator 162 { 163 size_t pos; 164 BtorSort *tuple; 165 }; 166 167 typedef struct BtorTupleSortIterator BtorTupleSortIterator; 168 169 void btor_iter_tuple_sort_init (BtorTupleSortIterator *it, 170 Btor *btor, 171 BtorSortId id); 172 173 bool btor_iter_tuple_sort_has_next (const BtorTupleSortIterator *it); 174 BtorSortId btor_iter_tuple_sort_next (BtorTupleSortIterator *it); 175 176 #endif 177