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 #ifndef BOOLECTOR_H_INCLUDED 9 #define BOOLECTOR_H_INCLUDED 10 11 /*------------------------------------------------------------------------*/ 12 13 #include <stdbool.h> 14 #include <stdint.h> 15 #include <stdio.h> 16 #include "btortypes.h" 17 18 #if __cplusplus 19 extern "C" { 20 #endif 21 /*------------------------------------------------------------------------*/ 22 23 /*! 24 Preprocessor constant representing status ``unknown``. 25 26 .. seealso:: 27 boolector_sat, boolector_limited_sat, boolector_simplify 28 */ 29 #define BOOLECTOR_UNKNOWN BTOR_RESULT_UNKNOWN 30 /*! 31 Preprocessor constant representing status ``satisfiable``. 32 33 .. seealso:: 34 boolector_sat, boolector_limited_sat, boolector_simplify 35 */ 36 #define BOOLECTOR_SAT BTOR_RESULT_SAT 37 /*! 38 Preprocessor constant representing status ``unsatisfiable``. 39 40 .. seealso:: 41 boolector_sat, boolector_limited_sat, boolector_simplify 42 */ 43 #define BOOLECTOR_UNSAT BTOR_RESULT_UNSAT 44 /*! 45 Preprocessor constant representing status ``parse error``. 46 47 .. seealso:: 48 boolector_parse 49 */ 50 #define BOOLECTOR_PARSE_ERROR 1 51 /*! 52 Preprocessor constant representing status ``parse unknown``. 53 54 .. seealso:: 55 boolector_parse 56 */ 57 #define BOOLECTOR_PARSE_UNKNOWN 2 58 59 /*------------------------------------------------------------------------*/ 60 61 /*! 62 Create a new instance of Boolector. 63 64 :return: New Boolector instance. 65 */ 66 Btor *boolector_new (void); 67 68 /*! 69 Clone an instance of Boolector. 70 71 The resulting Boolector instance is an exact copy of given Boolector instance 72 ``btor``. Consequently, in a clone and its parent, nodes with the same id 73 correspond to each other. Use boolector_match_node to match corresponding 74 nodes. 75 76 :param btor: Original Boolector instance. 77 :return: The exact (but disjunct) copy of the Boolector instance ``btor``. 78 79 .. note:: 80 If Lingeling is used as SAT solver, Boolector can be cloned at any time, 81 since Lingeling also supports cloning. However, with all other SAT solver 82 that do not support cloning, Boolector can only be cloned prior to the 83 first boolector_sat call. 84 */ 85 Btor *boolector_clone (Btor *btor); 86 87 /*! 88 Delete a boolector instance and free its resources. 89 90 :param btor: Boolector instance. 91 92 .. note:: 93 Expressions that have not been released properly will not be 94 deleted from memory. Use boolector_get_refs to debug reference 95 counting. You can also set option ``auto_cleanup`` via 96 boolector_set_opt in order to do the cleanup automatically. 97 */ 98 void boolector_delete (Btor *btor); 99 100 /*! 101 Set a termination callback. 102 103 :param btor: Boolector instance. 104 :param fun: The termination callback function. 105 :param state: The argument to the termination callback function. 106 107 .. seealso:: 108 boolector_terminate 109 */ 110 void boolector_set_term (Btor *btor, int32_t (*fun) (void *), void *state); 111 112 /*! 113 Determine if a given Boolector instance has been terminated (and or 114 terminate Boolector) via the previously configured termination callback 115 function. 116 117 :param btor: Boolector instance. 118 :return: True if Boolector is terminated, and false otherwise. 119 120 .. seealso:: 121 boolector_set_term 122 */ 123 int32_t boolector_terminate (Btor *btor); 124 125 /*! 126 Set an abort callback that is called instead of exit on abort conditions. 127 128 It is recommended to set this function prior to creating Boolector instances. 129 130 .. note:: 131 This function is not thread safe (the function pointer is maintained as 132 a global variable). It you use threading, make sure to set the abort 133 function prior to creating threads. 134 135 :param fun: The abort callback function. 136 :param msg: The abort error message. 137 */ 138 void boolector_set_abort (void (*fun) (const char* msg)); 139 140 /*! 141 Set a verbosity message prefix. 142 143 :param btor: Boolector instance. 144 :param prefix: Prefix string. 145 */ 146 void boolector_set_msg_prefix (Btor *btor, const char *prefix); 147 148 /*! 149 Get the number of external references to the boolector library. 150 151 Internally, Boolector manages an expression DAG with reference counting. 152 Use boolector_release to properly release an expression. Before you 153 finally call boolector_delete, boolector_get_refs should return 0. 154 155 :param btor: Boolector instance. 156 :return: Number of external references owned by the user. 157 */ 158 uint32_t boolector_get_refs (Btor *btor); 159 160 /*! 161 Reset time statistics. 162 163 :param btor: Boolector instance. 164 */ 165 void boolector_reset_time (Btor *btor); 166 167 /*! 168 Reset statistics (time statistics not included). 169 170 :param btor: Boolector instance. 171 */ 172 void boolector_reset_stats (Btor *btor); 173 174 /*! 175 Print statistics. 176 177 :param btor: Boolector instance. 178 */ 179 void boolector_print_stats (Btor *btor); 180 181 /*! 182 Set the output API trace file and enable API tracing. 183 184 :param btor: Boolector instance. 185 :param apitrace: Output file. 186 187 .. note:: 188 The API trace output file can also be set via the environment variable 189 BTORAPITRACE=<filename>. 190 */ 191 void boolector_set_trapi (Btor *btor, FILE *apitrace); 192 193 /*! 194 Return API trace file. 195 196 :param btor: Boolector instance. 197 :return: API trace output file. 198 */ 199 FILE *boolector_get_trapi (Btor *btor); 200 201 /*------------------------------------------------------------------------*/ 202 203 /*! 204 Push new context levels. 205 206 :param btor: Boolector instance. 207 :param level: Number of context levels to create (must be a least 1). 208 209 .. note:: 210 Assumptions added via boolector_assume are not affected by context level 211 changes and are only valid until the next boolector_sat call no matter at 212 what level they were assumed. 213 214 .. seealso:: 215 boolector_assume 216 */ 217 void boolector_push (Btor *btor, uint32_t level); 218 219 /*! 220 Pop context levels. 221 222 :param btor: Boolector instance. 223 :param level: Number of context levels to pop (must be at least 1). 224 225 .. note:: 226 Assumptions added via boolector_assume are not affected by context level 227 changes and are only valid until the next boolector_sat call no matter at 228 what level they were assumed. 229 230 .. seealso:: 231 boolector_assume 232 */ 233 void boolector_pop (Btor *btor, uint32_t level); 234 235 /*------------------------------------------------------------------------*/ 236 237 /*! 238 Add a constraint. 239 240 Use this function to assert ``node``. Added constraints can not be deleted 241 anymore. After ``node`` has been asserted, it can be safely released by 242 boolector_release. 243 244 :param btor: Boolector instance. 245 :param node: Bit-vector expression with bit width one. 246 */ 247 void boolector_assert (Btor *btor, BoolectorNode *node); 248 249 /*! 250 Add an assumption. 251 252 Use this function to assume ``node``. You must enable Boolector's 253 incremental usage via boolector_set_opt before you can add assumptions. In 254 contrast to assertions added via boolector_assert, assumptions are discarded 255 after each call to boolector_sat. Assumptions and assertions are logically 256 combined via Boolean ``and``. Assumption handling in Boolector is analogous 257 to assumptions in MiniSAT. 258 259 :param btor: Boolector instance. 260 :param node: Bit-vector expression with bit width one. 261 */ 262 void boolector_assume (Btor *btor, BoolectorNode *node); 263 264 /*! 265 Determine if assumption ``node`` is a failed assumption. 266 267 Failed assumptions are those assumptions, that force an input formula 268 to become unsatisfiable. Failed assumptions handling in Boolector is 269 analogous to failed assumptions in MiniSAT. 270 271 :param btor: Boolector instance. 272 :param node: Bit-vector expression with bit width one. 273 :return: true if assumption is failed, and false otherwise. 274 275 .. seealso:: 276 boolector_assume 277 */ 278 bool boolector_failed (Btor *btor, BoolectorNode *node); 279 280 /*! 281 Get all failed assumptions (see boolector_failed). 282 283 Returns the list of failed assumptions in a zero-terminated array of 284 pointers to BoolectorNodes. The nodes in this array do not have to be 285 released. The memory allocated for this array is maintained by Boolector, 286 it does not have to be freed. 287 288 :param btor: Boolector instance. 289 :returns: A pointer to an array of pointers to BoolectorNodes. 290 291 .. seealso:: 292 boolector_assume 293 boolector_failed 294 */ 295 BoolectorNode **boolector_get_failed_assumptions (Btor *btor); 296 297 /*! 298 Add all assumptions as assertions. 299 300 :param btor: Boolector instance. 301 302 .. seealso:: 303 boolector_assume 304 */ 305 void boolector_fixate_assumptions (Btor *btor); 306 307 /*! 308 Resets all added assumptions. 309 310 :param btor: Boolector instance. 311 312 .. seealso:: 313 boolector_assume 314 */ 315 void boolector_reset_assumptions (Btor *btor); 316 317 /*------------------------------------------------------------------------*/ 318 319 /*! 320 Solve an input formula. 321 322 An input formula is defined by constraints added via boolector_assert. 323 You can guide the search for a solution to an input formula by making 324 assumptions via boolector_assume. 325 Note that assertions and assumptions are combined by boolean ``and``. 326 327 If you want to call this function multiple times, you must enable 328 Boolector's incremental usage mode via boolector_set_opt 329 before. Otherwise, this function may only be called once. 330 331 :param btor: Boolector instance. 332 :return: BOOLECTOR_SAT if the instance is satisfiable and BOOLECTOR_UNSAT if 333 the instance is unsatisfiable. 334 335 .. seealso:: 336 boolector_bv_assignment, boolector_array_assignment 337 */ 338 int32_t boolector_sat (Btor *btor); 339 340 /*! 341 Solve an input formula and limit the search by the number of lemmas 342 generated and the number of conflicts encountered by the underlying 343 SAT solver. 344 345 An input formula is defined by constraints added via boolector_assert. 346 You can guide the search for a solution to an input formula by making 347 assumptions via boolector_assume. 348 349 If you want to call this function multiple times then you must enable 350 Boolector's incremental usage mode via boolector_set_opt before. 351 Otherwise, this function can only be called once. 352 353 :param btor: Boolector instance. 354 :param lod_limit: Lemma limit (-1 unlimited). 355 :param sat_limit: Conflict limit for SAT solver (-1 unlimited). 356 :return: BOOLECTOR_SAT if the input formula is satisfiable (under possibly 357 given assumptions), BOOLECTOR_UNSAT if the instance is 358 unsatisfiable, and BOOLECTOR_UNKNOWN if the instance could not be 359 solved within given limits. 360 361 .. seealso:: 362 boolector_bv_assignment, boolector_array_assignment 363 */ 364 int32_t boolector_limited_sat (Btor *btor, 365 int32_t lod_limit, 366 int32_t sat_limit); 367 368 /*------------------------------------------------------------------------*/ 369 370 /*! 371 Simplify current input formula. 372 373 :param btor: Boolector instance. 374 :return: BOOLECTOR_SAT if the input formula was simplified to true, 375 BOOLECTOR_UNSAT if it was simplified to false, and BOOLECTOR_UNKNOWN 376 otherwise. 377 378 .. note:: 379 Each call to boolector_sat simplifies the input formula as a preprocessing 380 step. 381 */ 382 int32_t boolector_simplify (Btor *btor); 383 384 /*------------------------------------------------------------------------*/ 385 386 /*! 387 Set the SAT solver to use. 388 389 Currently, we support ``Lingeling``, ``PicoSAT``, and ``MiniSAT`` as string 390 value of ``solver`` (case insensitive). This is however 391 only possible if the corresponding solvers were enabled at compile time. 392 Call this function after boolector_new. 393 394 :param btor: Boolector instance 395 :param solver: Solver identifier string. 396 */ 397 void boolector_set_sat_solver (Btor *btor, const char *solver); 398 399 /*------------------------------------------------------------------------*/ 400 401 /*! 402 Set option. 403 404 E.g., given a Boolector instance ``btor``, model generation is enabled via 405 406 .. code-block:: c 407 408 boolector_set_opt_noref (btor, BTOR_OPT_MODEL_GEN, 1); 409 410 .. include:: cboolector_options.rst 411 412 .. toctree:: 413 :hidden: 414 415 cboolector_options.rst 416 417 :param btor: Boolector instance. 418 :param opt: Option opt. 419 :param val: Option value. 420 */ 421 void boolector_set_opt (Btor *btor, BtorOption opt, uint32_t val); 422 423 /*! 424 Get the current value of an option. 425 426 :param btor: Btor instance. 427 :param opt: Option opt. 428 :return: Current value of ``opt``. 429 */ 430 uint32_t boolector_get_opt (Btor *btor, BtorOption opt); 431 432 /*! 433 Get the min value of an option. 434 435 :param btor: Btor instance. 436 :param opt: Option opt. 437 :return: Min value of ``opt``. 438 */ 439 uint32_t boolector_get_opt_min (Btor *btor, BtorOption opt); 440 441 /*! 442 Get the max value of an option. 443 444 :param btor: Btor instance. 445 :param opt: Option opt. 446 :return: Max value of ``opt``. 447 */ 448 uint32_t boolector_get_opt_max (Btor *btor, BtorOption opt); 449 450 /*! 451 Get the default value of an option. 452 453 :param btor: Btor instance. 454 :param opt: Option opt. 455 :return: Default value of ``opt``. 456 */ 457 uint32_t boolector_get_opt_dflt (Btor *btor, BtorOption opt); 458 459 /*! 460 Get the long name of an option. 461 462 :param btor: Btor instance. 463 :param opt: Option opt. 464 :return: Short opt of ``opt``. 465 */ 466 const char *boolector_get_opt_lng (Btor *btor, BtorOption opt); 467 468 /*! 469 Get the short name of an option. 470 471 :param btor: Btor instance. 472 :param opt: Option opt. 473 :return: Short opt of ``opt``. 474 */ 475 const char *boolector_get_opt_shrt (Btor *btor, BtorOption opt); 476 477 /*! 478 Get the description of an option. 479 480 :param btor: Btor instance. 481 :param opt: Option opt. 482 :return: Description of ``opt``. 483 */ 484 const char *boolector_get_opt_desc (Btor *btor, BtorOption opt); 485 486 /*! 487 Check if Boolector has a given option. 488 489 Given a Boolector instance ``btor``, you can use this in combination 490 with boolector_has_opt and boolector_next_opt in order to iterate over 491 Boolector options as follows: 492 493 .. code-block:: c 494 495 for (s = boolector_first_opt_noref (btor); 496 boolector_has_opt_noref (btor, s); 497 s = boolector_next_opt_noref (btor, s)) 498 {...} 499 500 :param btor: Btor instance. 501 :param opt: Option opt. 502 :return: True if Boolector has the given option, and false otherwise. 503 */ 504 bool boolector_has_opt (Btor *Btor, BtorOption opt); 505 506 /*! 507 Get the opt of the first option in Boolector's option list. 508 509 Given a Boolector instance ``btor``, you can use this in combination 510 with boolector_has_opt and boolector_next_opt in order to iterate over 511 Boolector options as follows: 512 513 .. code-block:: c 514 515 for (s = boolector_first_opt_noref (btor); 516 boolector_has_opt_noref (btor, s); 517 s = boolector_next_opt_noref (btor, s)) 518 {...} 519 520 :param btor: Btor instance. 521 :return: opt of the first option in Boolector's option list. 522 */ 523 BtorOption boolector_first_opt (Btor *btor); 524 525 /*! 526 Given current option ``opt``, get the opt of the next option in Boolector's 527 option list. 528 529 Given a Boolector instance ``btor``, you can use this in combination 530 with boolector_has_opt and boolector_next_opt in order to iterate over 531 Boolector options as follows: 532 533 .. code-block:: c 534 535 for (s = boolector_first_opt_noref (btor); 536 boolector_has_opt_noref (btor, s); 537 s = boolector_next_opt_noref (btor, s)) 538 {...} 539 540 :param btor: Btor instance. 541 :param opt: Option opt. 542 :return: opt of the next option in Boolector's option list, or 0 if no such 543 next option does exist. 544 */ 545 BtorOption boolector_next_opt (Btor *btor, BtorOption opt); 546 547 /*------------------------------------------------------------------------*/ 548 549 /*! 550 Copy expression (increments reference counter). 551 552 :param btor: Boolector instance. 553 :param node: Boolector node to be copied. 554 :return: Node ``node`` with reference counter incremented. 555 */ 556 BoolectorNode *boolector_copy (Btor *btor, BoolectorNode *node); 557 558 /*! 559 Release expression (decrements reference counter). 560 561 :param btor: Boolector instance. 562 :param node: Boolector node to be released. 563 */ 564 void boolector_release (Btor *btor, BoolectorNode *node); 565 566 /*! 567 Release all expressions and sorts. 568 569 :param btor: Boolector instance. 570 571 .. seealso:: 572 boolector_release, boolector_release_sort 573 */ 574 void boolector_release_all (Btor *btor); 575 576 /*------------------------------------------------------------------------*/ 577 578 /*! 579 Create constant true. This is represented by the bit-vector constant one 580 with bit width one. 581 582 :param btor: Boolector instance. 583 :return: Bit-vector constant one with bit width one. 584 */ 585 BoolectorNode *boolector_true (Btor *btor); 586 587 /*! 588 Create bit-vector constant zero with bit width one. 589 590 :param btor: Boolector instance. 591 :return: Bit-vector constant zero with bit width one. 592 */ 593 BoolectorNode *boolector_false (Btor *btor); 594 595 /*! 596 Create boolean implication. 597 598 The parameters ``n0`` and ``n1`` must have bit width one. 599 600 :param btor: Boolector instance. 601 :param n0: Bit-vector node representing the premise. 602 :param n1: Bit-vector node representing the conclusion. 603 :return: Implication n0 => n1 with bit width one. 604 */ 605 BoolectorNode *boolector_implies (Btor *btor, 606 BoolectorNode *n0, 607 BoolectorNode *n1); 608 609 /*! 610 Create Boolean equivalence. 611 612 The parameters ``n0`` and ``n1`` must have bit width one. 613 614 :param btor: Boolector instance. 615 :param n0: First bit-vector operand. 616 :param n1: Second bit-vector operand. 617 :return: Equivalence n0 <=> n1 with bit width one. 618 */ 619 BoolectorNode *boolector_iff (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 620 621 /*------------------------------------------------------------------------*/ 622 623 /*! 624 Create bit-vector or array equality. 625 626 Both operands are either bit-vectors with the same bit width or arrays 627 of the same type. 628 629 :param btor: Boolector instance. 630 :param n0: First operand. 631 :param n1: Second operand. 632 :return: Bit-vector with bit width one. 633 */ 634 BoolectorNode *boolector_eq (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 635 636 /*! 637 Create bit-vector or array inequality. 638 639 Both operands are either bit-vectors with the same bit width or arrays 640 of the same type. 641 642 :param btor: Boolector instance. 643 :param n0: First operand. 644 :param n1: Second operand. 645 :return: Bit-vector with bit width one. 646 */ 647 BoolectorNode *boolector_ne (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 648 649 /*------------------------------------------------------------------------*/ 650 651 /*! 652 Determine if given node is a bit-vector constant representing zero. 653 654 :param btor: Boolector instance. 655 :param node: Boolector node. 656 :return: True if ``node`` is a bit-vector constant representing zero, and 657 false otherwise. 658 */ 659 bool boolector_is_bv_const_zero (Btor *btor, BoolectorNode *node); 660 661 /*! 662 Determine if given node is a bit-vector constant representing one. 663 664 :param btor: Boolector instance. 665 :param node: Boolector node. 666 :return: True if ``node`` is a bit-vector constant representing one, and 667 false otherwise. 668 */ 669 bool boolector_is_bv_const_one (Btor *btor, BoolectorNode *node); 670 671 /*! 672 Determine if given node is a bit-vector constant representing the maximum 673 unsigned value (all ones).. 674 675 :param btor: Boolector instance. 676 :param node: Boolector node. 677 :return: True if ``node`` is a bit-vector constant with all ones, and false 678 otherwise. 679 */ 680 bool boolector_is_bv_const_ones (Btor *btor, BoolectorNode *node); 681 682 /*! 683 Determine if given node is a bit-vector constant representing the maximum 684 signed value (01...1). 685 686 :param btor: Boolector instance. 687 :param node: Boolector node. 688 :return: True if ``node`` is a bit-vector constant representing the maximum 689 signed value, and false otherwise. 690 */ 691 bool boolector_is_bv_const_max_signed (Btor *btor, BoolectorNode *node); 692 693 /*! 694 Determine if given node is a bit-vector constant representing the minimum 695 signed value (10...0). 696 697 :param btor: Boolector instance. 698 :param node: Boolector node. 699 :return: True if ``node`` is a bit-vector constant representing the minimum 700 signed value, and false otherwise. 701 */ 702 bool boolector_is_bv_const_min_signed (Btor *btor, BoolectorNode *node); 703 704 /*------------------------------------------------------------------------*/ 705 706 /*! 707 Create bit-vector constant representing the bit-vector ``bits``. 708 709 :param btor: Boolector instance. 710 :param bits: Non-empty and terminated string consisting of zeroes and/or ones 711 representing the bit-vector constant specified by ``bits``. 712 :return: Bit-vector constant with bit width ``strlen (bits)``. 713 */ 714 BoolectorNode *boolector_const (Btor *btor, const char *bits); 715 716 /*! 717 Create bit-vector constant representing the decimal number ``str``. 718 719 :param btor: Boolector instance. 720 :param sort: Bit-vector sort of 'str'. 721 :param str: Non-empty and terminated string representing a negative or 722 postive decimal number. 723 :return: Bit-vector constant with sort ``sort``. 724 */ 725 BoolectorNode *boolector_constd (Btor *btor, 726 BoolectorSort sort, 727 const char *str); 728 729 /*! 730 Create bit-vector constant representing the hexadecimal number ``str``. 731 732 :param btor: Boolector instance. 733 :param sort: Bit-vector sort of 'str'. 734 :param str: Non-empty and terminated string representing a hexadecimal 735 number. 736 :return: Bit-vector constant with sort ``sort``. 737 */ 738 BoolectorNode *boolector_consth (Btor *btor, 739 BoolectorSort sort, 740 const char *str); 741 742 /*! 743 Create bit-vector constant zero of sort ``sort``. 744 745 :param btor: Boolector instance. 746 :param sort: Sort of bit-vector constant. 747 :return: Bit-vector constant zero of sort ``sort``. 748 */ 749 BoolectorNode *boolector_zero (Btor *btor, BoolectorSort sort); 750 751 /*! 752 Create bit-vector constant of sort ``sort``, where each bit is set to one. 753 754 :param btor: Boolector instance. 755 :param sort: Sort of constant. 756 :return: Bit-vector constant -1 of sort ``sort``. 757 */ 758 BoolectorNode *boolector_ones (Btor *btor, BoolectorSort sort); 759 760 /*! 761 Create bit-vector constant one of sort ``sort``. 762 763 :param btor: Boolector instance. 764 :param sort: Sort of constant. 765 :return: Bit-vector constant one of sort ``sort``. 766 */ 767 BoolectorNode *boolector_one (Btor *btor, BoolectorSort sort); 768 769 /*! 770 Create bit-vector minimum signed value constant of sort ``sort``. 771 772 :param btor: Boolector instance. 773 :param sort: Sort of constant. 774 :return: Bit-vector constant representing the minimum signed value 775 of sort ``sort``. 776 */ 777 BoolectorNode *boolector_min_signed (Btor *btor, BoolectorSort sort); 778 779 /*! 780 Create bit-vector maximum signed value constant of sort ``sort``. 781 782 :param btor: Boolector instance. 783 :param sort: Sort of constant. 784 :return: Bit-vector constant representing the minimum signed value 785 of sort ``sort``. 786 */ 787 BoolectorNode *boolector_max_signed (Btor *btor, BoolectorSort sort); 788 789 /*! 790 Create bit-vector constant representing the unsigned integer ``u`` of sort 791 ``sort``. 792 793 The constant is obtained by either truncating bits or by 794 unsigned extension (padding with zeroes). 795 796 :param btor: Boolector instance. 797 :param u: Unsigned integer value. 798 :param sort: Sort of constant. 799 :return: Bit-vector constant of sort ``sort``. 800 */ 801 BoolectorNode *boolector_unsigned_int (Btor *btor, 802 uint32_t u, 803 BoolectorSort sort); 804 805 /*! 806 Create bit-vector constant representing the signed integer ``i`` of sort 807 ``sort``. 808 809 The constant is obtained by either truncating bits or by 810 signed extension (padding with ones). 811 812 :param btor: Boolector instance. 813 :param i: Signed integer value. 814 :param sort: Sort of constant. 815 :return: Bit-vector constant of sort ``sort``. 816 */ 817 BoolectorNode *boolector_int (Btor *btor, int32_t i, BoolectorSort sort); 818 819 /*------------------------------------------------------------------------*/ 820 821 /*! 822 Create a bit-vector variable of sort ``sort`` and with symbol ``symbol``. 823 824 A variable's symbol is used as a simple means of identification, either when 825 printing a model via boolector_print_model, or generating file dumps via 826 boolector_dump_btor and boolector_dump_smt2. A symbol 827 must be unique but may be NULL in case that no symbol should be assigned. 828 829 :param btor: Boolector instance. 830 :param sort: Variable sort. 831 :param symbol: Name of variable. 832 :return: Bit-vector variable of sort ``sort`` and with symbol ``symbol``. 833 834 .. note:: 835 In contrast to composite expressions, which are maintained uniquely 836 w.r.t. to their kind, inputs (and consequently, bit width), variables are 837 not. Hence, each call to this function returns a fresh bit-vector variable. 838 */ 839 BoolectorNode *boolector_var (Btor *btor, 840 BoolectorSort sort, 841 const char *symbol); 842 843 /*! 844 Create a one-dimensional bit-vector array with sort ``sort``. 845 846 An array variable's symbol is used as a simple means of identification, 847 either when printing a model via boolector_print_model, or generating file 848 dumps via boolector_dump_btor and boolector_dump_smt2. 849 A symbol must be unique but may be NULL in case that no symbol should be 850 assigned. 851 852 :param btor: Boolector instance. 853 :param sort: Array sort which maps bit-vectors to bit-vectors. 854 :param symbol: Name of array variable. 855 :return: Bit-vector array of sort ``sort`` and with symbol ``symbol``. 856 857 .. note:: 858 In contrast to composite expressions, which are maintained uniquely w.r.t. 859 to their kind, inputs (and consequently, bit width), array variables are 860 not. Hence, each call to boolector_array with the same arguments will 861 return a fresh array variable. 862 */ 863 BoolectorNode *boolector_array (Btor *btor, 864 BoolectorSort sort, 865 const char *symbol); 866 867 /*! 868 Create a one-dimensional constant bit-vector array with sort ``sort`` 869 initialized with value ``value``. 870 871 :param btor: Boolector instance. 872 :param sort: Array sort which maps bit-vectors to bit-vectors. 873 :param value: Value to initialize array. 874 :return: Constant bit-vector array of sort ``sort``. 875 876 .. seealso:: 877 boolector_array 878 */ 879 BoolectorNode *boolector_const_array (Btor *btor, 880 BoolectorSort sort, 881 BoolectorNode *value); 882 883 /*! 884 Create an uninterpreted function with sort ``sort`` and with symbol 885 ``symbol``. 886 ``btor`` Boolector instance. 887 888 An uninterpreted function's symbol is used as a simple means of 889 identification, either when printing a model via boolector_print_model, or 890 generating file dumps via boolector_dump_btor and 891 boolector_dump_smt2. A symbol must be unique but may be NULL in case that no 892 symbol should be assigned. 893 894 :param sort: Sort of the uninterpreted function. 895 :param symbol: Name of the uninterpreted function. 896 :return: Uninterpreted function of sort ``sort`` and with symbol ``symbol``. 897 898 .. note:: 899 In contrast to composite expressions, which are maintained 900 uniquely w.r.t. to their kind, inputs (and consequently, bit width), 901 uninterpreted functions are not. 902 Hence, each call to this function returns a fresh uninterpreted function. 903 904 .. seealso:: 905 boolector_apply, boolector_fun_sort 906 */ 907 BoolectorNode *boolector_uf (Btor *btor, 908 BoolectorSort sort, 909 const char *symbol); 910 911 /*------------------------------------------------------------------------*/ 912 913 /*! 914 Create the one's complement of bit-vector ``node``. 915 916 :param btor: Boolector instance. 917 :param node: bit-vector node. 918 :return: Bit-vector representing the one's complement of ``node`` with the 919 same bit width as ``node``. 920 */ 921 BoolectorNode *boolector_not (Btor *btor, BoolectorNode *node); 922 923 /*! 924 Create the two's complement of bit-vector ``node``. 925 926 :param btor: Boolector instance. 927 :param node: Bit-vector node. 928 :return: Bit-vector representing the two's complement of ``node`` with the 929 same bit width as ``node``. 930 */ 931 BoolectorNode *boolector_neg (Btor *btor, BoolectorNode *node); 932 933 /*! 934 Create *or* reduction of node ``node``. 935 936 All bits of node ``node`` are combined by a Boolean *or*. 937 938 :param btor: Boolector instance. 939 :param node: Bit-vector node. 940 :return: Bit-vector with bit width one. 941 */ 942 BoolectorNode *boolector_redor (Btor *btor, BoolectorNode *node); 943 944 /*! 945 Create *xor* reduction of node ``node``. 946 947 All bits of ``node`` are combined by a Boolean *xor*. 948 949 :param btor: Boolector instance. 950 :param node: Bit-vector node. 951 :return: Bit-vector with bit width one. 952 */ 953 BoolectorNode *boolector_redxor (Btor *btor, BoolectorNode *node); 954 955 /*! 956 Create *and* reduction of node ``node``. 957 958 All bits of ``node`` are combined by a Boolean *and*. 959 960 :param btor: Boolector instance. 961 :param node: Bit-vector node. 962 :return: Bit-vector with bit width one. 963 */ 964 BoolectorNode *boolector_redand (Btor *btor, BoolectorNode *node); 965 966 /*! 967 Create a bit-vector slice of ``node`` from index ``upper`` to index 968 ``lower``. 969 970 :param btor: Boolector instance. 971 :param node: Bit-vector node. 972 :param upper: Upper index which must be greater than or equal to zero, and 973 less than the bit width of ``node``. 974 :param lower: Lower index which must be greater than or equal to zero, and 975 less than or equal to ``upper``. 976 :return: Bit-vector with bit width ``upper - lower + 1``. 977 */ 978 BoolectorNode *boolector_slice (Btor *btor, 979 BoolectorNode *node, 980 uint32_t upper, 981 uint32_t lower); 982 983 /*! 984 Create unsigned extension. 985 986 The bit-vector ``node`` is padded with ``width`` * zeroes. 987 988 :param btor: Boolector instance. 989 :param node: Bit-vector node. 990 :param width: Number of zeroes to pad. 991 :return: A bit-vector extended by ``width`` zeroes. 992 */ 993 BoolectorNode *boolector_uext (Btor *btor, BoolectorNode *node, uint32_t width); 994 995 /*! 996 Create signed extension. 997 998 The bit-vector ``node`` is padded with ``width`` bits where the value 999 depends on the value of the most significant bit of node ``n``. 1000 1001 :param btor: Boolector instance. 1002 :param node: Bit-vector node. 1003 :param width: Number of bits to pad. 1004 :return: A bit-vector extended by ``width`` bits. 1005 */ 1006 BoolectorNode *boolector_sext (Btor *btor, BoolectorNode *node, uint32_t width); 1007 /*! 1008 Create a bit-vector *xor*. 1009 1010 The parameters ``n0`` and ``n1`` must have the same bit width. 1011 1012 :param btor: Boolector instance. 1013 :param n0: First bit-vector operand. 1014 :param n1: Second bit-vector operand. 1015 :return: Bit-vector with the same bit width as the operands. 1016 */ 1017 BoolectorNode *boolector_xor (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1018 1019 /*! 1020 Create a bit-vector *xnor*. 1021 1022 The parameters ``n0`` and ``n1`` must have the same bit width. 1023 1024 :param btor: Boolector instance. 1025 :param n0: First bit-vector operand. 1026 :param n1: Second bit-vector operand. 1027 :return: Bit-vector with the same bit width as the operands. 1028 */ 1029 BoolectorNode *boolector_xnor (Btor *btor, 1030 BoolectorNode *n0, 1031 BoolectorNode *n1); 1032 1033 /*! 1034 Create a bit-vector *and*. 1035 1036 The parameters ``n0`` and ``n1`` must have the same bit width. 1037 1038 :param btor: Boolector instance. 1039 :param n0: First bit-vector operand. 1040 :param n1: Second bit-vector operand. 1041 :return: Bit-vector with the same bit width as the operands. 1042 */ 1043 BoolectorNode *boolector_and (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1044 1045 /*! 1046 Create a bit-vector *nand*. 1047 1048 The parameters ``n0`` and ``n1`` must have the same bit width. 1049 1050 :param btor: Boolector instance. 1051 :param n0: First bit-vector operand. 1052 :param n1: Second bit-vector operand. 1053 :return: Bit-vector with the same bit width as the operands. 1054 */ 1055 BoolectorNode *boolector_nand (Btor *btor, 1056 BoolectorNode *n0, 1057 BoolectorNode *n1); 1058 1059 /*! 1060 Create a bit-vector *or*. 1061 1062 The parameters ``n0`` and ``n1`` must have the same bit width. 1063 1064 :param btor: Boolector instance. 1065 :param n0: First bit-vector operand. 1066 :param n1: Second bit-vector operand. 1067 :return: Bit-vector with the same bit width as the operands. 1068 */ 1069 BoolectorNode *boolector_or (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1070 1071 /*! 1072 Create a bit-vector *nor*. 1073 1074 The parameters ``n0`` and ``n1`` must have the same bit width. 1075 1076 :param btor: Boolector instance. 1077 :param n0: First bit-vector operand. 1078 :param n1: Second bit-vector operand. 1079 :return: Bit-vector with the same bit width as the operands. 1080 */ 1081 BoolectorNode *boolector_nor (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1082 1083 /*! 1084 Create bit-vector addition. 1085 1086 The parameters ``n0`` and ``n1`` must have the same bit width. 1087 1088 :param btor: Boolector instance. 1089 :param n0: First bit-vector operand. 1090 :param n1: Second bit-vector operand. 1091 :return: Bit-vector addition with the same bit width as the operands. 1092 */ 1093 BoolectorNode *boolector_add (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1094 1095 /*! 1096 Create an unsigned bit-vector addition overflow detection. 1097 1098 The parameters ``n0`` and ``n1`` must have the same bit width. 1099 1100 :param btor: Boolector instance. 1101 :param n0: First bit-vector operand. 1102 :param n1: Second bit-vector operand. 1103 :return: Bit-vector with bit width one, which indicates if the addition of 1104 ``n0`` and ``n1`` overflows in case both operands are treated 1105 unsigned. 1106 */ 1107 BoolectorNode *boolector_uaddo (Btor *btor, 1108 BoolectorNode *n0, 1109 BoolectorNode *n1); 1110 1111 /*! 1112 Create a signed bit-vector addition overflow detection. 1113 1114 The parameters ``n0`` and ``n1`` must have the same bit width. 1115 1116 :param btor: Boolector instance. 1117 :param n0: First bit-vector operand. 1118 :param n1: Second bit-vector operand. 1119 :return: Bit-vector with bit width one, which indicates if the addition of 1120 ``n0`` and ``n1`` overflows in case both operands are treated 1121 signed. 1122 */ 1123 BoolectorNode *boolector_saddo (Btor *btor, 1124 BoolectorNode *n0, 1125 BoolectorNode *n1); 1126 1127 /*! 1128 Create a bit-vector multiplication. 1129 1130 The parameters ``n0`` and ``n1`` must have the same bit width. 1131 1132 :param btor: Boolector instance. 1133 :param n0: First bit-vector operand. 1134 :param n1: Second bit-vector operand. 1135 :return: Bit-vector multiplication with the same bit width as the operands. 1136 */ 1137 BoolectorNode *boolector_mul (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1138 1139 /*! 1140 Create an unsigned bit-vector multiplication overflow detection. 1141 1142 The parameters ``n0`` and ``n1`` must have the same bit width. 1143 1144 :param btor: Boolector instance. 1145 :param n0: First bit-vector operand. 1146 :param n1: Second bit-vector operand. 1147 :return: Bit-vector with bit width one, which indicates if the multiplication 1148 of ``n0`` and ``n1`` overflows in case both operands are treated 1149 unsigned. 1150 */ 1151 BoolectorNode *boolector_umulo (Btor *btor, 1152 BoolectorNode *n0, 1153 BoolectorNode *n1); 1154 1155 /*! 1156 Create signed multiplication overflow detection. 1157 1158 The parameters ``n0`` and ``n1`` must have the same bit width. 1159 1160 :param btor: Boolector instance. 1161 :param n0: First bit-vector operand. 1162 :param n1: Second bit-vector operand. 1163 :return: Bit-vector with bit width one, which indicates if the multiplication 1164 of ``n0`` and ``n1`` overflows in case both operands are treated 1165 signed. 1166 */ 1167 BoolectorNode *boolector_smulo (Btor *btor, 1168 BoolectorNode *n0, 1169 BoolectorNode *n1); 1170 1171 /*! 1172 Create an unsigned less than. 1173 1174 The parameters ``n0`` and ``n1`` must have the same bit width. 1175 1176 :param btor: Boolector instance. 1177 :param n0: First bit-vector operand. 1178 :param n1: Second bit-vector operand. 1179 :return: Bit-vector with bit width one. 1180 */ 1181 BoolectorNode *boolector_ult (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1182 1183 /*! 1184 Create a signed less than. 1185 1186 The parameters ``n0`` and ``n1`` must have the same bit width. 1187 1188 :param btor: Boolector instance. 1189 :param n0: First bit-vector operand. 1190 :param n1: Second bit-vector operand. 1191 :return: Bit-vector with bit width one. 1192 */ 1193 BoolectorNode *boolector_slt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1194 1195 /*! 1196 Create an unsigned less than or equal. 1197 1198 The parameters ``n0`` and ``n1`` must have the same bit width. 1199 1200 :param btor: Boolector instance. 1201 :param n0: First bit-vector operand. 1202 :param n1: Second bit-vector operand. 1203 :return: Bit-vector with bit width one. 1204 */ 1205 BoolectorNode *boolector_ulte (Btor *btor, 1206 BoolectorNode *n0, 1207 BoolectorNode *n1); 1208 1209 /*! 1210 Create a signed less than or equal. 1211 1212 The parameters ``n0`` and ``n1`` must have the same bit width. 1213 1214 :param btor: Boolector instance. 1215 :param n0: First bit-vector operand. 1216 :param n1: Second bit-vector operand. 1217 :return: Bit-vector with bit width one. 1218 */ 1219 BoolectorNode *boolector_slte (Btor *btor, 1220 BoolectorNode *n0, 1221 BoolectorNode *n1); 1222 1223 /*! 1224 Create an unsigned greater than. 1225 1226 The parameters ``n0`` and ``n1`` must have the same bit width. 1227 1228 :param btor: Boolector instance. 1229 :param n0: First bit-vector operand. 1230 :param n1: Second bit-vector operand. 1231 :return: Bit-vector with bit width one. 1232 */ 1233 BoolectorNode *boolector_ugt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1234 1235 /*! 1236 Create a signed greater than. 1237 1238 The parameters ``n0`` and ``n1`` must have the same bit width. 1239 1240 :param btor: Boolector instance. 1241 :param n0: First bit-vector operand. 1242 :param n1: Second bit-vector operand. 1243 :return: Bit-vector with bit width one. 1244 */ 1245 BoolectorNode *boolector_sgt (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1246 1247 /*! 1248 Create an unsigned greater than or equal. 1249 1250 The parameters ``n0`` and ``n1`` must have the same bit width. 1251 1252 :param btor: Boolector instance. 1253 :param n0: First bit-vector operand. 1254 :param n1: Second bit-vector operand. 1255 :return: Bit-vector with bit width one. 1256 */ 1257 BoolectorNode *boolector_ugte (Btor *btor, 1258 BoolectorNode *n0, 1259 BoolectorNode *n1); 1260 1261 /*! 1262 Create a signed greater than or equal. 1263 1264 The parameters ``n0`` and ``n1`` must have the same bit width. 1265 1266 :param btor: Boolector instance. 1267 :param n0: First bit-vector operand. 1268 :param n1: Second bit-vector operand. 1269 :return: Bit-vector with bit width one. 1270 */ 1271 BoolectorNode *boolector_sgte (Btor *btor, 1272 BoolectorNode *n0, 1273 BoolectorNode *n1); 1274 1275 /*! 1276 Create a logical shift left. 1277 1278 The parameters ``n0`` and ``n1`` must either have the same bit width or 1279 the bit width of ``n0`` must be a power of two (greater than 1) and the 1280 bit width of ``n1`` must be log2 of the bit width of ``n0``. 1281 1282 :param btor: Boolector instance. 1283 :param n0: First bit-vector operand. 1284 :param n1: Second bit-vector operand. 1285 :return: Bit-vector with the same bit width as ``n0``. 1286 */ 1287 BoolectorNode *boolector_sll (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1288 1289 /*! 1290 Create a logical shift right. 1291 1292 The parameters ``n0`` and ``n1`` must either have the same bit width or 1293 the bit width of ``n0`` must be a power of two (greater than 1) and the 1294 bit width of ``n1`` must be log2 of the bit width of ``n0``. 1295 1296 :param btor: Boolector instance. 1297 :param n0: First bit-vector operand. 1298 :param n1: Second bit-vector operand. 1299 :return: Bit-vector with the same bit width as ``n0``. 1300 */ 1301 BoolectorNode *boolector_srl (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1302 1303 /*! 1304 Create an arithmetic shift right. 1305 1306 The parameters ``n0`` and ``n1`` must either have the same bit width or 1307 the bit width of ``n0`` must be a power of two (greater than 1) and the 1308 bit width of ``n1`` must be log2 of the bit width of ``n0``. 1309 1310 :param btor: Boolector instance. 1311 :param n0: First bit-vector operand. 1312 :param n1: Second bit-vector operand. 1313 :return: Bit-vector with the same bit width as ``n0``. 1314 */ 1315 BoolectorNode *boolector_sra (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1316 1317 /*! 1318 Create a rotate left, with the number of bits to rotate by given as a 1319 bit-vector. 1320 1321 The parameters ``n0`` and ``n1`` must either have the same bit width or 1322 the bit width of ``n0`` must be a power of two (greater than 1) and the 1323 bit width of ``n1`` must be log2 of the bit width of ``n0``. 1324 1325 :param btor: Boolector instance. 1326 :param n0: First bit-vector operand. 1327 :param n1: Second bit-vector operand. 1328 :return: Bit-vector with the same bit width as ``n0``. 1329 */ 1330 BoolectorNode *boolector_rol (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1331 1332 /*! 1333 Create a rotate right, with the number of bits to rotate by given as a 1334 bit-vector. 1335 1336 The parameters ``n0`` and ``n1`` must either have the same bit width or 1337 the bit width of ``n0`` must be a power of two (greater than 1) and the 1338 bit width of ``n1`` must be log2 of the bit width of ``n0``. 1339 1340 :param btor: Boolector instance. 1341 :param n0: First bit-vector operand. 1342 :param n1: Second bit-vector operand. 1343 :return: Bit-vector with the same bit width as ``n0``. 1344 */ 1345 BoolectorNode *boolector_ror (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1346 1347 /*! 1348 Create a rotate left, with the number of bits to rotate by given as a 1349 numeral (unsigned integer). 1350 1351 :param btor: Boolector instance. 1352 :param n: Bit-vector operand. 1353 :param nbits: Number of bits to rotate by. 1354 :return: Bit-vector with the same bit width as ``n``. 1355 */ 1356 BoolectorNode *boolector_roli (Btor *btor, BoolectorNode *n, uint32_t nbits); 1357 1358 /*! 1359 Create a rotate right, with the number of bits to rotate by given as a 1360 numeral (unsigned integer). 1361 1362 :param btor: Boolector instance. 1363 :param n: Bit-vector operand. 1364 :param nbits: Number of bits to rotate by. 1365 :return: Bit-vector with the same bit width as ``n``. 1366 */ 1367 BoolectorNode *boolector_rori (Btor *btor, BoolectorNode *n, uint32_t nbits); 1368 1369 /*! 1370 Create a bit-vector subtraction. 1371 1372 The parameters ``n0`` and ``n1`` must have the same bit width. 1373 1374 :param btor: Boolector instance. 1375 :param n0: First bit-vector operand. 1376 :param n1: Second bit-vector operand. 1377 :return: Bit-vector with the same bit width as the operands. 1378 */ 1379 BoolectorNode *boolector_sub (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 1380 1381 /*! 1382 Create an unsigned bit-vector subtraction overflow detection. 1383 1384 The parameters ``n0`` and ``n1`` must have the same bit width. 1385 1386 :param btor: Boolector instance. 1387 :param n0: First bit-vector operand. 1388 :param n1: Second bit-vector operand. 1389 :return: Bit-vector with bit width one, which indicates if the subtraction of 1390 ``n0`` and ``n1`` overflows in case both operands are treated 1391 unsigned. 1392 */ 1393 BoolectorNode *boolector_usubo (Btor *btor, 1394 BoolectorNode *n0, 1395 BoolectorNode *n1); 1396 1397 /*! 1398 Create a signed bit-vector subtraction overflow detection. 1399 1400 The parameters ``n0`` and ``n1`` must have the same bit width. 1401 1402 :param btor: Boolector instance. 1403 :param n0: First bit-vector operand. 1404 :param n1: Second bit-vector operand. 1405 :return: Bit-vector with bit width one, which indicates if the subtraction of 1406 ``n0`` and ``n1`` overflows in case both operands are treated 1407 signed. 1408 */ 1409 BoolectorNode *boolector_ssubo (Btor *btor, 1410 BoolectorNode *n0, 1411 BoolectorNode *n1); 1412 1413 /*! 1414 Create unsigned division. 1415 1416 The parameters ``n0`` and ``n1`` must have the same bit width. 1417 If ``n1`` is zero, then the result is -1. 1418 1419 :param btor: Boolector instance. 1420 :param n0: First bit-vector operand. 1421 :param n1: Second bit-vector operand. 1422 :return: Bit-vector with the same bit width as the operands. 1423 1424 .. note:: 1425 The behavior that division by zero returns -1 does not exactly 1426 comply with the SMT-LIB standard 1.2 and 2.0 where division by zero is 1427 handled as uninterpreted function. Our semantics are motivated by 1428 real circuits where division by zero cannot be uninterpreted and of course 1429 returns a result. 1430 */ 1431 BoolectorNode *boolector_udiv (Btor *btor, 1432 BoolectorNode *n0, 1433 BoolectorNode *n1); 1434 1435 /*! 1436 Create signed division. 1437 1438 The parameters ``n0`` and ``n1`` must have the same bit width. 1439 1440 :param btor: Boolector instance. 1441 :param n0: First bit-vector operand. 1442 :param n1: Second bit-vector operand. 1443 :return: Bit-vector with the same bit width as the operands. 1444 1445 .. note:: 1446 Signed division is expressed by means of unsigned 1447 division, where either node is normalized in case that its sign bit is 1. 1448 If the sign bits of ``a`` and ``b`` do not match, two's complement 1449 is performed on the result of the previous unsigned division. 1450 Hence, the behavior in case of a division by zero depends on 1451 boolector_udiv. 1452 */ 1453 BoolectorNode *boolector_sdiv (Btor *btor, 1454 BoolectorNode *n0, 1455 BoolectorNode *n1); 1456 1457 /*! 1458 Create a signed bit-vector division overflow detection. 1459 1460 The parameters ``n0`` and ``n1`` must have the same bit width. 1461 An overflow can happen if ``n0`` represents INT_MIN and ``n1`` represents -1. 1462 1463 :param btor: Boolector instance. 1464 :param n0: First bit-vector operand. 1465 :param n1: Second bit-vector operand. 1466 :return: Bit-vector with bit width one, which indicates if the division of 1467 ``n0`` and ``n1`` overflows in case both operands are treated 1468 signed. 1469 1470 .. note:: 1471 Unsigned division cannot overflow. 1472 */ 1473 BoolectorNode *boolector_sdivo (Btor *btor, 1474 BoolectorNode *n0, 1475 BoolectorNode *n1); 1476 1477 /*! 1478 Create an unsigned remainder. 1479 1480 The parameters ``n0`` and ``n1`` must have the same bit width. 1481 If ``n1`` is zero, then the result is ``n0``. 1482 1483 :param btor: Boolector instance. 1484 :param n0: First bit-vector operand. 1485 :param n1: Second bit-vector operand. 1486 :return: Bit-vector with the same bit width as the operands. 1487 1488 .. note:: 1489 As in boolector_udiv the behavior if ``n1`` is zero, does 1490 not exactly comply with the SMT-LIB standard 1.2 and 2.0 where the result 1491 is handled as uninterpreted function. Our semantics are motivated by 1492 real circuits, where results can not be uninterpreted. 1493 */ 1494 BoolectorNode *boolector_urem (Btor *btor, 1495 BoolectorNode *n0, 1496 BoolectorNode *n1); 1497 1498 /*! 1499 Create a signed remainder. 1500 1501 The parameters ``n0`` and ``n1`` must have the same bit width. 1502 If ``n1`` is zero, then the result is ``n0``. 1503 1504 :param btor: Boolector instance. 1505 :param n0: First bit-vector operand. 1506 :param n1: Second bit-vector operand. 1507 :return: Bit-vector with the same bit width as the operands. 1508 1509 .. note:: 1510 Analogously to boolector_sdiv, the signed remainder is expressed by means 1511 of the unsigned remainder, where either node is normalized in case that its 1512 sign bit is 1. Hence, in case that ``n1`` is zero, the result depends on 1513 boolector_urem. 1514 */ 1515 BoolectorNode *boolector_srem (Btor *btor, 1516 BoolectorNode *n0, 1517 BoolectorNode *n1); 1518 1519 /*! 1520 Create a, signed remainder where its sign matches the sign of the divisor. 1521 1522 The parameters ``n0`` and ``n1`` must have the same bit width. 1523 1524 :param btor: Boolector instance. 1525 :param n0: First bit-vector operand. 1526 :param n1: Second bit-vector operand. 1527 :return: Bit-vector with the same bit width as the operands. 1528 1529 .. note:: 1530 If ``n1`` is zero, the behavior of this function depends on boolector_urem. 1531 */ 1532 BoolectorNode *boolector_smod (Btor *btor, 1533 BoolectorNode *n0, 1534 BoolectorNode *n1); 1535 1536 /*! 1537 Create the concatenation of two bit-vectors. 1538 1539 :param btor: Boolector instance. 1540 :param n0: First bit-vector operand. 1541 :param n1: Second bit-vector operand. 1542 :return: Bit-vector with the bit width ``bit width of n0 + bit width of n1``. 1543 */ 1544 BoolectorNode *boolector_concat (Btor *btor, 1545 BoolectorNode *n0, 1546 BoolectorNode *n1); 1547 1548 /*! 1549 Create ``n`` concatenations of a given node ``node``. 1550 1551 :param btor: Boolector instance. 1552 :param node: Bit-vector operand. 1553 :param n: Number of times to repeat the given node. 1554 :return: A node representing ``n`` concatenations of node ``node``. 1555 */ 1556 BoolectorNode *boolector_repeat (Btor *btor, BoolectorNode *node, uint32_t n); 1557 1558 /*------------------------------------------------------------------------*/ 1559 1560 /*! 1561 Create a read on array ``n_array`` at position ``n_index``. 1562 1563 :param btor: Boolector instance. 1564 :param n_array: Array operand. 1565 :param n_index: Bit-vector index. The bit width of ``n_index`` must have the 1566 same bit width as the indices of ``n_array``. 1567 :return: Bit-vector with the same bit width as the elements of ``n_array``. 1568 */ 1569 BoolectorNode *boolector_read (Btor *btor, 1570 BoolectorNode *n_array, 1571 BoolectorNode *n_index); 1572 1573 /*! 1574 Create a write on array ``n_array`` at position ``n_index`` with value 1575 ``n_value``. 1576 1577 The array is updated at exactly one position, all other elements remain 1578 unchanged. The bit width of ``n_index`` must be the same as the bit width of 1579 the indices of ``n_array``. The bit width of ``n_value`` must be the same as 1580 the bit width of the elements of ``n_array``. 1581 1582 :param btor: Boolector instance. 1583 :param n_array: Array operand. 1584 :param n_index: Bit-vector index. 1585 :param n_value: Bit-vector value. 1586 :return: An array where the value at index ``n_index`` has been updated with 1587 ``n_value``. 1588 */ 1589 BoolectorNode *boolector_write (Btor *btor, 1590 BoolectorNode *n_array, 1591 BoolectorNode *n_index, 1592 BoolectorNode *n_value); 1593 1594 /*------------------------------------------------------------------------*/ 1595 1596 /*! 1597 Create an if-then-else. 1598 1599 If condition ``n_cond`` is true, then ``n_then`` is returned, else ``n_else`` 1600 is returned. 1601 Nodes ``n_then`` and ``n_else`` must be either both arrays or both bit 1602 vectors. 1603 1604 :param btor: Boolector instance. 1605 :param n_cond: Bit-vector condition with bit width one. 1606 :param n_then: Array or bit-vector operand representing the ``if`` case. 1607 :param n_else: Array or bit-vector operand representing the ``else`` case. 1608 :return: Either ``n_then`` or ``n_else``. 1609 */ 1610 BoolectorNode *boolector_cond (Btor *btor, 1611 BoolectorNode *n_cond, 1612 BoolectorNode *n_then, 1613 BoolectorNode *n_else); 1614 1615 /*------------------------------------------------------------------------*/ 1616 1617 /*! 1618 Create function parameter of sort ``sort``. 1619 1620 This kind of node is used to create parameterized expressions, which are 1621 used to create functions. Once a parameter is bound to a function, it 1622 cannot be re-used in other functions. 1623 1624 :param btor: Boolector instance. 1625 :param sort: Parameter sort. 1626 :param symbol: Name of parameter. 1627 :return: Parameter expression of sort ``sort`` and with symbol ``symbol``. 1628 1629 .. seealso:: 1630 boolector_fun, boolector_apply 1631 */ 1632 BoolectorNode *boolector_param (Btor *btor, 1633 BoolectorSort sort, 1634 const char *symbol); 1635 1636 /*! 1637 Create a function with body ``node`` parameterized over parameters 1638 ``param_nodes``. 1639 1640 This kind of node is similar to macros in the SMT-LIB standard 2.0. 1641 Note that as soon as a parameter is bound to a function, it can not be 1642 reused in other functions. 1643 Call a function via boolector_apply. 1644 1645 :param btor: Boolector instance. 1646 :param param_nodes: Parameters of function. 1647 :param paramc: Number of parameters. 1648 :param node: Function body parameterized over ``param_nodes``. 1649 :return: Function over parameterized expression ``node``. 1650 1651 .. seealso:: 1652 boolector_apply, boolector_param 1653 */ 1654 BoolectorNode *boolector_fun (Btor *btor, 1655 BoolectorNode **param_nodes, 1656 uint32_t paramc, 1657 BoolectorNode *node); 1658 1659 /*! 1660 Create a function application on function ``n_fun`` with arguments 1661 ``arg_nodes``. 1662 1663 :param btor: Boolector instance. 1664 :param arg_nodes: Arguments to be applied. 1665 :param argc: Number of arguments to be applied. 1666 :param n_fun: Function expression. 1667 :return: Function application on function ``n_fun`` with arguments 1668 ``arg_nodes``. 1669 1670 .. seealso:: 1671 boolector_fun, boolector_uf 1672 */ 1673 BoolectorNode *boolector_apply (Btor *btor, 1674 BoolectorNode **arg_nodes, 1675 uint32_t argc, 1676 BoolectorNode *n_fun); 1677 1678 /*------------------------------------------------------------------------*/ 1679 1680 /*! 1681 Create bit-vector expression that increments bit-vector ``node`` by one. 1682 1683 :param btor: Boolector instance. 1684 :param node: Bit-vector operand. 1685 :return: Bit-vector with the same bit width as ``node`` incremented by one. 1686 */ 1687 BoolectorNode *boolector_inc (Btor *btor, BoolectorNode *node); 1688 1689 /*! 1690 Create bit-vector expression that decrements bit-vector ``node`` by one. 1691 1692 :param btor: Boolector instance. 1693 :param node: Bit-vector operand. 1694 :return: Bit-vector with the same bit width as ``node`` decremented by one. 1695 */ 1696 BoolectorNode *boolector_dec (Btor *btor, BoolectorNode *node); 1697 1698 /*------------------------------------------------------------------------*/ 1699 1700 /*! 1701 Create a universally quantified formula. 1702 1703 \forall (params[0] ... params[paramc - 1]) body 1704 1705 :param btor: Boolector instance. 1706 :param params: Array of quantified variables. 1707 :param paramc: length of ``params`` array. 1708 :param body: Term where ``params`` may occur. 1709 :return: Universally quantified formula. 1710 */ 1711 BoolectorNode *boolector_forall (Btor *btor, 1712 BoolectorNode *params[], 1713 uint32_t paramc, 1714 BoolectorNode *body); 1715 1716 /*! 1717 Create an existentially quantifed formula. 1718 1719 \exists (params[0] ... params[paramc - 1]) body 1720 1721 :param btor: Boolector instance. 1722 :param params: Array of quantified variables. 1723 :param paramc: length of ``params`` array. 1724 :param body: Term where ``params`` may occur. 1725 :return: Existentially quantified formula. 1726 */ 1727 BoolectorNode *boolector_exists (Btor *btor, 1728 BoolectorNode *param[], 1729 uint32_t paramc, 1730 BoolectorNode *body); 1731 1732 /*------------------------------------------------------------------------*/ 1733 1734 /*! 1735 Return the Boolector instance to which ``node`` belongs. 1736 1737 :param node: Boolector node. 1738 :return: Boolector instance. 1739 */ 1740 Btor *boolector_get_btor (BoolectorNode *node); 1741 1742 /*! 1743 Get the id of a given node. 1744 1745 :param btor: Boolector instance. 1746 :param node: Boolector node. 1747 :return: Id of ``node``. 1748 */ 1749 int32_t boolector_get_node_id (Btor *btor, BoolectorNode *node); 1750 1751 /*! 1752 Get the sort of given ``node``. The result does not have to be released. 1753 1754 :param btor: Boolector instance. 1755 :param node: Boolector node. 1756 :return: Sort of ``node``. 1757 */ 1758 BoolectorSort boolector_get_sort (Btor *btor, const BoolectorNode *node); 1759 1760 /*! 1761 Get the domain sort of given function node ``node``. 1762 The result does not have to be released. 1763 1764 :param btor: Boolector instance. 1765 :param node: Boolector function node. 1766 :return: Domain sort of function ``node``. 1767 */ 1768 BoolectorSort boolector_fun_get_domain_sort (Btor *btor, 1769 const BoolectorNode *node); 1770 1771 /*! 1772 Get the codomain sort of given function node ``node``. 1773 The result does not have to be released. 1774 1775 :param btor: Boolector instance. 1776 :param node: Boolector function node. 1777 :return: Codomain sort of function ``node``. 1778 */ 1779 BoolectorSort boolector_fun_get_codomain_sort (Btor *btor, 1780 const BoolectorNode *node); 1781 1782 /*------------------------------------------------------------------------*/ 1783 1784 /*! 1785 Retrieve the node belonging to Boolector instance ``btor`` that matches 1786 given ``id``. Aborts if no node with given ``id`` exists in given Boolector 1787 instance. 1788 1789 :param btor: Boolector instance. 1790 :param id: Boolector node id. 1791 :return: The Boolector node that matches given ``node`` in Boolector instance 1792 ``btor`` by id. 1793 1794 .. note:: 1795 Matching a node against another increases the reference 1796 count of the returned match, which must therefore be released appropriately 1797 (boolector_release). 1798 Only nodes created before a boolector_clone call can be matched. 1799 */ 1800 BoolectorNode *boolector_match_node_by_id (Btor *btor, int32_t id); 1801 1802 /*! 1803 Retrieve the node belonging to Boolector instance ``btor`` that matches 1804 given ``symbol``. Aborts if no node with given ``symbol`` exists in given 1805 Boolector instance. 1806 1807 :param btor: Boolector instance. 1808 :param symbol: The symbol of an expression. 1809 :return: The Boolector node that matches given ``node`` in Boolector instance 1810 ``btor`` by id. 1811 1812 .. note:: 1813 Matching a node against another increases the reference 1814 count of the returned match, which must therefore be released appropriately 1815 (boolector_release). 1816 Only nodes created before a boolector_clone call can be matched. 1817 */ 1818 BoolectorNode *boolector_match_node_by_symbol (Btor *btor, const char *symbol); 1819 1820 /*! 1821 Retrieve the node belonging to Boolector instance ``btor`` that matches 1822 given BoolectorNode ``node`` by id. This is intended to be used for handling 1823 expressions of a cloned instance (boolector_clone). 1824 Aborts no matching node exists in given Boolector instance. 1825 1826 :param btor: Boolector instance. 1827 :param node: Boolector node. 1828 :return: The Boolector node that matches given ``node`` in Boolector instance 1829 ``btor`` by id. 1830 1831 .. note:: 1832 Matching a node against another increases the reference 1833 count of the returned match, which must therefore be released appropriately 1834 (boolector_release). 1835 Only nodes created before a boolector_clone call can be matched. 1836 */ 1837 BoolectorNode *boolector_match_node (Btor *btor, BoolectorNode *node); 1838 1839 /*------------------------------------------------------------------------*/ 1840 1841 /*! 1842 Get the symbol of an expression. 1843 1844 :param btor: Boolector instance. 1845 :param node: Boolector node. 1846 :return: Symbol of expression. 1847 1848 .. seealso:: 1849 boolector_var, boolector_array, boolector_uf, boolector_param 1850 */ 1851 const char *boolector_get_symbol (Btor *btor, BoolectorNode *node); 1852 1853 /*! 1854 Set the symbol of an expression. 1855 1856 :param btor: Boolector instance. 1857 :param node: Boolector node. 1858 :param symbol: The symbol to be set. 1859 1860 .. seealso:: 1861 boolector_var, boolector_array, boolector_uf, boolector_param 1862 */ 1863 void boolector_set_symbol (Btor *btor, BoolectorNode *node, const char *symbol); 1864 1865 /*! 1866 Get the bit width of an expression. 1867 1868 If the expression is an array, it returns the bit width of the array 1869 elements. 1870 If the expression is a function, it returns the bit width of the function's 1871 return value. 1872 1873 :param btor: Boolector instance. 1874 :param node: Boolector node. 1875 :return: Bit width of ``node``. 1876 */ 1877 uint32_t boolector_get_width (Btor *btor, BoolectorNode *node); 1878 1879 /*! 1880 Get the bit width of indices of ``n_array``. 1881 1882 :param btor: Boolector instance. 1883 :param n_array: Array operand. 1884 :return: Bit width of indices of ``n_array`` 1885 */ 1886 uint32_t boolector_get_index_width (Btor *btor, BoolectorNode *n_array); 1887 1888 /*! 1889 Get the bit-vector of a constant node represented as a bit string. 1890 Must be freed via boolector_free_bits. 1891 1892 :param btor: Boolector instance. 1893 :param node: Constant node. 1894 :return: String representing the bits of ``node``. 1895 1896 .. seealso:: 1897 boolector_free_bits 1898 */ 1899 const char *boolector_get_bits (Btor *btor, BoolectorNode *node); 1900 1901 /*! 1902 Free a bits string retrieved via boolector_get_bits. 1903 1904 :param btor: Boolector instance. 1905 :param bits: String which has to be freed. 1906 1907 .. seealso:: 1908 boolector_get_bits 1909 */ 1910 void boolector_free_bits (Btor *btor, const char *bits); 1911 1912 /*! 1913 Get the arity of function ``node``. 1914 1915 :param btor: Boolector instance. 1916 :param node: Function node. 1917 :return: Arity of ``node``. 1918 */ 1919 uint32_t boolector_get_fun_arity (Btor *btor, BoolectorNode *node); 1920 1921 /*------------------------------------------------------------------------*/ 1922 1923 /*! 1924 Determine if given node is a constant node. 1925 1926 :param btor: Boolector instance. 1927 :param node: Boolector node. 1928 :return: True if ``node`` is a constant, and false otherwise. 1929 */ 1930 bool boolector_is_const (Btor *btor, BoolectorNode *node); 1931 1932 /*! 1933 Determine if given node is a bit-vector variable. 1934 1935 :param btor: Boolector instance. 1936 :param node: Boolector node. 1937 :return: True if ``node`` is a bit-vector variable, and false otherwise. 1938 */ 1939 bool boolector_is_var (Btor *btor, BoolectorNode *node); 1940 1941 /*! 1942 Determine if given node is an array node. 1943 1944 :param btor: Boolector instance. 1945 :param node: Boolector node. 1946 :return: True if ``node`` is an array, and false otherwise. 1947 */ 1948 bool boolector_is_array (Btor *btor, BoolectorNode *node); 1949 1950 /*! 1951 Determine if given node is an array variable. 1952 1953 :param btor: Boolector instance. 1954 :param node: Boolector node. 1955 :return: True if ``node`` is an array variable, and false otherwise. 1956 */ 1957 bool boolector_is_array_var (Btor *btor, BoolectorNode *node); 1958 1959 /*! 1960 Determine if given node is a parameter node. 1961 1962 :param btor: Boolector instance. 1963 :param node: Boolector node. 1964 :return: True if ``node`` is a parameter, and false otherwise. 1965 */ 1966 bool boolector_is_param (Btor *btor, BoolectorNode *node); 1967 1968 /*! 1969 Determine if given parameter node is bound by a function. 1970 1971 :param btor: Boolector instance. 1972 :param node: Parameter node. 1973 :return: True if ``node`` is bound, and false otherwise. 1974 */ 1975 bool boolector_is_bound_param (Btor *btor, BoolectorNode *node); 1976 1977 /*! 1978 Determine if given node is an uninterpreted function node. 1979 1980 :param btor: Boolector instance. 1981 :param node: Boolector node. 1982 :return: True if ``node`` is an uninterpreted function, and false otherwise. 1983 */ 1984 bool boolector_is_uf (Btor *btor, BoolectorNode *node); 1985 1986 /*! 1987 Determine if given node is a function node. 1988 1989 :param btor: Boolector instance. 1990 :param node: Boolector node. 1991 :return: True if ``node`` is a function, and false otherwise. 1992 */ 1993 bool boolector_is_fun (Btor *btor, BoolectorNode *node); 1994 1995 /*------------------------------------------------------------------------*/ 1996 1997 /*! 1998 Check if sorts of given arguments matches the function signature. 1999 2000 :param btor: Boolector instance. 2001 :param arg_nodes: Arguments to be checked. 2002 :param argc: Number of arguments to be checked. 2003 :param n_fun: Function expression. 2004 :return: -1 if all sorts are correct, otherwise it returns the position of 2005 the incorrect argument. 2006 */ 2007 int32_t boolector_fun_sort_check (Btor *btor, 2008 BoolectorNode **arg_nodes, 2009 uint32_t argc, 2010 BoolectorNode *n_fun); 2011 2012 /*------------------------------------------------------------------------*/ 2013 2014 /*! 2015 Generate an assignment string for bit-vector expression if 2016 boolector_sat has returned BOOLECTOR_SAT and model generation has been 2017 enabled. 2018 2019 The expression can be an arbitrary bit-vector expression which 2020 occurs in an assertion or current assumption. The assignment string has to 2021 be freed by boolector_free_bv_assignment. 2022 2023 :param btor: Boolector instance. 2024 :param node: Bit-vector expression. 2025 :return: String representing a satisfying assignment to bit-vector variables 2026 and a consistent assignment for arbitrary bit-vector expressions. 2027 The string representation will use binary, decimal or hexadecimal 2028 number format, depending on the configuration of option 2029 ``BTOR_OPT_OUTPUT_NUMBER_FORMAT`` (binary by default). 2030 2031 .. seealso:: 2032 boolector_set_opt for enabling model generation. 2033 */ 2034 const char *boolector_bv_assignment (Btor *btor, BoolectorNode *node); 2035 2036 /*! 2037 Free an assignment string for bit-vectors. 2038 2039 :param btor: Boolector instance. 2040 :param assignment: String which has to be freed. 2041 2042 .. seealso:: 2043 boolector_bv_assignment 2044 */ 2045 void boolector_free_bv_assignment (Btor *btor, const char *assignment); 2046 2047 /*! 2048 Generate a model for an array expression. 2049 2050 If boolector_sat has returned BOOLECTOR_SAT and model generation has been 2051 enabled. The function creates and stores the array of indices into 2052 ``indices`` and the array of corresponding values into ``values``. The number 2053 size of ``indices`` resp. ``values`` is stored into ``size``. The array model 2054 simply inspects the set of reads rho, which is associated with each array 2055 expression. See our publication `Lemmas on Demand for Lambdas 2056 <http://fmv.jku.at/papers/PreinerNiemetzBiere-DIFTS13.pdf>`_ for details. At 2057 indices that do not occur in the model, it is assumed that the array stores a 2058 globally unique default value, for example 0. If the model of a constant array 2059 is queried the default value of the constant array is indicated via index '*'. 2060 The bit-vector assignments to the indices and values have to be freed by 2061 boolector_free_bv_assignment. Furthermore, the user has to free the array of 2062 indices and the array of values, respectively of size ``size``. 2063 2064 :param btor: Boolector instance. 2065 :param n_array: Array operand for which the array model should be built. 2066 :param indices: Pointer to array of index strings. The string representation 2067 will use binary, decimal or hexadecimal number format, 2068 depending on the configuration of option 2069 ``BTOR_OPT_OUTPUT_NUMBER_FORMAT`` (binary by default). 2070 :param values: Pointer to array of value strings. The string representation 2071 will use binary, decimal or hexadecimal number format, 2072 depending on the configuration of option 2073 ``BTOR_OPT_OUTPUT_NUMBER_FORMAT`` (binary by default). 2074 :param size: Pointer to size. 2075 2076 .. seealso:: 2077 boolector_set_opt for enabling model generation. 2078 */ 2079 void boolector_array_assignment (Btor *btor, 2080 BoolectorNode *n_array, 2081 char ***indices, 2082 char ***values, 2083 uint32_t *size); 2084 2085 /*! 2086 Free an assignment string for arrays of bit-vectors. 2087 2088 :param btor: Boolector instance. 2089 :param indices: Array of index strings of size ``size``. 2090 :param values: Array of values strings of size ``size``. 2091 :param size: Size of arrays ``indices`` and ``values``. 2092 2093 .. seealso:: 2094 boolector_array_assignment 2095 */ 2096 void boolector_free_array_assignment (Btor *btor, 2097 char **indices, 2098 char **values, 2099 uint32_t size); 2100 2101 /*! 2102 Generate a model for an uninterpreted function. 2103 The function creates and stores the assignments of the function's arguments 2104 to array ``args`` and the function's return values to array ``values``. 2105 Arrays ``args`` and ``values`` represent assignment pairs of arguments and 2106 values, i.e., instantiating a function with args[i] yields value values[i]. 2107 For functions with arity > 1 args[i] contains a space separated string of 2108 argument assignments, where the order of the assignment strings corresponds 2109 to the order of the function's arguments. 2110 2111 :param btor: Boolector instance. 2112 :param n_uf: Uninterpreted function node. 2113 :param args: Pointer to array of argument assignment strings. 2114 :param values: Pointer to array of value assignment strings. 2115 :param size: Size of arrays ``args`` and ``values``. 2116 2117 .. note:: 2118 This function can only be called if boolector_sat returned 2119 BOOLECTOR_SAT and model generation was enabled. 2120 2121 .. seealso:: 2122 boolector_set_opt for enabling model generation 2123 */ 2124 void boolector_uf_assignment (Btor *btor, 2125 BoolectorNode *n_uf, 2126 char ***args, 2127 char ***values, 2128 uint32_t *size); 2129 2130 /*! 2131 Free assignment strings for uninterpreted functions. 2132 2133 :param btor: Boolector instance. 2134 :param args: Array of argument strings of size ``size``. 2135 :param values: Array of value string of size ``size``. 2136 :param size: Size of arrays ``args`` and ``values``. 2137 2138 .. seealso:: 2139 boolector_uf_assignment 2140 */ 2141 void boolector_free_uf_assignment (Btor *btor, 2142 char **args, 2143 char **values, 2144 uint32_t size); 2145 2146 /*! 2147 Print model to output file. This function prints the model for all inputs 2148 to the output file ``file``. Supported output formats for the model to be 2149 printed are: 2150 2151 * **btor** 2152 2153 Use boolector's own output format for printing models. 2154 2155 .. code-block:: c 2156 2157 boolector_print_model_noref (btor, "btor", stdout); 2158 2159 A possible model would be: :: 2160 2161 2 00000100 x 2162 3 00010101 y 2163 4[00] 01 A 2164 2165 where the first column indicates the id of an input, the second column 2166 its assignment, and the third column its name (or symbol), if any. 2167 Note that in case that an input is an uninterpreted function or an 2168 array variable, 2169 values in square brackets indicate parameter resp. index values. 2170 2171 * **smt2** 2172 2173 Use `SMT-LIB v2`_ format for printing models. 2174 2175 .. code-block:: c 2176 2177 boolector_print_model_noref (btor, "smt2", stdout); 2178 2179 A possible model would be: :: 2180 2181 (model 2182 (define-fun x () (_ BitVec 8) #b00000100) 2183 (define-fun y () (_ BitVec 8) #b00010101) 2184 (define-fun y ( 2185 (y_x0 (_ BitVec 2))) 2186 (ite (= y_x0 #b00) #b01 2187 #00)) 2188 ) 2189 2190 :param btor: Boolector instance. 2191 :param format: A string identifying the output format. 2192 :param file: Output file. 2193 */ 2194 void boolector_print_model (Btor *btor, char *format, FILE *file); 2195 2196 /*------------------------------------------------------------------------*/ 2197 2198 /*! 2199 Create Boolean sort. 2200 2201 :param btor: Boolector instance. 2202 :return: Sort of type Boolean. 2203 2204 .. seealso:: 2205 boolector_var, boolector_param 2206 */ 2207 BoolectorSort boolector_bool_sort (Btor *btor); 2208 2209 /*! 2210 Create bit-vector sort of bit width ``width``. 2211 2212 :param btor: Boolector instance. 2213 :param width: Bit width. 2214 :return: Bit-vector sort of bit width ``width``. 2215 2216 .. seealso:: 2217 boolector_var, boolector_param 2218 */ 2219 BoolectorSort boolector_bitvec_sort (Btor *btor, uint32_t width); 2220 2221 /*! 2222 Create function sort. 2223 2224 :param btor: Boolector instance. 2225 :param domain: A list of all the function arguments' sorts. 2226 :param arity: Number of elements in domain (must be > 0). 2227 :param codomain: The sort of the function's return value. 2228 :return: Function sort which maps given domain to given codomain. 2229 2230 .. seealso:: 2231 boolector_uf 2232 */ 2233 BoolectorSort boolector_fun_sort (Btor *btor, 2234 BoolectorSort *domain, 2235 uint32_t arity, 2236 BoolectorSort codomain); 2237 2238 /*! 2239 Create array sort. 2240 2241 :param btor: Boolector instance. 2242 :param index: Index sort of array. 2243 :param element: Element sort of array. 2244 :return: Array sort which maps sort ``index`` to sort ``element``. 2245 2246 .. seealso:: 2247 boolector_array 2248 */ 2249 BoolectorSort boolector_array_sort (Btor *btor, 2250 BoolectorSort index, 2251 BoolectorSort element); 2252 2253 /*! 2254 Copy sort (increments reference counter). 2255 2256 :param btor: Boolector instance. 2257 :param sort: Sort to be copied. 2258 :return: Sort ``sort`` with reference counter incremented. 2259 */ 2260 BoolectorSort boolector_copy_sort (Btor *btor, BoolectorSort sort); 2261 2262 /*! 2263 Release sort (decrements reference counter). 2264 2265 :param btor: Boolector instance. 2266 :param sort: Sort to be released. 2267 */ 2268 void boolector_release_sort (Btor *btor, BoolectorSort sort); 2269 2270 /*! 2271 Determine if ``n0`` and ``n1`` have the same sort or not. 2272 2273 :param btor: Boolector instance. 2274 :param n0: First operand. 2275 :param n1: Second operand. 2276 :return: True if ``n0`` and ``n1`` have the same sort, and false otherwise. 2277 */ 2278 bool boolector_is_equal_sort (Btor *btor, BoolectorNode *n0, BoolectorNode *n1); 2279 2280 /*! 2281 Determine if ``sort`` is an array sort. 2282 2283 :param btor: Boolector instance. 2284 :param sort: Sort. 2285 :return: True if ``sort`` is an array sort, and false otherwise. 2286 */ 2287 bool boolector_is_array_sort (Btor *btor, BoolectorSort sort); 2288 2289 /*! 2290 Determine if ``sort`` is a bit-vector sort. 2291 2292 :param btor: Boolector instance. 2293 :param sort: Sort. 2294 :return: True if ``sort`` is a bit-vector sort, and false otherwise. 2295 */ 2296 bool boolector_is_bitvec_sort (Btor *btor, BoolectorSort sort); 2297 2298 /*! 2299 Determine if ``sort`` is a function sort. 2300 2301 :param btor: Boolector instance. 2302 :param sort: Sort. 2303 :return: True if ``sort`` is a function sort, and false otherwise. 2304 */ 2305 bool boolector_is_fun_sort (Btor *btor, BoolectorSort sort); 2306 2307 /*! 2308 Get the bit width of a bit-vector sort. 2309 2310 :param btor: Boolector instance. 2311 :param node: Boolector sort. 2312 :return: Bit width of ``sort``. 2313 */ 2314 uint32_t boolector_bitvec_sort_get_width (Btor *btor, BoolectorSort sort); 2315 2316 /*------------------------------------------------------------------------*/ 2317 2318 /*! 2319 Parse input file. 2320 2321 Input file format may be either `BTOR`_, `BTOR2`_, `SMT-LIB v1`_, or 2322 `SMT-LIB v2`_, the file type is detected automatically. If the parser 2323 encounters an error, an explanation of that error is stored in ``error_msg``. 2324 If the input file specifies a (known) status of the input formula (either sat 2325 or unsat), that status is stored in ``status``. All output (from commands 2326 like e.g. 'check-sat' in `SMT-LIB v2`_) is printed to ``outfile``. 2327 2328 :param btor: Boolector instance. 2329 :param infile: Input file. 2330 :param infile_name: Input file name. 2331 :param outfile: Output file. 2332 :param error_msg: Error message. 2333 :param status: Status of the input formula. 2334 :param parsed_smt2: Flag indicating if an SMT-LIB v2 was parsed. 2335 :return: If the input issues a call to check sat (in case of incremental 2336 SMT-LIB v1 case or SMT-LIB v2), this function returns either 2337 BOOLECTOR_SAT, BOOLECTOR_UNSAT or BOOLECTOR_UNKNOWN. Otherwise, it 2338 always returns BOOLECTOR_PARSE_UNKNOWN. If a parse error occurs the 2339 function returns BOOLECTOR_PARSE_ERROR. 2340 */ 2341 int32_t boolector_parse (Btor *btor, 2342 FILE *infile, 2343 const char *infile_name, 2344 FILE *outfile, 2345 char **error_msg, 2346 int32_t *status, 2347 bool *parsed_smt2); 2348 2349 /*! 2350 Parse input file in BTOR format. 2351 2352 See boolector_parse. 2353 2354 :param btor: Boolector instance. 2355 :param infile: Input file. 2356 :param infile_name: Input file name. 2357 :param outfile: Output file. 2358 :param error_msg: Error message. 2359 :param status: Status of the input formula. 2360 :return: BOOLECTOR_UNKNOWN or BOOLECTOR_PARSE_ERROR if a parse error 2361 occurred. 2362 */ 2363 int32_t boolector_parse_btor (Btor *btor, 2364 FILE *infile, 2365 const char *infile_name, 2366 FILE *outfile, 2367 char **error_msg, 2368 int32_t *status); 2369 2370 /*! 2371 Parse input file in BTOR2 format. 2372 2373 See boolector_parse. 2374 2375 :param btor: Boolector instance. 2376 :param infile: Input file. 2377 :param infile_name: Input file name. 2378 :param outfile: Output file. 2379 :param error_msg: Error message. 2380 :param status: Status of the input formula. 2381 :return: BOOLECTOR_UNKNOWN or BOOLECTOR_PARSE_ERROR if a parse error 2382 occurred. 2383 */ 2384 int32_t boolector_parse_btor2 (Btor *btor, 2385 FILE *infile, 2386 const char *infile_name, 2387 FILE *outfile, 2388 char **error_msg, 2389 int32_t *status); 2390 2391 /*! 2392 Parse input file in `SMT-LIB v1`_ format. 2393 2394 See boolector_parse. 2395 2396 :param btor: Boolector instance. 2397 :param infile: Input file. 2398 :param infile_name: Input file name. 2399 :param outfile: Input file. 2400 :param error_msg: Error message. 2401 :param status: Status of the input formula. 2402 :return: In the incremental case, the function returns either BOOLECTOR_SAT, 2403 BOOLECTOR_UNSAT or BOOLECTOR_UNKNOWN, otherwise it always returns 2404 BOOLECTOR_UNKNOWN. If a parse error occurs the function returns 2405 BOOLECTOR_PARSE_ERROR. 2406 */ 2407 int32_t boolector_parse_smt1 (Btor *btor, 2408 FILE *infile, 2409 const char *infile_name, 2410 FILE *outfile, 2411 char **error_msg, 2412 int32_t *status); 2413 2414 /*! 2415 Parse input file in `SMT-LIB v2`_ format. See boolector_parse. 2416 2417 :param btor: Boolector instance. 2418 :param infile: Input file. 2419 :param infile_name: Input file name. 2420 :param outfile: Output file. 2421 :param error_msg: Error message. 2422 :param status: Status of the input formula. 2423 :return: The function returns either BOOLECTOR_SAT, BOOLECTOR_UNSAT or 2424 BOOLECTOR_UNKNOWN. If a parse error occurs, the function returns 2425 BOOLECTOR_PARSE_ERROR. 2426 */ 2427 int32_t boolector_parse_smt2 (Btor *btor, 2428 FILE *infile, 2429 const char *infile_name, 2430 FILE *outfile, 2431 char **error_msg, 2432 int32_t *status); 2433 2434 /*------------------------------------------------------------------------*/ 2435 2436 /*! 2437 Recursively dump ``node`` to file in BTOR_ format. 2438 2439 :param btor: Boolector instance. 2440 :param file: File to which the expression should be dumped. The file must be 2441 have been opened by the user before. 2442 :param node: The expression which should be dumped. 2443 */ 2444 void boolector_dump_btor_node (Btor *btor, FILE *file, BoolectorNode *node); 2445 2446 /*! 2447 Dump formula to file in BTOR_ format. 2448 2449 :param btor: Boolector instance. 2450 :param file: File to which the formula should be dumped. The file must be 2451 have been opened by the user before. 2452 */ 2453 void boolector_dump_btor (Btor *btor, FILE *file); 2454 2455 /*! 2456 Recursively dump ``node`` to file in `SMT-LIB v2`_ format. 2457 2458 :param btor: Boolector instance. 2459 :param file: File to which the expression should be dumped. The file must be 2460 have been opened by the user before. 2461 :param node: The expression which should be dumped. 2462 */ 2463 void boolector_dump_smt2_node (Btor *btor, FILE *file, BoolectorNode *node); 2464 2465 /*! 2466 Dumps formula to file in `SMT-LIB v2`_ format. 2467 2468 :param btor: Boolector instance 2469 :param file: Output file. 2470 */ 2471 void boolector_dump_smt2 (Btor *btor, FILE *file); 2472 2473 /*! 2474 Dumps bit-vector formula to file in ascii AIGER format. 2475 2476 :param btor: Boolector instance 2477 :param file: Output file. 2478 :param merge_roots: Merge all roots of AIG. 2479 */ 2480 void boolector_dump_aiger_ascii (Btor *btor, FILE *file, bool merge_roots); 2481 2482 /*! 2483 Dumps bit-vector formula to file in ascii AIGER format. 2484 2485 :param btor: Boolector instance 2486 :param file: Output file. 2487 :param merge_roots: Merge all roots of AIG. 2488 */ 2489 void boolector_dump_aiger_binary (Btor *btor, FILE *file, bool merge_roots); 2490 2491 /*------------------------------------------------------------------------*/ 2492 2493 /*! 2494 Get Boolector's copyright notice. 2495 2496 :param btor: Boolector instance 2497 :return: A string with Boolector's copyright notice. 2498 */ 2499 const char *boolector_copyright (Btor *btor); 2500 2501 /*! 2502 Get Boolector's version string. 2503 2504 :param btor: Boolector instance. 2505 :return: A string with Boolector's version. 2506 */ 2507 const char *boolector_version (Btor *btor); 2508 2509 /*! 2510 Get Boolector's git id string. 2511 2512 :param btor: Boolector instance. 2513 :return: A string with Boolector's git id. 2514 */ 2515 const char *boolector_git_id (Btor *btor); 2516 2517 /*------------------------------------------------------------------------*/ 2518 #if __cplusplus 2519 } 2520 #endif 2521 #endif 2522