1 /* Boolector: Satisfiability Modulo Theories (SMT) solver. 2 * 3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file. 4 * 5 * This file is part of Boolector. 6 * See COPYING for more information on using this software. 7 */ 8 9 #ifndef BTORTYPES_H_INCLUDED 10 #define BTORTYPES_H_INCLUDED 11 12 typedef struct Btor Btor; 13 typedef struct BtorNode BtorNode; 14 15 enum BtorSolverResult 16 { 17 BTOR_RESULT_SAT = 10, 18 BTOR_RESULT_UNSAT = 20, 19 BTOR_RESULT_UNKNOWN = 0, 20 }; 21 22 typedef enum BtorSolverResult BtorSolverResult; 23 24 /* public API types */ 25 typedef struct BoolectorNode BoolectorNode; 26 27 typedef struct BoolectorAnonymous BoolectorAnonymous; 28 29 typedef BoolectorAnonymous* BoolectorSort; 30 31 /* --------------------------------------------------------------------- */ 32 /* Boolector options */ 33 /* --------------------------------------------------------------------- */ 34 35 // clang-format off 36 enum BtorOption 37 { 38 /* --------------------------------------------------------------------- */ 39 /*! 40 **General Options:** 41 */ 42 /* --------------------------------------------------------------------- */ 43 /*! 44 * **BTOR_OPT_MODEL_GEN** 45 46 | Enable (``value``: 1 or 2) or disable (``value``: 0) generation of a 47 model for satisfiable instances. 48 | There are two modes for model generation: 49 50 * generate model for asserted expressions only (``value``: 1) 51 * generate model for all expressions (``value``: 2) 52 */ 53 BTOR_OPT_MODEL_GEN, 54 55 /*! 56 * **BTOR_OPT_INCREMENTAL** 57 58 | Enable (``value``: 1) incremental mode. 59 | Note that incremental usage turns off some optimization techniques. 60 Disabling incremental usage is currently not supported. 61 */ 62 BTOR_OPT_INCREMENTAL, 63 64 /*! 65 * **BTOR_OPT_INCREMENTAL_SMT1** 66 67 | Set incremental mode for SMT-LIB v1 input. 68 69 * BTOR_INCREMENTAL_SMT1_BASIC [default]: 70 stop after first satisfiable formula 71 * BTOR_INCREMENTAL_SMT1_CONTINUE: 72 solve all formulas 73 */ 74 BTOR_OPT_INCREMENTAL_SMT1, 75 76 /*! 77 * **BTOR_OPT_INPUT_FORMAT** 78 79 | Force input file format. 80 | If unspecified, Boolector automatically detects the input file format 81 while parsing. 82 83 * BTOR_INPUT_FORMAT_BTOR: 84 `BTOR <http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf>`_ format 85 * BTOR_INPUT_FORMAT_BTOR2: 86 `BTOR2 <http://fmv.jku.at/papers/NiemetzPreinerWolfBiere-CAV18.pdf>`_ format 87 * BTOR_INPUT_FORMAT_SMT1: 88 `SMT-LIB v1 <http://smtlib.cs.uiowa.edu/papers/format-v1.2-r06.08.30.pdf>`_ format 89 * BTOR_INPUT_FORMAT_SMT2: 90 `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf>`_ format 91 */ 92 93 BTOR_OPT_INPUT_FORMAT, 94 /*! 95 * **BTOR_OPT_OUTPUT_NUMBER_FORMAT** 96 97 | Force output number format. 98 99 * BTOR_OUTPUT_BASE_BIN [default]: 100 binary 101 * BTOR_OUTPUT_BASE_HEX: 102 hexa-decimal 103 * BTOR_OUTPUT_BASE_DEC: 104 decimal 105 */ 106 BTOR_OPT_OUTPUT_NUMBER_FORMAT, 107 108 /*! 109 * **BTOR_OPT_OUTPUT_FORMAT** 110 111 | Force output file format (``value``: BTOR_: -1, `SMT-LIB v1`_: 1, 112 `SMT-LIB v2`_: 2). 113 114 * BTOR_OUTPUT_FORMAT_BTOR [default]: 115 `BTOR`_ format 116 * BTOR_OUTPUT_FORMAT_BTOR2: 117 `BTOR2`_ format 118 * BTOR_OUTPUT_FORMAT_SMT2: 119 `SMT-LIB v2`_ format 120 * BTOR_OUTPUT_FORMAT_AIGER_ASCII: 121 `Aiger ascii format <http://fmv.jku.at/papers/BiereHeljankoWieringa-FMV-TR-11-2.pdf>`_ 122 * BTOR_OUTPUT_FORMAT_AIGER_BINARY: 123 `Aiger binary format <http://fmv.jku.at/papers/BiereHeljankoWieringa-FMV-TR-11-2.pdf>`_ 124 */ 125 BTOR_OPT_OUTPUT_FORMAT, 126 127 /*! 128 * **BTOR_OPT_ENGINE** 129 130 | Set solver engine. 131 132 * BTOR_ENGINE_FUN [default]: 133 the default engine for all combinations of QF_AUFBV, uses lemmas on 134 demand for QF_AUFBV and eager bit-blasting for QF_BV 135 * BTOR_ENGINE_SLS: 136 the score-based local search QF_BV engine 137 * BTOR_ENGINE_PROP: 138 the propagation-based local search QF_BV engine 139 * BTOR_ENGINE_AIGPROP: 140 the propagation-based local search QF_BV engine that operates on the 141 bit-blasted formula (the AIG layer) 142 * BTOR_ENGINE_QUANT: 143 the quantifier engine (BV only) 144 */ 145 BTOR_OPT_ENGINE, 146 147 /*! 148 * **BTOR_OPT_SAT_ENGINE** 149 150 | Set sat solver engine. 151 | Available option values and default values depend on the sat solvers 152 configured. 153 154 * BTOR_SAT_ENGINE_CADICAL: 155 `CaDiCaL <https://fmv.jku.at/cadical>`_ 156 * BTOR_SAT_ENGINE_CMS: 157 `CryptoMiniSat <https://github.com/msoos/cryptominisat>`_ 158 * BTOR_SAT_ENGINE_LINGELING: 159 `Lingeling <https://fmv.jku.at/lingeling>`_ 160 * BTOR_SAT_ENGINE_MINISAT: 161 `MiniSat <https://github.com/niklasso/minisat>`_ 162 * BTOR_SAT_ENGINE_PICOSAT: 163 `PicoSAT <http://fmv.jku.at/picosat/>`_ 164 */ 165 BTOR_OPT_SAT_ENGINE, 166 167 /*! 168 * **BTOR_OPT_AUTO_CLEANUP** 169 170 Enable (``value``:1) or disable (``value``:0) auto cleanup of all 171 references held on exit. 172 */ 173 BTOR_OPT_AUTO_CLEANUP, 174 175 /*! 176 * **BTOR_OPT_PRETTY_PRINT** 177 178 Enable (``value``: 1) or disable (``value``: 0) pretty printing when 179 dumping. 180 */ 181 BTOR_OPT_PRETTY_PRINT, 182 183 /*! 184 * **BTOR_OPT_EXIT_CODES** 185 186 | Enable (``value``:1) or disable (``value``:0) the use of Boolector exit 187 codes (BOOLECTOR_SAT, BOOLECTOR_UNSAT, BOOLECTOR_UNKNOWN - see 188 :ref:`macros`). 189 | If disabled, on exit Boolector returns 0 if success (sat or unsat), and 190 1 in any other case. 191 */ 192 BTOR_OPT_EXIT_CODES, 193 194 /*! 195 * **BTOR_OPT_SEED** 196 197 | Set seed for Boolector's internal random number generator. 198 | Boolector uses 0 by default. 199 */ 200 BTOR_OPT_SEED, 201 202 /* 203 * **BTOR_OPT_VERBOSITY** 204 205 Set the level of verbosity. 206 */ 207 BTOR_OPT_VERBOSITY, 208 209 /* 210 * **BTOR_OPT_LOGLEVEL** 211 212 Set the log level. 213 */ 214 BTOR_OPT_LOGLEVEL, 215 216 /* --------------------------------------------------------------------- */ 217 /*! 218 **Simplifier Options:** 219 */ 220 /* --------------------------------------------------------------------- */ 221 222 /*! 223 * **BTOR_OPT_REWRITE_LEVEL** 224 225 | Set the rewrite level (``value``: 0-3) of the rewriting engine. 226 | Boolector uses rewrite level 3 by default, rewrite levels are 227 classified as follows: 228 229 * 0: no rewriting 230 * 1: term level rewriting 231 * 2: more simplification techniques 232 * 3: full rewriting/simplification 233 234 | Do not alter the rewrite level of the rewriting engine after creating 235 expressions. 236 */ 237 BTOR_OPT_REWRITE_LEVEL, 238 239 /*! 240 * **BTOR_OPT_SKELETON_PREPROC** 241 242 Enable (``value``: 1) or disable (``value``: 0) skeleton preprocessing 243 during simplification. 244 */ 245 BTOR_OPT_SKELETON_PREPROC, 246 247 /*! 248 * **BTOR_OPT_ACKERMANN** 249 250 Enable (``value``: 1) or disable (``value``: 0) the eager addition of 251 Ackermann constraints for function applications. 252 */ 253 BTOR_OPT_ACKERMANN, 254 255 /*! 256 * **BTOR_OPT_BETA_REDUCE** 257 258 Enable (``value``: 1) or disable (``value``: 0) the eager elimination of 259 lambda expressions via beta reduction. 260 */ 261 BTOR_OPT_BETA_REDUCE, 262 263 /*! 264 * **BTOR_OPT_ELIMINATE_SLICES** 265 266 Enable (``value``: 1) or disable (``value``: 0) slice elimination on bit 267 vector variables. 268 */ 269 BTOR_OPT_ELIMINATE_SLICES, 270 271 /*! 272 * **BTOR_OPT_VAR_SUBST** 273 274 Enable (``value``: 1) or disable (``value``: 0) variable substitution 275 during simplification. 276 */ 277 BTOR_OPT_VAR_SUBST, 278 279 /*! 280 * **BTOR_OPT_UCOPT** 281 282 Enable (``value``: 1) or disable (``value``: 0) unconstrained 283 optimization. 284 */ 285 BTOR_OPT_UCOPT, 286 287 /*! 288 * **BTOR_OPT_MERGE_LAMBDAS** 289 290 Enable (``value``: 1) or disable (``value``: 0) merging of lambda 291 expressions. 292 */ 293 BTOR_OPT_MERGE_LAMBDAS, 294 295 /*! 296 * **BTOR_OPT_EXTRACT_LAMBDAS** 297 298 Enable (``value``: 1) or disable (``value``: 0) extraction of common 299 array patterns as lambda terms. 300 */ 301 BTOR_OPT_EXTRACT_LAMBDAS, 302 303 /*! 304 * **BTOR_OPT_NORMALIZE** 305 306 Enable (``value``: 1) or disable (``value``: 0) normalization of 307 addition, multiplication and bit-wise and. 308 */ 309 BTOR_OPT_NORMALIZE, 310 311 /*! 312 * **BTOR_OPT_NORMALIZE_ADD** 313 314 Enable (``value``: 1) or disable (``value``: 0) normalization of 315 addition. 316 */ 317 BTOR_OPT_NORMALIZE_ADD, 318 319 /* --------------------------------------------------------------------- */ 320 /*! 321 **Fun Engine Options:** 322 */ 323 /* --------------------------------------------------------------------- */ 324 325 /*! 326 * **BTOR_OPT_FUN_PREPROP** 327 328 Enable (``value``: 1) or disable (``value``: 0) prop engine as 329 preprocessing step within sequential portfolio setting. 330 */ 331 BTOR_OPT_FUN_PREPROP, 332 333 /*! 334 * **BTOR_OPT_FUN_PRESLS** 335 336 Enable (``value``: 1) or disable (``value``: 0) sls engine as 337 preprocessing step within sequential portfolio setting. 338 */ 339 BTOR_OPT_FUN_PRESLS, 340 341 /*! 342 * **BTOR_OPT_FUN_DUAL_PROP** 343 344 Enable (``value``: 1) or disable (``value``: 0) dual propagation 345 optimization. 346 */ 347 BTOR_OPT_FUN_DUAL_PROP, 348 349 /*! 350 * **BTOR_OPT_FUN_DUAL_PROP_QSORT** 351 352 | Set order in which inputs are assumed in dual propagation clone. 353 354 * BTOR_DP_QSORT_JUST [default]: 355 order by score, highest score first 356 * BTOR_DP_QSORT_ASC: 357 order by input id, ascending 358 * BTOR_DP_QSORT_DESC: 359 order by input id, descending 360 */ 361 BTOR_OPT_FUN_DUAL_PROP_QSORT, 362 363 /*! 364 * **BTOR_OPT_FUN_JUST** 365 366 Enable (``value``: 1) or disable (``value``: 0) justification 367 optimization. 368 */ 369 BTOR_OPT_FUN_JUST, 370 371 /*! 372 * **BTOR_OPT_FUN_JUST_HEURISTIC** 373 374 | Set heuristic that determines path selection for justification 375 optimization. 376 377 * BTOR_JUST_HEUR_BRANCH_MIN_APP [default]: 378 choose branch with minimum number of applies 379 * BTOR_JUST_HEUR_BRANCH_MIN_DEP: 380 choose branch with minimum depth 381 * BTOR_JUST_HEUR_LEFT: 382 always choose left branch 383 */ 384 BTOR_OPT_FUN_JUST_HEURISTIC, 385 386 /*! 387 * **BTOR_OPT_FUN_LAZY_SYNTHESIZE** 388 389 Enable (``value``: 1) or disable (``value``: 0) lazy synthesis of bit 390 vector expressions. 391 */ 392 BTOR_OPT_FUN_LAZY_SYNTHESIZE, 393 394 /*! 395 * **BTOR_OPT_FUN_EAGER_LEMMAS** 396 397 | Select mode for eager generation lemmas. 398 399 * BTOR_FUN_EAGER_LEMMAS_NONE: 400 do not generate lemmas eagerly (generate one single lemma per 401 refinement iteration) 402 * BTOR_FUN_EAGER_LEMMAS_CONF: 403 only generate lemmas eagerly until the first conflict dependent on 404 another conflict is found 405 * BTOR_FUN_EAGER_LEMMAS_ALL: 406 in each refinement iteration, generate lemmas for all conflicts 407 */ 408 BTOR_OPT_FUN_EAGER_LEMMAS, 409 410 BTOR_OPT_FUN_STORE_LAMBDAS, 411 412 /*! 413 * **BTOR_OPT_PRINT_DIMACS** 414 415 Enable (``value``: 1) or disable (``value``: 0) DIMACS printer. 416 417 When enabled Boolector will record the CNF sent to the SAT solver and 418 prints it to stdout. 419 */ 420 BTOR_OPT_PRINT_DIMACS, 421 422 423 /* --------------------------------------------------------------------- */ 424 /*! 425 **SLS Engine Options:** 426 */ 427 /* --------------------------------------------------------------------- */ 428 429 /*! 430 * **BTOR_OPT_SLS_NFIPS** 431 Set the number of bit flips used as a limit for the sls engine. Disabled 432 if 0. 433 */ 434 BTOR_OPT_SLS_NFLIPS, 435 436 /*! 437 * **BTOR_OPT_SLS_STRATEGY** 438 439 | Select move strategy for SLS engine. 440 441 * BTOR_SLS_STRAT_BEST_MOVE: 442 always choose best score improving move 443 * BTOR_SLS_STRAT_RAND_WALK: 444 always choose random walk weighted by score 445 * BTOR_SLS_STRAT_FIRST_BEST_MOVE [default]: 446 always choose first best move (no matter if any other move is better) 447 * BTOR_SLS_STRAT_BEST_SAME_MOVE: 448 determine move as best move even if its score is not better but the 449 same as the score of the previous best move 450 * BTOR_SLS_STRAT_ALWAYS_PROP: 451 always choose propagation move (and recover with SLS move in case of 452 conflict) 453 */ 454 BTOR_OPT_SLS_STRATEGY, 455 456 /*! 457 * **BTOR_OPT_SLS_JUST** 458 459 Enable (``value``: 1) or disable (``value``: 0) justification based path 460 selection during candidate selection. 461 */ 462 BTOR_OPT_SLS_JUST, 463 464 /*! 465 * **BTOR_OPT_SLS_MOVE_GW** 466 467 Enable (``value``: 1) or disable (``value``: 0) group-wise moves, where 468 rather than changing the assignment of one single candidate variable, all 469 candidate variables are set at the same time (using the same strategy). 470 */ 471 BTOR_OPT_SLS_MOVE_GW, 472 473 /*! 474 * **BTOR_OPT_SLS_MOVE_RANGE** 475 476 Enable (``value``: 1) or disable (``value``: 0) range-wise bit-flip 477 moves, where the bits within all ranges from 2 to the bit width (starting 478 from the LSB) are flipped at once. 479 */ 480 BTOR_OPT_SLS_MOVE_RANGE, 481 482 /*! 483 * **BTOR_OPT_SLS_MOVE_SEGMENT** 484 485 Enable (``value``: 1) or disable (``value``: 0) segment-wise bit-flip 486 moves, where the bits within segments of multiples of 2 are flipped at 487 once. 488 */ 489 BTOR_OPT_SLS_MOVE_SEGMENT, 490 491 /*! 492 * **BTOR_OPT_SLS_MOVE_RAND_WALK** 493 494 Enable (``value``: 1) or disable (``value``: 0) random walk moves, where 495 one out of all possible neighbors is randomly selected (with given 496 probability, see BTOR_OPT_SLS_PROB_MOVE_RAND_WALK) for a randomly 497 selected candidate variable. 498 */ 499 BTOR_OPT_SLS_MOVE_RAND_WALK, 500 501 /*! 502 * **BTOR_OPT_SLS_PROB_MOVE_RAND_WALK** 503 504 Set the probability with which a random walk is chosen if random walks 505 are enabled (see BTOR_OPT_SLS_MOVE_RAND_WALK). 506 */ 507 BTOR_OPT_SLS_PROB_MOVE_RAND_WALK, 508 509 /*! 510 * **BTOR_OPT_SLS_MOVE_RAND_ALL** 511 512 Enable (``value``: 1) or disable (``value``: 0) the randomization of all 513 candidate variables (rather than a single randomly selected candidate 514 variable) in case no best move has been found. 515 */ 516 BTOR_OPT_SLS_MOVE_RAND_ALL, 517 518 /*! 519 * **BTOR_OPT_SLS_MOVE_RAND_RANGE** 520 521 Enable (``value``: 1) or disable (``value``: 0) the randomization of bit 522 ranges (rather than all bits) of a candidate variable(s) to be randomized 523 in case no best move has been found. 524 */ 525 BTOR_OPT_SLS_MOVE_RAND_RANGE, 526 527 /*! 528 * **BTOR_OPT_SLS_MOVE_PROP** 529 530 Enable (``value``: 1) or disable (``value``: 0) propagation moves (chosen 531 with a given ratio of number of propagation moves to number of regular 532 SLS moves, see BTOR_OPT_SLS_MOVE_PROP_N_PROP and 533 BTOR_OPT_SLS_MOVE_PROP_N_SLS). 534 */ 535 BTOR_OPT_SLS_MOVE_PROP, 536 537 /*! 538 * **BTOR_OPT_SLS_MOVE_PROP_N_PROP** 539 540 Set the number of propagation moves to be performed when propagation 541 moves are enabled (propagation moves are chosen with a ratio of 542 propagation moves to regular SLS moves, see BTOR_OPT_SLS_MOVE_PROP and 543 BTOR_OPT_SLS_MOVE_PROP_N_SLS). 544 */ 545 BTOR_OPT_SLS_MOVE_PROP_N_PROP, 546 547 /*! 548 * **BTOR_OPT_SLS_MOVE_PROP_N_SLS** 549 550 Set the number of regular SLS moves to be performed when propagation 551 moves are enabled (propagation moves are chosen with a ratio of 552 propagation moves to regular SLS moves, see BTOR_OPT_SLS_MOVE_PROP and 553 BTOR_OPT_SLS_MOVE_PROP_N_PROP). 554 */ 555 BTOR_OPT_SLS_MOVE_PROP_N_SLS, 556 557 /*! 558 * **BTOR_OPT_SLS_MOVE_PROP_FORCE_RW** 559 560 Enable (``value``: 1) or disable (``value``: 0) that random walks are 561 forcibly chosen as recovery moves in case of conflicts when a propagation 562 move is performed (rather than performing a regular SLS move). 563 */ 564 BTOR_OPT_SLS_MOVE_PROP_FORCE_RW, 565 566 /*! 567 * **BTOR_OPT_SLS_MOVE_INC_MOVE_TEST** 568 569 Enable (``value``: 1) or disable (``value``: 0) that during best move 570 selection, if the current candidate variable with a previous neighbor 571 yields the currently best score, this neighbor assignment is used as a 572 base for further neighborhood exploration (rather than its current 573 assignment). 574 */ 575 BTOR_OPT_SLS_MOVE_INC_MOVE_TEST, 576 577 /*! 578 * **BTOR_OPT_SLS_MOVE_RESTARTS** 579 580 Enable (``value``: 1) or disable (``value``: 0) restarts. 581 */ 582 BTOR_OPT_SLS_USE_RESTARTS, 583 584 /*! 585 * **BTOR_OPT_SLS_MOVE_RESTARTS** 586 587 | Enable (``value``: 1) or disable (``value``: 0) heuristic (bandit 588 scheme) for selecting root constraints. 589 | If disabled, candidate root constraints are selected randomly. 590 */ 591 BTOR_OPT_SLS_USE_BANDIT, 592 593 /* --------------------------------------------------------------------- */ 594 /*! 595 **Prop Engine Options**: 596 */ 597 /* --------------------------------------------------------------------- */ 598 599 /*! 600 * **BTOR_OPT_PROP_NPROPS** 601 602 Set the number of propagation (steps) used as a limit for the propagation 603 engine. Disabled if 0. 604 */ 605 BTOR_OPT_PROP_NPROPS, 606 607 /*! 608 * **BTOR_OPT_PROP_USE_RESTARTS** 609 610 Enable (``value``: 1) or disable (``value``: 0) restarts. 611 */ 612 BTOR_OPT_PROP_USE_RESTARTS, 613 614 /*! 615 * **BTOR_OPT_PROP_USE_RESTARTS** 616 617 | Enable (``value``: 1) or disable (``value``: 0) heuristic (bandit 618 scheme) for selecting root constraints. 619 | If enabled, root constraint selection via bandit scheme is based on a 620 scoring scheme similar to the one employed in the SLS engine. 621 | If disabled, candidate root constraints are selected randomly. 622 */ 623 BTOR_OPT_PROP_USE_BANDIT, 624 625 /*! 626 * **BTOR_OPT_PROP_PATH_SEL** 627 628 Select mode for path selection. 629 630 * BTOR_PROP_PATH_SEL_CONTROLLING: 631 select path based on controlling inputs 632 * BTOR_PROP_PATH_SEL_ESSENTIAL [default]: 633 select path based on essential inputs 634 * BTOR_PROP_PATH_SEL_RANDOM: 635 select path based on random inputs 636 */ 637 BTOR_OPT_PROP_PATH_SEL, 638 639 /*! 640 * **BTOR_OPT_PROP_PROB_USE_INV_VALUE** 641 642 Set probabiality with which to choose inverse values over consistent 643 values. 644 */ 645 BTOR_OPT_PROP_PROB_USE_INV_VALUE, 646 647 /*! 648 * **BTOR_OPT_PROP_PROB_FLIP_COND** 649 650 Set probability with which to select the path to the condition (in case of 651 an if-then-else operation) rather than the enabled branch during down 652 propagation. 653 */ 654 BTOR_OPT_PROP_PROB_FLIP_COND, 655 656 /*! 657 * **BTOR_OPT_PROP_PROB_FLIP_COND_CONST** 658 659 Set probbiality with which to select the path to the condition (in case of 660 an if-then-else operation) rather than the enabled branch during down 661 propagation if either of the 'then' or 'else' branch is constant. 662 */ 663 BTOR_OPT_PROP_PROB_FLIP_COND_CONST, 664 665 /*! 666 * **BTOR_OPT_PROP_FLIP_COND_CONST_DELTA** 667 668 Set delta by which BTOR_OPT_PROP_PROB_FLIP_COND_CONST is decreased or 669 increased after a limit BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL is reached. 670 */ 671 BTOR_OPT_PROP_FLIP_COND_CONST_DELTA, 672 673 /*! 674 * **BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL** 675 676 Set the limit for how often the path to the condition (in case of an 677 if-then-else operation) may be selected bevor 678 BTOR_OPT_PROP_PROB_FLIP_COND_CONST is decreased or increased by 679 BTOR_OPT_PROP_PROB_FLIP_COND_CONST_DELTA. 680 */ 681 BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL, 682 683 /*! 684 * **BTOR_OPT_PROP_PROB_SLICE_KEEP_DC** 685 686 Set probability with which to keep the current value of the don't care 687 bits of a slice operation (rather than fully randomizing all of them) 688 when selecting an inverse or consistent value. 689 */ 690 BTOR_OPT_PROP_PROB_SLICE_KEEP_DC, 691 692 /*! 693 * **BTOR_OPT_PROP_PROB_CONC_FLIP** 694 695 Set probability with which to use the corresponing slice of current 696 assignment with max. one of its bits flipped (rather than using the 697 corresponding slice of the down propagated assignment) as result of 698 consistent value selection for concats. 699 */ 700 BTOR_OPT_PROP_PROB_CONC_FLIP, 701 702 /*! 703 * **BTOR_OPT_PROP_PROB_SLICE_FLIP** 704 705 Set probability with which to use the current assignment of the operand of 706 a slice operation with one of the don't care bits flipped (rather than 707 fully randomizing all of them, both for inverse and consistent value 708 selection) if their current assignment is not kept (see 709 BTOR_OPT_PROP_PROB_SLICE_KEEP_DC). 710 */ 711 BTOR_OPT_PROP_PROB_SLICE_FLIP, 712 713 /*! 714 * **BTOR_OPT_PROP_PROB_EQ_FLIP** 715 716 Set probability with which the current assignment of the selected node 717 with one of its bits flipped (rather than a fully randomized bit-vector) 718 is down-propagated in case of an inequality (both for inverse and 719 consistent value selection). 720 */ 721 BTOR_OPT_PROP_PROB_EQ_FLIP, 722 723 /*! 724 * **BTOR_OPT_PROP_PROB_AND_FLIP** 725 726 Set probability with which the current assignment of the don't care bits 727 of the selected node with max. one of its bits flipped (rather than fully 728 randomizing all of them) in case of an and operation (for both inverse and 729 consistent value selection). 730 731 */ 732 BTOR_OPT_PROP_PROB_AND_FLIP, 733 734 /*! 735 * **BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT** 736 737 | Do not perform a propagation move when running into a conflict during 738 inverse computation. 739 | (This is the default behavior for the SLS engine when propagation moves 740 are enabled, where a conflict triggers a recovery by means of a regular 741 SLS move.) 742 */ 743 BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT, 744 745 /* --------------------------------------------------------------------- */ 746 /*! 747 **AIGProp Engine Options**: 748 */ 749 /* --------------------------------------------------------------------- */ 750 751 /*! 752 * **BTOR_OPT_AIGPROP_USE_RESTARTS** 753 754 Enable (``value``: 1) or disable (``value``: 0) restarts. 755 */ 756 BTOR_OPT_AIGPROP_USE_RESTARTS, 757 758 /*! 759 * **BTOR_OPT_AIGPROP_USE_RESTARTS** 760 761 | Enable (``value``: 1) or disable (``value``: 0) heuristic (bandit 762 scheme) for selecting root constraints. 763 | If enabled, root constraint selection via bandit scheme is based on a 764 scoring scheme similar to the one employed in the SLS engine. 765 | If disabled, candidate root constraints are selected randomly. 766 */ 767 BTOR_OPT_AIGPROP_USE_BANDIT, 768 769 /* QUANT engine ------------------------------------------------------- */ 770 /*! 771 * **BTOR_OPT_QUANT_SYNTH** 772 773 Select synthesis mode for Skolem functions. 774 775 * BTOR_QUANT_SYNTH_NONE: 776 do not synthesize skolem functions (use model values for instantiation) 777 * BTOR_QUANT_SYNTH_EL: 778 use enumerative learning to synthesize skolem functions 779 * BTOR_QUANT_SYNTH_ELMC: 780 use enumerative learning modulo the predicates in the cone of influence 781 of the existential variables to synthesize skolem functions 782 * BTOR_QUANT_SYNTH_EL_ELMC: 783 chain BTOR_QUANT_SYNTH_EL and BTOR_QUANT_SYNTH_ELMC approaches to 784 synthesize skolem functions 785 * BTOR_QUANT_SYNTH_ELMR: 786 use enumerative learning modulo the given root constraints to synthesize 787 skolem functions 788 */ 789 BTOR_OPT_QUANT_SYNTH, 790 791 /*! 792 * **BTOR_OPT_QUANT_DUAL_SOLVER** 793 794 Enable (``value``: 1) or disable (``value``: 0) solving the dual 795 (negated) version of the quantified bit-vector formula. 796 */ 797 BTOR_OPT_QUANT_DUAL_SOLVER, 798 799 /*! 800 * **BTOR_OPT_QUANT_SYNTH_LIMIT** 801 802 Set the limit of enumerated expressions for the enumerative learning 803 synthesis algorithm. 804 */ 805 BTOR_OPT_QUANT_SYNTH_LIMIT, 806 807 /*! 808 * **BTOR_OPT_SYNTH_QI** 809 810 Enable (``value``: 1) or disable (``value``: 0) generalization of 811 quantifier instantiations via enumerative learning. 812 */ 813 BTOR_OPT_QUANT_SYNTH_QI, 814 815 /*! 816 * **BTOR_OPT_QUANT_DER** 817 818 Enable (``value``: 1) or disable (``value``: 0) destructive equality 819 resolution simplification. 820 */ 821 BTOR_OPT_QUANT_DER, 822 823 /*! 824 * **BTOR_OPT_QUANT_CER** 825 826 Enable (``value``: 1) or disable (``value``: 0) constructive equality 827 resolution simplification. 828 */ 829 BTOR_OPT_QUANT_CER, 830 831 /*! 832 * **BTOR_OPT_QUANT_MINISCOPE** 833 834 Enable (``value``: 1) or disable (``value``: 0) miniscoping. 835 */ 836 BTOR_OPT_QUANT_MINISCOPE, 837 838 /* internal options --------------------------------------------------- */ 839 840 BTOR_OPT_SORT_EXP, 841 BTOR_OPT_SORT_AIG, 842 BTOR_OPT_SORT_AIGVEC, 843 BTOR_OPT_AUTO_CLEANUP_INTERNAL, 844 BTOR_OPT_SIMPLIFY_CONSTRAINTS, 845 BTOR_OPT_CHK_FAILED_ASSUMPTIONS, 846 BTOR_OPT_CHK_MODEL, 847 BTOR_OPT_CHK_UNCONSTRAINED, 848 BTOR_OPT_PARSE_INTERACTIVE, 849 BTOR_OPT_SAT_ENGINE_LGL_FORK, 850 BTOR_OPT_SAT_ENGINE_CADICAL_FREEZE, 851 BTOR_OPT_SAT_ENGINE_N_THREADS, 852 BTOR_OPT_SIMP_NORMAMLIZE_ADDERS, 853 BTOR_OPT_DECLSORT_BV_WIDTH, 854 BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE, 855 BTOR_OPT_QUANT_FIXSYNTH, 856 BTOR_OPT_RW_ZERO_LOWER_SLICE, 857 BTOR_OPT_NONDESTR_SUBST, 858 /* this MUST be the last entry! */ 859 BTOR_OPT_NUM_OPTS, 860 }; 861 // clang-format on 862 863 typedef enum BtorOption BtorOption; 864 865 /* --------------------------------------------------------------------- */ 866 /* Boolector option values */ 867 /* --------------------------------------------------------------------- */ 868 869 /* Note: enums with NONE values should start with NONE = 0. If there is no NONE 870 * value the enum range should start with 1. This allows us to determine if an 871 * option is set by checking if it is > 0. */ 872 873 enum BtorOptSatEngine 874 { 875 BTOR_SAT_ENGINE_LINGELING, 876 BTOR_SAT_ENGINE_PICOSAT, 877 BTOR_SAT_ENGINE_MINISAT, 878 BTOR_SAT_ENGINE_CADICAL, 879 BTOR_SAT_ENGINE_CMS, 880 }; 881 typedef enum BtorOptSatEngine BtorOptSatEngine; 882 883 enum BtorOptEngine 884 { 885 BTOR_ENGINE_FUN = 1, 886 BTOR_ENGINE_SLS, 887 BTOR_ENGINE_PROP, 888 BTOR_ENGINE_AIGPROP, 889 BTOR_ENGINE_QUANT, 890 }; 891 typedef enum BtorOptEngine BtorOptEngine; 892 893 enum BtorOptInputFormat 894 { 895 BTOR_INPUT_FORMAT_NONE, 896 BTOR_INPUT_FORMAT_BTOR, 897 BTOR_INPUT_FORMAT_BTOR2, 898 BTOR_INPUT_FORMAT_SMT1, 899 BTOR_INPUT_FORMAT_SMT2, 900 }; 901 typedef enum BtorOptInputFormat BtorOptInputFormat; 902 903 enum BtorOptOutputBase 904 { 905 BTOR_OUTPUT_BASE_BIN = 1, 906 BTOR_OUTPUT_BASE_HEX, 907 BTOR_OUTPUT_BASE_DEC, 908 }; 909 typedef enum BtorOptOutputBase BtorOptOutputBase; 910 911 enum BtorOptOutputFormat 912 { 913 BTOR_OUTPUT_FORMAT_NONE, 914 BTOR_OUTPUT_FORMAT_BTOR = 1, 915 // BTOR_OUTPUT_FORMAT_BTOR2, 916 BTOR_OUTPUT_FORMAT_SMT2, 917 BTOR_OUTPUT_FORMAT_AIGER_ASCII, 918 BTOR_OUTPUT_FORMAT_AIGER_BINARY, 919 }; 920 typedef enum BtorOptOutputFormat BtorOptOutputFormat; 921 922 enum BtorOptDPQsort 923 { 924 BTOR_DP_QSORT_JUST = 1, 925 BTOR_DP_QSORT_ASC, 926 BTOR_DP_QSORT_DESC, 927 }; 928 typedef enum BtorOptDPQsort BtorOptDPQsort; 929 930 enum BtorOptJustHeur 931 { 932 BTOR_JUST_HEUR_BRANCH_LEFT = 1, 933 BTOR_JUST_HEUR_BRANCH_MIN_APP, 934 BTOR_JUST_HEUR_BRANCH_MIN_DEP, 935 }; 936 typedef enum BtorOptJustHeur BtorOptJustHeur; 937 938 enum BtorOptSLSStrat 939 { 940 BTOR_SLS_STRAT_BEST_MOVE = 1, 941 BTOR_SLS_STRAT_RAND_WALK, 942 BTOR_SLS_STRAT_FIRST_BEST_MOVE, 943 BTOR_SLS_STRAT_BEST_SAME_MOVE, 944 BTOR_SLS_STRAT_ALWAYS_PROP, 945 }; 946 typedef enum BtorOptSLSStrat BtorOptSLSStrat; 947 948 enum BtorOptPropPathSel 949 { 950 BTOR_PROP_PATH_SEL_CONTROLLING = 1, 951 BTOR_PROP_PATH_SEL_ESSENTIAL, 952 BTOR_PROP_PATH_SEL_RANDOM, 953 }; 954 typedef enum BtorOptPropPathSel BtorOptPropPathSel; 955 956 enum BtorOptQuantSynth 957 { 958 BTOR_QUANT_SYNTH_NONE, 959 BTOR_QUANT_SYNTH_EL, 960 BTOR_QUANT_SYNTH_ELMC, 961 BTOR_QUANT_SYNTH_EL_ELMC, 962 BTOR_QUANT_SYNTH_ELMR, 963 }; 964 typedef enum BtorOptQuantSynth BtorOptQuantSynt; 965 966 enum BtorOptFunEagerLemmas 967 { 968 BTOR_FUN_EAGER_LEMMAS_NONE, 969 BTOR_FUN_EAGER_LEMMAS_CONF, 970 BTOR_FUN_EAGER_LEMMAS_ALL, 971 }; 972 typedef enum BtorOptFunEagerLemmas BtorOptFunEagerLemmas; 973 974 enum BtorOptIncrementalSMT1 975 { 976 BTOR_INCREMENTAL_SMT1_BASIC = 1, 977 BTOR_INCREMENTAL_SMT1_CONTINUE, 978 }; 979 typedef enum BtorOptIncrementalSMT1 BtorOptIncrementalSMT1; 980 981 enum BtorOptBetaReduceMode 982 { 983 BTOR_BETA_REDUCE_NONE, 984 BTOR_BETA_REDUCE_FUN, 985 BTOR_BETA_REDUCE_ALL, 986 }; 987 typedef enum BtorOptBetaReduceMode BtorOptBetaReduceMode; 988 989 /* --------------------------------------------------------------------- */ 990 991 /* Callback function to be executed on abort, primarily intended to be used for 992 * plugging in exception handling. */ 993 struct BtorAbortCallback 994 { 995 void (*abort_fun) (const char* msg); 996 void *cb_fun; /* abort callback function */ 997 }; 998 typedef struct BtorAbortCallback BtorAbortCallback; 999 1000 extern BtorAbortCallback btor_abort_callback; 1001 1002 #endif 1003