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 * TABLE OF ATOMS FOR ARITHMETIC SOLVERS
21 */
22
23 /*
24 * The atoms can be of the form (x >= k) or (x <= k) or (x == k),
25 * where x is a variable in the arithmetic solver and k is a rational
26 * constant. Each atom is identified by an index in the table.
27 * The table uses hash consing and it supports removal of atoms for push/pop
28 * operations.
29 *
30 * The components of an atom are:
31 * - a 2bit tag to specify the atom type (>=, <=, or ==)
32 * - the variable x (30bits index)
33 * - the rational constant k
34 * - a boolean variable (mapped to the atom in the smt-core)
35 * - a one bit mark: if the mark is 1, then the atom is assigned in the core
36 * otherwise, the atom is not assigned
37 */
38
39 #ifndef __ARITH_ATOMTABLE_H
40 #define __ARITH_ATOMTABLE_H
41
42 #include <stdint.h>
43 #include <stdbool.h>
44 #include <stddef.h>
45 #include <assert.h>
46
47 #include "solvers/cdcl/smt_core.h"
48 #include "solvers/egraph/egraph_base_types.h"
49 #include "terms/rationals.h"
50 #include "utils/bitvectors.h"
51 #include "utils/int_hash_tables.h"
52
53
54 /*
55 * Tags for atom types
56 */
57 typedef enum arithatm_tag {
58 GE_ATM = 0x00, // x >= k
59 LE_ATM = 0x01, // x <= k
60 EQ_ATM = 0x02, // x == k
61 } arithatm_tag_t;
62
63
64 /*
65 * Atom structure
66 * - header = variable index + tag
67 * - boolvar = boolean variable
68 * - bound = constant
69 */
70 typedef struct arith_atom_s {
71 uint32_t header;
72 bvar_t boolvar;
73 rational_t bound;
74 } arith_atom_t;
75
76
77
78 /*
79 * Access to variable and tag, and other atom components
80 */
var_of_atom(arith_atom_t * atom)81 static inline thvar_t var_of_atom(arith_atom_t *atom) {
82 return (thvar_t) (atom->header >> 2);
83 }
84
tag_of_atom(arith_atom_t * atom)85 static inline arithatm_tag_t tag_of_atom(arith_atom_t *atom) {
86 return (arithatm_tag_t) (atom->header & 0x3);
87 }
88
atom_is_ge(arith_atom_t * atm)89 static inline bool atom_is_ge(arith_atom_t *atm) {
90 return tag_of_atom(atm) == GE_ATM;
91 }
92
atom_is_le(arith_atom_t * atm)93 static inline bool atom_is_le(arith_atom_t *atm) {
94 return tag_of_atom(atm) == LE_ATM;
95 }
96
atom_is_eq(arith_atom_t * atm)97 static inline bool atom_is_eq(arith_atom_t *atm) {
98 return tag_of_atom(atm) == EQ_ATM;
99 }
100
boolvar_of_atom(arith_atom_t * atom)101 static inline bvar_t boolvar_of_atom(arith_atom_t *atom) {
102 return atom->boolvar;
103 }
104
bound_of_atom(arith_atom_t * atom)105 static inline rational_t *bound_of_atom(arith_atom_t *atom) {
106 return &atom->bound;
107 }
108
109
110
111 /*
112 * Build header for variable x and tag
113 */
arithatom_mk_header(int32_t x,arithatm_tag_t tag)114 static inline uint32_t arithatom_mk_header(int32_t x, arithatm_tag_t tag) {
115 assert(tag == GE_ATM || tag == LE_ATM || tag == EQ_ATM);
116 assert(0 <= x && x < UINT32_MAX/4);
117 return (((uint32_t) x) << 2) | ((uint32_t) tag);
118 }
119
120
121 /*
122 * Conversions between void* pointers and atom indices
123 * - an atom index is packed into a void * pointer, with a two-bit tag
124 * to indicate that this is an arithmetic atom (cf. egraph_types.h)
125 * - there's no loss of data even if pointers are 32 bits (because
126 * the tag is 2bits and i is less than MAX_ARITHATOMTABLE_SIZE (i.e., 2^32/16)
127 */
arithatom_idx2tagged_ptr(int32_t i)128 static inline void *arithatom_idx2tagged_ptr(int32_t i) {
129 return tagged_arith_atom((void *)((size_t) (i << 2)));
130 }
131
arithatom_tagged_ptr2idx(void * p)132 static inline int32_t arithatom_tagged_ptr2idx(void *p) {
133 return (int32_t)(((size_t) p) >> 2);
134 }
135
136
137
138 /*
139 * Atom table
140 * - size = size of the atom array
141 * - natoms = number of atoms created
142 * - atoms = atom array
143 * - mark = one bit per atom
144 * if mark = 1 the atom is assigned
145 * if mark = 0 the atom is unassigned
146 */
147 typedef struct arith_atomtable_s {
148 uint32_t size;
149 uint32_t natoms;
150 arith_atom_t *atoms;
151 byte_t *mark;
152
153 // pointer to the smt_core object
154 smt_core_t *core;
155
156 // table for hash consing
157 int_htbl_t htbl;
158
159 // auxiliary rational buffer
160 rational_t aux;
161 } arith_atomtable_t;
162
163
164 /*
165 * The table can store as many as (UINT32_MAX/16) atoms,
166 * which should be way more than what we can deal with.
167 */
168 #define DEF_ARITHATOMTABLE_SIZE 100
169 #define MAX_ARITHATOMTABLE_SIZE (UINT32_MAX/sizeof(arith_atom_t))
170
171
172
173 /*
174 * Initialization:
175 * - all data structures are allocated with their default initial size
176 * - core = smt_core attached to the arithmetic solver.
177 */
178 extern void init_arith_atomtable(arith_atomtable_t *table, smt_core_t *core);
179
180
181 /*
182 * Deletion: free all allocated memory (delete all atoms)
183 */
184 extern void delete_arith_atomtable(arith_atomtable_t *table);
185
186
187 /*
188 * Reset: empty the table: delete all atoms
189 */
190 extern void reset_arith_atomtable(arith_atomtable_t *table);
191
192
193 /*
194 * Support for pop: remove all atoms of index >= natoms
195 */
196 extern void arith_atomtable_remove_atoms(arith_atomtable_t *table, uint32_t natoms);
197
198
199
200
201
202 /*
203 * READ TABLE CONTENT
204 */
205
206 /*
207 * Get atom descriptor for atom i
208 */
arith_atom(arith_atomtable_t * table,int32_t i)209 static inline arith_atom_t *arith_atom(arith_atomtable_t *table, int32_t i) {
210 assert(0 <= i && i < table->natoms);
211 return table->atoms + i;
212 }
213
214 /*
215 * Get the index of atom a
216 */
arith_atom_id(arith_atomtable_t * table,arith_atom_t * a)217 static inline int32_t arith_atom_id(arith_atomtable_t *table, arith_atom_t *a) {
218 assert(table->atoms <= a && a < table->atoms + table->natoms);
219 return (int32_t)(a - table->atoms);
220 }
221
222 /*
223 * Number of atoms
224 */
num_arith_atoms(arith_atomtable_t * table)225 static inline uint32_t num_arith_atoms(arith_atomtable_t *table) {
226 return table->natoms;
227 }
228
229
230 /*
231 * Get atom index for boolean var v
232 * - return -1 if there's no atom for v or the atom is not arithmetic
233 */
234 extern int32_t arith_atom_id_for_bvar(arith_atomtable_t *table, bvar_t v);
235
236
237 /*
238 * Get atom descriptor for boolean variable v
239 * - return NULL if there's no atom for v or the atom is not arithmetic
240 */
241 extern arith_atom_t *arith_atom_for_bvar(arith_atomtable_t *table, bvar_t v);
242
243
244
245 /*
246 * MARKS
247 */
248
249 /*
250 * Check whether atom i is marked
251 */
arith_atom_is_marked(arith_atomtable_t * table,int32_t i)252 static inline bool arith_atom_is_marked(arith_atomtable_t *table, int32_t i) {
253 assert(0 <= i && i < table->natoms);
254 return tst_bit(table->mark, i);
255 }
256
arith_atom_is_unmarked(arith_atomtable_t * table,int32_t i)257 static inline bool arith_atom_is_unmarked(arith_atomtable_t *table, int32_t i) {
258 return ! arith_atom_is_marked(table, i);
259 }
260
261
262 /*
263 * Mark atom i
264 * - the atom must be unmarked
265 */
mark_arith_atom(arith_atomtable_t * table,int32_t i)266 static inline void mark_arith_atom(arith_atomtable_t *table, int32_t i) {
267 assert(arith_atom_is_unmarked(table, i));
268 set_bit(table->mark, i);
269 }
270
271 /*
272 * Put atom i back into the free list and clear its mark
273 * IMPORTANT: i must be the last marked atom
274 * (marking/unmarking must be done in LIFO order)
275 */
unmark_arith_atom(arith_atomtable_t * table,int32_t i)276 static inline void unmark_arith_atom(arith_atomtable_t *table, int32_t i) {
277 assert(arith_atom_is_marked(table, i));
278 clr_bit(table->mark, i);
279 }
280
281
282
283 /*
284 * ATOM CONSTRUCTION
285 */
286
287 /*
288 * Search for an atom (x op k) where op is one of GE_ATM, LE_ATM, EQ_ATM
289 * - return -1 if there's no such atom, otherwise, return the atom index
290 */
291 extern int32_t find_arith_atom(arith_atomtable_t *table, thvar_t x, arithatm_tag_t op, rational_t *k);
292
293 /*
294 * Search for atom (x op k)
295 * - create a new atom if it's not in the table
296 * - return the atom index
297 * - set new_atom to true if the result is a new atom, to false otherwise
298 *
299 * If a new atom is created, it's attached to the core and it's assigned to
300 * a fresh boolean variable.
301 */
302 extern int32_t get_arith_atom(arith_atomtable_t *table, thvar_t x, arithatm_tag_t op, rational_t *k, bool *new_atom);
303
304 /*
305 * Variants: return a literal, create a new atom if needed
306 * - is_int indicates whether x is an integer variable
307 * If x is an integer variable, then k must be an integer,
308 * and atom (x <= k) is rewritten to not (x >= k+1)
309 *
310 * Returned atom index in *new_idx:
311 * - *new_idx = -1 if the atom was already present in the table
312 * - if a new atom is created, *new_idx is set to that atom's index
313 */
314 extern literal_t get_literal_for_eq_atom(arith_atomtable_t *table, thvar_t x, rational_t *k, int32_t *new_idx);
315 extern literal_t get_literal_for_ge_atom(arith_atomtable_t *table, thvar_t x, bool is_int, rational_t *k, int32_t *new_idx);
316 extern literal_t get_literal_for_le_atom(arith_atomtable_t *table, thvar_t x, bool is_int, rational_t *k, int32_t *new_idx);
317
318
319
320 #endif /* __ARITH_ATOMTABLE_H */
321