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