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 /*------------------------------------------------------------------------*/
10
11 #include "boolector.h"
12
13 #include "btorabort.h"
14 #include "btorchkclone.h"
15 #include "btorclone.h"
16 #include "btorcore.h"
17 #include "btorexit.h"
18 #include "btorexp.h"
19 #include "btormodel.h"
20 #include "btorparse.h"
21 #include "btorprintmodel.h"
22 #include "btorsat.h"
23 #include "btorsort.h"
24 #include "btortrapi.h"
25 #include "dumper/btordumpaig.h"
26 #include "dumper/btordumpbtor.h"
27 #include "dumper/btordumpsmt.h"
28 #include "preprocess/btorpreprocess.h"
29 #include "utils/btorhashptr.h"
30 #include "utils/btorutil.h"
31
32 /*------------------------------------------------------------------------*/
33
34 #include <limits.h>
35 #include <stdio.h>
36 #include <string.h>
37
38 /*------------------------------------------------------------------------*/
39
40 static void
abort_aux(const char * msg)41 abort_aux (const char* msg)
42 {
43 if (btor_abort_callback.cb_fun)
44 ((void (*) (const char*)) btor_abort_callback.cb_fun) (msg);
45 }
46
47 BtorAbortCallback btor_abort_callback = {
48 .abort_fun = abort_aux, .cb_fun = btor_abort_fun};
49
50 /*------------------------------------------------------------------------*/
51
52 static void
inc_sort_ext_ref_counter(Btor * btor,BtorSortId id)53 inc_sort_ext_ref_counter (Btor *btor, BtorSortId id)
54 {
55 assert (btor);
56 assert (id);
57
58 BtorSort *sort;
59 sort = btor_sort_get_by_id (btor, id);
60
61 BTOR_ABORT (sort->ext_refs == INT32_MAX, "Node reference counter overflow");
62 sort->ext_refs += 1;
63 btor->external_refs += 1;
64 }
65
66 static void
dec_sort_ext_ref_counter(Btor * btor,BtorSortId id)67 dec_sort_ext_ref_counter (Btor *btor, BtorSortId id)
68 {
69 assert (btor);
70 assert (id);
71
72 BtorSort *sort;
73 sort = btor_sort_get_by_id (btor, id);
74 assert (sort->ext_refs > 0);
75 sort->ext_refs -= 1;
76 btor->external_refs -= 1;
77 }
78
79 /*------------------------------------------------------------------------*/
80
81 void
boolector_chkclone(Btor * btor)82 boolector_chkclone (Btor *btor)
83 {
84 BTOR_ABORT_ARG_NULL (btor);
85 BTOR_TRAPI ("");
86
87 #ifndef NDEBUG
88 BtorBVAss *bvass, *cbvass;
89 BtorBVAssList *bvasslist, *cbvasslist;
90 BtorFunAss *funass, *cfunass;
91 BtorFunAssList *funasslist, *cfunasslist;
92 char **indices, **values, **cindices, **cvalues;
93 uint32_t i;
94
95 if (btor->clone)
96 {
97 /* force auto cleanup (might have been disabled via btormbt) */
98 btor_opt_set (btor->clone, BTOR_OPT_AUTO_CLEANUP, 1);
99 btor_delete (btor->clone);
100 btor->clone = 0;
101 }
102 /* do not generate shadow clone if sat solver does not support cloning
103 * (else only expression layer will be cloned and shadowed API function
104 * calls may fail) */
105 if (!btor_sat_mgr_has_clone_support (btor_get_sat_mgr (btor))) return;
106 btor->clone = btor_clone_btor (btor);
107 btor->clone->apitrace = 0; /* disable tracing of shadow clone */
108 assert (btor->clone->mm);
109 assert ((!btor->avmgr && !btor->clone->avmgr)
110 || (btor->avmgr && btor->clone->avmgr));
111 /* update assignment lists */
112 bvasslist = btor->bv_assignments;
113 cbvasslist = btor->clone->bv_assignments;
114 for (bvass = bvasslist->first, cbvass = cbvasslist->first; bvass;
115 bvass = bvass->next, cbvass = cbvass->next)
116 {
117 assert (cbvass);
118 assert (
119 !strcmp (btor_ass_get_bv_str (bvass), btor_ass_get_bv_str (cbvass)));
120 bvass->cloned_assignment = btor_ass_get_bv_str (cbvass);
121 }
122 funasslist = btor->fun_assignments;
123 cfunasslist = btor->clone->fun_assignments;
124 for (funass = funasslist->first, cfunass = cfunasslist->first; funass;
125 funass = funass->next, cfunass = cfunass->next)
126 {
127 assert (cfunass);
128 assert (funass->size == cfunass->size);
129 btor_ass_get_fun_indices_values (funass, &indices, &values, funass->size);
130 btor_ass_get_fun_indices_values (
131 cfunass, &cindices, &cvalues, cfunass->size);
132 for (i = 0; i < funass->size; i++)
133 {
134 assert (!strcmp (indices[i], cindices[i]));
135 assert (!strcmp (values[i], cvalues[i]));
136 }
137 funass->cloned_indices = cindices;
138 funass->cloned_values = cvalues;
139 }
140 btor_chkclone (btor, btor->clone);
141 #endif
142 }
143
144 #ifndef NDEBUG
145 #define BTOR_CLONED_EXP(exp) \
146 ((btor->clone ? BTOR_EXPORT_BOOLECTOR_NODE ( \
147 btor_node_is_inverted (exp) \
148 ? btor_node_invert (BTOR_PEEK_STACK ( \
149 btor->clone->nodes_id_table, \
150 btor_node_real_addr (exp)->id)) \
151 : BTOR_PEEK_STACK (btor->clone->nodes_id_table, \
152 btor_node_real_addr (exp)->id)) \
153 : 0))
154
155 #else
156 #define BTOR_CLONED_EXP(exp) 0
157 #endif
158
159 /*------------------------------------------------------------------------*/
160
161 /* for internal use (parser), only */
162
163 void
boolector_set_btor_id(Btor * btor,BoolectorNode * node,int32_t id)164 boolector_set_btor_id (Btor *btor, BoolectorNode *node, int32_t id)
165 {
166 BtorNode *exp;
167
168 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
169 BTOR_ABORT_ARG_NULL (btor);
170 BTOR_TRAPI_UNFUN_EXT (exp, "%d", id);
171 BTOR_ABORT (!btor_node_is_bv_var (exp) && !btor_node_is_uf_array (exp),
172 "'exp' is neither BV/array variable nor UF");
173 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
174 btor_node_set_btor_id (btor, exp, id);
175 #ifndef NDEBUG
176 BTOR_CHKCLONE_NORES (set_btor_id, BTOR_CLONED_EXP (exp), id);
177 #endif
178 }
179
180 BtorMsg *
boolector_get_btor_msg(Btor * btor)181 boolector_get_btor_msg (Btor *btor)
182 {
183 BtorMsg *res;
184 /* do not trace, clutters the trace unnecessarily */
185 res = btor->msg;
186 #ifndef NDEBUG
187 BTOR_CHKCLONE_NORES (get_btor_msg);
188 #endif
189 return res;
190 }
191
192 void
boolector_print_value_smt2(Btor * btor,BoolectorNode * node,char * symbol_str,FILE * file)193 boolector_print_value_smt2 (Btor *btor,
194 BoolectorNode *node,
195 char *symbol_str,
196 FILE *file)
197 {
198 BtorNode *exp;
199
200 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
201 BTOR_ABORT_ARG_NULL (btor);
202 BTOR_TRAPI_UNFUN_EXT (exp, "%s", symbol_str);
203 BTOR_ABORT_ARG_NULL (file);
204 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_SAT
205 || !btor->valid_assignments,
206 "cannot retrieve model if input formula is not SAT");
207 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
208 "model generation has not been enabled");
209 BTOR_ABORT (btor->quantifiers->count,
210 "models are currently not supported with quantifiers");
211 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
212 btor_print_value_smt2 (btor, exp, symbol_str, file);
213 #ifndef NDEBUG
214 BTOR_CHKCLONE_NORES (
215 print_value_smt2, BTOR_CLONED_EXP (exp), symbol_str, file);
216 #endif
217 }
218
219 void
boolector_var_mark_bool(Btor * btor,BoolectorNode * node)220 boolector_var_mark_bool (Btor *btor, BoolectorNode *node)
221 {
222 BtorNode *exp;
223
224 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
225 BTOR_ABORT_ARG_NULL (btor);
226 BTOR_TRAPI_UNFUN (exp);
227 BTOR_ABORT_ARG_NULL (node);
228 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
229
230 BtorPtrHashBucket *b = btor_hashptr_table_get (btor->inputs, exp);
231 assert (b);
232 b->data.flag = true;
233 #ifndef NDEBUG
234 BTOR_CHKCLONE_NORES (var_mark_bool, BTOR_CLONED_EXP (exp));
235 #endif
236 }
237
238 void
boolector_add_output(Btor * btor,BoolectorNode * node)239 boolector_add_output (Btor *btor, BoolectorNode *node)
240 {
241 BtorNode *exp;
242
243 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
244 BTOR_ABORT_ARG_NULL (btor);
245 BTOR_TRAPI_UNFUN (exp);
246 BTOR_ABORT_ARG_NULL (node);
247 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
248 BTOR_PUSH_STACK (btor->outputs, btor_node_copy (btor, exp));
249 #ifndef NDEBUG
250 BTOR_CHKCLONE_NORES (add_output, BTOR_CLONED_EXP (exp));
251 #endif
252 }
253
254 /*------------------------------------------------------------------------*/
255
256 Btor *
boolector_new(void)257 boolector_new (void)
258 {
259 char *trname;
260 Btor *btor;
261
262 btor = btor_new ();
263 if ((trname = getenv ("BTORAPITRACE"))) btor_trapi_open_trace (btor, trname);
264 BTOR_TRAPI ("");
265 BTOR_TRAPI_RETURN_PTR (btor);
266 return btor;
267 }
268
269 Btor *
boolector_clone(Btor * btor)270 boolector_clone (Btor *btor)
271 {
272 Btor *clone;
273
274 BTOR_ABORT_ARG_NULL (btor);
275 BTOR_TRAPI ("");
276 clone = btor_clone_btor (btor);
277 BTOR_TRAPI_RETURN_PTR (clone);
278 #ifndef NDEBUG
279 if (btor->clone)
280 {
281 Btor *cshadow = boolector_clone (btor->clone);
282 btor_chkclone (btor->clone, cshadow);
283 btor_delete (cshadow);
284 }
285 #endif
286 return clone;
287 }
288
289 void
boolector_delete(Btor * btor)290 boolector_delete (Btor *btor)
291 {
292 BTOR_ABORT_ARG_NULL (btor);
293 BTOR_TRAPI ("");
294 if (btor->close_apitrace == 1)
295 fclose (btor->apitrace);
296 else if (btor->close_apitrace == 2)
297 pclose (btor->apitrace);
298 #ifndef NDEBUG
299 if (btor->clone) boolector_delete (btor->clone);
300 #endif
301 btor_delete (btor);
302 }
303
304 void
boolector_set_term(Btor * btor,int32_t (* fun)(void *),void * state)305 boolector_set_term (Btor *btor, int32_t (*fun) (void *), void *state)
306 {
307 BTOR_ABORT_ARG_NULL (btor);
308 btor_set_term (btor, fun, state);
309 #ifndef NDEBUG
310 BTOR_CHKCLONE_NORES (set_term, fun, state);
311 #endif
312 }
313
314 int32_t
boolector_terminate(Btor * btor)315 boolector_terminate (Btor *btor)
316 {
317 int32_t res;
318
319 BTOR_ABORT_ARG_NULL (btor);
320 res = btor_terminate (btor);
321 #ifndef NDEBUG
322 BTOR_CHKCLONE_RES_INT (res, terminate);
323 #endif
324 return res;
325 }
326
327 void
boolector_set_abort(void (* fun)(const char * msg))328 boolector_set_abort (void (*fun) (const char* msg))
329 {
330 btor_abort_callback.abort_fun = abort_aux;
331 btor_abort_callback.cb_fun = fun;
332 }
333
334 void
boolector_set_msg_prefix(Btor * btor,const char * prefix)335 boolector_set_msg_prefix (Btor *btor, const char *prefix)
336 {
337 BTOR_ABORT_ARG_NULL (btor);
338 BTOR_TRAPI ("%s", prefix);
339 btor_set_msg_prefix (btor, prefix);
340 #ifndef NDEBUG
341 BTOR_CHKCLONE_NORES (set_msg_prefix, prefix);
342 #endif
343 }
344
345 uint32_t
boolector_get_refs(Btor * btor)346 boolector_get_refs (Btor *btor)
347 {
348 uint32_t res;
349
350 BTOR_ABORT_ARG_NULL (btor);
351 BTOR_TRAPI ("");
352 res = btor->external_refs;
353 BTOR_TRAPI_RETURN_INT (res);
354 #ifndef NDEBUG
355 BTOR_CHKCLONE_RES_UINT (res, get_refs);
356 #endif
357 return res;
358 }
359
360 void
boolector_reset_time(Btor * btor)361 boolector_reset_time (Btor *btor)
362 {
363 BTOR_ABORT_ARG_NULL (btor);
364 BTOR_TRAPI ("");
365 btor_reset_time (btor);
366 #ifndef NDEBUG
367 BTOR_CHKCLONE_NORES (reset_time);
368 #endif
369 }
370
371 void
boolector_reset_stats(Btor * btor)372 boolector_reset_stats (Btor *btor)
373 {
374 BTOR_ABORT_ARG_NULL (btor);
375 BTOR_TRAPI ("");
376 btor_reset_stats (btor);
377 #ifndef NDEBUG
378 BTOR_CHKCLONE_NORES (reset_stats);
379 #endif
380 }
381
382 void
boolector_print_stats(Btor * btor)383 boolector_print_stats (Btor *btor)
384 {
385 BTOR_ABORT_ARG_NULL (btor);
386 BTOR_TRAPI ("");
387 btor_sat_print_stats (btor_get_sat_mgr (btor));
388 btor_print_stats (btor);
389 #ifndef NDEBUG
390 BTOR_CHKCLONE_NORES (print_stats);
391 #endif
392 }
393
394 void
boolector_set_trapi(Btor * btor,FILE * apitrace)395 boolector_set_trapi (Btor *btor, FILE *apitrace)
396 {
397 BTOR_ABORT_ARG_NULL (btor);
398 BTOR_ABORT (btor->apitrace, "API trace already set");
399 btor->apitrace = apitrace;
400 }
401
402 FILE *
boolector_get_trapi(Btor * btor)403 boolector_get_trapi (Btor *btor)
404 {
405 BTOR_ABORT_ARG_NULL (btor);
406 return btor->apitrace;
407 }
408
409 /*------------------------------------------------------------------------*/
410
411 void
boolector_push(Btor * btor,uint32_t level)412 boolector_push (Btor *btor, uint32_t level)
413 {
414 BTOR_ABORT_ARG_NULL (btor);
415 BTOR_TRAPI ("%u", level);
416 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
417 "incremental usage has not been enabled");
418
419 if (level == 0) return;
420
421 uint32_t i;
422 for (i = 0; i < level; i++)
423 {
424 BTOR_PUSH_STACK (btor->assertions_trail,
425 BTOR_COUNT_STACK (btor->assertions));
426 }
427 btor->num_push_pop++;
428 }
429
430 void
boolector_pop(Btor * btor,uint32_t level)431 boolector_pop (Btor *btor, uint32_t level)
432 {
433 BTOR_ABORT_ARG_NULL (btor);
434 BTOR_TRAPI ("%u", level);
435 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
436 "incremental usage has not been enabled");
437 BTOR_ABORT (level > BTOR_COUNT_STACK (btor->assertions_trail),
438 "can not pop more levels (%u) than created via push (%u).",
439 level,
440 BTOR_COUNT_STACK (btor->assertions_trail));
441
442 if (level == 0) return;
443
444 uint32_t i, pos;
445 BtorNode *cur;
446
447 for (i = 0, pos = 0; i < level; i++)
448 pos = BTOR_POP_STACK (btor->assertions_trail);
449
450 while (BTOR_COUNT_STACK (btor->assertions) > pos)
451 {
452 cur = BTOR_POP_STACK (btor->assertions);
453 btor_hashint_table_remove (btor->assertions_cache, btor_node_get_id (cur));
454 btor_node_release (btor, cur);
455 }
456 btor->num_push_pop++;
457 }
458
459 /*------------------------------------------------------------------------*/
460
461 void
boolector_assert(Btor * btor,BoolectorNode * node)462 boolector_assert (Btor *btor, BoolectorNode *node)
463 {
464 BtorNode *exp;
465
466 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
467 BTOR_ABORT_ARG_NULL (btor);
468 BTOR_TRAPI_UNFUN (exp);
469 BTOR_ABORT_ARG_NULL (exp);
470 BTOR_ABORT_REFS_NOT_POS (exp);
471 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
472 BTOR_ABORT_IS_NOT_BV (exp);
473 BTOR_ABORT (btor_node_bv_get_width (btor, exp) != 1,
474 "'exp' must have bit-width one");
475 BTOR_ABORT (!btor_sort_is_bool (btor, btor_node_real_addr (exp)->sort_id),
476 "'exp' must have bit-width one");
477 BTOR_ABORT (btor_node_real_addr (exp)->parameterized,
478 "assertion must not be parameterized");
479
480 /* all assertions at a context level > 0 are internally handled as
481 * assumptions. */
482 if (BTOR_COUNT_STACK (btor->assertions_trail) > 0)
483 {
484 int32_t id = btor_node_get_id (exp);
485 if (!btor_hashint_table_contains (btor->assertions_cache, id))
486 {
487 BTOR_PUSH_STACK (btor->assertions, btor_node_copy (btor, exp));
488 btor_hashint_table_add (btor->assertions_cache, id);
489 }
490 }
491 else
492 btor_assert_exp (btor, exp);
493 #ifndef NDEBUG
494 BTOR_CHKCLONE_NORES (assert, BTOR_CLONED_EXP (exp));
495 #endif
496 }
497
498 void
boolector_assume(Btor * btor,BoolectorNode * node)499 boolector_assume (Btor *btor, BoolectorNode *node)
500 {
501 BtorNode *exp;
502
503 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
504 BTOR_ABORT_ARG_NULL (btor);
505 BTOR_ABORT_ARG_NULL (exp);
506 BTOR_TRAPI_UNFUN (exp);
507 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
508 "incremental usage has not been enabled");
509 BTOR_ABORT_REFS_NOT_POS (exp);
510 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
511 BTOR_ABORT_IS_NOT_BV (exp);
512 BTOR_ABORT (!btor_sort_is_bool (btor, btor_node_real_addr (exp)->sort_id),
513 "'exp' must have bit-width one");
514 BTOR_ABORT (btor_node_real_addr (exp)->parameterized,
515 "assumption must not be parameterized");
516
517 btor_assume_exp (btor, exp);
518 BTOR_PUSH_STACK (btor->failed_assumptions, btor_node_copy (btor, exp));
519 #ifndef NDEBUG
520 BTOR_CHKCLONE_NORES (assume, BTOR_CLONED_EXP (exp));
521 #endif
522 }
523
524 bool
boolector_failed(Btor * btor,BoolectorNode * node)525 boolector_failed (Btor *btor, BoolectorNode *node)
526 {
527 bool res;
528 BtorNode *exp;
529
530 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
531 BTOR_ABORT_ARG_NULL (btor);
532 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_UNSAT,
533 "cannot check failed assumptions if input formula is not UNSAT");
534 BTOR_ABORT_ARG_NULL (exp);
535 BTOR_TRAPI_UNFUN (exp);
536 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
537 "incremental usage has not been enabled");
538 BTOR_ABORT_REFS_NOT_POS (exp);
539 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
540 BTOR_ABORT_IS_NOT_BV (exp);
541 BTOR_ABORT (btor_node_bv_get_width (btor, exp) != 1,
542 "'exp' must have bit-width one");
543 BTOR_ABORT (!btor_is_assumption_exp (btor, exp),
544 "'exp' must be an assumption");
545 res = btor_failed_exp (btor, exp);
546 BTOR_TRAPI_RETURN_BOOL (res);
547 #ifndef NDEBUG
548 BTOR_CHKCLONE_RES_BOOL (res, failed, BTOR_CLONED_EXP (exp));
549 #endif
550 return res;
551 }
552
553 BoolectorNode **
boolector_get_failed_assumptions(Btor * btor)554 boolector_get_failed_assumptions (Btor *btor)
555 {
556 BoolectorNode **res;
557 BtorNodePtrStack failed;
558 BtorNode *fass;
559 uint32_t i;
560
561 BTOR_ABORT_ARG_NULL (btor);
562 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_UNSAT,
563 "cannot check failed assumptions if input formula is not UNSAT");
564
565 BTOR_INIT_STACK (btor->mm, failed);
566 for (i = 0; i < BTOR_COUNT_STACK (btor->failed_assumptions); i++)
567 {
568 fass = BTOR_PEEK_STACK (btor->failed_assumptions, i);
569 if (!fass) continue;
570 assert (btor_hashptr_table_get (btor->orig_assumptions, fass));
571 if (btor_failed_exp (btor, fass))
572 BTOR_PUSH_STACK (failed, fass);
573 else
574 btor_node_release (btor, fass);
575 }
576 BTOR_PUSH_STACK (failed, NULL);
577 BTOR_RELEASE_STACK (btor->failed_assumptions);
578 btor->failed_assumptions = failed;
579 res = (BoolectorNode **) btor->failed_assumptions.start;
580 #ifndef NDEBUG
581 if (btor->clone)
582 {
583 BoolectorNode **cloneres;
584 cloneres = boolector_get_failed_assumptions (btor->clone);
585 for (i = 0; res[i] != NULL; i++)
586 btor_chkclone_exp (btor,
587 btor->clone,
588 BTOR_IMPORT_BOOLECTOR_NODE (res[i]),
589 BTOR_IMPORT_BOOLECTOR_NODE (cloneres[i]));
590 btor_chkclone (btor, btor->clone);
591 }
592 #endif
593 return res;
594 }
595
596 void
boolector_fixate_assumptions(Btor * btor)597 boolector_fixate_assumptions (Btor *btor)
598 {
599 BTOR_ABORT_ARG_NULL (btor);
600 BTOR_TRAPI ("");
601 BTOR_ABORT (
602 !btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
603 "incremental usage has not been enabled, no assumptions available");
604 btor_fixate_assumptions (btor);
605 #ifndef NDEBUG
606 BTOR_CHKCLONE_NORES (fixate_assumptions);
607 #endif
608 }
609
610 void
boolector_reset_assumptions(Btor * btor)611 boolector_reset_assumptions (Btor *btor)
612 {
613 BTOR_ABORT_ARG_NULL (btor);
614 BTOR_TRAPI ("");
615 BTOR_ABORT (
616 !btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
617 "incremental usage has not been enabled, no assumptions available");
618 btor_reset_assumptions (btor);
619 #ifndef NDEBUG
620 BTOR_CHKCLONE_NORES (reset_assumptions);
621 #endif
622 }
623
624 /*------------------------------------------------------------------------*/
625
626 int32_t
boolector_sat(Btor * btor)627 boolector_sat (Btor *btor)
628 {
629 int32_t res;
630
631 BTOR_ABORT_ARG_NULL (btor);
632 BTOR_TRAPI ("");
633 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL)
634 && btor->btor_sat_btor_called > 0,
635 "incremental usage has not been enabled."
636 "'boolector_sat' may only be called once");
637 res = btor_check_sat (btor, -1, -1);
638 BTOR_TRAPI_RETURN_INT (res);
639 #ifndef NDEBUG
640 BTOR_CHKCLONE_RES_INT (res, sat);
641 #endif
642 return res;
643 }
644
645 int32_t
boolector_limited_sat(Btor * btor,int32_t lod_limit,int32_t sat_limit)646 boolector_limited_sat (Btor *btor, int32_t lod_limit, int32_t sat_limit)
647 {
648 int32_t res;
649 BTOR_ABORT_ARG_NULL (btor);
650 BTOR_TRAPI ("%d %d", lod_limit, sat_limit);
651 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL)
652 && btor->btor_sat_btor_called > 0,
653 "incremental usage has not been enabled."
654 "'boolector_limited_sat' may only be called once");
655 res = btor_check_sat (btor, lod_limit, sat_limit);
656 BTOR_TRAPI_RETURN_INT (res);
657 #ifndef NDEBUG
658 BTOR_CHKCLONE_RES_INT (res, limited_sat, lod_limit, sat_limit);
659 #endif
660 return res;
661 }
662
663 /*------------------------------------------------------------------------*/
664
665 int32_t
boolector_simplify(Btor * btor)666 boolector_simplify (Btor *btor)
667 {
668 int32_t res;
669
670 BTOR_ABORT_ARG_NULL (btor);
671 BTOR_TRAPI ("");
672
673 res = btor_simplify (btor);
674 BTOR_TRAPI_RETURN_INT (res);
675 #ifndef NDEBUG
676 BTOR_CHKCLONE_RES_INT (res, simplify);
677 #endif
678 return res;
679 }
680
681 /*------------------------------------------------------------------------*/
682
683 void
boolector_set_sat_solver(Btor * btor,const char * solver)684 boolector_set_sat_solver (Btor *btor, const char *solver)
685 {
686 BtorPtrHashBucket *b;
687 uint32_t sat_engine, oldval;
688
689 BTOR_ABORT_ARG_NULL (btor);
690 BTOR_TRAPI ("%s", solver);
691 BTOR_ABORT_ARG_NULL (solver);
692 BTOR_ABORT (
693 btor->btor_sat_btor_called > 0,
694 "setting the SAT solver must be done before calling 'boolector_sat'");
695
696 sat_engine = BTOR_SAT_ENGINE_DFLT;
697 oldval = btor_opt_get (btor, BTOR_OPT_SAT_ENGINE);
698
699 if ((b = btor_hashptr_table_get (btor->options[BTOR_OPT_SAT_ENGINE].options,
700 solver)))
701 {
702 sat_engine = ((BtorOptHelp *) b->data.as_ptr)->val;
703 }
704 else
705 BTOR_ABORT (1, "invalid sat engine '%s' selected", solver);
706
707 if (false
708 #ifndef BTOR_USE_LINGELING
709 || sat_engine == BTOR_SAT_ENGINE_LINGELING
710 #endif
711 #ifndef BTOR_USE_CADICAL
712 || sat_engine == BTOR_SAT_ENGINE_CADICAL
713 #endif
714 #ifndef BTOR_USE_MINISAT
715 || sat_engine == BTOR_SAT_ENGINE_MINISAT
716 #endif
717 #ifndef BTOR_USE_PICOSAT
718 || sat_engine == BTOR_SAT_ENGINE_PICOSAT
719 #endif
720 #ifndef BTOR_USE_CMS
721 || sat_engine == BTOR_SAT_ENGINE_CMS
722 #endif
723 )
724 {
725 BTOR_WARN (true,
726 "SAT solver %s not compiled in, using %s",
727 g_btor_se_name[sat_engine],
728 g_btor_se_name[oldval]);
729 sat_engine = oldval;
730 }
731
732 btor_opt_set (btor, BTOR_OPT_SAT_ENGINE, sat_engine);
733 #ifndef NDEBUG
734 BTOR_CHKCLONE_NORES (set_sat_solver, solver);
735 #endif
736 }
737
738 /*------------------------------------------------------------------------*/
739
740 void
boolector_set_opt(Btor * btor,BtorOption opt,uint32_t val)741 boolector_set_opt (Btor *btor, BtorOption opt, uint32_t val)
742 {
743 BTOR_ABORT_ARG_NULL (btor);
744 BTOR_TRAPI ("%u %s %u", opt, btor_opt_get_lng (btor, opt), val);
745 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
746 BTOR_ABORT (
747 val < btor_opt_get_min (btor, opt) || val > btor_opt_get_max (btor, opt),
748 "invalid option value '%u' for option '%s'",
749 val,
750 btor_opt_get_lng (btor, opt));
751
752 if (val)
753 {
754 if (opt == BTOR_OPT_INCREMENTAL)
755 {
756 BTOR_ABORT (btor->btor_sat_btor_called > 0,
757 "enabling/disabling incremental usage must be done "
758 "before calling 'boolector_sat'");
759 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_UCOPT),
760 "incremental solving cannot be enabled "
761 "if unconstrained optimization is enabled");
762 }
763 else if (opt == BTOR_OPT_UCOPT)
764 {
765 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
766 "Unconstrained optimization cannot be enabled "
767 "if model generation is enabled");
768 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
769 "Unconstrained optimization cannot be enabled "
770 "in incremental mode");
771 }
772 else if (opt == BTOR_OPT_FUN_DUAL_PROP)
773 {
774 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_FUN_JUST),
775 "enabling multiple optimization techniques is not allowed");
776 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST),
777 "Non-destructive substitution is not supported with dual "
778 "propagation");
779 }
780 else if (opt == BTOR_OPT_FUN_JUST)
781 {
782 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_FUN_DUAL_PROP),
783 "enabling multiple optimization techniques is not allowed");
784 }
785 else if (opt == BTOR_OPT_NONDESTR_SUBST)
786 {
787 BTOR_ABORT (btor_opt_get (btor, BTOR_OPT_FUN_DUAL_PROP),
788 "Non-destructive substitution is not supported with dual "
789 "propagation");
790 }
791 }
792
793 uint32_t oldval = btor_opt_get (btor, opt);
794
795 if (opt == BTOR_OPT_SAT_ENGINE)
796 {
797 if (false
798 #ifndef BTOR_USE_LINGELING
799 || val == BTOR_SAT_ENGINE_LINGELING
800 #endif
801 #ifndef BTOR_USE_CADICAL
802 || val == BTOR_SAT_ENGINE_CADICAL
803 #endif
804 #ifndef BTOR_USE_MINISAT
805 || val == BTOR_SAT_ENGINE_MINISAT
806 #endif
807 #ifndef BTOR_USE_PICOSAT
808 || val == BTOR_SAT_ENGINE_PICOSAT
809 #endif
810 #ifndef BTOR_USE_CMS
811 || val == BTOR_SAT_ENGINE_CMS
812 #endif
813 )
814 {
815 BTOR_WARN (true,
816 "SAT solver %s not compiled in, using %s",
817 g_btor_se_name[val],
818 g_btor_se_name[oldval]);
819 val = oldval;
820 }
821 }
822 #ifndef BTOR_USE_LINGELING
823 if (opt == BTOR_OPT_SAT_ENGINE_LGL_FORK)
824 {
825 val = oldval;
826 BTOR_MSG (btor->msg,
827 1,
828 "SAT solver Lingeling not compiled in, will not set option "
829 "to clone/fork Lingeling");
830 }
831 #endif
832
833 if (opt == BTOR_OPT_REWRITE_LEVEL)
834 {
835 BTOR_ABORT (
836 BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
837 "setting rewrite level must be done before creating expressions");
838 }
839
840 btor_opt_set (btor, opt, val);
841 #ifndef NDEBUG
842 BTOR_CHKCLONE_NORES (set_opt, opt, val);
843 #endif
844 }
845
846 uint32_t
boolector_get_opt(Btor * btor,BtorOption opt)847 boolector_get_opt (Btor *btor, BtorOption opt)
848 {
849 uint32_t res;
850 BTOR_ABORT_ARG_NULL (btor);
851 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
852 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
853 res = btor_opt_get (btor, opt);
854 BTOR_TRAPI_RETURN_UINT (res);
855 #ifndef NDEBUG
856 BTOR_CHKCLONE_RES_UINT (res, get_opt, opt);
857 #endif
858 return res;
859 }
860
861 uint32_t
boolector_get_opt_min(Btor * btor,BtorOption opt)862 boolector_get_opt_min (Btor *btor, BtorOption opt)
863 {
864 uint32_t res;
865 BTOR_ABORT_ARG_NULL (btor);
866 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
867 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
868 res = btor_opt_get_min (btor, opt);
869 BTOR_TRAPI_RETURN_UINT (res);
870 #ifndef NDEBUG
871 BTOR_CHKCLONE_RES_UINT (res, get_opt_min, opt);
872 #endif
873 return res;
874 }
875
876 uint32_t
boolector_get_opt_max(Btor * btor,BtorOption opt)877 boolector_get_opt_max (Btor *btor, BtorOption opt)
878 {
879 uint32_t res;
880 BTOR_ABORT_ARG_NULL (btor);
881 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
882 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
883 res = btor_opt_get_max (btor, opt);
884 BTOR_TRAPI_RETURN_UINT (res);
885 #ifndef NDEBUG
886 BTOR_CHKCLONE_RES_UINT (res, get_opt_max, opt);
887 #endif
888 return res;
889 }
890
891 uint32_t
boolector_get_opt_dflt(Btor * btor,BtorOption opt)892 boolector_get_opt_dflt (Btor *btor, BtorOption opt)
893 {
894 uint32_t res;
895 BTOR_ABORT_ARG_NULL (btor);
896 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
897 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
898 res = btor_opt_get_dflt (btor, opt);
899 BTOR_TRAPI_RETURN_UINT (res);
900 #ifndef NDEBUG
901 BTOR_CHKCLONE_RES_UINT (res, get_opt_dflt, opt);
902 #endif
903 return res;
904 }
905
906 const char *
boolector_get_opt_lng(Btor * btor,BtorOption opt)907 boolector_get_opt_lng (Btor *btor, BtorOption opt)
908 {
909 const char *res;
910 BTOR_ABORT_ARG_NULL (btor);
911 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
912 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
913 res = btor_opt_get_lng (btor, opt);
914 BTOR_TRAPI_RETURN_STR (res);
915 #ifndef NDEBUG
916 BTOR_CHKCLONE_RES_STR (res, get_opt_lng, opt);
917 #endif
918 return res;
919 }
920
921 const char *
boolector_get_opt_shrt(Btor * btor,BtorOption opt)922 boolector_get_opt_shrt (Btor *btor, BtorOption opt)
923 {
924 const char *res;
925 BTOR_ABORT_ARG_NULL (btor);
926 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
927 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
928 res = btor_opt_get_shrt (btor, opt);
929 BTOR_TRAPI_RETURN_STR (res);
930 #ifndef NDEBUG
931 BTOR_CHKCLONE_RES_STR (res, get_opt_shrt, opt);
932 #endif
933 return res;
934 }
935
936 const char *
boolector_get_opt_desc(Btor * btor,BtorOption opt)937 boolector_get_opt_desc (Btor *btor, BtorOption opt)
938 {
939 const char *res;
940 BTOR_ABORT_ARG_NULL (btor);
941 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
942 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
943 res = btor_opt_get_desc (btor, opt);
944 BTOR_TRAPI_RETURN_STR (res);
945 #ifndef NDEBUG
946 BTOR_CHKCLONE_RES_STR (res, get_opt_desc, opt);
947 #endif
948 return res;
949 }
950
951 bool
boolector_has_opt(Btor * btor,BtorOption opt)952 boolector_has_opt (Btor *btor, BtorOption opt)
953 {
954 bool res;
955 BTOR_ABORT_ARG_NULL (btor);
956 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
957 res = btor_opt_is_valid (btor, opt);
958 BTOR_TRAPI_RETURN_BOOL (res);
959 #ifndef NDEBUG
960 BTOR_CHKCLONE_RES_BOOL (res, next_opt, opt);
961 #endif
962 return res;
963 }
964
965 BtorOption
boolector_first_opt(Btor * btor)966 boolector_first_opt (Btor *btor)
967 {
968 BtorOption res;
969 BTOR_ABORT_ARG_NULL (btor);
970 BTOR_TRAPI ("");
971 res = btor_opt_first (btor);
972 BTOR_TRAPI_RETURN_INT (res);
973 #ifndef NDEBUG
974 BTOR_CHKCLONE_RES_UINT (res, first_opt);
975 #endif
976 return res;
977 }
978
979 BtorOption
boolector_next_opt(Btor * btor,BtorOption opt)980 boolector_next_opt (Btor *btor, BtorOption opt)
981 {
982 BtorOption res;
983 BTOR_ABORT_ARG_NULL (btor);
984 BTOR_TRAPI ("%u %s", opt, btor_opt_get_lng (btor, opt));
985 BTOR_ABORT (!btor_opt_is_valid (btor, opt), "invalid option");
986 res = btor_opt_next (btor, opt);
987 BTOR_TRAPI_RETURN_INT (res);
988 #ifndef NDEBUG
989 BTOR_CHKCLONE_RES_UINT (res, next_opt, opt);
990 #endif
991 return res;
992 }
993
994 /*------------------------------------------------------------------------*/
995
996 BoolectorNode *
boolector_copy(Btor * btor,BoolectorNode * node)997 boolector_copy (Btor *btor, BoolectorNode *node)
998 {
999 BtorNode *exp, *res;
1000
1001 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1002 BTOR_ABORT_ARG_NULL (btor);
1003 BTOR_ABORT_ARG_NULL (exp);
1004 BTOR_TRAPI_UNFUN (exp);
1005 BTOR_ABORT_REFS_NOT_POS (exp);
1006 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1007 res = btor_node_copy (btor, exp);
1008 btor_node_inc_ext_ref_counter (btor, res);
1009 BTOR_TRAPI_RETURN_NODE (res);
1010 #ifndef NDEBUG
1011 BTOR_CHKCLONE_RES_PTR (res, copy, BTOR_CLONED_EXP (exp));
1012 #endif
1013 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1014 }
1015
1016 void
boolector_release(Btor * btor,BoolectorNode * node)1017 boolector_release (Btor *btor, BoolectorNode *node)
1018 {
1019 BtorNode *exp;
1020
1021 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1022 BTOR_ABORT_ARG_NULL (btor);
1023 BTOR_ABORT_ARG_NULL (exp);
1024 BTOR_TRAPI_UNFUN (exp);
1025 BTOR_ABORT_REFS_NOT_POS (exp);
1026 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1027 #ifndef NDEBUG
1028 BoolectorNode *cexp = BTOR_CLONED_EXP (exp);
1029 #endif
1030 assert (btor_node_real_addr (exp)->ext_refs);
1031 btor_node_dec_ext_ref_counter (btor, exp);
1032 btor_node_release (btor, exp);
1033 #ifndef NDEBUG
1034 BTOR_CHKCLONE_NORES (release, cexp);
1035 #endif
1036 }
1037
1038 void
boolector_release_all(Btor * btor)1039 boolector_release_all (Btor *btor)
1040 {
1041 BTOR_ABORT_ARG_NULL (btor);
1042 BTOR_TRAPI ("");
1043 btor_release_all_ext_refs (btor);
1044 #ifndef NDEBUG
1045 BTOR_CHKCLONE_NORES (release_all);
1046 #endif
1047 }
1048
1049 /*------------------------------------------------------------------------*/
1050
1051 BoolectorNode *
boolector_true(Btor * btor)1052 boolector_true (Btor *btor)
1053 {
1054 BtorNode *res;
1055
1056 BTOR_ABORT_ARG_NULL (btor);
1057 BTOR_TRAPI ("");
1058 res = btor_exp_true (btor);
1059 btor_node_inc_ext_ref_counter (btor, res);
1060 BTOR_TRAPI_RETURN_NODE (res);
1061 #ifndef NDEBUG
1062 BTOR_CHKCLONE_RES_PTR (res, true);
1063 #endif
1064 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1065 }
1066
1067 BoolectorNode *
boolector_false(Btor * btor)1068 boolector_false (Btor *btor)
1069 {
1070 BtorNode *res;
1071
1072 BTOR_ABORT_ARG_NULL (btor);
1073 BTOR_TRAPI ("");
1074 res = btor_exp_false (btor);
1075 btor_node_inc_ext_ref_counter (btor, res);
1076 BTOR_TRAPI_RETURN_NODE (res);
1077 #ifndef NDEBUG
1078 BTOR_CHKCLONE_RES_PTR (res, false);
1079 #endif
1080 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1081 }
1082
1083 BoolectorNode *
boolector_implies(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1084 boolector_implies (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1085 {
1086 BtorNode *e0, *e1, *res;
1087
1088 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1089 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1090 BTOR_ABORT_ARG_NULL (btor);
1091 BTOR_ABORT_ARG_NULL (e0);
1092 BTOR_ABORT_ARG_NULL (e1);
1093 BTOR_TRAPI_BINFUN (e0, e1);
1094 BTOR_ABORT_REFS_NOT_POS (e0);
1095 BTOR_ABORT_REFS_NOT_POS (e1);
1096 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1097 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1098 BTOR_ABORT_IS_NOT_BV (e0);
1099 BTOR_ABORT_IS_NOT_BV (e1);
1100 BTOR_ABORT (btor_node_bv_get_width (btor, e0) != 1
1101 || btor_node_bv_get_width (btor, e1) != 1,
1102 "bit-width of 'e0' and 'e1' must be 1");
1103 res = btor_exp_implies (btor, e0, e1);
1104 btor_node_inc_ext_ref_counter (btor, res);
1105 BTOR_TRAPI_RETURN_NODE (res);
1106 #ifndef NDEBUG
1107 BTOR_CHKCLONE_RES_PTR (
1108 res, implies, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1109 #endif
1110 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1111 }
1112
1113 BoolectorNode *
boolector_iff(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1114 boolector_iff (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1115 {
1116 BtorNode *e0, *e1, *res;
1117
1118 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1119 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1120 BTOR_ABORT_ARG_NULL (btor);
1121 BTOR_ABORT_ARG_NULL (e0);
1122 BTOR_ABORT_ARG_NULL (e1);
1123 BTOR_TRAPI_BINFUN (e0, e1);
1124 BTOR_ABORT_REFS_NOT_POS (e0);
1125 BTOR_ABORT_REFS_NOT_POS (e1);
1126 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1127 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1128 BTOR_ABORT_IS_NOT_BV (e0);
1129 BTOR_ABORT_IS_NOT_BV (e1);
1130 BTOR_ABORT (btor_node_bv_get_width (btor, e0) != 1
1131 || btor_node_bv_get_width (btor, e1) != 1,
1132 "bit-width of 'e0' and 'e1' must not be unequal to 1");
1133 res = btor_exp_iff (btor, e0, e1);
1134 btor_node_inc_ext_ref_counter (btor, res);
1135 BTOR_TRAPI_RETURN_NODE (res);
1136 #ifndef NDEBUG
1137 BTOR_CHKCLONE_RES_PTR (res, iff, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1138 #endif
1139 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1140 }
1141
1142 /*------------------------------------------------------------------------*/
1143
1144 BoolectorNode *
boolector_eq(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1145 boolector_eq (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1146 {
1147 BtorNode *e0, *e1, *res;
1148
1149 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1150 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1151 BTOR_ABORT_ARG_NULL (btor);
1152 BTOR_ABORT_ARG_NULL (e0);
1153 BTOR_ABORT_ARG_NULL (e1);
1154 BTOR_TRAPI_BINFUN (e0, e1);
1155 BTOR_ABORT_REFS_NOT_POS (e0);
1156 BTOR_ABORT_REFS_NOT_POS (e1);
1157 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1158 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1159 BTOR_ABORT (btor_node_get_sort_id (e0) != btor_node_get_sort_id (e1)
1160 || btor_node_real_addr (e0)->is_array
1161 != btor_node_real_addr (e1)->is_array,
1162 "nodes must have equal sorts");
1163 BTOR_ABORT (btor_sort_is_fun (btor, btor_node_get_sort_id (e0))
1164 && (btor_node_real_addr (e0)->parameterized
1165 || btor_node_real_addr (e1)->parameterized),
1166 "parameterized function equalities not supported");
1167 res = btor_exp_eq (btor, e0, e1);
1168 btor_node_inc_ext_ref_counter (btor, res);
1169 BTOR_TRAPI_RETURN_NODE (res);
1170 #ifndef NDEBUG
1171 BTOR_CHKCLONE_RES_PTR (res, eq, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1172 #endif
1173 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1174 }
1175
1176 BoolectorNode *
boolector_ne(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1177 boolector_ne (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1178 {
1179 BtorNode *e0, *e1, *res;
1180
1181 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1182 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1183 BTOR_ABORT_ARG_NULL (btor);
1184 BTOR_ABORT_ARG_NULL (e0);
1185 BTOR_ABORT_ARG_NULL (e1);
1186 BTOR_TRAPI_BINFUN (e0, e1);
1187 BTOR_ABORT_REFS_NOT_POS (e0);
1188 BTOR_ABORT_REFS_NOT_POS (e1);
1189 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1190 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1191 BTOR_ABORT (btor_node_get_sort_id (e0) != btor_node_get_sort_id (e1),
1192 "nodes must have equal sorts");
1193 BTOR_ABORT (btor_sort_is_fun (btor, btor_node_get_sort_id (e0))
1194 && (btor_node_real_addr (e0)->parameterized
1195 || btor_node_real_addr (e1)->parameterized),
1196 "parameterized function equalities not supported");
1197 res = btor_exp_ne (btor, e0, e1);
1198 btor_node_inc_ext_ref_counter (btor, res);
1199 BTOR_TRAPI_RETURN_NODE (res);
1200 #ifndef NDEBUG
1201 BTOR_CHKCLONE_RES_PTR (res, ne, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1202 #endif
1203 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1204 }
1205
1206 /*------------------------------------------------------------------------*/
1207
1208 BoolectorNode *
boolector_const(Btor * btor,const char * bits)1209 boolector_const (Btor *btor, const char *bits)
1210 {
1211 BtorNode *res;
1212 BtorBitVector *bv;
1213
1214 BTOR_ABORT_ARG_NULL (btor);
1215 BTOR_TRAPI ("%s", bits);
1216 BTOR_ABORT_ARG_NULL (bits);
1217 BTOR_ABORT (*bits == '\0', "'bits' must not be empty");
1218 bv = btor_bv_char_to_bv (btor->mm, (char *) bits);
1219 res = btor_exp_bv_const (btor, bv);
1220 btor_node_inc_ext_ref_counter (btor, res);
1221 btor_bv_free (btor->mm, bv);
1222 BTOR_TRAPI_RETURN_NODE (res);
1223 #ifndef NDEBUG
1224 BTOR_CHKCLONE_RES_PTR (res, const, bits);
1225 #endif
1226 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1227 }
1228
1229 BoolectorNode *
boolector_constd(Btor * btor,BoolectorSort sort,const char * str)1230 boolector_constd (Btor *btor, BoolectorSort sort, const char *str)
1231 {
1232 uint32_t w;
1233 BtorNode *res;
1234 BtorBitVector *bv;
1235 BtorSortId s;
1236
1237 BTOR_ABORT_ARG_NULL (btor);
1238 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT " %s", sort, str);
1239 BTOR_ABORT_ARG_NULL (str);
1240 BTOR_ABORT (*str == '\0', "'str' must not be empty");
1241
1242 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1243 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1244 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1245 "'sort' is not a bit vector sort");
1246 w = btor_sort_bv_get_width (btor, s);
1247 BTOR_ABORT (!btor_util_check_dec_to_bv (btor->mm, str, w),
1248 "'%s' does not fit into a bit-vector of size %u",
1249 str,
1250 w);
1251 bv = btor_bv_constd (btor->mm, str, w);
1252 res = btor_exp_bv_const (btor, bv);
1253 assert (btor_node_get_sort_id (res) == s);
1254 btor_bv_free (btor->mm, bv);
1255 btor_node_inc_ext_ref_counter (btor, res);
1256 BTOR_TRAPI_RETURN_NODE (res);
1257 #ifndef NDEBUG
1258 BTOR_CHKCLONE_RES_PTR (res, constd, sort, str);
1259 #endif
1260 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1261 }
1262
1263 BoolectorNode *
boolector_consth(Btor * btor,BoolectorSort sort,const char * str)1264 boolector_consth (Btor *btor, BoolectorSort sort, const char *str)
1265 {
1266 uint32_t w;
1267 BtorNode *res;
1268 BtorBitVector *bv;
1269 BtorSortId s;
1270
1271 BTOR_ABORT_ARG_NULL (btor);
1272 BTOR_TRAPI ("%s", str);
1273 BTOR_ABORT_ARG_NULL (str);
1274 BTOR_ABORT (*str == '\0', "'str' must not be empty");
1275
1276 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1277 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1278 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1279 "'sort' is not a bit vector sort");
1280 w = btor_sort_bv_get_width (btor, s);
1281 BTOR_ABORT (!btor_util_check_hex_to_bv (btor->mm, str, w),
1282 "'%s' does not fit into a bit-vector of size %u",
1283 str,
1284 w);
1285 bv = btor_bv_consth (btor->mm, str, w);
1286 res = btor_exp_bv_const (btor, bv);
1287 assert (btor_node_get_sort_id (res) == s);
1288 btor_bv_free (btor->mm, bv);
1289 btor_node_inc_ext_ref_counter (btor, res);
1290 BTOR_TRAPI_RETURN_NODE (res);
1291 #ifndef NDEBUG
1292 BTOR_CHKCLONE_RES_PTR (res, consth, sort, str);
1293 #endif
1294 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1295 }
1296
1297 /*------------------------------------------------------------------------*/
1298
1299 bool
boolector_is_bv_const_zero(Btor * btor,BoolectorNode * node)1300 boolector_is_bv_const_zero (Btor *btor, BoolectorNode *node)
1301 {
1302 BtorNode *exp;
1303 bool res;
1304 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1305 BTOR_ABORT_ARG_NULL (btor);
1306 BTOR_ABORT_ARG_NULL (exp);
1307 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1308 BTOR_TRAPI_UNFUN (exp);
1309 BTOR_ABORT_REFS_NOT_POS (exp);
1310 res = btor_node_is_bv_const_zero (btor, exp);
1311 BTOR_TRAPI_RETURN_BOOL (res);
1312 #ifndef NDEBUG
1313 BTOR_CHKCLONE_RES_BOOL (res, is_bv_const_zero, BTOR_CLONED_EXP (exp));
1314 #endif
1315 return res;
1316 }
1317
1318 bool
boolector_is_bv_const_one(Btor * btor,BoolectorNode * node)1319 boolector_is_bv_const_one (Btor *btor, BoolectorNode *node)
1320 {
1321 BtorNode *exp;
1322 bool res;
1323 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1324 BTOR_ABORT_ARG_NULL (btor);
1325 BTOR_ABORT_ARG_NULL (exp);
1326 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1327 BTOR_TRAPI_UNFUN (exp);
1328 BTOR_ABORT_REFS_NOT_POS (exp);
1329 res = btor_node_is_bv_const_one (btor, exp);
1330 BTOR_TRAPI_RETURN_BOOL (res);
1331 #ifndef NDEBUG
1332 BTOR_CHKCLONE_RES_BOOL (res, is_bv_const_one, BTOR_CLONED_EXP (exp));
1333 #endif
1334 return res;
1335 }
1336
1337 bool
boolector_is_bv_const_ones(Btor * btor,BoolectorNode * node)1338 boolector_is_bv_const_ones (Btor *btor, BoolectorNode *node)
1339 {
1340 BtorNode *exp;
1341 bool res;
1342 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1343 BTOR_ABORT_ARG_NULL (btor);
1344 BTOR_ABORT_ARG_NULL (exp);
1345 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1346 BTOR_TRAPI_UNFUN (exp);
1347 BTOR_ABORT_REFS_NOT_POS (exp);
1348 res = btor_node_is_bv_const_ones (btor, exp);
1349 BTOR_TRAPI_RETURN_BOOL (res);
1350 #ifndef NDEBUG
1351 BTOR_CHKCLONE_RES_BOOL (res, is_bv_const_ones, BTOR_CLONED_EXP (exp));
1352 #endif
1353 return res;
1354 }
1355
1356 bool
boolector_is_bv_const_max_signed(Btor * btor,BoolectorNode * node)1357 boolector_is_bv_const_max_signed (Btor *btor, BoolectorNode *node)
1358 {
1359 BtorNode *exp;
1360 bool res;
1361 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1362 BTOR_ABORT_ARG_NULL (btor);
1363 BTOR_ABORT_ARG_NULL (exp);
1364 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1365 BTOR_TRAPI_UNFUN (exp);
1366 BTOR_ABORT_REFS_NOT_POS (exp);
1367 res = btor_node_is_bv_const_max_signed (btor, exp);
1368 BTOR_TRAPI_RETURN_BOOL (res);
1369 #ifndef NDEBUG
1370 BTOR_CHKCLONE_RES_BOOL (res, is_bv_const_max_signed, BTOR_CLONED_EXP (exp));
1371 #endif
1372 return res;
1373 }
1374
1375 bool
boolector_is_bv_const_min_signed(Btor * btor,BoolectorNode * node)1376 boolector_is_bv_const_min_signed (Btor *btor, BoolectorNode *node)
1377 {
1378 BtorNode *exp;
1379 bool res;
1380 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1381 BTOR_ABORT_ARG_NULL (btor);
1382 BTOR_ABORT_ARG_NULL (exp);
1383 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1384 BTOR_TRAPI_UNFUN (exp);
1385 BTOR_ABORT_REFS_NOT_POS (exp);
1386 res = btor_node_is_bv_const_min_signed (btor, exp);
1387 BTOR_TRAPI_RETURN_BOOL (res);
1388 #ifndef NDEBUG
1389 BTOR_CHKCLONE_RES_BOOL (res, is_bv_const_min_signed, BTOR_CLONED_EXP (exp));
1390 #endif
1391 return res;
1392 }
1393
1394 /*------------------------------------------------------------------------*/
1395
1396 BoolectorNode *
boolector_zero(Btor * btor,BoolectorSort sort)1397 boolector_zero (Btor *btor, BoolectorSort sort)
1398 {
1399 BtorNode *res;
1400 BtorSortId s;
1401
1402 BTOR_ABORT_ARG_NULL (btor);
1403 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
1404 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1405 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1406 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1407 "'sort' is not a bit vector sort");
1408 res = btor_exp_bv_zero (btor, s);
1409 btor_node_inc_ext_ref_counter (btor, res);
1410 BTOR_TRAPI_RETURN_NODE (res);
1411 #ifndef NDEBUG
1412 BTOR_CHKCLONE_RES_PTR (res, zero, sort);
1413 #endif
1414 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1415 }
1416
1417 BoolectorNode *
boolector_ones(Btor * btor,BoolectorSort sort)1418 boolector_ones (Btor *btor, BoolectorSort sort)
1419 {
1420 BtorNode *res;
1421 BtorSortId s;
1422
1423 BTOR_ABORT_ARG_NULL (btor);
1424 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
1425 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1426 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1427 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1428 "'sort' is not a bit vector sort");
1429 res = btor_exp_bv_ones (btor, s);
1430 btor_node_inc_ext_ref_counter (btor, res);
1431 BTOR_TRAPI_RETURN_NODE (res);
1432 #ifndef NDEBUG
1433 BTOR_CHKCLONE_RES_PTR (res, ones, sort);
1434 #endif
1435 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1436 }
1437
1438 BoolectorNode *
boolector_one(Btor * btor,BoolectorSort sort)1439 boolector_one (Btor *btor, BoolectorSort sort)
1440 {
1441 BtorNode *res;
1442 BtorSortId s;
1443
1444 BTOR_ABORT_ARG_NULL (btor);
1445 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
1446 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1447 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1448 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1449 "'sort' is not a bit vector sort");
1450 res = btor_exp_bv_one (btor, s);
1451 btor_node_inc_ext_ref_counter (btor, res);
1452 BTOR_TRAPI_RETURN_NODE (res);
1453 #ifndef NDEBUG
1454 BTOR_CHKCLONE_RES_PTR (res, one, sort);
1455 #endif
1456 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1457 }
1458
1459 BoolectorNode *
boolector_min_signed(Btor * btor,BoolectorSort sort)1460 boolector_min_signed (Btor *btor, BoolectorSort sort)
1461 {
1462 BtorNode *res;
1463 BtorSortId s;
1464
1465 BTOR_ABORT_ARG_NULL (btor);
1466 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
1467 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1468 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1469 BTOR_ABORT (!btor_sort_is_bv (btor, s), "'sort' is not a bit vector sort");
1470 res = btor_exp_bv_min_signed (btor, s);
1471 btor_node_inc_ext_ref_counter (btor, res);
1472 BTOR_TRAPI_RETURN_NODE (res);
1473 #ifndef NDEBUG
1474 BTOR_CHKCLONE_RES_PTR (res, min_signed, sort);
1475 #endif
1476 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1477 }
1478
1479 BoolectorNode *
boolector_max_signed(Btor * btor,BoolectorSort sort)1480 boolector_max_signed (Btor *btor, BoolectorSort sort)
1481 {
1482 BtorNode *res;
1483 BtorSortId s;
1484
1485 BTOR_ABORT_ARG_NULL (btor);
1486 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
1487 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1488 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1489 BTOR_ABORT (!btor_sort_is_bv (btor, s), "'sort' is not a bit vector sort");
1490 res = btor_exp_bv_max_signed (btor, s);
1491 btor_node_inc_ext_ref_counter (btor, res);
1492 BTOR_TRAPI_RETURN_NODE (res);
1493 #ifndef NDEBUG
1494 BTOR_CHKCLONE_RES_PTR (res, max_signed, sort);
1495 #endif
1496 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1497 }
1498
1499 BoolectorNode *
boolector_unsigned_int(Btor * btor,uint32_t u,BoolectorSort sort)1500 boolector_unsigned_int (Btor *btor, uint32_t u, BoolectorSort sort)
1501 {
1502 BtorNode *res;
1503 BtorSortId s;
1504
1505 BTOR_ABORT_ARG_NULL (btor);
1506 BTOR_TRAPI ("%u " BTOR_TRAPI_SORT_FMT, u, sort, btor);
1507 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1508 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1509 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1510 "'sort' is not a bit vector sort");
1511 res = btor_exp_bv_unsigned (btor, u, s);
1512 btor_node_inc_ext_ref_counter (btor, res);
1513 BTOR_TRAPI_RETURN_NODE (res);
1514 #ifndef NDEBUG
1515 BTOR_CHKCLONE_RES_PTR (res, unsigned_int, u, sort);
1516 #endif
1517 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1518 }
1519
1520 BoolectorNode *
boolector_int(Btor * btor,int32_t i,BoolectorSort sort)1521 boolector_int (Btor *btor, int32_t i, BoolectorSort sort)
1522 {
1523 BtorNode *res;
1524 BtorSortId s;
1525
1526 BTOR_ABORT_ARG_NULL (btor);
1527 BTOR_TRAPI ("%d " BTOR_TRAPI_SORT_FMT, i, sort, btor);
1528 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1529 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1530 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1531 "'sort' is not a bit vector sort");
1532 res = btor_exp_bv_int (btor, i, s);
1533 btor_node_inc_ext_ref_counter (btor, res);
1534 BTOR_TRAPI_RETURN_NODE (res);
1535 #ifndef NDEBUG
1536 BTOR_CHKCLONE_RES_PTR (res, int, i, sort);
1537 #endif
1538 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1539 }
1540
1541 /*------------------------------------------------------------------------*/
1542
1543 /* Remove unique symbol prefix and return start address of original symbol
1544 * without prefix. */
1545 static const char *
remove_unique_symbol_prefix(Btor * btor,const char * symbol)1546 remove_unique_symbol_prefix (Btor *btor, const char *symbol)
1547 {
1548 if (symbol)
1549 {
1550 size_t len = strlen (symbol);
1551 size_t offset = 5 + btor_util_num_digits (btor->num_push_pop);
1552 if (len > offset && !strncmp (symbol, "BTOR_", 5) && symbol[offset] == '@')
1553 {
1554 return symbol + offset + 1;
1555 }
1556 }
1557 return symbol;
1558 }
1559
1560 /* Create symbol that is unique in the current scope. Prefix symbols with
1561 * BTOR_<num_push_pop>@<symbol> to make them unique in the current context. */
1562 static char *
mk_unique_symbol_aux(BtorMemMgr * mm,uint32_t num_push_pop,const char * symbol)1563 mk_unique_symbol_aux (BtorMemMgr *mm, uint32_t num_push_pop, const char *symbol)
1564 {
1565 char *symb;
1566 size_t len;
1567 if (num_push_pop)
1568 {
1569 len = strlen (symbol) + 1;
1570 len += strlen ("BTOR_@");
1571 len += btor_util_num_digits (num_push_pop);
1572 BTOR_CNEWN (mm, symb, len);
1573 sprintf (symb, "BTOR_%u@%s", num_push_pop, symbol);
1574 }
1575 else
1576 {
1577 symb = btor_mem_strdup (mm, symbol);
1578 }
1579 return symb;
1580 }
1581
1582 static char *
mk_unique_symbol(Btor * btor,const char * symbol)1583 mk_unique_symbol (Btor *btor, const char *symbol)
1584 {
1585 char *res = mk_unique_symbol_aux (btor->mm, btor->num_push_pop, symbol);
1586 assert (!symbol || !strcmp (symbol, remove_unique_symbol_prefix (btor, res)));
1587 return res;
1588 }
1589
1590 BoolectorNode *
boolector_var(Btor * btor,BoolectorSort sort,const char * symbol)1591 boolector_var (Btor *btor, BoolectorSort sort, const char *symbol)
1592 {
1593 BTOR_ABORT_ARG_NULL (btor);
1594
1595 BtorNode *res;
1596 char *symb;
1597 BtorSortId s;
1598
1599 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1600 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1601 BTOR_ABORT (!btor_sort_is_bv (btor, s),
1602 "'sort' is not a bit vector sort");
1603 symb = mk_unique_symbol (btor, symbol);
1604 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT " %s", sort, btor, symb);
1605 BTOR_ABORT (symb && btor_hashptr_table_get (btor->symbols, (char *) symb),
1606 "symbol '%s' is already in use in the current context",
1607 symb);
1608 res = btor_exp_var (btor, s, symb);
1609 btor_mem_freestr (btor->mm, symb);
1610 btor_node_inc_ext_ref_counter (btor, res);
1611 BTOR_TRAPI_RETURN_NODE (res);
1612 (void) btor_hashptr_table_add (btor->inputs, btor_node_copy (btor, res));
1613 #ifndef NDEBUG
1614 BTOR_CHKCLONE_RES_PTR (res, var, sort, symbol);
1615 #endif
1616 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1617 }
1618
1619 BoolectorNode *
boolector_array(Btor * btor,BoolectorSort sort,const char * symbol)1620 boolector_array (Btor *btor, BoolectorSort sort, const char *symbol)
1621 {
1622 BTOR_ABORT_ARG_NULL (btor);
1623
1624 BtorNode *res;
1625 char *symb;
1626 BtorSortId s;
1627
1628 symb = mk_unique_symbol (btor, symbol);
1629 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1630 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1631 BTOR_ABORT (!btor_sort_is_fun (btor, s)
1632 || btor_sort_tuple_get_arity (
1633 btor, btor_sort_fun_get_domain (btor, s))
1634 != 1,
1635 "'sort' is not an array sort");
1636 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT " %s", sort, btor, symb);
1637 BTOR_ABORT (symb && btor_hashptr_table_get (btor->symbols, symb),
1638 "symbol '%s' is already in use in the current context",
1639 symb);
1640 res = btor_exp_array (btor, s, symb);
1641 btor_mem_freestr (btor->mm, symb);
1642 btor_node_inc_ext_ref_counter (btor, res);
1643 BTOR_TRAPI_RETURN_NODE (res);
1644 (void) btor_hashptr_table_add (btor->inputs, btor_node_copy (btor, res));
1645 #ifndef NDEBUG
1646 BTOR_CHKCLONE_RES_PTR (res, array, sort, symbol);
1647 #endif
1648 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1649 }
1650
1651 BoolectorNode *
boolector_const_array(Btor * btor,BoolectorSort sort,BoolectorNode * value)1652 boolector_const_array (Btor *btor, BoolectorSort sort, BoolectorNode *value)
1653 {
1654 BTOR_ABORT_ARG_NULL (btor);
1655
1656 BtorNode *res, *val;
1657 BtorSortId s;
1658
1659 val = BTOR_IMPORT_BOOLECTOR_NODE (value);
1660
1661 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1662 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1663 BTOR_ABORT (!btor_sort_is_fun (btor, s)
1664 || btor_sort_tuple_get_arity (
1665 btor, btor_sort_fun_get_domain (btor, s))
1666 != 1,
1667 "'sort' is not an array sort");
1668 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT BTOR_TRAPI_NODE_FMT,
1669 sort,
1670 btor,
1671 BTOR_TRAPI_NODE_ID (val));
1672 BTOR_ABORT_ARG_NULL (val);
1673 BTOR_ABORT_REFS_NOT_POS (val);
1674 BTOR_ABORT_BTOR_MISMATCH (btor, val);
1675 BTOR_ABORT_IS_NOT_BV (val);
1676 BTOR_ABORT (
1677 btor_node_get_sort_id (val) != btor_sort_array_get_element (btor, s),
1678 "sort of 'value' does not match element sort of array");
1679
1680 res = btor_exp_const_array (btor, s, val);
1681
1682 btor_node_inc_ext_ref_counter (btor, res);
1683 BTOR_TRAPI_RETURN_NODE (res);
1684
1685 #ifndef NDEBUG
1686 BTOR_CHKCLONE_RES_PTR (res, const_array, sort, value);
1687 #endif
1688 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1689 }
1690
1691 BoolectorNode *
boolector_uf(Btor * btor,BoolectorSort sort,const char * symbol)1692 boolector_uf (Btor *btor, BoolectorSort sort, const char *symbol)
1693 {
1694 BTOR_ABORT_ARG_NULL (btor);
1695
1696 BtorNode *res;
1697 BtorSortId s;
1698 char *symb;
1699
1700 symb = mk_unique_symbol (btor, symbol);
1701 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
1702 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT "%s", sort, btor, symb);
1703 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
1704 BTOR_ABORT (!btor_sort_is_fun (btor, s),
1705 "%ssort%s%s%s%s must be a function sort",
1706 symbol ? "" : "'",
1707 symbol ? "" : "'",
1708 symbol ? " '" : "",
1709 symbol ? symbol : "",
1710 symbol ? "'" : "");
1711 BTOR_ABORT (symb && btor_hashptr_table_get (btor->symbols, symb),
1712 "symbol '%s' is already in use in the current context",
1713 symb);
1714
1715 res = btor_exp_uf (btor, s, symb);
1716 btor_mem_freestr (btor->mm, symb);
1717 assert (btor_node_is_regular (res));
1718 btor_node_inc_ext_ref_counter (btor, res);
1719 (void) btor_hashptr_table_add (btor->inputs, btor_node_copy (btor, res));
1720 BTOR_TRAPI_RETURN_NODE (res);
1721 #ifndef NDEBUG
1722 BTOR_CHKCLONE_RES_PTR (res, uf, sort, symbol);
1723 #endif
1724 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1725 }
1726
1727 /*------------------------------------------------------------------------*/
1728
1729 BoolectorNode *
boolector_not(Btor * btor,BoolectorNode * node)1730 boolector_not (Btor *btor, BoolectorNode *node)
1731 {
1732 BtorNode *exp, *res;
1733
1734 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1735 BTOR_ABORT_ARG_NULL (btor);
1736 BTOR_ABORT_ARG_NULL (exp);
1737 BTOR_TRAPI_UNFUN (exp);
1738 BTOR_ABORT_REFS_NOT_POS (exp);
1739 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1740 BTOR_ABORT_IS_NOT_BV (exp);
1741 res = btor_exp_bv_not (btor, exp);
1742 btor_node_inc_ext_ref_counter (btor, res);
1743 BTOR_TRAPI_RETURN_NODE (res);
1744 #ifndef NDEBUG
1745 BTOR_CHKCLONE_RES_PTR (res, not, BTOR_CLONED_EXP (exp));
1746 #endif
1747 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1748 }
1749
1750 BoolectorNode *
boolector_neg(Btor * btor,BoolectorNode * node)1751 boolector_neg (Btor *btor, BoolectorNode *node)
1752 {
1753 BtorNode *exp, *res;
1754
1755 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1756 BTOR_ABORT_ARG_NULL (btor);
1757 BTOR_ABORT_ARG_NULL (exp);
1758 BTOR_TRAPI_UNFUN (exp);
1759 BTOR_ABORT_REFS_NOT_POS (exp);
1760 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1761 BTOR_ABORT_IS_NOT_BV (exp);
1762 res = btor_exp_bv_neg (btor, exp);
1763 btor_node_inc_ext_ref_counter (btor, res);
1764 BTOR_TRAPI_RETURN_NODE (res);
1765 #ifndef NDEBUG
1766 BTOR_CHKCLONE_RES_PTR (res, neg, BTOR_CLONED_EXP (exp));
1767 #endif
1768 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1769 }
1770
1771 BoolectorNode *
boolector_redor(Btor * btor,BoolectorNode * node)1772 boolector_redor (Btor *btor, BoolectorNode *node)
1773 {
1774 BtorNode *exp, *res;
1775
1776 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1777 BTOR_ABORT_ARG_NULL (btor);
1778 BTOR_ABORT_ARG_NULL (exp);
1779 BTOR_TRAPI_UNFUN (exp);
1780 BTOR_ABORT_REFS_NOT_POS (exp);
1781 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1782 BTOR_ABORT_IS_NOT_BV (exp);
1783 res = btor_exp_bv_redor (btor, exp);
1784 btor_node_inc_ext_ref_counter (btor, res);
1785 BTOR_TRAPI_RETURN_NODE (res);
1786 #ifndef NDEBUG
1787 BTOR_CHKCLONE_RES_PTR (res, redor, BTOR_CLONED_EXP (exp));
1788 #endif
1789 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1790 }
1791
1792 BoolectorNode *
boolector_redxor(Btor * btor,BoolectorNode * node)1793 boolector_redxor (Btor *btor, BoolectorNode *node)
1794 {
1795 BtorNode *exp, *res;
1796
1797 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1798 BTOR_ABORT_ARG_NULL (btor);
1799 BTOR_ABORT_ARG_NULL (exp);
1800 BTOR_TRAPI_UNFUN (exp);
1801 BTOR_ABORT_REFS_NOT_POS (exp);
1802 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1803 BTOR_ABORT_IS_NOT_BV (exp);
1804 res = btor_exp_bv_redxor (btor, exp);
1805 btor_node_inc_ext_ref_counter (btor, res);
1806 BTOR_TRAPI_RETURN_NODE (res);
1807 #ifndef NDEBUG
1808 BTOR_CHKCLONE_RES_PTR (res, redxor, BTOR_CLONED_EXP (exp));
1809 #endif
1810 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1811 }
1812
1813 BoolectorNode *
boolector_redand(Btor * btor,BoolectorNode * node)1814 boolector_redand (Btor *btor, BoolectorNode *node)
1815 {
1816 BtorNode *exp, *res;
1817
1818 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1819 BTOR_ABORT_ARG_NULL (btor);
1820 BTOR_ABORT_ARG_NULL (exp);
1821 BTOR_TRAPI_UNFUN (exp);
1822 BTOR_ABORT_REFS_NOT_POS (exp);
1823 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1824 BTOR_ABORT_IS_NOT_BV (exp);
1825 res = btor_exp_bv_redand (btor, exp);
1826 btor_node_inc_ext_ref_counter (btor, res);
1827 BTOR_TRAPI_RETURN_NODE (res);
1828 #ifndef NDEBUG
1829 BTOR_CHKCLONE_RES_PTR (res, redand, BTOR_CLONED_EXP (exp));
1830 #endif
1831 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1832 }
1833
1834 BoolectorNode *
boolector_slice(Btor * btor,BoolectorNode * node,uint32_t upper,uint32_t lower)1835 boolector_slice (Btor *btor,
1836 BoolectorNode *node,
1837 uint32_t upper,
1838 uint32_t lower)
1839 {
1840 BtorNode *exp, *res;
1841
1842 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1843 BTOR_ABORT_ARG_NULL (btor);
1844 BTOR_ABORT_ARG_NULL (exp);
1845 BTOR_TRAPI_UNFUN_EXT (exp, "%u %u", upper, lower);
1846 BTOR_ABORT_REFS_NOT_POS (exp);
1847 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1848 BTOR_ABORT_IS_NOT_BV (exp);
1849 BTOR_ABORT (upper < lower, "'upper' must not be < 'lower'");
1850 BTOR_ABORT ((uint32_t) upper >= btor_node_bv_get_width (btor, exp),
1851 "'upper' must not be >= width of 'exp'");
1852 res = btor_exp_bv_slice (btor, exp, upper, lower);
1853 btor_node_inc_ext_ref_counter (btor, res);
1854 BTOR_TRAPI_RETURN_NODE (res);
1855 #ifndef NDEBUG
1856 BTOR_CHKCLONE_RES_PTR (res, slice, BTOR_CLONED_EXP (exp), upper, lower);
1857 #endif
1858 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1859 }
1860
1861 BoolectorNode *
boolector_uext(Btor * btor,BoolectorNode * node,uint32_t width)1862 boolector_uext (Btor *btor, BoolectorNode *node, uint32_t width)
1863 {
1864 BtorNode *exp, *res;
1865
1866 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1867 BTOR_ABORT_ARG_NULL (btor);
1868 BTOR_ABORT_ARG_NULL (exp);
1869 BTOR_TRAPI_UNFUN_EXT (exp, "%u", width);
1870 BTOR_ABORT_REFS_NOT_POS (exp);
1871 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1872 BTOR_ABORT_IS_NOT_BV (exp);
1873 BTOR_ABORT (width > UINT32_MAX - btor_node_bv_get_width (btor, exp),
1874 "extending 'exp' (width %u) by %u bits exceeds maximum "
1875 "bit-width of %u",
1876 btor_node_bv_get_width (btor, exp),
1877 width,
1878 UINT32_MAX);
1879 res = btor_exp_bv_uext (btor, exp, width);
1880 btor_node_inc_ext_ref_counter (btor, res);
1881 BTOR_TRAPI_RETURN_NODE (res);
1882 #ifndef NDEBUG
1883 BTOR_CHKCLONE_RES_PTR (res, uext, BTOR_CLONED_EXP (exp), width);
1884 #endif
1885 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1886 }
1887
1888 BoolectorNode *
boolector_sext(Btor * btor,BoolectorNode * node,uint32_t width)1889 boolector_sext (Btor *btor, BoolectorNode *node, uint32_t width)
1890 {
1891 BtorNode *exp, *res;
1892
1893 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
1894 BTOR_ABORT_ARG_NULL (btor);
1895 BTOR_ABORT_ARG_NULL (exp);
1896 BTOR_TRAPI_UNFUN_EXT (exp, "%u", width);
1897 BTOR_ABORT_REFS_NOT_POS (exp);
1898 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
1899 BTOR_ABORT_IS_NOT_BV (exp);
1900 BTOR_ABORT (width > UINT32_MAX - btor_node_bv_get_width (btor, exp),
1901 "extending 'exp' (width %u) by %u bits exceeds maximum "
1902 "bit-width of %u",
1903 btor_node_bv_get_width (btor, exp),
1904 width,
1905 UINT32_MAX);
1906 res = btor_exp_bv_sext (btor, exp, width);
1907 btor_node_inc_ext_ref_counter (btor, res);
1908 BTOR_TRAPI_RETURN_NODE (res);
1909 #ifndef NDEBUG
1910 BTOR_CHKCLONE_RES_PTR (res, sext, BTOR_CLONED_EXP (exp), width);
1911 #endif
1912 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1913 }
1914
1915 BoolectorNode *
boolector_xor(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1916 boolector_xor (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1917 {
1918 BtorNode *e0, *e1, *res;
1919
1920 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1921 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1922 BTOR_ABORT_ARG_NULL (btor);
1923 BTOR_ABORT_ARG_NULL (e0);
1924 BTOR_ABORT_ARG_NULL (e1);
1925 BTOR_TRAPI_BINFUN (e0, e1);
1926 BTOR_ABORT_REFS_NOT_POS (e0);
1927 BTOR_ABORT_REFS_NOT_POS (e1);
1928 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1929 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1930 BTOR_ABORT_IS_NOT_BV (e0);
1931 BTOR_ABORT_IS_NOT_BV (e1);
1932 BTOR_ABORT_SORT_MISMATCH (e0, e1);
1933 res = btor_exp_bv_xor (btor, e0, e1);
1934 btor_node_inc_ext_ref_counter (btor, res);
1935 BTOR_TRAPI_RETURN_NODE (res);
1936 #ifndef NDEBUG
1937 BTOR_CHKCLONE_RES_PTR (res, xor, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1938 #endif
1939 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1940 }
1941
1942 BoolectorNode *
boolector_xnor(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1943 boolector_xnor (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1944 {
1945 BtorNode *e0, *e1, *res;
1946
1947 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1948 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1949 BTOR_ABORT_ARG_NULL (btor);
1950 BTOR_ABORT_ARG_NULL (e0);
1951 BTOR_ABORT_ARG_NULL (e1);
1952 BTOR_TRAPI_BINFUN (e0, e1);
1953 BTOR_ABORT_REFS_NOT_POS (e0);
1954 BTOR_ABORT_REFS_NOT_POS (e1);
1955 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1956 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1957 BTOR_ABORT_IS_NOT_BV (e0);
1958 BTOR_ABORT_IS_NOT_BV (e1);
1959 BTOR_ABORT_SORT_MISMATCH (e0, e1);
1960 res = btor_exp_bv_xnor (btor, e0, e1);
1961 btor_node_inc_ext_ref_counter (btor, res);
1962 BTOR_TRAPI_RETURN_NODE (res);
1963 #ifndef NDEBUG
1964 BTOR_CHKCLONE_RES_PTR (res, xnor, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1965 #endif
1966 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1967 }
1968
1969 BoolectorNode *
boolector_and(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1970 boolector_and (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1971 {
1972 BtorNode *e0, *e1, *res;
1973
1974 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
1975 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
1976 BTOR_ABORT_ARG_NULL (btor);
1977 BTOR_ABORT_ARG_NULL (e0);
1978 BTOR_ABORT_ARG_NULL (e1);
1979 BTOR_TRAPI_BINFUN (e0, e1);
1980 BTOR_ABORT_REFS_NOT_POS (e0);
1981 BTOR_ABORT_REFS_NOT_POS (e1);
1982 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
1983 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
1984 BTOR_ABORT_IS_NOT_BV (e0);
1985 BTOR_ABORT_IS_NOT_BV (e1);
1986 BTOR_ABORT_SORT_MISMATCH (e0, e1);
1987 res = btor_exp_bv_and (btor, e0, e1);
1988 btor_node_inc_ext_ref_counter (btor, res);
1989 BTOR_TRAPI_RETURN_NODE (res);
1990 #ifndef NDEBUG
1991 BTOR_CHKCLONE_RES_PTR (res, and, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
1992 #endif
1993 return BTOR_EXPORT_BOOLECTOR_NODE (res);
1994 }
1995
1996 BoolectorNode *
boolector_nand(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)1997 boolector_nand (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
1998 {
1999 BtorNode *e0, *e1, *res;
2000
2001 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2002 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2003 BTOR_ABORT_ARG_NULL (btor);
2004 BTOR_ABORT_ARG_NULL (e0);
2005 BTOR_ABORT_ARG_NULL (e1);
2006 BTOR_TRAPI_BINFUN (e0, e1);
2007 BTOR_ABORT_REFS_NOT_POS (e0);
2008 BTOR_ABORT_REFS_NOT_POS (e1);
2009 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2010 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2011 BTOR_ABORT_IS_NOT_BV (e0);
2012 BTOR_ABORT_IS_NOT_BV (e1);
2013 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2014 res = btor_exp_bv_nand (btor, e0, e1);
2015 btor_node_inc_ext_ref_counter (btor, res);
2016 BTOR_TRAPI_RETURN_NODE (res);
2017 #ifndef NDEBUG
2018 BTOR_CHKCLONE_RES_PTR (res, nand, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2019 #endif
2020 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2021 }
2022
2023 BoolectorNode *
boolector_or(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2024 boolector_or (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2025 {
2026 BtorNode *e0, *e1, *res;
2027
2028 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2029 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2030 BTOR_ABORT_ARG_NULL (btor);
2031 BTOR_ABORT_ARG_NULL (e0);
2032 BTOR_ABORT_ARG_NULL (e1);
2033 BTOR_TRAPI_BINFUN (e0, e1);
2034 BTOR_ABORT_REFS_NOT_POS (e0);
2035 BTOR_ABORT_REFS_NOT_POS (e1);
2036 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2037 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2038 BTOR_ABORT_IS_NOT_BV (e0);
2039 BTOR_ABORT_IS_NOT_BV (e1);
2040 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2041 res = btor_exp_bv_or (btor, e0, e1);
2042 btor_node_inc_ext_ref_counter (btor, res);
2043 BTOR_TRAPI_RETURN_NODE (res);
2044 #ifndef NDEBUG
2045 BTOR_CHKCLONE_RES_PTR (res, or, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2046 #endif
2047 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2048 }
2049
2050 BoolectorNode *
boolector_nor(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2051 boolector_nor (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2052 {
2053 BtorNode *e0, *e1, *res;
2054
2055 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2056 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2057 BTOR_ABORT_ARG_NULL (btor);
2058 BTOR_ABORT_ARG_NULL (e0);
2059 BTOR_ABORT_ARG_NULL (e1);
2060 BTOR_TRAPI_BINFUN (e0, e1);
2061 BTOR_ABORT_REFS_NOT_POS (e0);
2062 BTOR_ABORT_REFS_NOT_POS (e1);
2063 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2064 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2065 BTOR_ABORT_IS_NOT_BV (e0);
2066 BTOR_ABORT_IS_NOT_BV (e1);
2067 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2068 res = btor_exp_bv_nor (btor, e0, e1);
2069 btor_node_inc_ext_ref_counter (btor, res);
2070 BTOR_TRAPI_RETURN_NODE (res);
2071 #ifndef NDEBUG
2072 BTOR_CHKCLONE_RES_PTR (res, nor, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2073 #endif
2074 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2075 }
2076
2077 BoolectorNode *
boolector_add(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2078 boolector_add (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2079 {
2080 BtorNode *e0, *e1, *res;
2081
2082 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2083 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2084 BTOR_ABORT_ARG_NULL (btor);
2085 BTOR_ABORT_ARG_NULL (e0);
2086 BTOR_ABORT_ARG_NULL (e1);
2087 BTOR_TRAPI_BINFUN (e0, e1);
2088 BTOR_ABORT_REFS_NOT_POS (e0);
2089 BTOR_ABORT_REFS_NOT_POS (e1);
2090 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2091 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2092 BTOR_ABORT_IS_NOT_BV (e0);
2093 BTOR_ABORT_IS_NOT_BV (e1);
2094 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2095 res = btor_exp_bv_add (btor, e0, e1);
2096 btor_node_inc_ext_ref_counter (btor, res);
2097 BTOR_TRAPI_RETURN_NODE (res);
2098 #ifndef NDEBUG
2099 BTOR_CHKCLONE_RES_PTR (res, add, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2100 #endif
2101 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2102 }
2103
2104 BoolectorNode *
boolector_uaddo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2105 boolector_uaddo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2106 {
2107 BtorNode *e0, *e1, *res;
2108
2109 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2110 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2111 BTOR_ABORT_ARG_NULL (btor);
2112 BTOR_ABORT_ARG_NULL (e0);
2113 BTOR_ABORT_ARG_NULL (e1);
2114 BTOR_TRAPI_BINFUN (e0, e1);
2115 BTOR_ABORT_REFS_NOT_POS (e0);
2116 BTOR_ABORT_REFS_NOT_POS (e1);
2117 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2118 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2119 BTOR_ABORT_IS_NOT_BV (e0);
2120 BTOR_ABORT_IS_NOT_BV (e1);
2121 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2122 res = btor_exp_bv_uaddo (btor, e0, e1);
2123 btor_node_inc_ext_ref_counter (btor, res);
2124 BTOR_TRAPI_RETURN_NODE (res);
2125 #ifndef NDEBUG
2126 BTOR_CHKCLONE_RES_PTR (
2127 res, uaddo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2128 #endif
2129 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2130 }
2131
2132 BoolectorNode *
boolector_saddo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2133 boolector_saddo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2134 {
2135 BtorNode *e0, *e1, *res;
2136
2137 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2138 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2139 BTOR_ABORT_ARG_NULL (btor);
2140 BTOR_ABORT_ARG_NULL (e0);
2141 BTOR_ABORT_ARG_NULL (e1);
2142 BTOR_TRAPI_BINFUN (e0, e1);
2143 BTOR_ABORT_REFS_NOT_POS (e0);
2144 BTOR_ABORT_REFS_NOT_POS (e1);
2145 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2146 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2147 BTOR_ABORT_IS_NOT_BV (e0);
2148 BTOR_ABORT_IS_NOT_BV (e1);
2149 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2150 res = btor_exp_bv_saddo (btor, e0, e1);
2151 btor_node_inc_ext_ref_counter (btor, res);
2152 BTOR_TRAPI_RETURN_NODE (res);
2153 #ifndef NDEBUG
2154 BTOR_CHKCLONE_RES_PTR (
2155 res, saddo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2156 #endif
2157 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2158 }
2159
2160 BoolectorNode *
boolector_mul(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2161 boolector_mul (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2162 {
2163 BtorNode *e0, *e1, *res;
2164
2165 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2166 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2167 BTOR_ABORT_ARG_NULL (btor);
2168 BTOR_ABORT_ARG_NULL (e0);
2169 BTOR_ABORT_ARG_NULL (e1);
2170 BTOR_TRAPI_BINFUN (e0, e1);
2171 BTOR_ABORT_REFS_NOT_POS (e0);
2172 BTOR_ABORT_REFS_NOT_POS (e1);
2173 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2174 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2175 BTOR_ABORT_IS_NOT_BV (e0);
2176 BTOR_ABORT_IS_NOT_BV (e1);
2177 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2178 res = btor_exp_bv_mul (btor, e0, e1);
2179 btor_node_inc_ext_ref_counter (btor, res);
2180 BTOR_TRAPI_RETURN_NODE (res);
2181 #ifndef NDEBUG
2182 BTOR_CHKCLONE_RES_PTR (res, mul, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2183 #endif
2184 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2185 }
2186
2187 BoolectorNode *
boolector_umulo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2188 boolector_umulo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2189 {
2190 BtorNode *e0, *e1, *res;
2191
2192 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2193 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2194 BTOR_ABORT_ARG_NULL (btor);
2195 BTOR_ABORT_ARG_NULL (e0);
2196 BTOR_ABORT_ARG_NULL (e1);
2197 BTOR_TRAPI_BINFUN (e0, e1);
2198 BTOR_ABORT_REFS_NOT_POS (e0);
2199 BTOR_ABORT_REFS_NOT_POS (e1);
2200 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2201 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2202 BTOR_ABORT_IS_NOT_BV (e0);
2203 BTOR_ABORT_IS_NOT_BV (e1);
2204 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2205 res = btor_exp_bv_umulo (btor, e0, e1);
2206 btor_node_inc_ext_ref_counter (btor, res);
2207 BTOR_TRAPI_RETURN_NODE (res);
2208 #ifndef NDEBUG
2209 BTOR_CHKCLONE_RES_PTR (
2210 res, umulo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2211 #endif
2212 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2213 }
2214
2215 BoolectorNode *
boolector_smulo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2216 boolector_smulo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2217 {
2218 BtorNode *e0, *e1, *res;
2219
2220 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2221 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2222 BTOR_ABORT_ARG_NULL (btor);
2223 BTOR_ABORT_ARG_NULL (e0);
2224 BTOR_ABORT_ARG_NULL (e1);
2225 BTOR_TRAPI_BINFUN (e0, e1);
2226 BTOR_ABORT_ARG_NULL (e1);
2227 BTOR_ABORT_REFS_NOT_POS (e0);
2228 BTOR_ABORT_REFS_NOT_POS (e1);
2229 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2230 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2231 BTOR_ABORT_IS_NOT_BV (e0);
2232 BTOR_ABORT_IS_NOT_BV (e1);
2233 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2234 res = btor_exp_bv_smulo (btor, e0, e1);
2235 btor_node_inc_ext_ref_counter (btor, res);
2236 BTOR_TRAPI_RETURN_NODE (res);
2237 #ifndef NDEBUG
2238 BTOR_CHKCLONE_RES_PTR (
2239 res, smulo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2240 #endif
2241 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2242 }
2243
2244 BoolectorNode *
boolector_ult(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2245 boolector_ult (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2246 {
2247 BtorNode *e0, *e1, *res;
2248
2249 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2250 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2251 BTOR_ABORT_ARG_NULL (btor);
2252 BTOR_ABORT_ARG_NULL (e0);
2253 BTOR_ABORT_ARG_NULL (e1);
2254 BTOR_TRAPI_BINFUN (e0, e1);
2255 BTOR_ABORT_REFS_NOT_POS (e0);
2256 BTOR_ABORT_REFS_NOT_POS (e1);
2257 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2258 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2259 BTOR_ABORT_IS_NOT_BV (e0);
2260 BTOR_ABORT_IS_NOT_BV (e1);
2261 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2262 res = btor_exp_bv_ult (btor, e0, e1);
2263 btor_node_inc_ext_ref_counter (btor, res);
2264 BTOR_TRAPI_RETURN_NODE (res);
2265 #ifndef NDEBUG
2266 BTOR_CHKCLONE_RES_PTR (res, ult, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2267 #endif
2268 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2269 }
2270
2271 BoolectorNode *
boolector_slt(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2272 boolector_slt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2273 {
2274 BtorNode *e0, *e1, *res;
2275
2276 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2277 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2278 BTOR_ABORT_ARG_NULL (btor);
2279 BTOR_ABORT_ARG_NULL (e0);
2280 BTOR_ABORT_ARG_NULL (e1);
2281 BTOR_TRAPI_BINFUN (e0, e1);
2282 BTOR_ABORT_REFS_NOT_POS (e0);
2283 BTOR_ABORT_REFS_NOT_POS (e1);
2284 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2285 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2286 BTOR_ABORT_IS_NOT_BV (e0);
2287 BTOR_ABORT_IS_NOT_BV (e1);
2288 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2289 res = btor_exp_bv_slt (btor, e0, e1);
2290 btor_node_inc_ext_ref_counter (btor, res);
2291 BTOR_TRAPI_RETURN_NODE (res);
2292 #ifndef NDEBUG
2293 BTOR_CHKCLONE_RES_PTR (res, slt, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2294 #endif
2295 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2296 }
2297
2298 BoolectorNode *
boolector_ulte(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2299 boolector_ulte (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2300 {
2301 BtorNode *e0, *e1, *res;
2302
2303 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2304 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2305 BTOR_ABORT_ARG_NULL (btor);
2306 BTOR_ABORT_ARG_NULL (e0);
2307 BTOR_ABORT_ARG_NULL (e1);
2308 BTOR_TRAPI_BINFUN (e0, e1);
2309 BTOR_ABORT_REFS_NOT_POS (e0);
2310 BTOR_ABORT_REFS_NOT_POS (e1);
2311 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2312 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2313 BTOR_ABORT_IS_NOT_BV (e0);
2314 BTOR_ABORT_IS_NOT_BV (e1);
2315 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2316 res = btor_exp_bv_ulte (btor, e0, e1);
2317 btor_node_inc_ext_ref_counter (btor, res);
2318 BTOR_TRAPI_RETURN_NODE (res);
2319 #ifndef NDEBUG
2320 BTOR_CHKCLONE_RES_PTR (res, ulte, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2321 #endif
2322 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2323 }
2324
2325 BoolectorNode *
boolector_slte(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2326 boolector_slte (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2327 {
2328 BtorNode *e0, *e1, *res;
2329
2330 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2331 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2332 BTOR_ABORT_ARG_NULL (btor);
2333 BTOR_ABORT_ARG_NULL (e0);
2334 BTOR_ABORT_ARG_NULL (e1);
2335 BTOR_TRAPI_BINFUN (e0, e1);
2336 BTOR_ABORT_REFS_NOT_POS (e0);
2337 BTOR_ABORT_REFS_NOT_POS (e1);
2338 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2339 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2340 BTOR_ABORT_IS_NOT_BV (e0);
2341 BTOR_ABORT_IS_NOT_BV (e1);
2342 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2343 res = btor_exp_bv_slte (btor, e0, e1);
2344 btor_node_inc_ext_ref_counter (btor, res);
2345 BTOR_TRAPI_RETURN_NODE (res);
2346 #ifndef NDEBUG
2347 BTOR_CHKCLONE_RES_PTR (res, slte, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2348 #endif
2349 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2350 }
2351
2352 BoolectorNode *
boolector_ugt(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2353 boolector_ugt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2354 {
2355 BtorNode *e0, *e1, *res;
2356
2357 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2358 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2359 BTOR_ABORT_ARG_NULL (btor);
2360 BTOR_ABORT_ARG_NULL (e0);
2361 BTOR_ABORT_ARG_NULL (e1);
2362 BTOR_TRAPI_BINFUN (e0, e1);
2363 BTOR_ABORT_REFS_NOT_POS (e0);
2364 BTOR_ABORT_REFS_NOT_POS (e1);
2365 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2366 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2367 BTOR_ABORT_IS_NOT_BV (e0);
2368 BTOR_ABORT_IS_NOT_BV (e1);
2369 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2370 res = btor_exp_bv_ugt (btor, e0, e1);
2371 btor_node_inc_ext_ref_counter (btor, res);
2372 BTOR_TRAPI_RETURN_NODE (res);
2373 #ifndef NDEBUG
2374 BTOR_CHKCLONE_RES_PTR (res, ugt, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2375 #endif
2376 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2377 }
2378
2379 BoolectorNode *
boolector_sgt(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2380 boolector_sgt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2381 {
2382 BtorNode *e0, *e1, *res;
2383
2384 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2385 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2386 BTOR_ABORT_ARG_NULL (btor);
2387 BTOR_ABORT_ARG_NULL (e0);
2388 BTOR_ABORT_ARG_NULL (e1);
2389 BTOR_TRAPI_BINFUN (e0, e1);
2390 BTOR_ABORT_REFS_NOT_POS (e0);
2391 BTOR_ABORT_REFS_NOT_POS (e1);
2392 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2393 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2394 BTOR_ABORT_IS_NOT_BV (e0);
2395 BTOR_ABORT_IS_NOT_BV (e1);
2396 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2397 res = btor_exp_bv_sgt (btor, e0, e1);
2398 btor_node_inc_ext_ref_counter (btor, res);
2399 BTOR_TRAPI_RETURN_NODE (res);
2400 #ifndef NDEBUG
2401 BTOR_CHKCLONE_RES_PTR (res, sgt, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2402 #endif
2403 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2404 }
2405
2406 BoolectorNode *
boolector_ugte(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2407 boolector_ugte (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2408 {
2409 BtorNode *e0, *e1, *res;
2410
2411 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2412 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2413 BTOR_ABORT_ARG_NULL (btor);
2414 BTOR_ABORT_ARG_NULL (e0);
2415 BTOR_ABORT_ARG_NULL (e1);
2416 BTOR_TRAPI_BINFUN (e0, e1);
2417 BTOR_ABORT_REFS_NOT_POS (e0);
2418 BTOR_ABORT_REFS_NOT_POS (e1);
2419 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2420 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2421 BTOR_ABORT_IS_NOT_BV (e0);
2422 BTOR_ABORT_IS_NOT_BV (e1);
2423 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2424 res = btor_exp_bv_ugte (btor, e0, e1);
2425 btor_node_inc_ext_ref_counter (btor, res);
2426 BTOR_TRAPI_RETURN_NODE (res);
2427 #ifndef NDEBUG
2428 BTOR_CHKCLONE_RES_PTR (res, ugte, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2429 #endif
2430 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2431 }
2432
2433 BoolectorNode *
boolector_sgte(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2434 boolector_sgte (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2435 {
2436 BtorNode *e0, *e1, *res;
2437
2438 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2439 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2440 BTOR_ABORT_ARG_NULL (btor);
2441 BTOR_ABORT_ARG_NULL (e0);
2442 BTOR_ABORT_ARG_NULL (e1);
2443 BTOR_TRAPI_BINFUN (e0, e1);
2444 BTOR_ABORT_REFS_NOT_POS (e0);
2445 BTOR_ABORT_REFS_NOT_POS (e1);
2446 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2447 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2448 BTOR_ABORT_IS_NOT_BV (e0);
2449 BTOR_ABORT_IS_NOT_BV (e1);
2450 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2451 res = btor_exp_bv_sgte (btor, e0, e1);
2452 btor_node_inc_ext_ref_counter (btor, res);
2453 BTOR_TRAPI_RETURN_NODE (res);
2454 #ifndef NDEBUG
2455 BTOR_CHKCLONE_RES_PTR (res, sgte, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2456 #endif
2457 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2458 }
2459
2460 BoolectorNode *
boolector_sll(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2461 boolector_sll (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2462 {
2463 uint32_t width0, width1;
2464 BtorNode *e0, *e1, *res;
2465
2466 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2467 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2468 BTOR_ABORT_ARG_NULL (btor);
2469 BTOR_ABORT_ARG_NULL (e0);
2470 BTOR_ABORT_ARG_NULL (e1);
2471 BTOR_TRAPI_BINFUN (e0, e1);
2472 BTOR_ABORT_REFS_NOT_POS (e0);
2473 BTOR_ABORT_REFS_NOT_POS (e1);
2474 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2475 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2476 BTOR_ABORT_IS_NOT_BV (e0);
2477 BTOR_ABORT_IS_NOT_BV (e1);
2478
2479 width0 = btor_node_bv_get_width (btor, e0);
2480 width1 = btor_node_bv_get_width (btor, e1);
2481 if (width0 == width1)
2482 {
2483 res = btor_exp_bv_sll (btor, e0, e1);
2484 }
2485 else
2486 {
2487 BTOR_ABORT (!btor_util_is_power_of_2 (width0),
2488 "bit-width of 'e0' must be a power of 2");
2489 BTOR_ABORT (btor_util_log_2 (width0) != width1,
2490 "bit-width of 'e1' must be equal to log2(bit-width of 'e0')");
2491 BtorNode *tmp_e1 = btor_exp_bv_uext (btor, e1, width0 - width1);
2492 res = btor_exp_bv_sll (btor, e0, tmp_e1);
2493 btor_node_release (btor, tmp_e1);
2494 }
2495 btor_node_inc_ext_ref_counter (btor, res);
2496 BTOR_TRAPI_RETURN_NODE (res);
2497 #ifndef NDEBUG
2498 BTOR_CHKCLONE_RES_PTR (res, sll, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2499 #endif
2500 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2501 }
2502
2503 BoolectorNode *
boolector_srl(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2504 boolector_srl (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2505 {
2506 uint32_t width0, width1;
2507 BtorNode *e0, *e1, *res;
2508
2509 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2510 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2511 BTOR_ABORT_ARG_NULL (btor);
2512 BTOR_ABORT_ARG_NULL (e0);
2513 BTOR_ABORT_ARG_NULL (e1);
2514 BTOR_TRAPI_BINFUN (e0, e1);
2515 BTOR_ABORT_REFS_NOT_POS (e0);
2516 BTOR_ABORT_REFS_NOT_POS (e1);
2517 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2518 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2519 BTOR_ABORT_IS_NOT_BV (e0);
2520 BTOR_ABORT_IS_NOT_BV (e1);
2521 width0 = btor_node_bv_get_width (btor, e0);
2522 width1 = btor_node_bv_get_width (btor, e1);
2523 if (width0 == width1)
2524 {
2525 res = btor_exp_bv_srl (btor, e0, e1);
2526 }
2527 else
2528 {
2529 BTOR_ABORT (!btor_util_is_power_of_2 (width0),
2530 "bit-width of 'e0' must be a power of 2");
2531 BTOR_ABORT (btor_util_log_2 (width0) != width1,
2532 "bit-width of 'e1' must be equal to log2(bit-width of 'e0')");
2533 BtorNode *tmp_e1 = btor_exp_bv_uext (btor, e1, width0 - width1);
2534 res = btor_exp_bv_srl (btor, e0, tmp_e1);
2535 btor_node_release (btor, tmp_e1);
2536 }
2537 btor_node_inc_ext_ref_counter (btor, res);
2538 BTOR_TRAPI_RETURN_NODE (res);
2539 #ifndef NDEBUG
2540 BTOR_CHKCLONE_RES_PTR (res, srl, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2541 #endif
2542 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2543 }
2544
2545 BoolectorNode *
boolector_sra(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2546 boolector_sra (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2547 {
2548 uint32_t width0, width1;
2549 BtorNode *e0, *e1, *res;
2550
2551 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2552 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2553 BTOR_ABORT_ARG_NULL (btor);
2554 BTOR_ABORT_ARG_NULL (e0);
2555 BTOR_ABORT_ARG_NULL (e1);
2556 BTOR_TRAPI_BINFUN (e0, e1);
2557 BTOR_ABORT_REFS_NOT_POS (e0);
2558 BTOR_ABORT_REFS_NOT_POS (e1);
2559 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2560 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2561 BTOR_ABORT_IS_NOT_BV (e0);
2562 BTOR_ABORT_IS_NOT_BV (e1);
2563 width0 = btor_node_bv_get_width (btor, e0);
2564 width1 = btor_node_bv_get_width (btor, e1);
2565 if (width0 == width1)
2566 {
2567 res = btor_exp_bv_sra (btor, e0, e1);
2568 }
2569 else
2570 {
2571 BTOR_ABORT (!btor_util_is_power_of_2 (width0),
2572 "bit-width of 'e0' must be a power of 2");
2573 BTOR_ABORT (btor_util_log_2 (width0) != width1,
2574 "bit-width of 'e1' must be equal to log2(bit-width of 'e0')");
2575 BtorNode *tmp_e1 = btor_exp_bv_uext (btor, e1, width0 - width1);
2576 res = btor_exp_bv_sra (btor, e0, tmp_e1);
2577 btor_node_release (btor, tmp_e1);
2578 }
2579 btor_node_inc_ext_ref_counter (btor, res);
2580 BTOR_TRAPI_RETURN_NODE (res);
2581 #ifndef NDEBUG
2582 BTOR_CHKCLONE_RES_PTR (res, sra, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2583 #endif
2584 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2585 }
2586
2587 BoolectorNode *
boolector_rol(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2588 boolector_rol (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2589 {
2590 uint32_t width0, width1;
2591 BtorNode *e0, *e1, *res;
2592
2593 BTOR_ABORT_ARG_NULL (btor);
2594 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2595 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2596 BTOR_ABORT_ARG_NULL (e0);
2597 BTOR_ABORT_ARG_NULL (e1);
2598 BTOR_TRAPI_BINFUN (e0, e1);
2599 BTOR_ABORT_REFS_NOT_POS (e0);
2600 BTOR_ABORT_REFS_NOT_POS (e1);
2601 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2602 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2603 BTOR_ABORT_IS_NOT_BV (e0);
2604 BTOR_ABORT_IS_NOT_BV (e1);
2605 width0 = btor_node_bv_get_width (btor, e0);
2606 width1 = btor_node_bv_get_width (btor, e1);
2607 if (width0 == width1)
2608 {
2609 res = btor_exp_bv_rol (btor, e0, e1);
2610 }
2611 else
2612 {
2613 BTOR_ABORT (!btor_util_is_power_of_2 (width0),
2614 "bit-width of 'e0' must be a power of 2");
2615 BTOR_ABORT (btor_util_log_2 (width0) != width1,
2616 "bit-width of 'e1' must be equal to log2(bit-width of 'e0')");
2617 BtorNode *tmp_e1 = btor_exp_bv_uext (btor, e1, width0 - width1);
2618 res = btor_exp_bv_rol (btor, e0, tmp_e1);
2619 btor_node_release (btor, tmp_e1);
2620 }
2621 btor_node_inc_ext_ref_counter (btor, res);
2622 BTOR_TRAPI_RETURN_NODE (res);
2623 #ifndef NDEBUG
2624 BTOR_CHKCLONE_RES_PTR (res, rol, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2625 #endif
2626 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2627 }
2628
2629 BoolectorNode *
boolector_ror(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2630 boolector_ror (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2631 {
2632 uint32_t width0, width1;
2633 BtorNode *e0, *e1, *res;
2634
2635 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2636 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2637 BTOR_ABORT_ARG_NULL (btor);
2638 BTOR_ABORT_ARG_NULL (e0);
2639 BTOR_ABORT_ARG_NULL (e1);
2640 BTOR_TRAPI_BINFUN (e0, e1);
2641 BTOR_ABORT_REFS_NOT_POS (e0);
2642 BTOR_ABORT_REFS_NOT_POS (e1);
2643 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2644 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2645 BTOR_ABORT_IS_NOT_BV (e0);
2646 BTOR_ABORT_IS_NOT_BV (e1);
2647 width0 = btor_node_bv_get_width (btor, e0);
2648 width1 = btor_node_bv_get_width (btor, e1);
2649 if (width0 == width1)
2650 {
2651 res = btor_exp_bv_ror (btor, e0, e1);
2652 }
2653 else
2654 {
2655 BTOR_ABORT (!btor_util_is_power_of_2 (width0),
2656 "bit-width of 'e0' must be a power of 2");
2657 BTOR_ABORT (btor_util_log_2 (width0) != width1,
2658 "bit-width of 'e1' must be equal to log2(bit-width of 'e0')");
2659 BtorNode *tmp_e1 = btor_exp_bv_uext (btor, e1, width0 - width1);
2660 res = btor_exp_bv_ror (btor, e0, tmp_e1);
2661 btor_node_release (btor, tmp_e1);
2662 }
2663 btor_node_inc_ext_ref_counter (btor, res);
2664 BTOR_TRAPI_RETURN_NODE (res);
2665 #ifndef NDEBUG
2666 BTOR_CHKCLONE_RES_PTR (res, ror, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2667 #endif
2668 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2669 }
2670
2671 BoolectorNode *
boolector_roli(Btor * btor,BoolectorNode * n,uint32_t nbits)2672 boolector_roli (Btor *btor, BoolectorNode *n, uint32_t nbits)
2673 {
2674 BtorNode *exp, *res;
2675
2676 exp = BTOR_IMPORT_BOOLECTOR_NODE (n);
2677 BTOR_ABORT_ARG_NULL (btor);
2678 BTOR_ABORT_ARG_NULL (exp);
2679 BTOR_TRAPI_UNFUN_EXT (exp, "%u", nbits);
2680 BTOR_ABORT_REFS_NOT_POS (exp);
2681 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
2682 BTOR_ABORT_IS_NOT_BV (exp);
2683 res = btor_exp_bv_roli (btor, exp, nbits);
2684 btor_node_inc_ext_ref_counter (btor, res);
2685 BTOR_TRAPI_RETURN_NODE (res);
2686 #ifndef NDEBUG
2687 BTOR_CHKCLONE_RES_PTR (res, roli, BTOR_CLONED_EXP (exp), nbits);
2688 #endif
2689 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2690 }
2691
2692 BoolectorNode *
boolector_rori(Btor * btor,BoolectorNode * n,uint32_t nbits)2693 boolector_rori (Btor *btor, BoolectorNode *n, uint32_t nbits)
2694 {
2695 BtorNode *exp, *res;
2696
2697 exp = BTOR_IMPORT_BOOLECTOR_NODE (n);
2698 BTOR_ABORT_ARG_NULL (btor);
2699 BTOR_ABORT_ARG_NULL (exp);
2700 BTOR_TRAPI_UNFUN_EXT (exp, "%u", nbits);
2701 BTOR_ABORT_REFS_NOT_POS (exp);
2702 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
2703 BTOR_ABORT_IS_NOT_BV (exp);
2704 res = btor_exp_bv_rori (btor, exp, nbits);
2705 btor_node_inc_ext_ref_counter (btor, res);
2706 BTOR_TRAPI_RETURN_NODE (res);
2707 #ifndef NDEBUG
2708 BTOR_CHKCLONE_RES_PTR (res, rori, BTOR_CLONED_EXP (exp), nbits);
2709 #endif
2710 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2711 }
2712
2713 BoolectorNode *
boolector_sub(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2714 boolector_sub (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2715 {
2716 BtorNode *e0, *e1, *res;
2717
2718 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2719 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2720 BTOR_ABORT_ARG_NULL (btor);
2721 BTOR_ABORT_ARG_NULL (e0);
2722 BTOR_ABORT_ARG_NULL (e1);
2723 BTOR_TRAPI_BINFUN (e0, e1);
2724 BTOR_ABORT_REFS_NOT_POS (e0);
2725 BTOR_ABORT_REFS_NOT_POS (e1);
2726 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2727 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2728 BTOR_ABORT_IS_NOT_BV (e0);
2729 BTOR_ABORT_IS_NOT_BV (e1);
2730 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2731 res = btor_exp_bv_sub (btor, e0, e1);
2732 btor_node_inc_ext_ref_counter (btor, res);
2733 BTOR_TRAPI_RETURN_NODE (res);
2734 #ifndef NDEBUG
2735 BTOR_CHKCLONE_RES_PTR (res, sub, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2736 #endif
2737 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2738 }
2739
2740 BoolectorNode *
boolector_usubo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2741 boolector_usubo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2742 {
2743 BtorNode *e0, *e1, *res;
2744
2745 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2746 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2747 BTOR_ABORT_ARG_NULL (btor);
2748 BTOR_ABORT_ARG_NULL (e0);
2749 BTOR_ABORT_ARG_NULL (e1);
2750 BTOR_TRAPI_BINFUN (e0, e1);
2751 BTOR_ABORT_REFS_NOT_POS (e0);
2752 BTOR_ABORT_REFS_NOT_POS (e1);
2753 BTOR_ABORT_IS_NOT_BV (e0);
2754 BTOR_ABORT_IS_NOT_BV (e1);
2755 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2756 res = btor_exp_bv_usubo (btor, e0, e1);
2757 btor_node_inc_ext_ref_counter (btor, res);
2758 BTOR_TRAPI_RETURN_NODE (res);
2759 #ifndef NDEBUG
2760 BTOR_CHKCLONE_RES_PTR (
2761 res, usubo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2762 #endif
2763 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2764 }
2765
2766 BoolectorNode *
boolector_ssubo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2767 boolector_ssubo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2768 {
2769 BtorNode *e0, *e1, *res;
2770
2771 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2772 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2773 BTOR_ABORT_ARG_NULL (btor);
2774 BTOR_ABORT_ARG_NULL (e0);
2775 BTOR_ABORT_ARG_NULL (e1);
2776 BTOR_TRAPI_BINFUN (e0, e1);
2777 BTOR_ABORT_REFS_NOT_POS (e0);
2778 BTOR_ABORT_REFS_NOT_POS (e1);
2779 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2780 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2781 BTOR_ABORT_IS_NOT_BV (e0);
2782 BTOR_ABORT_IS_NOT_BV (e1);
2783 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2784 res = btor_exp_bv_ssubo (btor, e0, e1);
2785 btor_node_inc_ext_ref_counter (btor, res);
2786 BTOR_TRAPI_RETURN_NODE (res);
2787 #ifndef NDEBUG
2788 BTOR_CHKCLONE_RES_PTR (
2789 res, ssubo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2790 #endif
2791 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2792 }
2793
2794 BoolectorNode *
boolector_udiv(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2795 boolector_udiv (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2796 {
2797 BtorNode *e0, *e1, *res;
2798
2799 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2800 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2801 BTOR_ABORT_ARG_NULL (btor);
2802 BTOR_ABORT_ARG_NULL (e0);
2803 BTOR_ABORT_ARG_NULL (e1);
2804 BTOR_TRAPI_BINFUN (e0, e1);
2805 BTOR_ABORT_REFS_NOT_POS (e0);
2806 BTOR_ABORT_REFS_NOT_POS (e1);
2807 BTOR_ABORT_IS_NOT_BV (e0);
2808 BTOR_ABORT_IS_NOT_BV (e1);
2809 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2810 res = btor_exp_bv_udiv (btor, e0, e1);
2811 btor_node_inc_ext_ref_counter (btor, res);
2812 BTOR_TRAPI_RETURN_NODE (res);
2813 #ifndef NDEBUG
2814 BTOR_CHKCLONE_RES_PTR (res, udiv, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2815 #endif
2816 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2817 }
2818
2819 BoolectorNode *
boolector_sdiv(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2820 boolector_sdiv (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2821 {
2822 BtorNode *e0, *e1, *res;
2823
2824 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2825 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2826 BTOR_ABORT_ARG_NULL (btor);
2827 BTOR_ABORT_ARG_NULL (e0);
2828 BTOR_ABORT_ARG_NULL (e1);
2829 BTOR_TRAPI_BINFUN (e0, e1);
2830 BTOR_ABORT_REFS_NOT_POS (e0);
2831 BTOR_ABORT_REFS_NOT_POS (e1);
2832 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2833 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2834 BTOR_ABORT_IS_NOT_BV (e0);
2835 BTOR_ABORT_IS_NOT_BV (e1);
2836 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2837 res = btor_exp_bv_sdiv (btor, e0, e1);
2838 btor_node_inc_ext_ref_counter (btor, res);
2839 BTOR_TRAPI_RETURN_NODE (res);
2840 #ifndef NDEBUG
2841 BTOR_CHKCLONE_RES_PTR (res, sdiv, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2842 #endif
2843 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2844 }
2845
2846 BoolectorNode *
boolector_sdivo(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2847 boolector_sdivo (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2848 {
2849 BtorNode *e0, *e1, *res;
2850
2851 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2852 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2853 BTOR_ABORT_ARG_NULL (btor);
2854 BTOR_ABORT_ARG_NULL (e0);
2855 BTOR_ABORT_ARG_NULL (e1);
2856 BTOR_TRAPI_BINFUN (e0, e1);
2857 BTOR_ABORT_REFS_NOT_POS (e0);
2858 BTOR_ABORT_REFS_NOT_POS (e1);
2859 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2860 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2861 BTOR_ABORT_IS_NOT_BV (e0);
2862 BTOR_ABORT_IS_NOT_BV (e1);
2863 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2864 res = btor_exp_bv_sdivo (btor, e0, e1);
2865 btor_node_inc_ext_ref_counter (btor, res);
2866 BTOR_TRAPI_RETURN_NODE (res);
2867 #ifndef NDEBUG
2868 BTOR_CHKCLONE_RES_PTR (
2869 res, sdivo, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2870 #endif
2871 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2872 }
2873
2874 BoolectorNode *
boolector_urem(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2875 boolector_urem (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2876 {
2877 BtorNode *e0, *e1, *res;
2878
2879 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2880 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2881 BTOR_ABORT_ARG_NULL (btor);
2882 BTOR_ABORT_ARG_NULL (e0);
2883 BTOR_ABORT_ARG_NULL (e1);
2884 BTOR_TRAPI_BINFUN (e0, e1);
2885 BTOR_ABORT_REFS_NOT_POS (e0);
2886 BTOR_ABORT_REFS_NOT_POS (e1);
2887 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2888 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2889 BTOR_ABORT_IS_NOT_BV (e0);
2890 BTOR_ABORT_IS_NOT_BV (e1);
2891 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2892 res = btor_exp_bv_urem (btor, e0, e1);
2893 btor_node_inc_ext_ref_counter (btor, res);
2894 BTOR_TRAPI_RETURN_NODE (res);
2895 #ifndef NDEBUG
2896 BTOR_CHKCLONE_RES_PTR (res, urem, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2897 #endif
2898 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2899 }
2900
2901 BoolectorNode *
boolector_srem(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2902 boolector_srem (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2903 {
2904 BtorNode *e0, *e1, *res;
2905
2906 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2907 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2908 BTOR_ABORT_ARG_NULL (btor);
2909 BTOR_ABORT_ARG_NULL (e0);
2910 BTOR_ABORT_ARG_NULL (e1);
2911 BTOR_TRAPI_BINFUN (e0, e1);
2912 BTOR_ABORT_REFS_NOT_POS (e0);
2913 BTOR_ABORT_REFS_NOT_POS (e1);
2914 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2915 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2916 BTOR_ABORT_IS_NOT_BV (e0);
2917 BTOR_ABORT_IS_NOT_BV (e1);
2918 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2919 res = btor_exp_bv_srem (btor, e0, e1);
2920 btor_node_inc_ext_ref_counter (btor, res);
2921 BTOR_TRAPI_RETURN_NODE (res);
2922 #ifndef NDEBUG
2923 BTOR_CHKCLONE_RES_PTR (res, srem, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2924 #endif
2925 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2926 }
2927
2928 BoolectorNode *
boolector_smod(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2929 boolector_smod (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2930 {
2931 BtorNode *e0, *e1, *res;
2932
2933 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2934 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2935 BTOR_ABORT_ARG_NULL (btor);
2936 BTOR_ABORT_ARG_NULL (e0);
2937 BTOR_ABORT_ARG_NULL (e1);
2938 BTOR_TRAPI_BINFUN (e0, e1);
2939 BTOR_ABORT_REFS_NOT_POS (e0);
2940 BTOR_ABORT_REFS_NOT_POS (e1);
2941 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2942 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2943 BTOR_ABORT_IS_NOT_BV (e0);
2944 BTOR_ABORT_IS_NOT_BV (e1);
2945 BTOR_ABORT_SORT_MISMATCH (e0, e1);
2946 res = btor_exp_bv_smod (btor, e0, e1);
2947 btor_node_inc_ext_ref_counter (btor, res);
2948 BTOR_TRAPI_RETURN_NODE (res);
2949 #ifndef NDEBUG
2950 BTOR_CHKCLONE_RES_PTR (res, smod, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2951 #endif
2952 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2953 }
2954
2955 BoolectorNode *
boolector_concat(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)2956 boolector_concat (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
2957 {
2958 BtorNode *e0, *e1, *res;
2959
2960 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
2961 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
2962 BTOR_ABORT_ARG_NULL (btor);
2963 BTOR_ABORT_ARG_NULL (e0);
2964 BTOR_ABORT_ARG_NULL (e1);
2965 BTOR_TRAPI_BINFUN (e0, e1);
2966 BTOR_ABORT_REFS_NOT_POS (e0);
2967 BTOR_ABORT_REFS_NOT_POS (e1);
2968 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
2969 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
2970 BTOR_ABORT_IS_NOT_BV (e0);
2971 BTOR_ABORT_IS_NOT_BV (e1);
2972 BTOR_ABORT (btor_node_bv_get_width (btor, e0)
2973 > UINT32_MAX - btor_node_bv_get_width (btor, e1),
2974 "bit-width of result is too large");
2975 res = btor_exp_bv_concat (btor, e0, e1);
2976 btor_node_inc_ext_ref_counter (btor, res);
2977 BTOR_TRAPI_RETURN_NODE (res);
2978 #ifndef NDEBUG
2979 BTOR_CHKCLONE_RES_PTR (
2980 res, concat, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
2981 #endif
2982 return BTOR_EXPORT_BOOLECTOR_NODE (res);
2983 }
2984
2985 BoolectorNode *
boolector_repeat(Btor * btor,BoolectorNode * node,uint32_t n)2986 boolector_repeat (Btor *btor, BoolectorNode *node, uint32_t n)
2987 {
2988 BtorNode *exp, *res;
2989
2990 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
2991 BTOR_ABORT_ARG_NULL (btor);
2992 BTOR_ABORT_ARG_NULL (exp);
2993 BTOR_TRAPI_UNFUN_EXT (exp, "%u", n);
2994 BTOR_ABORT_REFS_NOT_POS (exp);
2995 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
2996 BTOR_ABORT_IS_NOT_BV (exp);
2997 BTOR_ABORT (
2998 ((uint32_t) (UINT32_MAX / n)) < btor_node_bv_get_width (btor, exp),
2999 "resulting bit-width of 'repeat' too large");
3000 res = btor_exp_bv_repeat (btor, exp, n);
3001 btor_node_inc_ext_ref_counter (btor, res);
3002 BTOR_TRAPI_RETURN_NODE (res);
3003 #ifndef NDEBUG
3004 BTOR_CHKCLONE_RES_PTR (res, repeat, BTOR_CLONED_EXP (exp), n);
3005 #endif
3006 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3007 }
3008
3009 /*------------------------------------------------------------------------*/
3010
3011 BoolectorNode *
boolector_read(Btor * btor,BoolectorNode * n_array,BoolectorNode * n_index)3012 boolector_read (Btor *btor, BoolectorNode *n_array, BoolectorNode *n_index)
3013 {
3014 BtorNode *e_array, *e_index, *res;
3015
3016 e_array = BTOR_IMPORT_BOOLECTOR_NODE (n_array);
3017 e_index = BTOR_IMPORT_BOOLECTOR_NODE (n_index);
3018 BTOR_ABORT_ARG_NULL (btor);
3019 BTOR_ABORT_ARG_NULL (e_array);
3020 BTOR_ABORT_ARG_NULL (e_index);
3021 BTOR_TRAPI_BINFUN (e_array, e_index);
3022 BTOR_ABORT_REFS_NOT_POS (e_array);
3023 BTOR_ABORT_REFS_NOT_POS (e_index);
3024 BTOR_ABORT_BTOR_MISMATCH (btor, e_array);
3025 BTOR_ABORT_BTOR_MISMATCH (btor, e_index);
3026 BTOR_ABORT_IS_NOT_ARRAY (e_array);
3027 BTOR_ABORT_IS_NOT_BV (e_index);
3028 BTOR_ABORT (
3029 btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
3030 != btor_node_get_sort_id (e_index),
3031 "index bit-width of 'e_array' and bit-width of 'e_index' must be equal");
3032 res = btor_exp_read (btor, e_array, e_index);
3033 btor_node_inc_ext_ref_counter (btor, res);
3034 BTOR_TRAPI_RETURN_NODE (res);
3035 #ifndef NDEBUG
3036 BTOR_CHKCLONE_RES_PTR (
3037 res, read, BTOR_CLONED_EXP (e_array), BTOR_CLONED_EXP (e_index));
3038 #endif
3039 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3040 }
3041
3042 BoolectorNode *
boolector_write(Btor * btor,BoolectorNode * n_array,BoolectorNode * n_index,BoolectorNode * n_value)3043 boolector_write (Btor *btor,
3044 BoolectorNode *n_array,
3045 BoolectorNode *n_index,
3046 BoolectorNode *n_value)
3047 {
3048 BtorNode *e_array, *e_index, *e_value;
3049 BtorNode *res;
3050
3051 e_array = BTOR_IMPORT_BOOLECTOR_NODE (n_array);
3052 e_index = BTOR_IMPORT_BOOLECTOR_NODE (n_index);
3053 e_value = BTOR_IMPORT_BOOLECTOR_NODE (n_value);
3054 BTOR_ABORT_ARG_NULL (btor);
3055 BTOR_ABORT_ARG_NULL (e_array);
3056 BTOR_ABORT_ARG_NULL (e_index);
3057 BTOR_ABORT_ARG_NULL (e_value);
3058 BTOR_TRAPI_TERFUN (e_array, e_index, e_value);
3059 BTOR_ABORT_REFS_NOT_POS (e_array);
3060 BTOR_ABORT_REFS_NOT_POS (e_index);
3061 BTOR_ABORT_REFS_NOT_POS (e_value);
3062 BTOR_ABORT_BTOR_MISMATCH (btor, e_array);
3063 BTOR_ABORT_BTOR_MISMATCH (btor, e_index);
3064 BTOR_ABORT_BTOR_MISMATCH (btor, e_value);
3065 BTOR_ABORT_IS_NOT_ARRAY (e_array);
3066 BTOR_ABORT_IS_NOT_BV (e_index);
3067 BTOR_ABORT_IS_NOT_BV (e_value);
3068 BTOR_ABORT (
3069 btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
3070 != btor_node_get_sort_id (e_index),
3071 "index bit-width of 'e_array' and bit-width of 'e_index' must be equal");
3072 BTOR_ABORT (
3073 btor_sort_array_get_element (btor, btor_node_get_sort_id (e_array))
3074 != btor_node_get_sort_id (e_value),
3075 "element bit-width of 'e_array' and bit-width of 'e_value' must be "
3076 "equal");
3077 res = btor_exp_write (btor, e_array, e_index, e_value);
3078 btor_node_inc_ext_ref_counter (btor, res);
3079 BTOR_TRAPI_RETURN_NODE (res);
3080 #ifndef NDEBUG
3081 BTOR_CHKCLONE_RES_PTR (res,
3082 write,
3083 BTOR_CLONED_EXP (e_array),
3084 BTOR_CLONED_EXP (e_index),
3085 BTOR_CLONED_EXP (e_value));
3086 #endif
3087 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3088 }
3089
3090 /*------------------------------------------------------------------------*/
3091
3092 BoolectorNode *
boolector_cond(Btor * btor,BoolectorNode * n_cond,BoolectorNode * n_then,BoolectorNode * n_else)3093 boolector_cond (Btor *btor,
3094 BoolectorNode *n_cond,
3095 BoolectorNode *n_then,
3096 BoolectorNode *n_else)
3097 {
3098 BtorNode *e_cond, *e_if, *e_else;
3099 BtorNode *res;
3100
3101 e_cond = BTOR_IMPORT_BOOLECTOR_NODE (n_cond);
3102 e_if = BTOR_IMPORT_BOOLECTOR_NODE (n_then);
3103 e_else = BTOR_IMPORT_BOOLECTOR_NODE (n_else);
3104 BTOR_ABORT_ARG_NULL (btor);
3105 BTOR_ABORT_ARG_NULL (e_cond);
3106 BTOR_ABORT_ARG_NULL (e_if);
3107 BTOR_ABORT_ARG_NULL (e_else);
3108 BTOR_TRAPI_TERFUN (e_cond, e_if, e_else);
3109 BTOR_ABORT_REFS_NOT_POS (e_cond);
3110 BTOR_ABORT_REFS_NOT_POS (e_if);
3111 BTOR_ABORT_REFS_NOT_POS (e_else);
3112 BTOR_ABORT_BTOR_MISMATCH (btor, e_cond);
3113 BTOR_ABORT_BTOR_MISMATCH (btor, e_if);
3114 BTOR_ABORT_BTOR_MISMATCH (btor, e_else);
3115 BTOR_ABORT_IS_NOT_BV (e_cond);
3116 BTOR_ABORT (btor_node_bv_get_width (btor, e_cond) != 1,
3117 "bit-width of 'e_cond' must be equal to 1");
3118 BTOR_ABORT (btor_node_get_sort_id (e_if) != btor_node_get_sort_id (e_else),
3119 "sorts of 'e_if' and 'e_else' branch must be equal");
3120 res = btor_exp_cond (btor, e_cond, e_if, e_else);
3121 btor_node_inc_ext_ref_counter (btor, res);
3122 BTOR_TRAPI_RETURN_NODE (res);
3123 #ifndef NDEBUG
3124 BTOR_CHKCLONE_RES_PTR (res,
3125 cond,
3126 BTOR_CLONED_EXP (e_cond),
3127 BTOR_CLONED_EXP (e_if),
3128 BTOR_CLONED_EXP (e_else));
3129 #endif
3130 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3131 }
3132
3133 /*------------------------------------------------------------------------*/
3134
3135 BoolectorNode *
boolector_param(Btor * btor,BoolectorSort sort,const char * symbol)3136 boolector_param (Btor *btor, BoolectorSort sort, const char *symbol)
3137 {
3138 BTOR_ABORT_ARG_NULL (btor);
3139
3140 BtorNode *res;
3141 char *symb;
3142 BtorSortId s;
3143
3144 symb = mk_unique_symbol (btor, symbol);
3145 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT " %s", sort, btor, symb);
3146 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
3147 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
3148 BTOR_ABORT (!btor_sort_is_bv (btor, s),
3149 "'sort' is not a bit vector sort");
3150 BTOR_ABORT (symb && btor_hashptr_table_get (btor->symbols, symb),
3151 "symbol '%s' is already in use in the current context",
3152 symb);
3153 res = btor_exp_param (btor, s, symb);
3154 btor_mem_freestr (btor->mm, symb);
3155 btor_node_inc_ext_ref_counter (btor, res);
3156
3157 BTOR_TRAPI_RETURN_NODE (res);
3158 #ifndef NDEBUG
3159 BTOR_CHKCLONE_RES_PTR (res, param, sort, symbol);
3160 #endif
3161 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3162 }
3163
3164 BoolectorNode *
boolector_fun(Btor * btor,BoolectorNode ** param_nodes,uint32_t paramc,BoolectorNode * node)3165 boolector_fun (Btor *btor,
3166 BoolectorNode **param_nodes,
3167 uint32_t paramc,
3168 BoolectorNode *node)
3169 {
3170 uint32_t i;
3171 BtorNode **params, *exp, *res;
3172
3173 params = BTOR_IMPORT_BOOLECTOR_NODE_ARRAY (param_nodes);
3174 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3175
3176 BTOR_ABORT_ARG_NULL (btor);
3177 BTOR_ABORT_ARG_NULL (params);
3178 BTOR_ABORT_ARG_NULL (exp);
3179 BTOR_ABORT_REFS_NOT_POS (exp);
3180 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3181 BTOR_ABORT (paramc < 1, "'paramc' must not be < 1");
3182
3183 BTOR_TRAPI_PRINT ("%s %p %u ", __FUNCTION__ + 10, btor, paramc);
3184 for (i = 0; i < paramc; i++)
3185 {
3186 BTOR_ABORT (!params[i] || !btor_node_is_param (params[i]),
3187 "'params[%u]' is not a parameter",
3188 i);
3189 BTOR_ABORT (btor_node_param_is_bound (params[i]),
3190 "'params[%u]' already bound");
3191 BTOR_ABORT_REFS_NOT_POS (params[i]);
3192 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (params[i]));
3193 }
3194 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (exp));
3195 BTOR_TRAPI_PRINT ("\n");
3196
3197 BTOR_ABORT (btor_node_is_uf (btor_simplify_exp (btor, exp)),
3198 "expected bit vector term as function body");
3199 res = btor_exp_fun (btor, params, paramc, exp);
3200 btor_node_inc_ext_ref_counter (btor, res);
3201 BTOR_TRAPI_RETURN_NODE (res);
3202 #ifndef NDEBUG
3203 BoolectorNode *cparam_nodes[paramc];
3204 for (i = 0; btor->clone && i < paramc; i++)
3205 cparam_nodes[i] = BTOR_CLONED_EXP (params[i]);
3206 BTOR_CHKCLONE_RES_PTR (res, fun, cparam_nodes, paramc, BTOR_CLONED_EXP (exp));
3207 #endif
3208 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3209 }
3210
3211 BoolectorNode *
boolector_apply(Btor * btor,BoolectorNode ** arg_nodes,uint32_t argc,BoolectorNode * n_fun)3212 boolector_apply (Btor *btor,
3213 BoolectorNode **arg_nodes,
3214 uint32_t argc,
3215 BoolectorNode *n_fun)
3216 {
3217 uint32_t i;
3218 int32_t fcheck;
3219 BtorNode **args, *e_fun, *res;
3220
3221 args = BTOR_IMPORT_BOOLECTOR_NODE_ARRAY (arg_nodes);
3222 e_fun = BTOR_IMPORT_BOOLECTOR_NODE (n_fun);
3223
3224 BTOR_ABORT_ARG_NULL (btor);
3225 BTOR_ABORT_ARG_NULL (e_fun);
3226
3227 BTOR_ABORT_REFS_NOT_POS (e_fun);
3228 BTOR_ABORT_BTOR_MISMATCH (btor, e_fun);
3229
3230 BTOR_TRAPI_PRINT ("%s %p %u ", __FUNCTION__ + 10, btor, argc);
3231 for (i = 0; i < argc; i++)
3232 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (args[i]));
3233 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (e_fun));
3234 BTOR_TRAPI_PRINT ("\n");
3235
3236 BTOR_ABORT (!btor_sort_is_fun (btor, btor_node_get_sort_id (e_fun)),
3237 "'e_fun' must be a function");
3238 BTOR_ABORT (
3239 (uint32_t) argc != btor_node_fun_get_arity (btor, e_fun),
3240 "number of arguments must be equal to the number of parameters in "
3241 "'e_fun'");
3242 BTOR_ABORT (argc < 1, "'argc' must not be < 1");
3243 BTOR_ABORT (argc >= 1 && !args, "no arguments given but argc defined > 0");
3244 fcheck = btor_fun_sort_check (btor, args, argc, e_fun);
3245 BTOR_ABORT (fcheck >= 0, "invalid argument given at position %d", fcheck);
3246 res = btor_exp_apply_n (btor, e_fun, args, argc);
3247 btor_node_inc_ext_ref_counter (btor, res);
3248 BTOR_TRAPI_RETURN_NODE (res);
3249 #ifndef NDEBUG
3250 BoolectorNode *carg_nodes[argc];
3251 for (i = 0; btor->clone && i < argc; i++)
3252 carg_nodes[i] = BTOR_CLONED_EXP (args[i]);
3253 BTOR_CHKCLONE_RES_PTR (res, apply, carg_nodes, argc, BTOR_CLONED_EXP (e_fun));
3254 #endif
3255 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3256 }
3257
3258 /*------------------------------------------------------------------------*/
3259
3260 BoolectorNode *
boolector_inc(Btor * btor,BoolectorNode * node)3261 boolector_inc (Btor *btor, BoolectorNode *node)
3262 {
3263 BtorNode *exp, *res;
3264
3265 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3266 BTOR_ABORT_ARG_NULL (btor);
3267 BTOR_ABORT_ARG_NULL (exp);
3268 BTOR_TRAPI_UNFUN (exp);
3269 BTOR_ABORT_REFS_NOT_POS (exp);
3270 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3271 BTOR_ABORT_IS_NOT_BV (exp);
3272
3273 res = btor_exp_bv_inc (btor, exp);
3274 btor_node_inc_ext_ref_counter (btor, res);
3275 BTOR_TRAPI_RETURN_NODE (res);
3276 #ifndef NDEBUG
3277 BTOR_CHKCLONE_RES_PTR (res, inc, BTOR_CLONED_EXP (exp));
3278 #endif
3279 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3280 }
3281
3282 BoolectorNode *
boolector_dec(Btor * btor,BoolectorNode * node)3283 boolector_dec (Btor *btor, BoolectorNode *node)
3284 {
3285 BtorNode *exp, *res;
3286
3287 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3288 BTOR_ABORT_ARG_NULL (btor);
3289 BTOR_ABORT_ARG_NULL (exp);
3290 BTOR_TRAPI_UNFUN (exp);
3291 BTOR_ABORT_REFS_NOT_POS (exp);
3292 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3293 BTOR_ABORT_IS_NOT_BV (exp);
3294
3295 res = btor_exp_bv_dec (btor, exp);
3296 btor_node_inc_ext_ref_counter (btor, res);
3297 BTOR_TRAPI_RETURN_NODE (res);
3298 #ifndef NDEBUG
3299 BTOR_CHKCLONE_RES_PTR (res, dec, BTOR_CLONED_EXP (exp));
3300 #endif
3301 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3302 }
3303
3304 /*------------------------------------------------------------------------*/
3305
3306 static bool
params_distinct(Btor * btor,BtorNode * params[],uint32_t paramc)3307 params_distinct (Btor *btor, BtorNode *params[], uint32_t paramc)
3308 {
3309 bool res = true;
3310 BtorIntHashTable *cache = btor_hashint_table_new (btor->mm);
3311 for (uint32_t i = 0; i < paramc; i++)
3312 {
3313 if (btor_hashint_table_contains (cache, btor_node_get_id (params[i])))
3314 {
3315 res = false;
3316 break;
3317 }
3318 btor_hashint_table_add (cache, btor_node_get_id (params[i]));
3319 }
3320 btor_hashint_table_delete (cache);
3321 return res;
3322 }
3323
3324 BoolectorNode *
boolector_forall(Btor * btor,BoolectorNode * param_nodes[],uint32_t paramc,BoolectorNode * body_node)3325 boolector_forall (Btor *btor,
3326 BoolectorNode *param_nodes[],
3327 uint32_t paramc,
3328 BoolectorNode *body_node)
3329 {
3330 uint32_t i;
3331 BtorNode **params, *body, *res;
3332
3333 params = BTOR_IMPORT_BOOLECTOR_NODE_ARRAY (param_nodes);
3334 body = BTOR_IMPORT_BOOLECTOR_NODE (body_node);
3335 BTOR_ABORT_ARG_NULL (btor);
3336 BTOR_ABORT_ARG_NULL (params);
3337 BTOR_ABORT_ARG_NULL (body);
3338
3339 BTOR_TRAPI_PRINT ("%s %p %u ", __FUNCTION__ + 10, btor, paramc);
3340 for (i = 0; i < paramc; i++)
3341 {
3342 BTOR_ABORT (!params[i] || !btor_node_is_param (params[i]),
3343 "'params[%u]' is not a parameter",
3344 i);
3345 BTOR_ABORT (btor_node_param_is_bound (params[i]),
3346 "'params[%u]' already bound");
3347 BTOR_ABORT_REFS_NOT_POS (params[i]);
3348 BTOR_ABORT_BTOR_MISMATCH (btor, params[i]);
3349 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (params[i]));
3350 }
3351 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (body));
3352 BTOR_TRAPI_PRINT ("\n");
3353 BTOR_ABORT (!params_distinct (btor, params, paramc),
3354 "given parameters are not distinct");
3355
3356 BTOR_ABORT_REFS_NOT_POS (body);
3357 BTOR_ABORT_BTOR_MISMATCH (btor, body);
3358 BTOR_ABORT (!btor_sort_is_bool (btor, btor_node_real_addr (body)->sort_id),
3359 "body of forall must be bit width 1, but has "
3360 "%u instead",
3361 btor_node_bv_get_width (btor, body));
3362
3363 res = btor_exp_forall_n (btor, params, paramc, body);
3364 btor_node_inc_ext_ref_counter (btor, res);
3365 BTOR_TRAPI_RETURN_NODE (res);
3366 #ifndef NDEBUG
3367 BoolectorNode *cparam_nodes[paramc];
3368 for (i = 0; btor->clone && i < paramc; i++)
3369 cparam_nodes[i] = BTOR_CLONED_EXP (params[i]);
3370 BTOR_CHKCLONE_RES_PTR (
3371 res, forall, cparam_nodes, paramc, BTOR_CLONED_EXP (body));
3372 #endif
3373 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3374 }
3375
3376 BoolectorNode *
boolector_exists(Btor * btor,BoolectorNode * param_nodes[],uint32_t paramc,BoolectorNode * body_node)3377 boolector_exists (Btor *btor,
3378 BoolectorNode *param_nodes[],
3379 uint32_t paramc,
3380 BoolectorNode *body_node)
3381 {
3382 uint32_t i;
3383 BtorNode **params, *body, *res;
3384
3385 params = BTOR_IMPORT_BOOLECTOR_NODE_ARRAY (param_nodes);
3386 body = BTOR_IMPORT_BOOLECTOR_NODE (body_node);
3387 BTOR_ABORT_ARG_NULL (btor);
3388 BTOR_ABORT_ARG_NULL (params);
3389 BTOR_ABORT_ARG_NULL (body);
3390
3391 BTOR_TRAPI_PRINT ("%s %p %u ", __FUNCTION__ + 10, btor, paramc);
3392 for (i = 0; i < paramc; i++)
3393 {
3394 BTOR_ABORT (!params[i] || !btor_node_is_param (params[i]),
3395 "'params[%u]' is not a parameter",
3396 i);
3397 BTOR_ABORT (btor_node_param_is_bound (params[i]),
3398 "'params[%u]' already bound");
3399 BTOR_ABORT_REFS_NOT_POS (params[i]);
3400 BTOR_ABORT_BTOR_MISMATCH (btor, params[i]);
3401 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (params[i]));
3402 }
3403 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (body));
3404 BTOR_TRAPI_PRINT ("\n");
3405 BTOR_ABORT (!params_distinct (btor, params, paramc),
3406 "given parameters are not distinct");
3407
3408 BTOR_ABORT_REFS_NOT_POS (body);
3409 BTOR_ABORT_BTOR_MISMATCH (btor, body);
3410 BTOR_ABORT (!btor_sort_is_bool (btor, btor_node_real_addr (body)->sort_id),
3411 "body of exists must be bit width 1, but has "
3412 "%u instead",
3413 btor_node_bv_get_width (btor, body));
3414
3415 res = btor_exp_exists_n (btor, params, paramc, body);
3416 btor_node_inc_ext_ref_counter (btor, res);
3417 BTOR_TRAPI_RETURN_NODE (res);
3418 #ifndef NDEBUG
3419 BoolectorNode *cparam_nodes[paramc];
3420 for (i = 0; btor->clone && i < paramc; i++)
3421 cparam_nodes[i] = BTOR_CLONED_EXP (params[i]);
3422 BTOR_CHKCLONE_RES_PTR (
3423 res, exists, cparam_nodes, paramc, BTOR_CLONED_EXP (body));
3424 #endif
3425 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3426 }
3427
3428 /*------------------------------------------------------------------------*/
3429
3430 Btor *
boolector_get_btor(BoolectorNode * node)3431 boolector_get_btor (BoolectorNode *node)
3432 {
3433 BtorNode *exp, *real_exp;
3434 Btor *btor;
3435 BTOR_ABORT_ARG_NULL (node);
3436 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3437 BTOR_ABORT_REFS_NOT_POS (exp);
3438 real_exp = btor_node_real_addr (exp);
3439 btor = real_exp->btor;
3440 BTOR_TRAPI_UNFUN (exp);
3441 BTOR_TRAPI_RETURN_PTR (btor);
3442 #ifndef NDEBUG
3443 if (btor->clone)
3444 {
3445 Btor *clone = boolector_get_btor (BTOR_CLONED_EXP (exp));
3446 assert (clone == btor->clone);
3447 btor_chkclone (btor, btor->clone);
3448 }
3449 #endif
3450 return btor;
3451 }
3452
3453 int32_t
boolector_get_node_id(Btor * btor,BoolectorNode * node)3454 boolector_get_node_id (Btor *btor, BoolectorNode *node)
3455 {
3456 int32_t res;
3457 BtorNode *exp;
3458
3459 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3460 BTOR_ABORT_ARG_NULL (btor);
3461 BTOR_ABORT_ARG_NULL (node);
3462 BTOR_TRAPI_UNFUN (exp);
3463 BTOR_ABORT_REFS_NOT_POS (exp);
3464 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3465 res = btor_node_get_id (btor_node_real_addr (exp));
3466 BTOR_TRAPI_RETURN_INT (res);
3467 #ifndef NDEBUG
3468 BTOR_CHKCLONE_RES_INT (res, get_node_id, BTOR_CLONED_EXP (exp));
3469 #endif
3470 return res;
3471 }
3472
3473 BoolectorSort
boolector_get_sort(Btor * btor,const BoolectorNode * node)3474 boolector_get_sort (Btor *btor, const BoolectorNode *node)
3475 {
3476 BtorNode *exp;
3477 BtorSortId res;
3478
3479 BTOR_ABORT_ARG_NULL (btor);
3480 BTOR_ABORT_ARG_NULL (node);
3481 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3482 BTOR_TRAPI_UNFUN (exp);
3483 res = btor_node_get_sort_id (exp);
3484 BTOR_TRAPI_RETURN_SORT (res);
3485 #ifndef NDEBUG
3486 BTOR_CHKCLONE_RES_SORT (res, get_sort, BTOR_CLONED_EXP (exp));
3487 #endif
3488 return BTOR_EXPORT_BOOLECTOR_SORT (res);
3489 }
3490
3491 BoolectorSort
boolector_fun_get_domain_sort(Btor * btor,const BoolectorNode * node)3492 boolector_fun_get_domain_sort (Btor *btor, const BoolectorNode *node)
3493 {
3494 BtorNode *exp;
3495 BtorSortId res;
3496
3497 BTOR_ABORT_ARG_NULL (btor);
3498 BTOR_ABORT_ARG_NULL (node);
3499 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3500 BTOR_ABORT (!btor_node_is_fun (btor_simplify_exp (btor, exp)),
3501 "node must be a function node");
3502 BTOR_TRAPI_UNFUN (exp);
3503 res = ((BtorFunSort) btor_sort_get_by_id (btor, btor_node_get_sort_id (exp))
3504 ->fun)
3505 .domain->id;
3506 BTOR_TRAPI_RETURN_SORT (res);
3507 #ifndef NDEBUG
3508 BTOR_CHKCLONE_RES_SORT (res, fun_get_domain_sort, BTOR_CLONED_EXP (exp));
3509 #endif
3510 return BTOR_EXPORT_BOOLECTOR_SORT (res);
3511 }
3512
3513 BoolectorSort
boolector_fun_get_codomain_sort(Btor * btor,const BoolectorNode * node)3514 boolector_fun_get_codomain_sort (Btor *btor, const BoolectorNode *node)
3515 {
3516 BtorNode *exp;
3517 BtorSortId res;
3518
3519 BTOR_ABORT_ARG_NULL (btor);
3520 BTOR_ABORT_ARG_NULL (node);
3521 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3522 BTOR_ABORT (!btor_node_is_fun (btor_simplify_exp (btor, exp)),
3523 "node must be a function node");
3524 BTOR_TRAPI_UNFUN (exp);
3525 res = ((BtorFunSort) btor_sort_get_by_id (btor, btor_node_get_sort_id (exp))
3526 ->fun)
3527 .codomain->id;
3528 BTOR_TRAPI_RETURN_SORT (res);
3529 #ifndef NDEBUG
3530 BTOR_CHKCLONE_RES_SORT (res, fun_get_codomain_sort, BTOR_CLONED_EXP (exp));
3531 #endif
3532 return BTOR_EXPORT_BOOLECTOR_SORT (res);
3533 }
3534
3535 /*------------------------------------------------------------------------*/
3536
3537 BoolectorNode *
boolector_match_node_by_id(Btor * btor,int32_t id)3538 boolector_match_node_by_id (Btor *btor, int32_t id)
3539 {
3540 BtorNode *res;
3541 BTOR_ABORT_ARG_NULL (btor);
3542 BTOR_ABORT (id <= 0, "node id must be > 0");
3543 BTOR_TRAPI ("%d", id);
3544 res = btor_node_match_by_id (btor, id);
3545 BTOR_ABORT (
3546 !res,
3547 "invalid node id '%d', no matching node in given Boolector instance",
3548 id);
3549 btor_node_inc_ext_ref_counter (btor, res);
3550 BTOR_TRAPI_RETURN_NODE (res);
3551 #ifndef NDEBUG
3552 BTOR_CHKCLONE_RES_PTR (res, match_node_by_id, id);
3553 #endif
3554 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3555 }
3556
3557 BoolectorNode *
boolector_match_node_by_symbol(Btor * btor,const char * symbol)3558 boolector_match_node_by_symbol (Btor *btor, const char *symbol)
3559 {
3560 char *symb;
3561 uint32_t i;
3562 BtorNode *res;
3563 BTOR_ABORT_ARG_NULL (btor);
3564 BTOR_ABORT_ARG_NULL (symbol);
3565 BTOR_TRAPI ("%s", symbol);
3566 for (i = 0, res = 0; !res && i <= btor->num_push_pop; i++)
3567 {
3568 symb = mk_unique_symbol_aux (btor->mm, i, symbol);
3569 res = btor_node_match_by_symbol (btor, symb);
3570 btor_mem_freestr (btor->mm, symb);
3571 }
3572 BTOR_ABORT (
3573 !res,
3574 "invalid symbol'%s', no matching node in given Boolector instance",
3575 symbol);
3576 btor_node_inc_ext_ref_counter (btor, res);
3577 BTOR_TRAPI_RETURN_NODE (res);
3578 #ifndef NDEBUG
3579 BTOR_CHKCLONE_RES_PTR (res, match_node_by_symbol, symbol);
3580 #endif
3581 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3582 }
3583
3584 BoolectorNode *
boolector_match_node(Btor * btor,BoolectorNode * node)3585 boolector_match_node (Btor *btor, BoolectorNode *node)
3586 {
3587 BtorNode *res, *exp;
3588
3589 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3590 BTOR_ABORT_ARG_NULL (btor);
3591 BTOR_TRAPI_UNFUN (exp);
3592 BTOR_ABORT_REFS_NOT_POS (exp);
3593 res = btor_node_match (btor, exp);
3594 BTOR_ABORT (!res,
3595 "invalid node, no matching node in given Boolector instance");
3596 btor_node_inc_ext_ref_counter (btor, res);
3597 BTOR_TRAPI_RETURN_NODE (res);
3598 #ifndef NDEBUG
3599 BTOR_CHKCLONE_RES_PTR (res, match_node, BTOR_CLONED_EXP (exp));
3600 #endif
3601 return BTOR_EXPORT_BOOLECTOR_NODE (res);
3602 }
3603
3604 /*------------------------------------------------------------------------*/
3605
3606 const char *
boolector_get_symbol(Btor * btor,BoolectorNode * node)3607 boolector_get_symbol (Btor *btor, BoolectorNode *node)
3608 {
3609 const char *res;
3610 BtorNode *exp;
3611
3612 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3613 BTOR_ABORT_ARG_NULL (btor);
3614 BTOR_ABORT_ARG_NULL (exp);
3615 BTOR_TRAPI_UNFUN (exp);
3616 BTOR_ABORT_REFS_NOT_POS (exp);
3617 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3618 res = remove_unique_symbol_prefix (btor, btor_node_get_symbol (btor, exp));
3619 BTOR_TRAPI_RETURN_STR (res);
3620 #ifndef NDEBUG
3621 BTOR_CHKCLONE_RES_STR (res, get_symbol, BTOR_CLONED_EXP (exp));
3622 #endif
3623 return res;
3624 }
3625
3626 void
boolector_set_symbol(Btor * btor,BoolectorNode * node,const char * symbol)3627 boolector_set_symbol (Btor *btor, BoolectorNode *node, const char *symbol)
3628 {
3629 char *symb;
3630 BtorNode *exp;
3631
3632 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3633 BTOR_ABORT_ARG_NULL (btor);
3634 BTOR_ABORT_ARG_NULL (exp);
3635 BTOR_ABORT_ARG_NULL (symbol);
3636 BTOR_TRAPI_UNFUN_EXT (exp, "%s", symbol);
3637 BTOR_ABORT_REFS_NOT_POS (exp);
3638 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3639 symb = mk_unique_symbol (btor, symbol);
3640
3641 if (btor_hashptr_table_get (btor->symbols, symb))
3642 {
3643 BTOR_WARN (
3644 true, "symbol %s already defined, ignoring setting symbol", symbol);
3645 }
3646 else
3647 {
3648 btor_node_set_symbol (btor, exp, symb);
3649 }
3650 btor_mem_freestr (btor->mm, symb);
3651 #ifndef NDEBUG
3652 BTOR_CHKCLONE_NORES (set_symbol, BTOR_CLONED_EXP (exp), symbol);
3653 #endif
3654 }
3655
3656 uint32_t
boolector_get_width(Btor * btor,BoolectorNode * node)3657 boolector_get_width (Btor *btor, BoolectorNode *node)
3658 {
3659 uint32_t res;
3660 BtorNode *exp;
3661
3662 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3663 BTOR_ABORT_ARG_NULL (btor);
3664 BTOR_ABORT_ARG_NULL (exp);
3665 BTOR_TRAPI_UNFUN (exp);
3666 BTOR_ABORT_REFS_NOT_POS (exp);
3667 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3668 if (btor_sort_is_fun (btor, btor_node_get_sort_id (exp)))
3669 res = btor_node_fun_get_width (btor, exp);
3670 else
3671 res = btor_node_bv_get_width (btor, exp);
3672 BTOR_TRAPI_RETURN_UINT (res);
3673 #ifndef NDEBUG
3674 BTOR_CHKCLONE_RES_UINT (res, get_width, BTOR_CLONED_EXP (exp));
3675 #endif
3676 return res;
3677 }
3678
3679 uint32_t
boolector_get_index_width(Btor * btor,BoolectorNode * n_array)3680 boolector_get_index_width (Btor *btor, BoolectorNode *n_array)
3681 {
3682 uint32_t res;
3683 BtorNode *e_array;
3684
3685 e_array = BTOR_IMPORT_BOOLECTOR_NODE (n_array);
3686 BTOR_ABORT_ARG_NULL (btor);
3687 BTOR_ABORT_ARG_NULL (e_array);
3688 BTOR_TRAPI_UNFUN (e_array);
3689 BTOR_ABORT_REFS_NOT_POS (e_array);
3690 BTOR_ABORT_BTOR_MISMATCH (btor, e_array);
3691 BTOR_ABORT_IS_NOT_ARRAY (e_array);
3692 BTOR_ABORT (btor_node_fun_get_arity (btor, e_array) > 1,
3693 "'n_array' is a function with arity > 1");
3694 res = btor_node_array_get_index_width (btor, e_array);
3695 BTOR_TRAPI_RETURN_UINT (res);
3696 #ifndef NDEBUG
3697 BTOR_CHKCLONE_RES_UINT (res, get_index_width, BTOR_CLONED_EXP (e_array));
3698 #endif
3699 return res;
3700 }
3701
3702 const char *
boolector_get_bits(Btor * btor,BoolectorNode * node)3703 boolector_get_bits (Btor *btor, BoolectorNode *node)
3704 {
3705 BtorNode *exp, *real;
3706 BtorBVAss *bvass;
3707 char *bits;
3708 const char *res;
3709
3710 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3711 BTOR_ABORT_ARG_NULL (btor);
3712 BTOR_TRAPI_UNFUN (exp);
3713 BTOR_ABORT_ARG_NULL (node);
3714 BTOR_ABORT_REFS_NOT_POS (exp);
3715 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3716 BTOR_ABORT (!btor_node_is_bv_const (exp), "argument is not a constant node");
3717 real = btor_node_real_addr (exp);
3718 /* representations of bits of const nodes are maintained analogously
3719 * to bv assignment strings */
3720 if (!btor_node_is_inverted (exp))
3721 bits = btor_bv_to_char (btor->mm, btor_node_bv_const_get_bits (exp));
3722 else
3723 bits = btor_bv_to_char (btor->mm, btor_node_bv_const_get_invbits (real));
3724 bvass = btor_ass_new_bv (btor->bv_assignments, bits);
3725 btor_mem_freestr (btor->mm, bits);
3726 res = btor_ass_get_bv_str (bvass);
3727 BTOR_TRAPI_RETURN_PTR (res);
3728 #ifndef NDEBUG
3729 if (btor->clone)
3730 {
3731 const char *cloneres =
3732 boolector_get_bits (btor->clone, BTOR_CLONED_EXP (exp));
3733 assert (!strcmp (cloneres, res));
3734 bvass->cloned_assignment = cloneres;
3735 btor_chkclone (btor, btor->clone);
3736 }
3737 #endif
3738 return res;
3739 }
3740
3741 void
boolector_free_bits(Btor * btor,const char * bits)3742 boolector_free_bits (Btor *btor, const char *bits)
3743 {
3744 BTOR_ABORT_ARG_NULL (btor);
3745 BTOR_TRAPI ("%p", bits);
3746 BTOR_ABORT_ARG_NULL (bits);
3747 #ifndef NDEBUG
3748 char *cass;
3749 cass = (char *) btor_ass_get_bv ((const char *) bits)->cloned_assignment;
3750 #endif
3751 btor_ass_release_bv (btor->bv_assignments, bits);
3752 #ifndef NDEBUG
3753 BTOR_CHKCLONE_NORES (free_bits, cass);
3754 #endif
3755 }
3756
3757 uint32_t
boolector_get_fun_arity(Btor * btor,BoolectorNode * node)3758 boolector_get_fun_arity (Btor *btor, BoolectorNode *node)
3759 {
3760 uint32_t res;
3761 BtorNode *exp;
3762
3763 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3764 BTOR_ABORT_ARG_NULL (btor);
3765 BTOR_ABORT_ARG_NULL (exp);
3766 BTOR_TRAPI_UNFUN (exp);
3767 BTOR_ABORT_REFS_NOT_POS (exp);
3768 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3769 BTOR_ABORT (!btor_node_is_fun (btor_simplify_exp (btor, exp)),
3770 "given expression is not a function node");
3771 res = btor_node_fun_get_arity (btor, exp);
3772 BTOR_TRAPI_RETURN_UINT (res);
3773 #ifndef NDEBUG
3774 BTOR_CHKCLONE_RES_UINT (res, get_fun_arity, BTOR_CLONED_EXP (exp));
3775 #endif
3776 return res;
3777 }
3778
3779 /*------------------------------------------------------------------------*/
3780
3781 bool
boolector_is_const(Btor * btor,BoolectorNode * node)3782 boolector_is_const (Btor *btor, BoolectorNode *node)
3783 {
3784 BtorNode *exp;
3785 bool res;
3786 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3787 BTOR_ABORT_ARG_NULL (btor);
3788 BTOR_ABORT_ARG_NULL (exp);
3789 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3790 BTOR_TRAPI_UNFUN (exp);
3791 BTOR_ABORT_REFS_NOT_POS (exp);
3792 res = btor_node_is_bv_const (exp);
3793 BTOR_TRAPI_RETURN_BOOL (res);
3794 #ifndef NDEBUG
3795 BTOR_CHKCLONE_RES_BOOL (res, is_const, BTOR_CLONED_EXP (exp));
3796 #endif
3797 return res;
3798 }
3799
3800 bool
boolector_is_var(Btor * btor,BoolectorNode * node)3801 boolector_is_var (Btor *btor, BoolectorNode *node)
3802 {
3803 BtorNode *exp;
3804 bool res;
3805 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3806 BTOR_ABORT_ARG_NULL (btor);
3807 BTOR_ABORT_ARG_NULL (exp);
3808 BTOR_TRAPI_UNFUN (exp);
3809 BTOR_ABORT_REFS_NOT_POS (exp);
3810 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3811 res = btor_node_is_bv_var (btor_simplify_exp (btor, exp));
3812 BTOR_TRAPI_RETURN_BOOL (res);
3813 #ifndef NDEBUG
3814 BTOR_CHKCLONE_RES_BOOL (res, is_var, BTOR_CLONED_EXP (exp));
3815 #endif
3816 return res;
3817 }
3818
3819 bool
boolector_is_array(Btor * btor,BoolectorNode * node)3820 boolector_is_array (Btor *btor, BoolectorNode *node)
3821 {
3822 bool res;
3823 BtorNode *exp;
3824
3825 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3826 BTOR_ABORT_ARG_NULL (btor);
3827 BTOR_ABORT_ARG_NULL (exp);
3828 BTOR_TRAPI_UNFUN (exp);
3829 BTOR_ABORT_REFS_NOT_POS (exp);
3830 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3831 res = btor_node_is_array (btor_simplify_exp (btor, exp));
3832 BTOR_TRAPI_RETURN_BOOL (res);
3833 #ifndef NDEBUG
3834 BTOR_CHKCLONE_RES_BOOL (res, is_array, BTOR_CLONED_EXP (exp));
3835 #endif
3836 return res;
3837 }
3838
3839 bool
boolector_is_array_var(Btor * btor,BoolectorNode * node)3840 boolector_is_array_var (Btor *btor, BoolectorNode *node)
3841 {
3842 bool res;
3843 BtorNode *exp;
3844
3845 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3846 BTOR_ABORT_ARG_NULL (btor);
3847 BTOR_ABORT_ARG_NULL (exp);
3848 BTOR_TRAPI_UNFUN (exp);
3849 BTOR_ABORT_REFS_NOT_POS (exp);
3850 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3851 res = btor_node_is_uf_array (btor_simplify_exp (btor, exp));
3852 BTOR_TRAPI_RETURN_BOOL (res);
3853 #ifndef NDEBUG
3854 BTOR_CHKCLONE_RES_BOOL (res, is_array_var, BTOR_CLONED_EXP (exp));
3855 #endif
3856 return res;
3857 }
3858
3859 bool
boolector_is_param(Btor * btor,BoolectorNode * node)3860 boolector_is_param (Btor *btor, BoolectorNode *node)
3861 {
3862 BtorNode *exp;
3863 bool res;
3864
3865 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3866 BTOR_ABORT_ARG_NULL (btor);
3867 BTOR_ABORT_ARG_NULL (exp);
3868 BTOR_TRAPI_UNFUN (exp);
3869 BTOR_ABORT_REFS_NOT_POS (exp);
3870 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3871 res = btor_node_is_param (btor_simplify_exp (btor, exp));
3872 BTOR_TRAPI_RETURN_BOOL (res);
3873 #ifndef NDEBUG
3874 BTOR_CHKCLONE_RES_BOOL (res, is_param, BTOR_CLONED_EXP (exp));
3875 #endif
3876 return res;
3877 }
3878
3879 bool
boolector_is_bound_param(Btor * btor,BoolectorNode * node)3880 boolector_is_bound_param (Btor *btor, BoolectorNode *node)
3881 {
3882 BtorNode *exp;
3883 bool res;
3884
3885 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3886 BTOR_ABORT_ARG_NULL (btor);
3887 BTOR_ABORT_ARG_NULL (exp);
3888 BTOR_TRAPI_UNFUN (exp);
3889 BTOR_ABORT_REFS_NOT_POS (exp);
3890 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3891 BTOR_ABORT (!btor_node_is_param (btor_simplify_exp (btor, exp)),
3892 "given expression is not a parameter node");
3893 res = btor_node_param_is_bound (exp);
3894 BTOR_TRAPI_RETURN_BOOL (res);
3895 #ifndef NDEBUG
3896 BTOR_CHKCLONE_RES_BOOL (res, is_bound_param, BTOR_CLONED_EXP (exp));
3897 #endif
3898 return res;
3899 }
3900
3901 bool
boolector_is_uf(Btor * btor,BoolectorNode * node)3902 boolector_is_uf (Btor *btor, BoolectorNode *node)
3903 {
3904 bool res;
3905 BtorNode *exp;
3906
3907 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3908 BTOR_ABORT_ARG_NULL (btor);
3909 BTOR_ABORT_ARG_NULL (exp);
3910 BTOR_TRAPI_UNFUN (exp);
3911 BTOR_ABORT_REFS_NOT_POS (exp);
3912 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3913 res = btor_node_is_uf (btor_simplify_exp (btor, exp));
3914 BTOR_TRAPI_RETURN_BOOL (res);
3915 #ifndef NDEBUG
3916 BTOR_CHKCLONE_RES_BOOL (res, is_uf, BTOR_CLONED_EXP (exp));
3917 #endif
3918 return res;
3919 }
3920
3921 bool
boolector_is_fun(Btor * btor,BoolectorNode * node)3922 boolector_is_fun (Btor *btor, BoolectorNode *node)
3923 {
3924 bool res;
3925 BtorNode *exp;
3926
3927 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3928 BTOR_ABORT_ARG_NULL (btor);
3929 BTOR_ABORT_ARG_NULL (exp);
3930 BTOR_TRAPI_UNFUN (exp);
3931 BTOR_ABORT_REFS_NOT_POS (exp);
3932 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
3933 res = btor_node_is_fun (btor_simplify_exp (btor, exp));
3934 BTOR_TRAPI_RETURN_BOOL (res);
3935 #ifndef NDEBUG
3936 BTOR_CHKCLONE_RES_BOOL (res, is_fun, BTOR_CLONED_EXP (exp));
3937 #endif
3938 return res;
3939 }
3940
3941 /*------------------------------------------------------------------------*/
3942
3943 int32_t
boolector_fun_sort_check(Btor * btor,BoolectorNode ** arg_nodes,uint32_t argc,BoolectorNode * n_fun)3944 boolector_fun_sort_check (Btor *btor,
3945 BoolectorNode **arg_nodes,
3946 uint32_t argc,
3947 BoolectorNode *n_fun)
3948 {
3949 BtorNode **args, *e_fun;
3950 uint32_t i;
3951 int32_t res;
3952
3953 args = BTOR_IMPORT_BOOLECTOR_NODE_ARRAY (arg_nodes);
3954 e_fun = BTOR_IMPORT_BOOLECTOR_NODE (n_fun);
3955 BTOR_ABORT_ARG_NULL (btor);
3956 BTOR_ABORT_ARG_NULL (e_fun);
3957 BTOR_ABORT (argc < 1, "'argc' must not be < 1");
3958 BTOR_ABORT (argc >= 1 && !args, "no arguments given but argc defined > 0");
3959
3960 BTOR_TRAPI_PRINT ("%s %p %u ", __FUNCTION__ + 10, btor, argc);
3961 for (i = 0; i < argc; i++)
3962 {
3963 BTOR_ABORT_ARG_NULL (args[i]);
3964 BTOR_ABORT_REFS_NOT_POS (args[i]);
3965 BTOR_ABORT_BTOR_MISMATCH (btor, args[i]);
3966 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (args[i]));
3967 }
3968 BTOR_TRAPI_PRINT (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (e_fun));
3969 BTOR_TRAPI_PRINT ("\n");
3970
3971 res = btor_fun_sort_check (btor, args, argc, e_fun);
3972 BTOR_TRAPI_RETURN_INT (res);
3973 #ifndef NDEBUG
3974 BoolectorNode *carg_nodes[argc];
3975 for (i = 0; btor->clone && i < argc; i++)
3976 carg_nodes[i] = BTOR_CLONED_EXP (args[i]);
3977 BTOR_CHKCLONE_RES_INT (
3978 res, fun_sort_check, carg_nodes, argc, BTOR_CLONED_EXP (e_fun));
3979 #endif
3980 return res;
3981 }
3982
3983 /*------------------------------------------------------------------------*/
3984
3985 const char *
boolector_bv_assignment(Btor * btor,BoolectorNode * node)3986 boolector_bv_assignment (Btor *btor, BoolectorNode *node)
3987 {
3988 char *ass;
3989 const char *res;
3990 BtorNode *exp;
3991 BtorBVAss *bvass;
3992 uint32_t opt;
3993
3994 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
3995 BTOR_ABORT_ARG_NULL (btor);
3996 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_SAT
3997 || !btor->valid_assignments,
3998 "cannot retrieve model if input formula is not SAT");
3999 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
4000 "model generation has not been enabled");
4001 BTOR_ABORT (btor->quantifiers->count,
4002 "models are currently not supported with quantifiers");
4003 BTOR_ABORT_ARG_NULL (exp);
4004 BTOR_TRAPI_UNFUN (exp);
4005 BTOR_ABORT_REFS_NOT_POS (exp);
4006 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
4007 BTOR_ABORT_IS_NOT_BV (exp);
4008 opt = btor_opt_get (btor, BTOR_OPT_OUTPUT_NUMBER_FORMAT);
4009 switch (opt)
4010 {
4011 case BTOR_OUTPUT_BASE_HEX:
4012 ass = btor_bv_to_hex_char (btor->mm, btor_model_get_bv (btor, exp));
4013 break;
4014 case BTOR_OUTPUT_BASE_DEC:
4015 ass = btor_bv_to_dec_char (btor->mm, btor_model_get_bv (btor, exp));
4016 break;
4017 default:
4018 assert (opt == BTOR_OUTPUT_BASE_BIN);
4019 ass = btor_bv_to_char (btor->mm, btor_model_get_bv (btor, exp));
4020 }
4021 bvass = btor_ass_new_bv (btor->bv_assignments, ass);
4022 btor_mem_freestr (btor->mm, ass);
4023 res = btor_ass_get_bv_str (bvass);
4024 BTOR_TRAPI_RETURN_PTR (res);
4025 #ifndef NDEBUG
4026 if (btor->clone)
4027 {
4028 const char *cloneres =
4029 boolector_bv_assignment (btor->clone, BTOR_CLONED_EXP (exp));
4030 assert (!strcmp (cloneres, res));
4031 bvass->cloned_assignment = cloneres;
4032 btor_chkclone (btor, btor->clone);
4033 }
4034 #endif
4035 return res;
4036 }
4037
4038 void
boolector_free_bv_assignment(Btor * btor,const char * assignment)4039 boolector_free_bv_assignment (Btor *btor, const char *assignment)
4040 {
4041 BTOR_ABORT_ARG_NULL (btor);
4042 BTOR_TRAPI ("%p", assignment);
4043 BTOR_ABORT_ARG_NULL (assignment);
4044 #ifndef NDEBUG
4045 char *cass;
4046 cass =
4047 (char *) btor_ass_get_bv ((const char *) assignment)->cloned_assignment;
4048 #endif
4049 btor_ass_release_bv (btor->bv_assignments, assignment);
4050 #ifndef NDEBUG
4051 BTOR_CHKCLONE_NORES (free_bv_assignment, cass);
4052 #endif
4053 }
4054
4055 static void
generate_fun_model_str(Btor * btor,BtorNode * exp,char *** args,char *** values,uint32_t * size)4056 generate_fun_model_str (
4057 Btor *btor, BtorNode *exp, char ***args, char ***values, uint32_t *size)
4058 {
4059 assert (btor);
4060 assert (exp);
4061 assert (args);
4062 assert (values);
4063 assert (size);
4064 assert (btor_node_is_regular (exp));
4065
4066 char *arg, *tmp, **bv;
4067 uint32_t i, j, len;
4068 BtorPtrHashTableIterator it;
4069 const BtorPtrHashTable *model;
4070 BtorBitVector *value;
4071 BtorBitVectorTuple *t;
4072 uint32_t opt;
4073
4074 opt = btor_opt_get (btor, BTOR_OPT_OUTPUT_NUMBER_FORMAT);
4075
4076 exp = btor_simplify_exp (btor, exp);
4077 assert (btor_node_is_fun (exp));
4078
4079 model = btor_model_get_fun_aux (btor, btor->bv_model, btor->fun_model, exp);
4080
4081 if ((btor_node_is_lambda (exp) && btor_node_fun_get_arity (btor, exp) > 1)
4082 || !btor->fun_model || !model)
4083 {
4084 *size = 0;
4085 return;
4086 }
4087
4088 assert (model->count > 0);
4089
4090 *size = model->count;
4091 BTOR_NEWN (btor->mm, *args, *size);
4092 BTOR_NEWN (btor->mm, *values, *size);
4093
4094 i = 0;
4095 btor_iter_hashptr_init (&it, (BtorPtrHashTable *) model);
4096 while (btor_iter_hashptr_has_next (&it))
4097 {
4098 value = (BtorBitVector *) it.bucket->data.as_ptr;
4099
4100 /* build assignment string for all arguments */
4101 t = (BtorBitVectorTuple *) btor_iter_hashptr_next (&it);
4102 if (t->arity)
4103 {
4104 BTOR_CNEWN (btor->mm, bv, t->arity);
4105 len = t->arity;
4106 for (j = 0; j < t->arity; j++)
4107 {
4108 switch (opt)
4109 {
4110 case BTOR_OUTPUT_BASE_HEX:
4111 bv[j] = btor_bv_to_hex_char (btor->mm, t->bv[j]);
4112 break;
4113 case BTOR_OUTPUT_BASE_DEC:
4114 bv[j] = btor_bv_to_dec_char (btor->mm, t->bv[j]);
4115 break;
4116 default:
4117 assert (opt == BTOR_OUTPUT_BASE_BIN);
4118 bv[j] = btor_bv_to_char (btor->mm, t->bv[j]);
4119 }
4120 len += strlen (bv[j]);
4121 }
4122 BTOR_CNEWN (btor->mm, arg, len);
4123 tmp = arg;
4124 strncpy (tmp, bv[0], len);
4125 len -= strlen (bv[0]);
4126
4127 for (j = 1; j < t->arity; j++)
4128 {
4129 strncat (tmp, " ", len);
4130 len -= 1;
4131 strncat (tmp, bv[j], len);
4132 len -= strlen (bv[j]);
4133 }
4134 for (j = 0; j < t->arity; j++) btor_mem_freestr (btor->mm, bv[j]);
4135 BTOR_DELETEN (btor->mm, bv, t->arity);
4136 len -= 1;
4137 assert (len == 0);
4138 }
4139 /* If argument tuple has arity 0, value represents the default value for
4140 * the function/array (constant arrays). */
4141 else
4142 {
4143 BTOR_CNEWN (btor->mm, arg, 2);
4144 arg[0] = '*';
4145 }
4146
4147 (*args)[i] = arg;
4148 switch (opt)
4149 {
4150 case BTOR_OUTPUT_BASE_HEX:
4151 (*values)[i] = (char *) btor_bv_to_hex_char (btor->mm, value);
4152 break;
4153 case BTOR_OUTPUT_BASE_DEC:
4154 (*values)[i] = (char *) btor_bv_to_dec_char (btor->mm, value);
4155 break;
4156 default:
4157 assert (opt == BTOR_OUTPUT_BASE_BIN);
4158 (*values)[i] = (char *) btor_bv_to_char (btor->mm, value);
4159 }
4160 i++;
4161 }
4162 }
4163
4164 static void
fun_assignment(Btor * btor,BtorNode * n,char *** args,char *** values,uint32_t * size,BtorFunAss ** ass)4165 fun_assignment (Btor *btor,
4166 BtorNode *n,
4167 char ***args,
4168 char ***values,
4169 uint32_t *size,
4170 BtorFunAss **ass)
4171 {
4172 assert (btor);
4173 assert (n);
4174 assert (args);
4175 assert (values);
4176 assert (size);
4177 assert (btor_node_is_regular (n));
4178
4179 uint32_t i;
4180 char **a = 0, **v = 0;
4181
4182 *ass = 0;
4183 generate_fun_model_str (btor, n, &a, &v, size);
4184
4185 if (*size)
4186 {
4187 *ass = btor_ass_new_fun (btor->fun_assignments, a, v, *size);
4188 for (i = 0; i < *size; i++)
4189 {
4190 btor_mem_freestr (btor->mm, a[i]);
4191 btor_mem_freestr (btor->mm, v[i]);
4192 }
4193 btor_mem_free (btor->mm, a, *size * sizeof (*a));
4194 btor_mem_free (btor->mm, v, *size * sizeof (*v));
4195 btor_ass_get_fun_indices_values (*ass, args, values, *size);
4196 }
4197 }
4198
4199 void
boolector_array_assignment(Btor * btor,BoolectorNode * n_array,char *** indices,char *** values,uint32_t * size)4200 boolector_array_assignment (Btor *btor,
4201 BoolectorNode *n_array,
4202 char ***indices,
4203 char ***values,
4204 uint32_t *size)
4205 {
4206 BtorNode *e_array;
4207 BtorFunAss *ass;
4208
4209 e_array = BTOR_IMPORT_BOOLECTOR_NODE (n_array);
4210 BTOR_ABORT_ARG_NULL (btor);
4211 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_SAT
4212 || !btor->valid_assignments,
4213 "cannot retrieve model if input formula is not SAT");
4214 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
4215 "model generation has not been enabled");
4216 BTOR_ABORT_ARG_NULL (e_array);
4217 BTOR_TRAPI_UNFUN (e_array);
4218 BTOR_ABORT_ARG_NULL (indices);
4219 BTOR_ABORT_ARG_NULL (values);
4220 BTOR_ABORT_ARG_NULL (size);
4221 BTOR_ABORT_REFS_NOT_POS (e_array);
4222 BTOR_ABORT_BTOR_MISMATCH (btor, e_array);
4223 BTOR_ABORT_IS_NOT_ARRAY (e_array);
4224
4225 fun_assignment (btor, e_array, indices, values, size, &ass);
4226
4227 /* special case: we treat out parameters as return values for btoruntrace */
4228 BTOR_TRAPI_RETURN ("%p %p %u", *indices, *values, *size);
4229
4230 #ifndef NDEBUG
4231 if (btor->clone)
4232 {
4233 char **cindices, **cvalues;
4234 uint32_t i, csize;
4235 boolector_array_assignment (
4236 btor->clone, BTOR_CLONED_EXP (e_array), &cindices, &cvalues, &csize);
4237 assert (csize == *size);
4238 for (i = 0; i < *size; i++)
4239 {
4240 assert (!strcmp ((*indices)[i], cindices[i]));
4241 assert (!strcmp ((*values)[i], cvalues[i]));
4242 }
4243 if (ass)
4244 {
4245 assert (*size);
4246 ass->cloned_indices = cindices;
4247 ass->cloned_values = cvalues;
4248 }
4249 btor_chkclone (btor, btor->clone);
4250 }
4251 #endif
4252 }
4253
4254 void
boolector_free_array_assignment(Btor * btor,char ** indices,char ** values,uint32_t size)4255 boolector_free_array_assignment (Btor *btor,
4256 char **indices,
4257 char **values,
4258 uint32_t size)
4259 {
4260 BtorFunAss *funass;
4261
4262 BTOR_ABORT_ARG_NULL (btor);
4263 BTOR_TRAPI ("%p %p %u", indices, values, size);
4264 BTOR_ABORT (size && !indices, "size > 0 but 'indices' are zero");
4265 BTOR_ABORT (size && !values, "size > 0 but 'values' are zero");
4266 BTOR_ABORT (!size && indices, "non zero 'indices' but 'size == 0'");
4267 BTOR_ABORT (!size && values, "non zero 'values' but 'size == 0'");
4268 if (!size) { return; }
4269
4270 funass =
4271 btor_ass_get_fun ((const char **) indices, (const char **) values, size);
4272 BTOR_ABORT (size != funass->size,
4273 "wrong size given, expected %u, but got %u", funass->size, size);
4274 #ifndef NDEBUG
4275 char **cindices, **cvalues;
4276 cindices = funass->cloned_indices;
4277 cvalues = funass->cloned_values;
4278 #endif
4279 btor_ass_release_fun (btor->fun_assignments, indices, values, size);
4280 #ifndef NDEBUG
4281 BTOR_CHKCLONE_NORES (free_array_assignment, cindices, cvalues, size);
4282 #endif
4283 }
4284
4285 void
boolector_uf_assignment(Btor * btor,BoolectorNode * n_uf,char *** args,char *** values,uint32_t * size)4286 boolector_uf_assignment (Btor *btor,
4287 BoolectorNode *n_uf,
4288 char ***args,
4289 char ***values,
4290 uint32_t *size)
4291 {
4292 BtorNode *e_uf;
4293 BtorFunAss *ass;
4294
4295 e_uf = BTOR_IMPORT_BOOLECTOR_NODE (n_uf);
4296 BTOR_ABORT_ARG_NULL (btor);
4297 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_SAT
4298 || !btor->valid_assignments,
4299 "cannot retrieve model if input formula is not SAT");
4300 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
4301 "model generation has not been enabled");
4302 BTOR_ABORT_ARG_NULL (e_uf);
4303 BTOR_TRAPI_UNFUN (e_uf);
4304 BTOR_ABORT_ARG_NULL (args);
4305 BTOR_ABORT_ARG_NULL (values);
4306 BTOR_ABORT_ARG_NULL (size);
4307 BTOR_ABORT_REFS_NOT_POS (e_uf);
4308 BTOR_ABORT_BTOR_MISMATCH (btor, e_uf);
4309 BTOR_ABORT_IS_NOT_FUN (e_uf);
4310
4311 fun_assignment (btor, e_uf, args, values, size, &ass);
4312
4313 /* special case: we treat out parameters as return values for btoruntrace */
4314 BTOR_TRAPI_RETURN ("%p %p %u", *args, *values, *size);
4315
4316 #ifndef NDEBUG
4317 if (btor->clone)
4318 {
4319 char **cargs, **cvalues;
4320 uint32_t i, csize;
4321 boolector_uf_assignment (
4322 btor->clone, BTOR_CLONED_EXP (e_uf), &cargs, &cvalues, &csize);
4323 assert (csize == *size);
4324 for (i = 0; i < *size; i++)
4325 {
4326 assert (!strcmp ((*args)[i], cargs[i]));
4327 assert (!strcmp ((*values)[i], cvalues[i]));
4328 }
4329 if (ass)
4330 {
4331 assert (*size);
4332 ass->cloned_indices = cargs;
4333 ass->cloned_values = cvalues;
4334 }
4335 btor_chkclone (btor, btor->clone);
4336 }
4337 #endif
4338 }
4339
4340 void
boolector_free_uf_assignment(Btor * btor,char ** args,char ** values,uint32_t size)4341 boolector_free_uf_assignment (Btor *btor,
4342 char **args,
4343 char **values,
4344 uint32_t size)
4345 {
4346 BtorFunAss *funass;
4347
4348 BTOR_ABORT_ARG_NULL (btor);
4349 BTOR_TRAPI ("%p %p %u", args, values, size);
4350 BTOR_ABORT (size && !args, "size > 0 but 'args' are zero");
4351 BTOR_ABORT (size && !values, "size > 0 but 'values' are zero");
4352 BTOR_ABORT (!size && args, "non zero 'args' but 'size == 0'");
4353 BTOR_ABORT (!size && values, "non zero 'values' but 'size == 0'");
4354 funass =
4355 btor_ass_get_fun ((const char **) args, (const char **) values, size);
4356 BTOR_ABORT (size != funass->size,
4357 "wrong size given, expected %u, but got %u", funass->size, size);
4358 #ifndef NDEBUG
4359 char **cargs, **cvalues;
4360 cargs = funass->cloned_indices;
4361 cvalues = funass->cloned_values;
4362 #endif
4363 btor_ass_release_fun (btor->fun_assignments, args, values, size);
4364 #ifndef NDEBUG
4365 BTOR_CHKCLONE_NORES (free_array_assignment, cargs, cvalues, size);
4366 #endif
4367 }
4368
4369 void
boolector_print_model(Btor * btor,char * format,FILE * file)4370 boolector_print_model (Btor *btor, char *format, FILE *file)
4371 {
4372 BTOR_ABORT_ARG_NULL (btor);
4373 BTOR_ABORT_ARG_NULL (format);
4374 BTOR_TRAPI ("%s", format);
4375 BTOR_ABORT_ARG_NULL (file);
4376 BTOR_ABORT (strcmp (format, "btor") && strcmp (format, "smt2"),
4377 "invalid model output format: %s",
4378 format);
4379 BTOR_ABORT (btor->last_sat_result != BTOR_RESULT_SAT
4380 || !btor->valid_assignments,
4381 "cannot retrieve model if input formula is not SAT");
4382 BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_MODEL_GEN),
4383 "model generation has not been enabled");
4384 btor_print_model (btor, format, file);
4385 #ifndef NDEBUG
4386 BTOR_CHKCLONE_NORES (print_model, format, file);
4387 #endif
4388 }
4389
4390 /*------------------------------------------------------------------------*/
4391
4392 BoolectorSort
boolector_bool_sort(Btor * btor)4393 boolector_bool_sort (Btor *btor)
4394 {
4395 BTOR_ABORT_ARG_NULL (btor);
4396 BTOR_TRAPI ("");
4397
4398 BtorSortId res;
4399 res = btor_sort_bool (btor);
4400 inc_sort_ext_ref_counter (btor, res);
4401 BTOR_TRAPI_RETURN_SORT (res);
4402 #ifndef NDEBUG
4403 BTOR_CHKCLONE_RES_SORT (res, bool_sort);
4404 #endif
4405 return BTOR_EXPORT_BOOLECTOR_SORT (res);
4406 }
4407
4408 BoolectorSort
boolector_bitvec_sort(Btor * btor,uint32_t width)4409 boolector_bitvec_sort (Btor *btor, uint32_t width)
4410 {
4411 BTOR_ABORT_ARG_NULL (btor);
4412 BTOR_TRAPI ("%u", width);
4413 BTOR_ABORT (width == 0, "'width' must be > 0");
4414
4415 BtorSortId res;
4416 res = btor_sort_bv (btor, width);
4417 inc_sort_ext_ref_counter (btor, res);
4418 BTOR_TRAPI_RETURN_SORT (res);
4419 #ifndef NDEBUG
4420 BTOR_CHKCLONE_RES_SORT (res, bitvec_sort, width);
4421 #endif
4422 return BTOR_EXPORT_BOOLECTOR_SORT (res);
4423 }
4424
4425 static BtorSortId
boolector_tuple_sort(Btor * btor,BoolectorSort * sorts,size_t num_elements)4426 boolector_tuple_sort (Btor *btor, BoolectorSort *sorts, size_t num_elements)
4427 {
4428 BtorSortId element_ids[num_elements];
4429 size_t i;
4430 for (i = 0; i < num_elements; i++)
4431 element_ids[i] = BTOR_IMPORT_BOOLECTOR_SORT (sorts[i]);
4432 return btor_sort_tuple (btor, element_ids, num_elements);
4433 }
4434
4435 BoolectorSort
boolector_fun_sort(Btor * btor,BoolectorSort domain[],uint32_t arity,BoolectorSort codomain)4436 boolector_fun_sort (Btor *btor,
4437 BoolectorSort domain[],
4438 uint32_t arity,
4439 BoolectorSort codomain)
4440 {
4441 BTOR_ABORT_ARG_NULL (btor);
4442 BTOR_ABORT_ARG_NULL (domain);
4443 BTOR_ABORT (arity <= 0, "'arity' must be > 0");
4444
4445 uint32_t i;
4446 BtorSortId res, tup, cos, s;
4447
4448 BTOR_TRAPI_PRINT ("%s %p ", __FUNCTION__ + 10, btor);
4449 BTOR_TRAPI_PRINT (
4450 BTOR_TRAPI_SORT_FMT, BTOR_IMPORT_BOOLECTOR_SORT ((domain[0])), btor);
4451 for (i = 1; i < arity; i++)
4452 BTOR_TRAPI_PRINT (
4453 BTOR_TRAPI_SORT_FMT, BTOR_IMPORT_BOOLECTOR_SORT (domain[i]), btor);
4454 BTOR_TRAPI_PRINT (
4455 BTOR_TRAPI_SORT_FMT, BTOR_IMPORT_BOOLECTOR_SORT (codomain), btor);
4456 BTOR_TRAPI_PRINT ("\n");
4457
4458 for (i = 0; i < arity; i++)
4459 {
4460 s = BTOR_IMPORT_BOOLECTOR_SORT (domain[i]);
4461 BTOR_ABORT (!btor_sort_is_valid (btor, s),
4462 "'domain' sort at position %u is not a valid sort",
4463 i);
4464 BTOR_ABORT (
4465 !btor_sort_is_bv (btor, s) && !btor_sort_is_bool (btor, s),
4466 "'domain' sort at position %u must be a bool or bit vector sort",
4467 i);
4468 }
4469 cos = BTOR_IMPORT_BOOLECTOR_SORT (codomain);
4470 BTOR_ABORT (!btor_sort_is_valid (btor, cos),
4471 "'codomain' sort is not a valid sort");
4472 BTOR_ABORT (
4473 !btor_sort_is_bv (btor, cos) && !btor_sort_is_bool (btor, cos),
4474 "'codomain' sort must be a bool or bit vector sort");
4475
4476 tup = boolector_tuple_sort (btor, domain, arity);
4477
4478 res = btor_sort_fun (btor, tup, cos);
4479 btor_sort_release (btor, tup);
4480 inc_sort_ext_ref_counter (btor, res);
4481 BTOR_TRAPI_RETURN_SORT (res);
4482 #ifndef NDEBUG
4483 BTOR_CHKCLONE_RES_SORT (res, fun_sort, domain, arity, codomain);
4484 #endif
4485 return BTOR_EXPORT_BOOLECTOR_SORT (res);
4486 }
4487
4488 BoolectorSort
boolector_array_sort(Btor * btor,BoolectorSort index,BoolectorSort element)4489 boolector_array_sort (Btor *btor, BoolectorSort index, BoolectorSort element)
4490 {
4491 BTOR_ABORT_ARG_NULL (btor);
4492 BTOR_TRAPI (
4493 BTOR_TRAPI_SORT_FMT " " BTOR_TRAPI_SORT_FMT, index, btor, element, btor);
4494
4495 BtorSortId is, es, res;
4496
4497 is = BTOR_IMPORT_BOOLECTOR_SORT (index);
4498 es = BTOR_IMPORT_BOOLECTOR_SORT (element);
4499
4500 BTOR_ABORT (!btor_sort_is_valid (btor, is),
4501 "'index' sort is not a valid sort");
4502 BTOR_ABORT (!btor_sort_is_bv (btor, is),
4503 "'index' is not a bit vector sort");
4504 BTOR_ABORT (!btor_sort_is_valid (btor, es),
4505 "'element' sort is not a valid sort");
4506 BTOR_ABORT (!btor_sort_is_bv (btor, es),
4507 "'element' is not a bit vector sort");
4508
4509 res = btor_sort_array (btor, is, es);
4510 inc_sort_ext_ref_counter (btor, res);
4511 BTOR_TRAPI_RETURN_SORT (res);
4512 #ifndef NDEBUG
4513 BTOR_CHKCLONE_RES_SORT (res, array_sort, index, element);
4514 #endif
4515 return BTOR_EXPORT_BOOLECTOR_SORT (res);
4516 }
4517
4518 BoolectorSort
boolector_copy_sort(Btor * btor,BoolectorSort sort)4519 boolector_copy_sort (Btor *btor, BoolectorSort sort)
4520 {
4521 BTOR_ABORT_ARG_NULL (btor);
4522 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, BTOR_IMPORT_BOOLECTOR_SORT (sort), btor);
4523
4524 BtorSortId s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4525 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4526 BtorSortId res = btor_sort_copy (btor, s);
4527 inc_sort_ext_ref_counter (btor, res);
4528 BTOR_TRAPI_RETURN_SORT (res);
4529 #ifndef NDEBUG
4530 BTOR_CHKCLONE_RES_SORT (res, copy_sort, sort);
4531 #endif
4532 return BTOR_EXPORT_BOOLECTOR_SORT (res);
4533 }
4534
4535 void
boolector_release_sort(Btor * btor,BoolectorSort sort)4536 boolector_release_sort (Btor *btor, BoolectorSort sort)
4537 {
4538 BTOR_ABORT_ARG_NULL (btor);
4539 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, BTOR_IMPORT_BOOLECTOR_SORT (sort), btor);
4540
4541 BtorSortId s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4542 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4543 dec_sort_ext_ref_counter (btor, s);
4544 btor_sort_release (btor, s);
4545 #ifndef NDEBUG
4546 BTOR_CHKCLONE_NORES (release_sort, sort);
4547 #endif
4548 }
4549
4550 bool
boolector_is_equal_sort(Btor * btor,BoolectorNode * n0,BoolectorNode * n1)4551 boolector_is_equal_sort (Btor *btor, BoolectorNode *n0, BoolectorNode *n1)
4552 {
4553 bool res;
4554 BtorNode *e0, *e1;
4555
4556 e0 = BTOR_IMPORT_BOOLECTOR_NODE (n0);
4557 e1 = BTOR_IMPORT_BOOLECTOR_NODE (n1);
4558 BTOR_ABORT_ARG_NULL (btor);
4559 BTOR_ABORT_ARG_NULL (e0);
4560 BTOR_ABORT_ARG_NULL (e1);
4561 BTOR_TRAPI_BINFUN (e0, e1);
4562 BTOR_ABORT_REFS_NOT_POS (e0);
4563 BTOR_ABORT_REFS_NOT_POS (e1);
4564 BTOR_ABORT_BTOR_MISMATCH (btor, e0);
4565 BTOR_ABORT_BTOR_MISMATCH (btor, e1);
4566 res = btor_node_get_sort_id (e0) == btor_node_get_sort_id (e1);
4567 BTOR_TRAPI_RETURN_BOOL (res);
4568 #ifndef NDEBUG
4569 BTOR_CHKCLONE_RES_BOOL (
4570 res, is_equal_sort, BTOR_CLONED_EXP (e0), BTOR_CLONED_EXP (e1));
4571 #endif
4572 return res;
4573 }
4574
4575 bool
boolector_is_array_sort(Btor * btor,BoolectorSort sort)4576 boolector_is_array_sort (Btor *btor, BoolectorSort sort)
4577 {
4578 bool res;
4579 BtorSortId s;
4580
4581 BTOR_ABORT_ARG_NULL (btor);
4582 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
4583 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4584
4585 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4586
4587 res = btor_sort_is_array (btor, s);
4588 BTOR_TRAPI_RETURN_BOOL (res);
4589 #ifndef NDEBUG
4590 BTOR_CHKCLONE_RES_BOOL (res, is_array_sort, sort);
4591 #endif
4592 return res;
4593 }
4594
4595 bool
boolector_is_bitvec_sort(Btor * btor,BoolectorSort sort)4596 boolector_is_bitvec_sort (Btor *btor, BoolectorSort sort)
4597 {
4598 bool res;
4599 BtorSortId s;
4600
4601 BTOR_ABORT_ARG_NULL (btor);
4602 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
4603 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4604
4605 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4606
4607 res = btor_sort_is_bv (btor, s);
4608 BTOR_TRAPI_RETURN_BOOL (res);
4609 #ifndef NDEBUG
4610 BTOR_CHKCLONE_RES_BOOL (res, is_bitvec_sort, sort);
4611 #endif
4612 return res;
4613 }
4614
4615 bool
boolector_is_fun_sort(Btor * btor,BoolectorSort sort)4616 boolector_is_fun_sort (Btor *btor, BoolectorSort sort)
4617 {
4618 bool res;
4619 BtorSortId s;
4620
4621 BTOR_ABORT_ARG_NULL (btor);
4622 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
4623 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4624
4625 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4626
4627 res = btor_sort_is_fun (btor, s);
4628 BTOR_TRAPI_RETURN_BOOL (res);
4629 #ifndef NDEBUG
4630 BTOR_CHKCLONE_RES_BOOL (res, is_fun_sort, sort);
4631 #endif
4632 return res;
4633 }
4634
4635 uint32_t
boolector_bitvec_sort_get_width(Btor * btor,BoolectorSort sort)4636 boolector_bitvec_sort_get_width (Btor *btor, BoolectorSort sort)
4637 {
4638 uint32_t res;
4639 BtorSortId s;
4640
4641 BTOR_ABORT_ARG_NULL (btor);
4642 BTOR_TRAPI (BTOR_TRAPI_SORT_FMT, sort, btor);
4643 s = BTOR_IMPORT_BOOLECTOR_SORT (sort);
4644
4645 BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
4646
4647 res = btor_sort_bv_get_width (btor, s);
4648 BTOR_TRAPI_RETURN_UINT (res);
4649 #ifndef NDEBUG
4650 BTOR_CHKCLONE_RES_UINT (res, bitvec_sort_get_width, sort);
4651 #endif
4652 return res;
4653 }
4654
4655 /*------------------------------------------------------------------------*/
4656
4657 /* Note: no need to trace parse function calls!! */
4658
4659 int32_t
boolector_parse(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status,bool * parsed_smt2)4660 boolector_parse (Btor *btor,
4661 FILE *infile,
4662 const char *infile_name,
4663 FILE *outfile,
4664 char **error_msg,
4665 int32_t *status,
4666 bool *parsed_smt2)
4667 {
4668 int32_t res;
4669
4670 BTOR_ABORT_ARG_NULL (btor);
4671 BTOR_ABORT_ARG_NULL (infile);
4672 BTOR_ABORT_ARG_NULL (infile_name);
4673 BTOR_ABORT_ARG_NULL (outfile);
4674 BTOR_ABORT_ARG_NULL (error_msg);
4675 BTOR_ABORT_ARG_NULL (status);
4676 BTOR_ABORT (BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
4677 "file parsing must be done before creating expressions");
4678 res = btor_parse (
4679 btor, infile, infile_name, outfile, error_msg, status, parsed_smt2);
4680 /* shadow clone can not shadow boolector_parse* (parser uses API calls only,
4681 * hence all API calls issued while parsing are already shadowed and the
4682 * shadow clone already maintains the parsed formula) */
4683 return res;
4684 }
4685
4686 int32_t
boolector_parse_btor(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)4687 boolector_parse_btor (Btor *btor,
4688 FILE *infile,
4689 const char *infile_name,
4690 FILE *outfile,
4691 char **error_msg,
4692 int32_t *status)
4693 {
4694 int32_t res;
4695
4696 BTOR_ABORT_ARG_NULL (btor);
4697 BTOR_ABORT_ARG_NULL (infile);
4698 BTOR_ABORT_ARG_NULL (infile_name);
4699 BTOR_ABORT_ARG_NULL (outfile);
4700 BTOR_ABORT_ARG_NULL (error_msg);
4701 BTOR_ABORT_ARG_NULL (status);
4702 BTOR_ABORT (BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
4703 "file parsing must be done before creating expressions");
4704 res = btor_parse_btor (btor, infile, infile_name, outfile, error_msg, status);
4705 /* shadow clone can not shadow boolector_parse* (parser uses API calls only,
4706 * hence all API calls issued while parsing are already shadowed and the
4707 * shadow clone already maintains the parsed formula) */
4708 return res;
4709 }
4710
4711 int32_t
boolector_parse_btor2(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)4712 boolector_parse_btor2 (Btor *btor,
4713 FILE *infile,
4714 const char *infile_name,
4715 FILE *outfile,
4716 char **error_msg,
4717 int32_t *status)
4718 {
4719 int32_t res;
4720
4721 BTOR_ABORT_ARG_NULL (btor);
4722 BTOR_ABORT_ARG_NULL (infile);
4723 BTOR_ABORT_ARG_NULL (infile_name);
4724 BTOR_ABORT_ARG_NULL (outfile);
4725 BTOR_ABORT_ARG_NULL (error_msg);
4726 BTOR_ABORT_ARG_NULL (status);
4727 BTOR_ABORT (BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
4728 "file parsing must be done before creating expressions");
4729 res = btor_parse_btor2 (btor, infile, infile_name, outfile, error_msg, status);
4730 /* shadow clone can not shadow boolector_parse* (parser uses API calls only,
4731 * hence all API calls issued while parsing are already shadowed and the
4732 * shadow clone already maintains the parsed formula) */
4733 return res;
4734 }
4735
4736 int32_t
boolector_parse_smt1(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)4737 boolector_parse_smt1 (Btor *btor,
4738 FILE *infile,
4739 const char *infile_name,
4740 FILE *outfile,
4741 char **error_msg,
4742 int32_t *status)
4743 {
4744 int32_t res;
4745
4746 BTOR_ABORT_ARG_NULL (btor);
4747 BTOR_ABORT_ARG_NULL (infile);
4748 BTOR_ABORT_ARG_NULL (infile_name);
4749 BTOR_ABORT_ARG_NULL (outfile);
4750 BTOR_ABORT_ARG_NULL (error_msg);
4751 BTOR_ABORT_ARG_NULL (status);
4752 BTOR_ABORT (BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
4753 "file parsing must be done before creating expressions");
4754 res = btor_parse_smt1 (btor, infile, infile_name, outfile, error_msg, status);
4755 /* shadow clone can not shadow boolector_parse* (parser uses API calls only,
4756 * hence all API calls issued while parsing are already shadowed and the
4757 * shadow clone already maintains the parsed formula) */
4758 return res;
4759 }
4760
4761 int32_t
boolector_parse_smt2(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)4762 boolector_parse_smt2 (Btor *btor,
4763 FILE *infile,
4764 const char *infile_name,
4765 FILE *outfile,
4766 char **error_msg,
4767 int32_t *status)
4768 {
4769 int32_t res;
4770
4771 BTOR_ABORT_ARG_NULL (btor);
4772 BTOR_ABORT_ARG_NULL (infile);
4773 BTOR_ABORT_ARG_NULL (infile_name);
4774 BTOR_ABORT_ARG_NULL (outfile);
4775 BTOR_ABORT_ARG_NULL (error_msg);
4776 BTOR_ABORT_ARG_NULL (status);
4777 BTOR_ABORT (BTOR_COUNT_STACK (btor->nodes_id_table) > 2,
4778 "file parsing must be done before creating expressions");
4779 res = btor_parse_smt2 (btor, infile, infile_name, outfile, error_msg, status);
4780 /* shadow clone can not shadow boolector_parse* (parser uses API calls only,
4781 * hence all API calls issued while parsing are already shadowed and the
4782 * shadow clone already maintains the parsed formula) */
4783 return res;
4784 }
4785
4786 /*------------------------------------------------------------------------*/
4787
4788 void
boolector_dump_btor_node(Btor * btor,FILE * file,BoolectorNode * node)4789 boolector_dump_btor_node (Btor *btor, FILE *file, BoolectorNode *node)
4790 {
4791 BtorNode *exp;
4792
4793 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
4794 BTOR_TRAPI_UNFUN (exp);
4795 BTOR_ABORT_ARG_NULL (btor);
4796 BTOR_ABORT_ARG_NULL (file);
4797 BTOR_ABORT_ARG_NULL (exp);
4798 BTOR_ABORT_REFS_NOT_POS (exp);
4799 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
4800 btor_dumpbtor_dump_node (btor, file, btor_simplify_exp (btor, exp));
4801 #ifndef NDEBUG
4802 BTOR_CHKCLONE_NORES (dump_btor_node, stdout, BTOR_CLONED_EXP (exp));
4803 #endif
4804 }
4805
4806 void
boolector_dump_btor(Btor * btor,FILE * file)4807 boolector_dump_btor (Btor *btor, FILE *file)
4808 {
4809 BTOR_TRAPI ("");
4810 BTOR_ABORT_ARG_NULL (btor);
4811 BTOR_ABORT_ARG_NULL (file);
4812 BTOR_ABORT (!btor_dumpbtor_can_be_dumped (btor),
4813 "formula cannot be dumped in BTOR format as it does "
4814 "not support uninterpreted functions yet.");
4815 BTOR_WARN (btor->assumptions->count > 0,
4816 "dumping in incremental mode only captures the current state "
4817 "of the input formula without assumptions");
4818 btor_dumpbtor_dump (btor, file, 1);
4819 #ifndef NDEBUG
4820 BTOR_CHKCLONE_NORES (dump_btor, stdout);
4821 #endif
4822 }
4823
4824 void
boolector_dump_smt2_node(Btor * btor,FILE * file,BoolectorNode * node)4825 boolector_dump_smt2_node (Btor *btor, FILE *file, BoolectorNode *node)
4826 {
4827 BtorNode *exp;
4828
4829 exp = BTOR_IMPORT_BOOLECTOR_NODE (node);
4830 BTOR_TRAPI_UNFUN (exp);
4831 BTOR_ABORT_ARG_NULL (btor);
4832 BTOR_ABORT_ARG_NULL (file);
4833 BTOR_ABORT_ARG_NULL (exp);
4834 BTOR_ABORT_REFS_NOT_POS (exp);
4835 BTOR_ABORT_BTOR_MISMATCH (btor, exp);
4836 btor_dumpsmt_dump_node (btor, file, btor_simplify_exp (btor, exp), 0);
4837 #ifndef NDEBUG
4838 BTOR_CHKCLONE_NORES (dump_smt2_node, stdout, BTOR_CLONED_EXP (exp));
4839 #endif
4840 }
4841
4842 void
boolector_dump_smt2(Btor * btor,FILE * file)4843 boolector_dump_smt2 (Btor *btor, FILE *file)
4844 {
4845 BTOR_TRAPI ("");
4846 BTOR_ABORT_ARG_NULL (btor);
4847 BTOR_ABORT_ARG_NULL (file);
4848 BTOR_WARN (btor->assumptions->count > 0,
4849 "dumping in incremental mode only captures the current state "
4850 "of the input formula without assumptions");
4851 btor_dumpsmt_dump (btor, file);
4852 #ifndef NDEBUG
4853 BTOR_CHKCLONE_NORES (dump_smt2, stdout);
4854 #endif
4855 }
4856
4857 void
boolector_dump_aiger_ascii(Btor * btor,FILE * file,bool merge_roots)4858 boolector_dump_aiger_ascii (Btor *btor, FILE *file, bool merge_roots)
4859 {
4860 BTOR_TRAPI ("%d", merge_roots);
4861 BTOR_ABORT_ARG_NULL (btor);
4862 BTOR_ABORT_ARG_NULL (file);
4863 BTOR_ABORT (btor->lambdas->count > 0 || btor->ufs->count > 0,
4864 "dumping to ASCII AIGER is supported for QF_BV only");
4865 BTOR_WARN (btor->assumptions->count > 0,
4866 "dumping in incremental mode only captures the current state "
4867 "of the input formula without assumptions");
4868 btor_dumpaig_dump (btor, false, file, merge_roots);
4869 #ifndef NDEBUG
4870 BTOR_CHKCLONE_NORES (dump_aiger_ascii, stdout, merge_roots);
4871 #endif
4872 }
4873
4874 void
boolector_dump_aiger_binary(Btor * btor,FILE * file,bool merge_roots)4875 boolector_dump_aiger_binary (Btor *btor, FILE *file, bool merge_roots)
4876 {
4877 BTOR_TRAPI ("%d", merge_roots);
4878 BTOR_ABORT_ARG_NULL (btor);
4879 BTOR_ABORT_ARG_NULL (file);
4880 BTOR_ABORT (btor->lambdas->count > 0 || btor->ufs->count > 0,
4881 "dumping to binary AIGER is supported for QF_BV only");
4882 BTOR_WARN (btor->assumptions->count > 0,
4883 "dumping in incremental mode only captures the current state "
4884 "of the input formula without assumptions");
4885 btor_dumpaig_dump (btor, true, file, merge_roots);
4886 #ifndef NDEBUG
4887 BTOR_CHKCLONE_NORES (dump_aiger_binary, stdout, merge_roots);
4888 #endif
4889 }
4890
4891 /*------------------------------------------------------------------------*/
4892
4893 const char *
boolector_copyright(Btor * btor)4894 boolector_copyright (Btor *btor)
4895 {
4896 /* do not trace, not necessary */
4897 BTOR_ABORT_ARG_NULL (btor);
4898 return "This software is\n"
4899 "Copyright (c) 2007-2009 Robert Brummayer\n"
4900 "Copyright (c) 2007-2018 Armin Biere\n"
4901 "Copyright (c) 2012-2021 Aina Niemetz, Mathias Preiner\n"
4902 #ifdef BTOR_USE_LINGELING
4903 "\n"
4904 "This software is linked against Lingeling\n"
4905 "Copyright (c) 2010-2018 Armin Biere\n"
4906 #endif
4907 #ifdef BTOR_USE_PICOSAT
4908 "\n"
4909 "This software is linked against PicoSAT\n"
4910 "Copyright (c) 2006-2016 Armin Biere\n"
4911 #endif
4912 #ifdef BTOR_USE_MINISAT
4913 "\n"
4914 "This software is linked against MiniSAT\n"
4915 "Copyright (c) 2003-2013, Niklas Een, Niklas Sorensson\n"
4916 #endif
4917 #ifdef BTOR_USE_CADICAL
4918 "\n"
4919 "This software is linked against CaDiCaL\n"
4920 "Copyright (c) 2016-2020 Armin Biere\n"
4921 #endif
4922 #ifdef BTOR_USE_CMS
4923 "\n"
4924 "This software is linked against CryptoMiniSat\n"
4925 "Copyright (c) 2009-2020 Mate Soos\n"
4926 #endif
4927 "";
4928 }
4929
4930 const char *
boolector_version(Btor * btor)4931 boolector_version (Btor *btor)
4932 {
4933 /* do not trace, not necessary */
4934 BTOR_ABORT_ARG_NULL (btor);
4935 return btor_version (btor);
4936 }
4937
4938 const char *
boolector_git_id(Btor * btor)4939 boolector_git_id (Btor *btor)
4940 {
4941 /* do not trace, not necessary */
4942 BTOR_ABORT_ARG_NULL (btor);
4943 return btor_git_id (btor);
4944 }
4945