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 BTORNODE_H_INCLUDED
10 #define BTORNODE_H_INCLUDED
11
12 #include "btoraigvec.h"
13 #include "btorbv.h"
14 #include "btorsort.h"
15 #include "btortypes.h"
16 #include "utils/btorhashptr.h"
17 #include "utils/btorqueue.h"
18 #include "utils/btorstack.h"
19
20 /*------------------------------------------------------------------------*/
21
22 BTOR_DECLARE_STACK (BtorNodePtr, BtorNode *);
23 BTOR_DECLARE_STACK (BtorNodePtrPtr, BtorNode **);
24 BTOR_DECLARE_QUEUE (BtorNodePtr, BtorNode *);
25
26 /*------------------------------------------------------------------------*/
27
28 /* NOTE: DO NOT REORDER THE INDICES. CERTAIN MACROS DEPEND ON ORDER.
29 *
30 * Some code also depends the order of this enum, in particular that
31 * BTOR_INVALID_NODE is the first entry.
32 * It also relies on that BTOR_PROXY_NODE is BTOR_NUM_OPS_NODE - 1.
33 *
34 * FURTHER NOTE:
35 * binary nodes: [BTOR_BV_AND_NODE, ..., BTOR_LAMBDA_NODE]
36 * ternary nodes: [BTOR_BCOND_NODE]
37 * commutative nodes: [BTOR_BV_AND_NODE, ..., BTOR_BV_MUL_NODE]
38 */
39 enum BtorNodeKind
40 {
41 BTOR_INVALID_NODE = 0, /* for debugging purposes only */
42 BTOR_BV_CONST_NODE,
43 BTOR_VAR_NODE,
44 BTOR_PARAM_NODE, /* parameter for lambda expressions */
45 BTOR_BV_SLICE_NODE,
46 BTOR_BV_AND_NODE,
47 BTOR_BV_EQ_NODE, /* equality on bit vectors */
48 BTOR_FUN_EQ_NODE, /* equality on arrays */
49 BTOR_BV_ADD_NODE,
50 BTOR_BV_MUL_NODE,
51 BTOR_BV_ULT_NODE,
52 BTOR_BV_SLL_NODE,
53 BTOR_BV_SRL_NODE,
54 BTOR_BV_UDIV_NODE,
55 BTOR_BV_UREM_NODE,
56 BTOR_BV_CONCAT_NODE,
57 BTOR_APPLY_NODE,
58 BTOR_FORALL_NODE,
59 BTOR_EXISTS_NODE,
60 BTOR_LAMBDA_NODE, /* lambda expression */
61 BTOR_COND_NODE, /* conditional on bit vectors */
62 BTOR_ARGS_NODE,
63 BTOR_UPDATE_NODE,
64 BTOR_UF_NODE,
65 BTOR_PROXY_NODE, /* simplified expression without children */
66 BTOR_NUM_OPS_NODE
67
68 // NOTE: do not change this without changing 'g_btor_op2string' too ...
69 };
70
71 typedef enum BtorNodeKind BtorNodeKind;
72
73 extern const char *const g_btor_op2str[BTOR_NUM_OPS_NODE];
74
75 /*------------------------------------------------------------------------*/
76
77 #define BTOR_NODE_STRUCT \
78 struct \
79 { \
80 BtorNodeKind kind : 5; /* kind of expression */ \
81 uint8_t constraint : 1; /* top level constraint ? */ \
82 uint8_t erased : 1; /* for debugging purposes */ \
83 uint8_t disconnected : 1; /* for debugging purposes */ \
84 uint8_t unique : 1; /* in unique table? */ \
85 uint8_t parameterized : 1; /* param as sub expression ? */ \
86 uint8_t lambda_below : 1; /* lambda as sub expression ? */ \
87 uint8_t quantifier_below : 1; /* quantifier as sub expression ? */ \
88 uint8_t apply_below : 1; /* apply as sub expression ? */ \
89 uint8_t propagated : 1; /* is set during propagation */ \
90 uint8_t is_array : 1; /* function represents array ? */ \
91 uint8_t rebuild : 1; /* indicates whether rebuild is required \
92 during substitution */ \
93 uint8_t arity : 2; /* arity of operator (at most 3) */ \
94 uint8_t bytes; /* allocated bytes */ \
95 int32_t id; /* unique expression id */ \
96 uint32_t refs; /* reference counter (incl. ext_refs) */ \
97 uint32_t ext_refs; /* external references counter */ \
98 uint32_t parents; /* number of parents */ \
99 BtorSortId sort_id; /* sort id */ \
100 union \
101 { \
102 BtorAIGVec *av; /* synthesized AIG vector */ \
103 BtorPtrHashTable *rho; /* for finding array conflicts */ \
104 }; \
105 BtorNode *next; /* next in unique table */ \
106 BtorNode *simplified; /* simplified expression */ \
107 Btor *btor; /* boolector instance */ \
108 BtorNode *first_parent; /* head of parent list */ \
109 BtorNode *last_parent; /* tail of parent list */ \
110 }
111
112 #define BTOR_BV_ADDITIONAL_NODE_STRUCT \
113 struct \
114 { \
115 BtorNode *e[3]; /* expression children */ \
116 BtorNode *prev_parent[3]; /* prev in parent list of child i */ \
117 BtorNode *next_parent[3]; /* next in parent list of child i */ \
118 }
119
120 #define BTOR_FP_ADDITIONAL_NODE_STRUCT \
121 struct \
122 { \
123 BtorNode *e[4]; /* expression children */ \
124 BtorNode *prev_parent[4]; /* prev in parent list of child i */ \
125 BtorNode *next_parent[4]; /* next in parent list of child i */ \
126 }
127
128 /*------------------------------------------------------------------------*/
129
130 struct BtorBVVarNode
131 {
132 BTOR_NODE_STRUCT;
133 };
134 typedef struct BtorBVVarNode BtorBVVarNode;
135
136 struct BtorUFNode
137 {
138 BTOR_NODE_STRUCT;
139 };
140 typedef struct BtorUFNode BtorUFNode;
141
142 struct BtorBVConstNode
143 {
144 BTOR_NODE_STRUCT;
145 BtorBitVector *bits;
146 BtorBitVector *invbits;
147 };
148 typedef struct BtorBVConstNode BtorBVConstNode;
149
150 struct BtorBVSliceNode
151 {
152 BTOR_NODE_STRUCT;
153 BTOR_BV_ADDITIONAL_NODE_STRUCT;
154 uint32_t upper;
155 uint32_t lower;
156 };
157 typedef struct BtorBVSliceNode BtorBVSliceNode;
158
159 struct BtorBVNode
160 {
161 BTOR_NODE_STRUCT;
162 BTOR_BV_ADDITIONAL_NODE_STRUCT;
163 };
164 typedef struct BtorBVNode BtorBVNode;
165
166 /*------------------------------------------------------------------------*/
167
168 struct BtorNode
169 {
170 BTOR_NODE_STRUCT;
171 BTOR_BV_ADDITIONAL_NODE_STRUCT;
172 };
173
174 /*------------------------------------------------------------------------*/
175
176 struct BtorFPVarNode
177 {
178 BTOR_NODE_STRUCT;
179 };
180 typedef struct BtorFPVarNode BtorFPVarNode;
181
182 struct BtorFPNode
183 {
184 BTOR_NODE_STRUCT;
185 BTOR_FP_ADDITIONAL_NODE_STRUCT;
186 };
187 typedef struct BtorFPNode BtorFPNode;
188
189 /*------------------------------------------------------------------------*/
190
191 #define BTOR_BINDER_STRUCT \
192 struct \
193 { \
194 BTOR_NODE_STRUCT; \
195 BTOR_BV_ADDITIONAL_NODE_STRUCT; \
196 BtorNode *body; /* short-cut for curried binder terms */ \
197 }
198
199 struct BtorBinderNode
200 {
201 BTOR_BINDER_STRUCT;
202 };
203 typedef struct BtorBinderNode BtorBinderNode;
204
205 struct BtorLambdaNode
206 {
207 BTOR_BINDER_STRUCT;
208 BtorPtrHashTable *static_rho;
209 };
210 typedef struct BtorLambdaNode BtorLambdaNode;
211
212 struct BtorParamNode
213 {
214 BTOR_NODE_STRUCT;
215 BtorNode *binder; /* exp that binds the param (lambda, forall, exists) */
216 BtorNode *assigned_exp;
217 };
218 typedef struct BtorParamNode BtorParamNode;
219
220 struct BtorArgsNode
221 {
222 BTOR_NODE_STRUCT;
223 BTOR_BV_ADDITIONAL_NODE_STRUCT;
224 };
225 typedef struct BtorArgsNode BtorArgsNode;
226
227 /*------------------------------------------------------------------------*/
228
229 static inline BtorNode *
btor_node_set_tag(BtorNode * node,uintptr_t tag)230 btor_node_set_tag (BtorNode *node, uintptr_t tag)
231 {
232 assert (tag <= 3);
233 return (BtorNode *) (tag | (uintptr_t) node);
234 }
235
236 static inline BtorNode *
btor_node_invert(const BtorNode * node)237 btor_node_invert (const BtorNode *node)
238 {
239 return (BtorNode *) ((uintptr_t) 1 ^ (uintptr_t) node);
240 }
241
242 static inline BtorNode *
btor_node_cond_invert(const BtorNode * cond,const BtorNode * node)243 btor_node_cond_invert (const BtorNode *cond, const BtorNode *node)
244 {
245 return (BtorNode *) (((uintptr_t) cond & (uintptr_t) 1) ^ (uintptr_t) node);
246 }
247
248 static inline bool
btor_node_is_inverted(const BtorNode * node)249 btor_node_is_inverted (const BtorNode *node)
250 {
251 return ((uintptr_t) 1 & (uintptr_t) node) != 0;
252 }
253
254 static inline BtorNode *
btor_node_real_addr(const BtorNode * node)255 btor_node_real_addr (const BtorNode *node)
256 {
257 return (BtorNode *) (~(uintptr_t) 3 & (uintptr_t) node);
258 }
259
260 static inline bool
btor_node_is_regular(const BtorNode * node)261 btor_node_is_regular (const BtorNode *node)
262 {
263 return ((uintptr_t) 3 & (uintptr_t) node) == 0;
264 }
265
266 static inline bool
btor_node_is_synth(const BtorNode * node)267 btor_node_is_synth (const BtorNode *node)
268 {
269 return btor_node_real_addr (node)->av != 0;
270 }
271
272 /*------------------------------------------------------------------------*/
273
274 static inline bool
btor_node_is_unary_kind(BtorNodeKind kind)275 btor_node_is_unary_kind (BtorNodeKind kind)
276 {
277 return kind == BTOR_BV_SLICE_NODE;
278 }
279
280 static inline bool
btor_node_is_binary_kind(BtorNodeKind kind)281 btor_node_is_binary_kind (BtorNodeKind kind)
282 {
283 return kind >= BTOR_BV_AND_NODE && kind <= BTOR_LAMBDA_NODE;
284 }
285
286 static inline bool
btor_node_is_binary_commutative_kind(BtorNodeKind kind)287 btor_node_is_binary_commutative_kind (BtorNodeKind kind)
288 {
289 return kind >= BTOR_BV_AND_NODE && kind <= BTOR_BV_MUL_NODE;
290 }
291
292 static inline bool
btor_node_is_ternary_kind(BtorNodeKind kind)293 btor_node_is_ternary_kind (BtorNodeKind kind)
294 {
295 return kind >= BTOR_COND_NODE && kind <= BTOR_UPDATE_NODE;
296 }
297
298 static inline bool
btor_node_is_unary(const BtorNode * exp)299 btor_node_is_unary (const BtorNode *exp)
300 {
301 assert (exp);
302 return btor_node_is_unary_kind (btor_node_real_addr (exp)->kind);
303 }
304
305 static inline bool
btor_node_is_binary(const BtorNode * exp)306 btor_node_is_binary (const BtorNode *exp)
307 {
308 assert (exp);
309 return btor_node_is_binary_kind (btor_node_real_addr (exp)->kind);
310 }
311
312 static inline bool
btor_node_is_binary_commutative(const BtorNode * exp)313 btor_node_is_binary_commutative (const BtorNode *exp)
314 {
315 assert (exp);
316 return btor_node_is_binary_commutative_kind (btor_node_real_addr (exp)->kind);
317 }
318
319 static inline bool
btor_node_is_ternary(const BtorNode * exp)320 btor_node_is_ternary (const BtorNode *exp)
321 {
322 assert (exp);
323 return btor_node_is_ternary_kind (btor_node_real_addr (exp)->kind);
324 }
325
326 static inline bool
btor_node_is_invalid(const BtorNode * exp)327 btor_node_is_invalid (const BtorNode *exp)
328 {
329 assert (exp);
330 return btor_node_real_addr (exp)->kind == BTOR_INVALID_NODE;
331 }
332
333 static inline bool
btor_node_is_proxy(const BtorNode * exp)334 btor_node_is_proxy (const BtorNode *exp)
335 {
336 assert (exp);
337 return btor_node_real_addr (exp)->kind == BTOR_PROXY_NODE;
338 }
339
340 static inline bool
btor_node_is_bv_const(const BtorNode * exp)341 btor_node_is_bv_const (const BtorNode *exp)
342 {
343 assert (exp);
344 exp = btor_node_real_addr (exp);
345 return btor_sort_is_bv (exp->btor, exp->sort_id)
346 && exp->kind == BTOR_BV_CONST_NODE;
347 }
348
349 static inline bool
btor_node_is_bv_var(const BtorNode * exp)350 btor_node_is_bv_var (const BtorNode *exp)
351 {
352 assert (exp);
353 exp = btor_node_real_addr (exp);
354 return btor_sort_is_bv (exp->btor, exp->sort_id)
355 && exp->kind == BTOR_VAR_NODE;
356 }
357
358 static inline bool
btor_node_is_bv_eq(const BtorNode * exp)359 btor_node_is_bv_eq (const BtorNode *exp)
360 {
361 assert (exp);
362 return btor_node_real_addr (exp)->kind == BTOR_BV_EQ_NODE;
363 }
364
365 static inline bool
btor_node_is_fun_eq(const BtorNode * exp)366 btor_node_is_fun_eq (const BtorNode *exp)
367 {
368 assert (exp);
369 return btor_node_real_addr (exp)->kind == BTOR_FUN_EQ_NODE;
370 }
371
372 static inline bool
btor_node_is_bv_and(const BtorNode * exp)373 btor_node_is_bv_and (const BtorNode *exp)
374 {
375 assert (exp);
376 return btor_node_real_addr (exp)->kind == BTOR_BV_AND_NODE;
377 }
378
379 static inline bool
btor_node_is_bv_ult(const BtorNode * exp)380 btor_node_is_bv_ult (const BtorNode *exp)
381 {
382 assert (exp);
383 return btor_node_real_addr (exp)->kind == BTOR_BV_ULT_NODE;
384 }
385
386 static inline bool
btor_node_is_bv_add(const BtorNode * exp)387 btor_node_is_bv_add (const BtorNode *exp)
388 {
389 assert (exp);
390 return btor_node_real_addr (exp)->kind == BTOR_BV_ADD_NODE;
391 }
392
393 static inline bool
btor_node_is_bv_mul(const BtorNode * exp)394 btor_node_is_bv_mul (const BtorNode *exp)
395 {
396 assert (exp);
397 return btor_node_real_addr (exp)->kind == BTOR_BV_MUL_NODE;
398 }
399
400 static inline bool
btor_node_is_bv_udiv(const BtorNode * exp)401 btor_node_is_bv_udiv (const BtorNode *exp)
402 {
403 assert (exp);
404 return btor_node_real_addr (exp)->kind == BTOR_BV_UDIV_NODE;
405 }
406
407 static inline bool
btor_node_is_bv_urem(const BtorNode * exp)408 btor_node_is_bv_urem (const BtorNode *exp)
409 {
410 assert (exp);
411 return btor_node_real_addr (exp)->kind == BTOR_BV_UREM_NODE;
412 }
413
414 static inline bool
btor_node_is_bv_slice(const BtorNode * exp)415 btor_node_is_bv_slice (const BtorNode *exp)
416 {
417 assert (exp);
418 return btor_node_real_addr (exp)->kind == BTOR_BV_SLICE_NODE;
419 }
420
421 static inline bool
btor_node_is_bv_concat(const BtorNode * exp)422 btor_node_is_bv_concat (const BtorNode *exp)
423 {
424 assert (exp);
425 return btor_node_real_addr (exp)->kind == BTOR_BV_CONCAT_NODE;
426 }
427
428 static inline bool
btor_node_is_cond(const BtorNode * exp)429 btor_node_is_cond (const BtorNode *exp)
430 {
431 assert (exp);
432 return btor_node_real_addr (exp)->kind == BTOR_COND_NODE;
433 }
434
435 bool btor_node_is_bv_cond (const BtorNode *exp);
436 bool btor_node_is_fun_cond (const BtorNode *exp);
437
438 static inline bool
btor_node_is_uf(const BtorNode * exp)439 btor_node_is_uf (const BtorNode *exp)
440 {
441 assert (exp);
442 return btor_node_real_addr (exp)->kind == BTOR_UF_NODE;
443 }
444
445 static inline bool
btor_node_is_array(const BtorNode * exp)446 btor_node_is_array (const BtorNode *exp)
447 {
448 assert (exp);
449 return btor_node_real_addr (exp)->is_array == 1;
450 }
451
452 static inline bool
btor_node_is_const_array(const BtorNode * exp)453 btor_node_is_const_array (const BtorNode *exp)
454 {
455 assert (exp);
456 exp = btor_node_real_addr (exp);
457 return btor_node_is_array (exp) && exp->kind == BTOR_LAMBDA_NODE
458 && !btor_node_real_addr (exp->e[1])->parameterized;
459 }
460
461 static inline bool
btor_node_is_forall(const BtorNode * exp)462 btor_node_is_forall (const BtorNode *exp)
463 {
464 assert (exp);
465 return btor_node_real_addr (exp)->kind == BTOR_FORALL_NODE;
466 }
467
468 static inline bool
btor_node_is_exists(const BtorNode * exp)469 btor_node_is_exists (const BtorNode *exp)
470 {
471 assert (exp);
472 return btor_node_real_addr (exp)->kind == BTOR_EXISTS_NODE;
473 }
474
475 static inline bool
btor_node_is_quantifier(const BtorNode * exp)476 btor_node_is_quantifier (const BtorNode *exp)
477 {
478 return btor_node_is_forall (exp) || btor_node_is_exists (exp);
479 }
480
481 static inline bool
btor_node_is_lambda(const BtorNode * exp)482 btor_node_is_lambda (const BtorNode *exp)
483 {
484 assert (exp);
485 return btor_node_real_addr (exp)->kind == BTOR_LAMBDA_NODE;
486 }
487
488 static inline bool
btor_node_is_binder(const BtorNode * exp)489 btor_node_is_binder (const BtorNode *exp)
490 {
491 return btor_node_is_quantifier (exp) || btor_node_is_lambda (exp);
492 }
493
494 static inline bool
btor_node_is_update(const BtorNode * exp)495 btor_node_is_update (const BtorNode *exp)
496 {
497 assert (exp);
498 return btor_node_real_addr (exp)->kind == BTOR_UPDATE_NODE;
499 }
500
501 static inline bool
btor_node_is_fun(const BtorNode * exp)502 btor_node_is_fun (const BtorNode *exp)
503 {
504 return btor_node_is_lambda (exp) || btor_node_is_uf (exp)
505 || btor_node_is_fun_cond (exp) || btor_node_is_update (exp);
506 }
507
508 static inline bool
btor_node_is_uf_array(const BtorNode * exp)509 btor_node_is_uf_array (const BtorNode *exp)
510 {
511 return btor_node_is_uf (exp)
512 && ((BtorUFNode *) btor_node_real_addr (exp))->is_array;
513 }
514
515 static inline bool
btor_node_is_param(const BtorNode * exp)516 btor_node_is_param (const BtorNode *exp)
517 {
518 assert (exp);
519 return btor_node_real_addr (exp)->kind == BTOR_PARAM_NODE;
520 }
521
522 static inline bool
btor_node_is_args(const BtorNode * exp)523 btor_node_is_args (const BtorNode *exp)
524 {
525 assert (exp);
526 return btor_node_real_addr (exp)->kind == BTOR_ARGS_NODE;
527 }
528
529 static inline bool
btor_node_is_apply(const BtorNode * exp)530 btor_node_is_apply (const BtorNode *exp)
531 {
532 assert (exp);
533 return btor_node_real_addr (exp)->kind == BTOR_APPLY_NODE;
534 }
535
536 static inline bool
btor_node_is_array_or_bv_eq(const BtorNode * exp)537 btor_node_is_array_or_bv_eq (const BtorNode *exp)
538 {
539 return btor_node_is_fun_eq (exp) || btor_node_is_bv_eq (exp);
540 }
541
542 static inline bool
btor_node_is_bv_sll(const BtorNode * exp)543 btor_node_is_bv_sll (const BtorNode *exp)
544 {
545 return btor_node_real_addr (exp)->kind == BTOR_BV_SLL_NODE;
546 }
547
548 static inline bool
btor_node_is_bv_srl(const BtorNode * exp)549 btor_node_is_bv_srl (const BtorNode *exp)
550 {
551 return btor_node_real_addr (exp)->kind == BTOR_BV_SRL_NODE;
552 }
553
554 /*------------------------------------------------------------------------*/
555
556 bool btor_node_is_bv_const_zero (Btor *btor, BtorNode *exp);
557 bool btor_node_is_bv_const_one (Btor *btor, BtorNode *exp);
558 bool btor_node_is_bv_const_ones (Btor *btor, BtorNode *exp);
559
560 bool btor_node_is_bv_const_min_signed (Btor *btor, BtorNode *exp);
561 bool btor_node_is_bv_const_max_signed (Btor *btor, BtorNode *exp);
562
563 bool btor_node_bv_is_neg (Btor *btor, BtorNode *exp, BtorNode **res);
564
565 /*------------------------------------------------------------------------*/
566
567 /* Get the id of an expression (negative if exp is inverted). */
568 static inline int32_t
btor_node_get_id(const BtorNode * exp)569 btor_node_get_id (const BtorNode *exp)
570 {
571 assert (exp);
572 return btor_node_is_inverted (exp) ? -btor_node_real_addr (exp)->id : exp->id;
573 }
574
575 static inline int32_t
btor_node_get_tag(const BtorNode * exp)576 btor_node_get_tag (const BtorNode *exp)
577 {
578 return (int32_t) ((uintptr_t) 3 & (uintptr_t) exp);
579 }
580
581 /*========================================================================*/
582
583 /* Copies expression (increments reference counter). */
584 BtorNode *btor_node_copy (Btor *btor, BtorNode *exp);
585
586 /* Releases expression (decrements reference counter). */
587 void btor_node_release (Btor *btor, BtorNode *exp);
588
589 /*------------------------------------------------------------------------*/
590
591 /* Get the id of the sort of the given node.
592 * Do not release the returned sort. */
593 static inline BtorSortId
btor_node_get_sort_id(const BtorNode * exp)594 btor_node_get_sort_id (const BtorNode *exp)
595 {
596 assert (exp);
597 return btor_node_real_addr (exp)->sort_id;
598 }
599
600 /* Set the sort id of the given node. */
601 static inline void
btor_node_set_sort_id(BtorNode * exp,BtorSortId id)602 btor_node_set_sort_id (BtorNode *exp, BtorSortId id)
603 {
604 assert (exp);
605 btor_node_real_addr (exp)->sort_id = id;
606 }
607
608 /*------------------------------------------------------------------------*/
609
610 void btor_node_inc_ext_ref_counter (Btor *btor, BtorNode *e);
611
612 void btor_node_dec_ext_ref_counter (Btor *btor, BtorNode *e);
613
614 /*------------------------------------------------------------------------*/
615
616 /* Convert 'exp' to a proxy expression.
617 * NOTE: 'exp' must be already simplified */
618 void btor_node_set_to_proxy (Btor *btor, BtorNode *exp);
619
620 static inline bool
btor_node_is_simplified(const BtorNode * exp)621 btor_node_is_simplified (const BtorNode *exp)
622 {
623 return btor_node_real_addr (exp)->simplified != 0;
624 }
625
626 /*------------------------------------------------------------------------*/
627
628 /* Set parsed id (BTOR format only, needed for model output). */
629 void btor_node_set_btor_id (Btor *btor, BtorNode *exp, int32_t id);
630
631 /* Get parsed id (BTOR format only, needed for model output). */
632 int32_t btor_node_get_btor_id (BtorNode *exp);
633
634 /* Get the exp (belonging to instance 'btor') that matches given id.
635 * Note: The main difference to 'btor_node_match_by_id' is that this function
636 * does NOT increase the reference counter, and passing and 'id' < 0
637 * will return an inverted node */
638 BtorNode *btor_node_get_by_id (Btor *btor, int32_t id);
639
640 /* Retrieve the exp (belonging to instance 'btor') that matches given id.
641 * Note: increases ref counter of returned match!
642 * Note: 'id' must be greater 0
643 * -> will not return a conditionally inverted node */
644 BtorNode *btor_node_match_by_id (Btor *btor, int32_t id);
645
646 /*------------------------------------------------------------------------*/
647
648 /* Gets the symbol of an expression. */
649 char *btor_node_get_symbol (Btor *btor, const BtorNode *exp);
650
651 /* Sets the symbol of an expression. */
652 void btor_node_set_symbol (Btor *btor, BtorNode *exp, const char *symbol);
653
654 /* Get the exp (belonging to instance 'btor') that matches given symbol.
655 * Note: does NOT increase the ref counter */
656 BtorNode *btor_node_get_by_symbol (Btor *btor, const char *sym);
657
658 /* Retrieve the exp (belonging to instance 'btor') that matches given symbol.
659 * Note: increases ref counter of returned match! */
660 BtorNode *btor_node_match_by_symbol (Btor *btor, const char *sym);
661
662 /*------------------------------------------------------------------------*/
663
664 /* Retrieve the exp (belonging to instance 'btor') that matches given
665 * expression by id. This is intended to be used for handling expressions
666 * of a cloned instance (in a clone and its parent, expressions
667 * with the same id correspond to each other, i.e. initially, the cloned
668 * expression is an identical copy of the parent expression).
669 * (Note: increases ref counter of return match!) */
670 BtorNode *btor_node_match (Btor *btor, BtorNode *exp);
671
672 /*------------------------------------------------------------------------*/
673
674 /* Compares two expression pairs by ID */
675 int32_t btor_node_compare_by_id (const BtorNode *exp0, const BtorNode *exp1);
676 /* Compare function for expressions (by ID) to be used for qsort */
677 int32_t btor_node_compare_by_id_qsort_desc (const void *p, const void *q);
678 int32_t btor_node_compare_by_id_qsort_asc (const void *p, const void *q);
679
680 /* Hashes expression by ID */
681 uint32_t btor_node_hash_by_id (const BtorNode *exp);
682
683 /*------------------------------------------------------------------------*/
684
685 /* Get the bit width of a bit vector expression */
686 uint32_t btor_node_bv_get_width (Btor *btor, const BtorNode *exp);
687 /* Get the bit width of the array elements / function return value. */
688 uint32_t btor_node_fun_get_width (Btor *btor, const BtorNode *exp);
689 /* Get the index width of an array expression */
690 uint32_t btor_node_array_get_index_width (Btor *btor, const BtorNode *e_array);
691
692 /*------------------------------------------------------------------------*/
693
694 BtorBitVector *btor_node_bv_const_get_bits (BtorNode *exp);
695 BtorBitVector *btor_node_bv_const_get_invbits (BtorNode *exp);
696 void btor_node_bv_const_set_bits (BtorNode *exp, BtorBitVector *bits);
697 void btor_node_bv_const_set_invbits (BtorNode *exp, BtorBitVector *bits);
698
699 /*------------------------------------------------------------------------*/
700
701 /* Gets the number of arguments of lambda expression 'exp'. */
702 uint32_t btor_node_fun_get_arity (Btor *btor, BtorNode *exp);
703
704 /* Gets the number of arguments of an argument expression 'exp'. */
705 uint32_t btor_node_args_get_arity (Btor *btor, BtorNode *exp);
706
707 /*------------------------------------------------------------------------*/
708
709 BtorNode *btor_node_binder_get_body (BtorNode *binder);
710 void btor_node_binder_set_body (BtorNode *binder, BtorNode *body);
711
712 /*------------------------------------------------------------------------*/
713
714 BtorPtrHashTable *btor_node_lambda_get_static_rho (BtorNode *lambda);
715
716 void btor_node_lambda_set_static_rho (BtorNode *lambda,
717 BtorPtrHashTable *static_rho);
718
719 BtorPtrHashTable *btor_node_lambda_copy_static_rho (Btor *btor,
720 BtorNode *lambda);
721
722 void btor_node_lambda_delete_static_rho (Btor *btor, BtorNode *lambda);
723
724 /*------------------------------------------------------------------------*/
725
726 uint32_t btor_node_bv_slice_get_upper (BtorNode *slice);
727 uint32_t btor_node_bv_slice_get_lower (BtorNode *slice);
728
729 /*------------------------------------------------------------------------*/
730
731 BtorNode *btor_node_param_get_binder (BtorNode *param);
732
733 void btor_node_param_set_binder (BtorNode *param, BtorNode *lambda);
734
735 bool btor_node_param_is_bound (BtorNode *param);
736
737 bool btor_node_param_is_exists_var (BtorNode *param);
738
739 bool btor_node_param_is_forall_var (BtorNode *param);
740
741 BtorNode *btor_node_param_get_assigned_exp (BtorNode *param);
742
743 BtorNode *btor_node_param_set_assigned_exp (BtorNode *param, BtorNode *exp);
744
745 /*------------------------------------------------------------------------*/
746
747 BtorNode *btor_node_create_bv_const (Btor *btor, const BtorBitVector *bits);
748
749 BtorNode *btor_node_create_var (Btor *btor,
750 BtorSortId sort,
751 const char *symbol);
752
753 BtorNode *btor_node_create_uf (Btor *btor, BtorSortId sort, const char *symbol);
754
755 BtorNode *btor_node_create_param (Btor *btor,
756 BtorSortId sort,
757 const char *symbol);
758
759 BtorNode *btor_node_create_bv_slice (Btor *btor,
760 BtorNode *exp,
761 uint32_t upper,
762 uint32_t lower);
763
764 BtorNode *btor_node_create_bv_and (Btor *btor, BtorNode *e0, BtorNode *e1);
765
766 BtorNode *btor_node_create_eq (Btor *btor, BtorNode *e0, BtorNode *e1);
767
768 BtorNode *btor_node_create_bv_add (Btor *btor, BtorNode *e0, BtorNode *e1);
769
770 BtorNode *btor_node_create_bv_mul (Btor *btor, BtorNode *e0, BtorNode *e1);
771
772 BtorNode *btor_node_create_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1);
773
774 BtorNode *btor_node_create_bv_sll (Btor *btor, BtorNode *e0, BtorNode *e1);
775
776 BtorNode *btor_node_create_bv_srl (Btor *btor, BtorNode *e0, BtorNode *e1);
777
778 BtorNode *btor_node_create_bv_udiv (Btor *btor, BtorNode *e0, BtorNode *e1);
779
780 BtorNode *btor_node_create_bv_urem (Btor *btor, BtorNode *e0, BtorNode *e1);
781
782 BtorNode *btor_node_create_bv_concat (Btor *btor, BtorNode *e0, BtorNode *e1);
783
784 BtorNode *btor_node_create_cond (Btor *btor,
785 BtorNode *e_cond,
786 BtorNode *e_if,
787 BtorNode *e_else);
788
789 BtorNode *btor_node_create_args (Btor *btor, BtorNode *args[], uint32_t argc);
790
791 BtorNode *btor_node_create_apply (Btor *btor, BtorNode *fun, BtorNode *args);
792
793 BtorNode *btor_node_create_lambda (Btor *btor, BtorNode *param, BtorNode *body);
794
795 BtorNode *btor_node_create_forall (Btor *btor, BtorNode *param, BtorNode *body);
796
797 BtorNode *btor_node_create_quantifier (Btor *btor,
798 BtorNodeKind kind,
799 BtorNode *param,
800 BtorNode *body);
801
802 BtorNode *btor_node_create_exists (Btor *btor, BtorNode *param, BtorNode *body);
803
804 BtorNode *btor_node_create_update (Btor *btor,
805 BtorNode *fun,
806 BtorNode *args,
807 BtorNode *value);
808
809 /*========================================================================*/
810
811 struct BtorNodePair
812 {
813 BtorNode *node1;
814 BtorNode *node2;
815 };
816
817 typedef struct BtorNodePair BtorNodePair;
818
819 BtorNodePair *btor_node_pair_new (Btor *, BtorNode *, BtorNode *);
820
821 void btor_node_pair_delete (Btor *, BtorNodePair *);
822
823 uint32_t btor_node_pair_hash (const BtorNodePair *);
824
825 int32_t btor_node_pair_compare (const BtorNodePair *, const BtorNodePair *);
826
827 #endif
828