1id = "QUANTIFIERS" 2name = "Quantifiers" 3header = "options/quantifiers_options.h" 4 5# Whether to mini-scope quantifiers. 6# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to 7# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) 8[[option]] 9 name = "miniscopeQuant" 10 category = "regular" 11 long = "miniscope-quant" 12 type = "bool" 13 default = "true" 14 help = "miniscope quantifiers" 15 16# Whether to mini-scope quantifiers based on formulas with no free variables. 17# For example, forall x. ( P( x ) V Q ) will be rewritten to 18# ( forall x. P( x ) ) V Q 19[[option]] 20 name = "miniscopeQuantFreeVar" 21 category = "regular" 22 long = "miniscope-quant-fv" 23 type = "bool" 24 default = "true" 25 help = "miniscope quantifiers for ground subformulas" 26 27[[option]] 28 name = "quantSplit" 29 category = "regular" 30 long = "quant-split" 31 type = "bool" 32 default = "true" 33 help = "apply splitting to quantified formulas based on variable disjoint disjuncts" 34 35[[option]] 36 name = "prenexQuant" 37 category = "regular" 38 long = "prenex-quant=MODE" 39 type = "CVC4::theory::quantifiers::PrenexQuantMode" 40 default = "CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE" 41 handler = "stringToPrenexQuantMode" 42 includes = ["options/quantifiers_modes.h"] 43 help = "prenex mode for quantified formulas" 44 45[[option]] 46 name = "prenexQuantUser" 47 category = "regular" 48 long = "prenex-quant-user" 49 type = "bool" 50 default = "false" 51 help = "prenex quantified formulas with user patterns" 52 53# Whether to variable-eliminate quantifiers. 54# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to 55# forall y. P( c, y ) 56[[option]] 57 name = "varElimQuant" 58 category = "regular" 59 long = "var-elim-quant" 60 type = "bool" 61 default = "true" 62 read_only = true 63 help = "enable simple variable elimination for quantified formulas" 64 65[[option]] 66 name = "varIneqElimQuant" 67 category = "regular" 68 long = "var-ineq-elim-quant" 69 type = "bool" 70 default = "true" 71 read_only = true 72 help = "enable variable elimination based on infinite projection of unbound arithmetic variables" 73 74[[option]] 75 name = "dtVarExpandQuant" 76 category = "regular" 77 long = "dt-var-exp-quant" 78 type = "bool" 79 default = "true" 80 read_only = true 81 help = "expand datatype variables bound to one constructor in quantifiers" 82 83[[option]] 84 name = "iteLiftQuant" 85 category = "regular" 86 long = "ite-lift-quant=MODE" 87 type = "CVC4::theory::quantifiers::IteLiftQuantMode" 88 default = "CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE" 89 handler = "stringToIteLiftQuantMode" 90 includes = ["options/quantifiers_modes.h"] 91 help = "ite lifting mode for quantified formulas" 92 93[[option]] 94 name = "condVarSplitQuant" 95 category = "regular" 96 long = "cond-var-split-quant" 97 type = "bool" 98 default = "true" 99 read_only = true 100 help = "split quantified formulas that lead to variable eliminations" 101 102[[option]] 103 name = "condVarSplitQuantAgg" 104 category = "regular" 105 long = "cond-var-split-agg-quant" 106 type = "bool" 107 default = "false" 108 read_only = true 109 help = "aggressive split quantified formulas that lead to variable eliminations" 110 111[[option]] 112 name = "iteDtTesterSplitQuant" 113 category = "regular" 114 long = "ite-dtt-split-quant" 115 type = "bool" 116 default = "false" 117 help = "split ites with dt testers as conditions" 118 119# Whether to pre-skolemize quantifier bodies. 120# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to 121# forall x. P( x ) => f( S( x ) ) = x 122[[option]] 123 name = "preSkolemQuant" 124 category = "regular" 125 long = "pre-skolem-quant" 126 type = "bool" 127 default = "false" 128 help = "apply skolemization eagerly to bodies of quantified formulas" 129 130[[option]] 131 name = "preSkolemQuantNested" 132 category = "regular" 133 long = "pre-skolem-quant-nested" 134 type = "bool" 135 default = "true" 136 help = "apply skolemization to nested quantified formulas" 137 138[[option]] 139 name = "preSkolemQuantAgg" 140 category = "regular" 141 long = "pre-skolem-quant-agg" 142 type = "bool" 143 default = "true" 144 help = "apply skolemization to quantified formulas aggressively" 145 146[[option]] 147 name = "aggressiveMiniscopeQuant" 148 category = "regular" 149 long = "ag-miniscope-quant" 150 type = "bool" 151 default = "false" 152 read_only = true 153 help = "perform aggressive miniscoping for quantifiers" 154 155[[option]] 156 name = "elimTautQuant" 157 category = "regular" 158 long = "elim-taut-quant" 159 type = "bool" 160 default = "true" 161 read_only = true 162 help = "eliminate tautological disjuncts of quantified formulas" 163 164[[option]] 165 name = "elimExtArithQuant" 166 category = "regular" 167 long = "elim-ext-arith-quant" 168 type = "bool" 169 default = "true" 170 help = "eliminate extended arithmetic symbols in quantified formulas" 171 172[[option]] 173 name = "condRewriteQuant" 174 category = "regular" 175 long = "cond-rewrite-quant" 176 type = "bool" 177 default = "true" 178 read_only = true 179 help = "conditional rewriting of quantified formulas" 180 181[[option]] 182 name = "globalNegate" 183 category = "regular" 184 long = "global-negate" 185 type = "bool" 186 default = "false" 187 help = "do global negation of input formula" 188 189#### E-matching options 190 191[[option]] 192 name = "eMatching" 193 category = "regular" 194 long = "e-matching" 195 type = "bool" 196 default = "true" 197 help = "whether to do heuristic E-matching" 198 199[[option]] 200 name = "termDbMode" 201 category = "regular" 202 long = "term-db-mode=MODE" 203 type = "CVC4::theory::quantifiers::TermDbMode" 204 default = "CVC4::theory::quantifiers::TERM_DB_ALL" 205 handler = "stringToTermDbMode" 206 includes = ["options/quantifiers_modes.h"] 207 help = "which ground terms to consider for instantiation" 208 209[[option]] 210 name = "registerQuantBodyTerms" 211 category = "regular" 212 long = "register-quant-body-terms" 213 type = "bool" 214 default = "false" 215 read_only = true 216 help = "consider ground terms within bodies of quantified formulas for matching" 217 218[[option]] 219 name = "inferArithTriggerEq" 220 category = "regular" 221 long = "infer-arith-trigger-eq" 222 type = "bool" 223 default = "false" 224 read_only = true 225 help = "infer equalities for trigger terms based on solving arithmetic equalities" 226 227[[option]] 228 name = "strictTriggers" 229 category = "regular" 230 long = "strict-triggers" 231 type = "bool" 232 default = "false" 233 read_only = true 234 help = "only instantiate quantifiers with user patterns based on triggers" 235 236[[option]] 237 name = "relevantTriggers" 238 category = "regular" 239 long = "relevant-triggers" 240 type = "bool" 241 default = "false" 242 read_only = true 243 help = "prefer triggers that are more relevant based on SInE style analysis" 244 245[[option]] 246 name = "relationalTriggers" 247 category = "regular" 248 long = "relational-triggers" 249 type = "bool" 250 default = "false" 251 read_only = true 252 help = "choose relational triggers such as x = f(y), x >= f(y)" 253 254[[option]] 255 name = "purifyTriggers" 256 category = "regular" 257 long = "purify-triggers" 258 type = "bool" 259 default = "false" 260 help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1" 261 262[[option]] 263 name = "purifyDtTriggers" 264 category = "regular" 265 long = "purify-dt-triggers" 266 type = "bool" 267 default = "false" 268 help = "purify dt triggers, match all constructors of correct form instead of selectors" 269 270[[option]] 271 name = "pureThTriggers" 272 category = "regular" 273 long = "pure-th-triggers" 274 type = "bool" 275 default = "false" 276 help = "use pure theory terms as single triggers" 277 278[[option]] 279 name = "partialTriggers" 280 category = "regular" 281 long = "partial-triggers" 282 type = "bool" 283 default = "false" 284 help = "use triggers that do not contain all free variables" 285 286[[option]] 287 name = "multiTriggerWhenSingle" 288 category = "regular" 289 long = "multi-trigger-when-single" 290 type = "bool" 291 default = "false" 292 read_only = true 293 help = "select multi triggers when single triggers exist" 294 295[[option]] 296 name = "multiTriggerPriority" 297 category = "regular" 298 long = "multi-trigger-priority" 299 type = "bool" 300 default = "false" 301 read_only = true 302 help = "only try multi triggers if single triggers give no instantiations" 303 304[[option]] 305 name = "multiTriggerCache" 306 category = "regular" 307 long = "multi-trigger-cache" 308 type = "bool" 309 default = "false" 310 read_only = true 311 help = "caching version of multi triggers" 312 313[[option]] 314 name = "multiTriggerLinear" 315 category = "regular" 316 long = "multi-trigger-linear" 317 type = "bool" 318 default = "true" 319 read_only = true 320 help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms" 321 322[[option]] 323 name = "triggerSelMode" 324 category = "regular" 325 long = "trigger-sel=MODE" 326 type = "CVC4::theory::quantifiers::TriggerSelMode" 327 default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN" 328 handler = "stringToTriggerSelMode" 329 includes = ["options/quantifiers_modes.h"] 330 help = "selection mode for triggers" 331 332[[option]] 333 name = "triggerActiveSelMode" 334 category = "regular" 335 long = "trigger-active-sel=MODE" 336 type = "CVC4::theory::quantifiers::TriggerActiveSelMode" 337 default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL" 338 handler = "stringToTriggerActiveSelMode" 339 includes = ["options/quantifiers_modes.h"] 340 help = "selection mode to activate triggers" 341 342[[option]] 343 name = "userPatternsQuant" 344 category = "regular" 345 long = "user-pat=MODE" 346 type = "CVC4::theory::quantifiers::UserPatMode" 347 default = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST" 348 handler = "stringToUserPatMode" 349 includes = ["options/quantifiers_modes.h"] 350 help = "policy for handling user-provided patterns for quantifier instantiation" 351 352[[option]] 353 name = "incrementTriggers" 354 category = "regular" 355 long = "increment-triggers" 356 type = "bool" 357 default = "true" 358 read_only = true 359 help = "generate additional triggers as needed during search" 360 361[[option]] 362 name = "instWhenMode" 363 category = "regular" 364 long = "inst-when=MODE" 365 type = "CVC4::theory::quantifiers::InstWhenMode" 366 default = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL" 367 handler = "stringToInstWhenMode" 368 predicates = ["checkInstWhenMode"] 369 includes = ["options/quantifiers_modes.h"] 370 help = "when to apply instantiation" 371 372[[option]] 373 name = "instWhenStrictInterleave" 374 category = "regular" 375 long = "inst-when-strict-interleave" 376 type = "bool" 377 default = "true" 378 help = "ensure theory combination and standard quantifier effort strategies take turns" 379 380[[option]] 381 name = "instWhenPhase" 382 category = "regular" 383 long = "inst-when-phase=N" 384 type = "int" 385 default = "2" 386 help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen" 387 388[[option]] 389 name = "instWhenTcFirst" 390 category = "regular" 391 long = "inst-when-tc-first" 392 type = "bool" 393 default = "true" 394 help = "allow theory combination to happen once initially, before quantifier strategies are run" 395 396[[option]] 397 name = "quantModelEe" 398 category = "regular" 399 long = "quant-model-ee" 400 type = "bool" 401 default = "false" 402 read_only = true 403 help = "use equality engine of model for last call effort" 404 405[[option]] 406 name = "instMaxLevel" 407 category = "regular" 408 long = "inst-max-level=N" 409 type = "int" 410 default = "-1" 411 help = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)" 412 413[[option]] 414 name = "instLevelInputOnly" 415 category = "regular" 416 long = "inst-level-input-only" 417 type = "bool" 418 default = "true" 419 read_only = true 420 help = "only input terms are assigned instantiation level zero" 421 422[[option]] 423 name = "quantRepMode" 424 category = "regular" 425 long = "quant-rep-mode=MODE" 426 type = "CVC4::theory::quantifiers::QuantRepMode" 427 default = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST" 428 handler = "stringToQuantRepMode" 429 includes = ["options/quantifiers_modes.h"] 430 help = "selection mode for representatives in quantifiers engine" 431 432[[option]] 433 name = "fullSaturateQuant" 434 category = "regular" 435 long = "full-saturate-quant" 436 type = "bool" 437 default = "false" 438 help = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown" 439 440[[option]] 441 name = "fullSaturateQuantRd" 442 category = "regular" 443 long = "full-saturate-quant-rd" 444 type = "bool" 445 default = "true" 446 read_only = true 447 help = "whether to use relevant domain first for full saturation instantiation strategy" 448 449[[option]] 450 name = "fullSaturateInterleave" 451 category = "regular" 452 long = "fs-interleave" 453 type = "bool" 454 default = "false" 455 read_only = true 456 help = "interleave full saturate instantiation with other techniques" 457 458[[option]] 459 name = "literalMatchMode" 460 category = "regular" 461 long = "literal-matching=MODE" 462 type = "CVC4::theory::quantifiers::LiteralMatchMode" 463 default = "CVC4::theory::quantifiers::LITERAL_MATCH_USE" 464 handler = "stringToLiteralMatchMode" 465 predicates = ["checkLiteralMatchMode"] 466 includes = ["options/quantifiers_modes.h"] 467 read_only = true 468 help = "choose literal matching mode" 469 470### Finite model finding options 471 472[[option]] 473 name = "finiteModelFind" 474 category = "regular" 475 long = "finite-model-find" 476 type = "bool" 477 default = "false" 478 help = "use finite model finding heuristic for quantifier instantiation" 479 480[[option]] 481 name = "quantFunWellDefined" 482 category = "regular" 483 long = "quant-fun-wd" 484 type = "bool" 485 default = "false" 486 read_only = true 487 help = "assume that function defined by quantifiers are well defined" 488 489[[option]] 490 name = "fmfFunWellDefined" 491 category = "regular" 492 long = "fmf-fun" 493 type = "bool" 494 default = "false" 495 help = "find models for recursively defined functions, assumes functions are admissible" 496 497[[option]] 498 name = "fmfFunWellDefinedRelevant" 499 category = "regular" 500 long = "fmf-fun-rlv" 501 type = "bool" 502 default = "false" 503 read_only = true 504 help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant" 505 506[[option]] 507 name = "fmfEmptySorts" 508 category = "regular" 509 long = "fmf-empty-sorts" 510 type = "bool" 511 default = "false" 512 read_only = true 513 help = "allow finite model finding to assume sorts that do not occur in ground assertions are empty" 514 515[[option]] 516 name = "mbqiMode" 517 category = "regular" 518 long = "mbqi=MODE" 519 type = "CVC4::theory::quantifiers::MbqiMode" 520 default = "CVC4::theory::quantifiers::MBQI_FMC" 521 handler = "stringToMbqiMode" 522 predicates = ["checkMbqiMode"] 523 includes = ["options/quantifiers_modes.h"] 524 help = "choose mode for model-based quantifier instantiation" 525 526[[option]] 527 name = "fmfOneInstPerRound" 528 category = "regular" 529 long = "mbqi-one-inst-per-round" 530 type = "bool" 531 default = "false" 532 help = "only add one instantiation per quantifier per round for mbqi" 533 534[[option]] 535 name = "fmfOneQuantPerRound" 536 category = "regular" 537 long = "mbqi-one-quant-per-round" 538 type = "bool" 539 default = "false" 540 read_only = true 541 help = "only add instantiations for one quantifier per round for mbqi" 542 543[[option]] 544 name = "mbqiInterleave" 545 category = "regular" 546 long = "mbqi-interleave" 547 type = "bool" 548 default = "false" 549 read_only = true 550 help = "interleave model-based quantifier instantiation with other techniques" 551 552[[option]] 553 name = "fmfInstEngine" 554 category = "regular" 555 long = "fmf-inst-engine" 556 type = "bool" 557 default = "false" 558 help = "use instantiation engine in conjunction with finite model finding" 559 560[[option]] 561 name = "fmfInstGen" 562 category = "regular" 563 long = "fmf-inst-gen" 564 type = "bool" 565 default = "true" 566 read_only = true 567 help = "enable Inst-Gen instantiation techniques for finite model finding" 568 569[[option]] 570 name = "fmfInstGenOneQuantPerRound" 571 category = "regular" 572 long = "fmf-inst-gen-one-quant-per-round" 573 type = "bool" 574 default = "false" 575 read_only = true 576 help = "only perform Inst-Gen instantiation techniques on one quantifier per round" 577 578[[option]] 579 name = "fmfFreshDistConst" 580 category = "regular" 581 long = "fmf-fresh-dc" 582 type = "bool" 583 default = "false" 584 read_only = true 585 help = "use fresh distinguished representative when applying Inst-Gen techniques" 586 587[[option]] 588 name = "fmfFmcSimple" 589 category = "regular" 590 long = "fmf-fmc-simple" 591 type = "bool" 592 default = "true" 593 read_only = true 594 help = "simple models in full model check for finite model finding" 595 596[[option]] 597 name = "fmfBoundInt" 598 category = "regular" 599 long = "fmf-bound-int" 600 type = "bool" 601 default = "false" 602 help = "finite model finding on bounded integer quantification" 603 604[[option]] 605 name = "fmfBound" 606 category = "regular" 607 long = "fmf-bound" 608 type = "bool" 609 default = "false" 610 help = "finite model finding on bounded quantification" 611 612[[option]] 613 name = "fmfBoundLazy" 614 category = "regular" 615 long = "fmf-bound-lazy" 616 type = "bool" 617 default = "false" 618 help = "enforce bounds for bounded quantification lazily via use of proxy variables" 619 620[[option]] 621 name = "fmfTypeCompletionThresh" 622 category = "regular" 623 long = "fmf-type-completion-thresh=N" 624 type = "int" 625 default = "1000" 626 read_only = true 627 help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" 628 629[[option]] 630 name = "quantConflictFind" 631 category = "regular" 632 long = "quant-cf" 633 type = "bool" 634 default = "true" 635 help = "enable conflict find mechanism for quantifiers" 636 637[[option]] 638 name = "qcfMode" 639 category = "regular" 640 long = "quant-cf-mode=MODE" 641 type = "CVC4::theory::quantifiers::QcfMode" 642 default = "CVC4::theory::quantifiers::QCF_PROP_EQ" 643 handler = "stringToQcfMode" 644 includes = ["options/quantifiers_modes.h"] 645 read_only = true 646 help = "what effort to apply conflict find mechanism" 647 648[[option]] 649 name = "qcfWhenMode" 650 category = "regular" 651 long = "quant-cf-when=MODE" 652 type = "CVC4::theory::quantifiers::QcfWhenMode" 653 default = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT" 654 handler = "stringToQcfWhenMode" 655 includes = ["options/quantifiers_modes.h"] 656 read_only = true 657 help = "when to invoke conflict find mechanism for quantifiers" 658 659[[option]] 660 name = "qcfTConstraint" 661 category = "regular" 662 long = "qcf-tconstraint" 663 type = "bool" 664 default = "false" 665 help = "enable entailment checks for t-constraints in qcf algorithm" 666 667[[option]] 668 name = "qcfAllConflict" 669 category = "regular" 670 long = "qcf-all-conflict" 671 type = "bool" 672 default = "false" 673 help = "add all available conflicting instances during conflict-based instantiation" 674 675[[option]] 676 name = "qcfNestedConflict" 677 category = "regular" 678 long = "qcf-nested-conflict" 679 type = "bool" 680 default = "false" 681 read_only = true 682 help = "consider conflicts for nested quantifiers" 683 684[[option]] 685 name = "qcfVoExp" 686 category = "regular" 687 long = "qcf-vo-exp" 688 type = "bool" 689 default = "false" 690 read_only = true 691 help = "qcf experimental variable ordering" 692 693[[option]] 694 name = "instNoEntail" 695 category = "regular" 696 long = "inst-no-entail" 697 type = "bool" 698 default = "true" 699 help = "do not consider instances of quantified formulas that are currently entailed" 700 701[[option]] 702 name = "instNoModelTrue" 703 category = "regular" 704 long = "inst-no-model-true" 705 type = "bool" 706 default = "false" 707 help = "do not consider instances of quantified formulas that are currently true in model, if it is available" 708 709[[option]] 710 name = "instPropagate" 711 category = "regular" 712 long = "inst-prop" 713 type = "bool" 714 default = "false" 715 help = "internal propagation for instantiations for selecting relevant instances" 716 717[[option]] 718 name = "qcfEagerTest" 719 category = "regular" 720 long = "qcf-eager-test" 721 type = "bool" 722 default = "true" 723 read_only = true 724 help = "optimization, test qcf instances eagerly" 725 726[[option]] 727 name = "qcfEagerCheckRd" 728 category = "regular" 729 long = "qcf-eager-check-rd" 730 type = "bool" 731 default = "true" 732 read_only = true 733 help = "optimization, eagerly check relevant domain of matched position" 734 735[[option]] 736 name = "qcfSkipRd" 737 category = "regular" 738 long = "qcf-skip-rd" 739 type = "bool" 740 default = "false" 741 read_only = true 742 help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas" 743 744### Rewrite rules options 745 746[[option]] 747 name = "quantRewriteRules" 748 category = "regular" 749 long = "rewrite-rules" 750 type = "bool" 751 default = "false" 752 read_only = true 753 help = "use rewrite rules module" 754 755[[option]] 756 name = "rrOneInstPerRound" 757 category = "regular" 758 long = "rr-one-inst-per-round" 759 type = "bool" 760 default = "false" 761 read_only = true 762 help = "add one instance of rewrite rule per round" 763 764### Induction options 765 766[[option]] 767 name = "quantInduction" 768 category = "regular" 769 long = "quant-ind" 770 type = "bool" 771 default = "false" 772 read_only = true 773 help = "use all available techniques for inductive reasoning" 774 775[[option]] 776 name = "dtStcInduction" 777 category = "regular" 778 long = "dt-stc-ind" 779 type = "bool" 780 default = "false" 781 help = "apply strengthening for existential quantification over datatypes based on structural induction" 782 783[[option]] 784 name = "intWfInduction" 785 category = "regular" 786 long = "int-wf-ind" 787 type = "bool" 788 default = "false" 789 help = "apply strengthening for integers based on well-founded induction" 790 791[[option]] 792 name = "conjectureGen" 793 category = "regular" 794 long = "conjecture-gen" 795 type = "bool" 796 default = "false" 797 help = "generate candidate conjectures for inductive proofs" 798 799[[option]] 800 name = "conjectureGenPerRound" 801 category = "regular" 802 long = "conjecture-gen-per-round=N" 803 type = "int" 804 default = "1" 805 read_only = true 806 help = "number of conjectures to generate per instantiation round" 807 808[[option]] 809 name = "conjectureNoFilter" 810 category = "regular" 811 long = "conjecture-no-filter" 812 type = "bool" 813 default = "false" 814 read_only = true 815 help = "do not filter conjectures" 816 817[[option]] 818 name = "conjectureFilterActiveTerms" 819 category = "regular" 820 long = "conjecture-filter-active-terms" 821 type = "bool" 822 default = "true" 823 help = "filter based on active terms" 824 825[[option]] 826 name = "conjectureFilterCanonical" 827 category = "regular" 828 long = "conjecture-filter-canonical" 829 type = "bool" 830 default = "true" 831 help = "filter based on canonicity" 832 833[[option]] 834 name = "conjectureFilterModel" 835 category = "regular" 836 long = "conjecture-filter-model" 837 type = "bool" 838 default = "true" 839 help = "filter based on model" 840 841[[option]] 842 name = "conjectureGenGtEnum" 843 category = "regular" 844 long = "conjecture-gen-gt-enum=N" 845 type = "int" 846 default = "50" 847 read_only = true 848 help = "number of ground terms to generate for model filtering" 849 850[[option]] 851 name = "conjectureUeeIntro" 852 category = "regular" 853 long = "conjecture-gen-uee-intro" 854 type = "bool" 855 default = "false" 856 read_only = true 857 help = "more aggressive merging for universal equality engine, introduces terms" 858 859[[option]] 860 name = "conjectureGenMaxDepth" 861 category = "regular" 862 long = "conjecture-gen-max-depth=N" 863 type = "int" 864 default = "3" 865 read_only = true 866 help = "maximum depth of terms to consider for conjectures" 867 868### Synthesis options 869 870[[option]] 871 name = "sygusInference" 872 category = "regular" 873 long = "sygus-inference" 874 type = "bool" 875 default = "false" 876 read_only = false 877 help = "attempt to preprocess arbitrary inputs to sygus conjectures" 878 879[[option]] 880 name = "sygusAbduct" 881 category = "regular" 882 long = "sygus-abduct" 883 type = "bool" 884 default = "false" 885 read_only = false 886 help = "compute abductions using sygus" 887 888[[option]] 889 name = "ceGuidedInst" 890 category = "regular" 891 long = "cegqi" 892 type = "bool" 893 default = "false" 894 help = "counterexample-guided quantifier instantiation for sygus" 895 896[[option]] 897 name = "cegqiSingleInvMode" 898 category = "regular" 899 long = "cegqi-si=MODE" 900 type = "CVC4::theory::quantifiers::CegqiSingleInvMode" 901 default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE" 902 handler = "stringToCegqiSingleInvMode" 903 includes = ["options/quantifiers_modes.h"] 904 help = "mode for processing single invocation synthesis conjectures" 905 906[[option]] 907 name = "cegqiSingleInvPartial" 908 category = "regular" 909 long = "cegqi-si-partial" 910 type = "bool" 911 default = "false" 912 read_only = true 913 help = "combined techniques for synthesis conjectures that are partially single invocation" 914 915[[option]] 916 name = "cegqiSingleInvReconstruct" 917 category = "regular" 918 long = "cegqi-si-rcons=MODE" 919 type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode" 920 default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT" 921 handler = "stringToCegqiSingleInvRconsMode" 922 includes = ["options/quantifiers_modes.h"] 923 help = "policy for reconstructing solutions for single invocation conjectures" 924 925[[option]] 926 name = "cegqiSingleInvReconstructLimit" 927 category = "regular" 928 long = "cegqi-si-rcons-limit=N" 929 type = "int" 930 default = "10000" 931 read_only = true 932 help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" 933 934[[option]] 935 name = "cegqiSingleInvReconstructConst" 936 category = "regular" 937 long = "cegqi-si-reconstruct-const" 938 type = "bool" 939 default = "true" 940 read_only = true 941 help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" 942 943[[option]] 944 name = "cegqiSolMinCore" 945 category = "regular" 946 long = "cegqi-si-sol-min-core" 947 type = "bool" 948 default = "false" 949 read_only = true 950 help = "minimize solutions for single invocation conjectures based on unsat core" 951 952[[option]] 953 name = "cegqiSolMinInst" 954 category = "regular" 955 long = "cegqi-si-sol-min-inst" 956 type = "bool" 957 default = "true" 958 read_only = true 959 help = "minimize individual instantiations for single invocation conjectures based on unsat core" 960 961[[option]] 962 name = "cegqiSingleInvAbort" 963 category = "regular" 964 long = "cegqi-si-abort" 965 type = "bool" 966 default = "false" 967 read_only = true 968 help = "abort if synthesis conjecture is not single invocation" 969 970[[option]] 971 name = "sygusConstRepairAbort" 972 category = "regular" 973 long = "sygus-crepair-abort" 974 type = "bool" 975 default = "false" 976 read_only = true 977 help = "abort if constant repair techniques are not applicable" 978 979[[option]] 980 name = "sygusUnif" 981 category = "regular" 982 long = "sygus-unif" 983 type = "bool" 984 default = "false" 985 help = "Unification-based function synthesis" 986 987[[option]] 988 name = "sygusUnifCondIndependent" 989 category = "regular" 990 long = "sygus-unif-cond-independent" 991 type = "bool" 992 default = "false" 993 help = "Synthesize conditions indepedently from return values (may generate bigger solutions)" 994 995[[option]] 996 name = "sygusUnifShuffleCond" 997 category = "regular" 998 long = "sygus-unif-shuffle-cond" 999 type = "bool" 1000 default = "false" 1001 help = "Shuffle condition pool when building solutions (may change solutions sizes)" 1002 1003[[option]] 1004 name = "sygusUnifBooleanHeuristicDt" 1005 category = "regular" 1006 long = "sygus-unif-boolean-heuristic-dt" 1007 type = "bool" 1008 default = "false" 1009 help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)" 1010 1011[[option]] 1012 name = "sygusUnifCondIndNoRepeatSol" 1013 category = "regular" 1014 long = "sygus-unif-cond-independent-no-repeat-sol" 1015 type = "bool" 1016 default = "true" 1017 help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis" 1018 1019[[option]] 1020 name = "sygusBoolIteReturnConst" 1021 category = "regular" 1022 long = "sygus-bool-ite-return-const" 1023 type = "bool" 1024 default = "true" 1025 help = "Only use Boolean constants for return values in unification-based function synthesis" 1026 1027[[option]] 1028 name = "sygusQePreproc" 1029 category = "regular" 1030 long = "sygus-qe-preproc" 1031 type = "bool" 1032 default = "false" 1033 read_only = true 1034 help = "use quantifier elimination as a preprocessing step for sygus" 1035 1036[[option]] 1037 name = "sygusRepairConst" 1038 category = "regular" 1039 long = "sygus-repair-const" 1040 type = "bool" 1041 default = "false" 1042 help = "use approach to repair constants in sygus candidate solutions" 1043 1044[[option]] 1045 name = "sygusRepairConstTimeout" 1046 category = "regular" 1047 long = "sygus-repair-const-timeout=N" 1048 type = "unsigned long" 1049 help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" 1050 1051[[option]] 1052 name = "sygusActiveGenMode" 1053 category = "regular" 1054 long = "sygus-active-gen=MODE" 1055 type = "CVC4::theory::quantifiers::SygusActiveGenMode" 1056 default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO" 1057 handler = "stringToSygusActiveGenMode" 1058 includes = ["options/quantifiers_modes.h"] 1059 read_only = true 1060 help = "mode for actively-generated sygus enumerators" 1061 1062[[option]] 1063 name = "sygusActiveGenEnumConsts" 1064 category = "regular" 1065 long = "sygus-active-gen-cfactor=N" 1066 type = "unsigned long" 1067 default = "5" 1068 help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum" 1069 1070[[option]] 1071 name = "sygusMinGrammar" 1072 category = "regular" 1073 long = "sygus-min-grammar" 1074 type = "bool" 1075 default = "true" 1076 read_only = true 1077 help = "statically minimize sygus grammars" 1078 1079[[option]] 1080 name = "sygusAddConstGrammar" 1081 category = "regular" 1082 long = "sygus-add-const-grammar" 1083 type = "bool" 1084 default = "false" 1085 read_only = true 1086 help = "statically add constants appearing in conjecture to grammars" 1087 1088[[option]] 1089 name = "sygusGrammarNorm" 1090 category = "regular" 1091 long = "sygus-grammar-norm" 1092 type = "bool" 1093 default = "false" 1094 read_only = true 1095 help = "statically normalize sygus grammars based on flattening (linearization)" 1096 1097[[option]] 1098 name = "sygusTemplEmbedGrammar" 1099 category = "regular" 1100 long = "sygus-templ-embed-grammar" 1101 type = "bool" 1102 default = "false" 1103 read_only = true 1104 help = "embed sygus templates into grammars" 1105 1106[[option]] 1107 name = "sygusInvTemplMode" 1108 category = "regular" 1109 long = "sygus-inv-templ=MODE" 1110 type = "CVC4::theory::quantifiers::SygusInvTemplMode" 1111 default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" 1112 handler = "stringToSygusInvTemplMode" 1113 includes = ["options/quantifiers_modes.h"] 1114 help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" 1115 1116[[option]] 1117 name = "sygusInvTemplWhenSyntax" 1118 category = "regular" 1119 long = "sygus-inv-templ-when-sg" 1120 type = "bool" 1121 default = "false" 1122 read_only = false 1123 help = "use invariant templates (with solution reconstruction) for syntax guided problems" 1124 1125[[option]] 1126 name = "sygusInvAutoUnfold" 1127 category = "regular" 1128 long = "sygus-auto-unfold" 1129 type = "bool" 1130 default = "true" 1131 read_only = true 1132 help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems" 1133 1134[[option]] 1135 name = "sygusUnifPbe" 1136 category = "regular" 1137 long = "sygus-pbe" 1138 type = "bool" 1139 default = "true" 1140 help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures" 1141 1142[[option]] 1143 name = "sygusPbeMultiFair" 1144 category = "regular" 1145 long = "sygus-pbe-multi-fair" 1146 type = "bool" 1147 default = "false" 1148 help = "when using multiple enumerators, ensure that we only register value of minimial term size" 1149 1150[[option]] 1151 name = "sygusPbeMultiFairDiff" 1152 category = "regular" 1153 long = "sygus-pbe-multi-fair-diff=N" 1154 type = "int" 1155 default = "0" 1156 help = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)" 1157 1158[[option]] 1159 name = "sygusEvalUnfold" 1160 category = "regular" 1161 long = "sygus-eval-unfold" 1162 type = "bool" 1163 default = "true" 1164 read_only = true 1165 help = "do unfolding of sygus evaluation functions" 1166 1167[[option]] 1168 name = "sygusEvalUnfoldBool" 1169 category = "regular" 1170 long = "sygus-eval-unfold-bool" 1171 type = "bool" 1172 default = "true" 1173 read_only = true 1174 help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas" 1175 1176[[option]] 1177 name = "sygusRefEval" 1178 category = "regular" 1179 long = "sygus-ref-eval" 1180 type = "bool" 1181 default = "true" 1182 read_only = true 1183 help = "direct evaluation of refinement lemmas for conflict analysis" 1184 1185[[option]] 1186 name = "sygusStream" 1187 category = "regular" 1188 long = "sygus-stream" 1189 type = "bool" 1190 default = "false" 1191 help = "enumerate a stream of solutions instead of terminating after the first one" 1192 1193[[option]] 1194 name = "sygusVerifySubcall" 1195 category = "regular" 1196 long = "sygus-verify-subcall" 1197 type = "bool" 1198 default = "true" 1199 help = "use separate copy of the SMT solver for verification lemmas in sygus" 1200 1201[[option]] 1202 name = "sygusExtRew" 1203 category = "regular" 1204 long = "sygus-ext-rew" 1205 type = "bool" 1206 default = "true" 1207 help = "use extended rewriter for sygus" 1208 1209[[option]] 1210 name = "cegisSample" 1211 category = "regular" 1212 long = "cegis-sample=MODE" 1213 type = "CVC4::theory::quantifiers::CegisSampleMode" 1214 default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE" 1215 handler = "stringToCegisSampleMode" 1216 includes = ["options/quantifiers_modes.h"] 1217 help = "mode for using samples in the counterexample-guided inductive synthesis loop" 1218 1219[[option]] 1220 name = "minSynthSol" 1221 category = "regular" 1222 long = "min-synth-sol" 1223 type = "bool" 1224 default = "true" 1225 help = "Minimize synthesis solutions" 1226 1227[[option]] 1228 name = "sygusEvalOpt" 1229 category = "regular" 1230 long = "sygus-eval-opt" 1231 type = "bool" 1232 default = "true" 1233 help = "use optimized approach for evaluation in sygus" 1234 1235[[option]] 1236 name = "sygusArgRelevant" 1237 category = "regular" 1238 long = "sygus-arg-relevant" 1239 type = "bool" 1240 default = "false" 1241 help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant" 1242 1243# Internal uses of sygus 1244 1245[[option]] 1246 name = "sygusRew" 1247 category = "regular" 1248 long = "sygus-rr" 1249 type = "bool" 1250 default = "false" 1251 read_only = true 1252 help = "use sygus to enumerate and verify correctness of rewrite rules" 1253 1254[[option]] 1255 name = "sygusRewSynth" 1256 category = "regular" 1257 long = "sygus-rr-synth" 1258 type = "bool" 1259 default = "false" 1260 help = "use sygus to enumerate candidate rewrite rules" 1261 1262[[option]] 1263 name = "sygusRewSynthFilterOrder" 1264 category = "regular" 1265 long = "sygus-rr-synth-filter-order" 1266 type = "bool" 1267 default = "true" 1268 help = "filter candidate rewrites based on variable ordering" 1269 1270[[option]] 1271 name = "sygusRewSynthFilterMatch" 1272 category = "regular" 1273 long = "sygus-rr-synth-filter-match" 1274 type = "bool" 1275 default = "true" 1276 help = "filter candidate rewrites based on matching" 1277 1278[[option]] 1279 name = "sygusRewSynthFilterCong" 1280 category = "regular" 1281 long = "sygus-rr-synth-filter-cong" 1282 type = "bool" 1283 default = "true" 1284 help = "filter candidate rewrites based on congruence" 1285 1286[[option]] 1287 name = "sygusRewSynthFilterNonLinear" 1288 category = "regular" 1289 long = "sygus-rr-synth-filter-nl" 1290 type = "bool" 1291 default = "false" 1292 help = "filter non-linear candidate rewrites" 1293 1294[[option]] 1295 name = "sygusRewVerify" 1296 category = "regular" 1297 long = "sygus-rr-verify" 1298 type = "bool" 1299 default = "false" 1300 help = "use sygus to verify the correctness of rewrite rules via sampling" 1301 1302[[option]] 1303 name = "sygusRewVerifyAbort" 1304 category = "regular" 1305 long = "sygus-rr-verify-abort" 1306 type = "bool" 1307 default = "true" 1308 help = "abort when sygus-rr-verify finds an instance of unsoundness" 1309 1310[[option]] 1311 name = "sygusSamples" 1312 category = "regular" 1313 long = "sygus-samples=N" 1314 type = "int" 1315 default = "1000" 1316 help = "number of points to consider when doing sygus rewriter sample testing" 1317 1318[[option]] 1319 name = "sygusSampleGrammar" 1320 category = "regular" 1321 long = "sygus-sample-grammar" 1322 type = "bool" 1323 default = "true" 1324 read_only = true 1325 help = "when applicable, use grammar for choosing sample points" 1326 1327[[option]] 1328 name = "sygusSampleFpUniform" 1329 category = "regular" 1330 long = "sygus-sample-fp-uniform" 1331 type = "bool" 1332 default = "false" 1333 help = "sample floating-point values uniformly instead of in a biased fashion" 1334 1335[[option]] 1336 name = "sygusRewSynthAccel" 1337 category = "regular" 1338 long = "sygus-rr-synth-accel" 1339 type = "bool" 1340 default = "false" 1341 help = "add dynamic symmetry breaking clauses based on candidate rewrites" 1342 1343[[option]] 1344 name = "sygusRewSynthCheck" 1345 category = "regular" 1346 long = "sygus-rr-synth-check" 1347 type = "bool" 1348 default = "false" 1349 help = "use satisfiability check to verify correctness of candidate rewrites" 1350 1351[[option]] 1352 name = "sygusRewSynthInput" 1353 category = "regular" 1354 long = "sygus-rr-synth-input" 1355 type = "bool" 1356 default = "false" 1357 help = "synthesize rewrite rules based on the input formula" 1358 1359[[option]] 1360 name = "sygusRewSynthInputNVars" 1361 category = "regular" 1362 long = "sygus-rr-synth-input-nvars=N" 1363 type = "int" 1364 default = "3" 1365 help = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input" 1366 1367[[option]] 1368 name = "sygusRewSynthInputUseBool" 1369 category = "regular" 1370 long = "sygus-rr-synth-input-use-bool" 1371 type = "bool" 1372 default = "false" 1373 help = "synthesize Boolean rewrite rules based on the input formula" 1374 1375[[option]] 1376 name = "sygusExprMinerCheckTimeout" 1377 category = "regular" 1378 long = "sygus-expr-miner-check-timeout=N" 1379 type = "unsigned long" 1380 help = "timeout (in milliseconds) for satisfiability checks in expression miners" 1381 1382[[option]] 1383 name = "sygusRewSynthRec" 1384 category = "regular" 1385 long = "sygus-rr-synth-rec" 1386 type = "bool" 1387 default = "false" 1388 help = "synthesize rewrite rules over all sygus grammar types recursively" 1389 1390[[option]] 1391 name = "sygusQueryGen" 1392 category = "regular" 1393 long = "sygus-query-gen" 1394 type = "bool" 1395 default = "false" 1396 help = "use sygus to enumerate interesting satisfiability queries" 1397 1398[[option]] 1399 name = "sygusQueryGenThresh" 1400 category = "regular" 1401 long = "sygus-query-gen-thresh=N" 1402 type = "unsigned" 1403 default = "5" 1404 help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen" 1405 1406[[option]] 1407 name = "sygusQueryGenCheck" 1408 category = "regular" 1409 long = "sygus-query-gen-check" 1410 type = "bool" 1411 default = "true" 1412 help = "use interesting satisfiability queries to check soundness of CVC4" 1413 1414[[option]] 1415 name = "sygusQueryGenDumpFiles" 1416 category = "regular" 1417 long = "sygus-query-gen-dump-files" 1418 type = "bool" 1419 default = "false" 1420 help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" 1421 1422[[option]] 1423 name = "sygusFilterSolMode" 1424 category = "regular" 1425 long = "sygus-filter-sol=MODE" 1426 type = "CVC4::theory::quantifiers::SygusFilterSolMode" 1427 default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" 1428 handler = "stringToSygusFilterSolMode" 1429 includes = ["options/quantifiers_modes.h"] 1430 help = "mode for filtering sygus solutions" 1431 1432[[option]] 1433 name = "sygusFilterSolRevSubsume" 1434 category = "expert" 1435 long = "sygus-filter-sol-rev" 1436 type = "bool" 1437 default = "false" 1438 help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" 1439 1440 1441[[option]] 1442 name = "sygusExprMinerCheckUseExport" 1443 category = "expert" 1444 long = "sygus-expr-miner-check-use-export" 1445 type = "bool" 1446 default = "true" 1447 help = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners" 1448 1449# CEGQI applied to general quantified formulas 1450 1451[[option]] 1452 name = "cbqi" 1453 category = "regular" 1454 long = "cbqi" 1455 type = "bool" 1456 default = "false" 1457 help = "turns on counterexample-based quantifier instantiation" 1458 1459[[option]] 1460 name = "cbqiFullEffort" 1461 category = "regular" 1462 long = "cbqi-full" 1463 type = "bool" 1464 default = "false" 1465 help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation" 1466 1467[[option]] 1468 name = "recurseCbqi" 1469 category = "regular" 1470 long = "cbqi-recurse" 1471 type = "bool" 1472 default = "true" 1473 read_only = true 1474 help = "turns on recursive counterexample-based quantifier instantiation" 1475 1476[[option]] 1477 name = "cbqiSat" 1478 category = "regular" 1479 long = "cbqi-sat" 1480 type = "bool" 1481 default = "true" 1482 help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation" 1483 1484[[option]] 1485 name = "cbqiModel" 1486 category = "regular" 1487 long = "cbqi-model" 1488 type = "bool" 1489 default = "true" 1490 help = "guide instantiations by model values for counterexample-based quantifier instantiation" 1491 1492[[option]] 1493 name = "cbqiAll" 1494 category = "regular" 1495 long = "cbqi-all" 1496 type = "bool" 1497 default = "false" 1498 help = "apply counterexample-based instantiation to all quantified formulas" 1499 1500[[option]] 1501 name = "cbqiMultiInst" 1502 category = "regular" 1503 long = "cbqi-multi-inst" 1504 type = "bool" 1505 default = "false" 1506 help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation" 1507 1508[[option]] 1509 name = "cbqiRepeatLit" 1510 category = "regular" 1511 long = "cbqi-repeat-lit" 1512 type = "bool" 1513 default = "false" 1514 help = "solve literals more than once in counterexample-based quantifier instantiation" 1515 1516[[option]] 1517 name = "cbqiInnermost" 1518 category = "regular" 1519 long = "cbqi-innermost" 1520 type = "bool" 1521 default = "true" 1522 help = "only process innermost quantified formulas in counterexample-based quantifier instantiation" 1523 1524[[option]] 1525 name = "cbqiNestedQE" 1526 category = "regular" 1527 long = "cbqi-nested-qe" 1528 type = "bool" 1529 default = "false" 1530 help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation" 1531 1532# CEGQI for arithmetic 1533 1534[[option]] 1535 name = "cbqiUseInfInt" 1536 category = "regular" 1537 long = "cbqi-use-inf-int" 1538 type = "bool" 1539 default = "false" 1540 help = "use integer infinity for vts in counterexample-based quantifier instantiation" 1541 1542[[option]] 1543 name = "cbqiUseInfReal" 1544 category = "regular" 1545 long = "cbqi-use-inf-real" 1546 type = "bool" 1547 default = "false" 1548 help = "use real infinity for vts in counterexample-based quantifier instantiation" 1549 1550[[option]] 1551 name = "cbqiPreRegInst" 1552 category = "regular" 1553 long = "cbqi-prereg-inst" 1554 type = "bool" 1555 default = "false" 1556 help = "preregister ground instantiations in counterexample-based quantifier instantiation" 1557 1558[[option]] 1559 name = "cbqiMinBounds" 1560 category = "regular" 1561 long = "cbqi-min-bounds" 1562 type = "bool" 1563 default = "false" 1564 read_only = true 1565 help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation" 1566 1567[[option]] 1568 name = "cbqiRoundUpLowerLia" 1569 category = "regular" 1570 long = "cbqi-round-up-lia" 1571 type = "bool" 1572 default = "false" 1573 read_only = true 1574 help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation" 1575 1576[[option]] 1577 name = "cbqiMidpoint" 1578 category = "regular" 1579 long = "cbqi-midpoint" 1580 type = "bool" 1581 default = "false" 1582 help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation" 1583 1584[[option]] 1585 name = "cbqiNopt" 1586 category = "regular" 1587 long = "cbqi-nopt" 1588 type = "bool" 1589 default = "true" 1590 read_only = true 1591 help = "non-optimal bounds for counterexample-based quantifier instantiation" 1592 1593[[option]] 1594 name = "cbqiLitDepend" 1595 category = "regular" 1596 long = "cbqi-lit-dep" 1597 type = "bool" 1598 default = "true" 1599 read_only = true 1600 help = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation" 1601 1602# CEGQI for EPR 1603 1604[[option]] 1605 name = "quantEpr" 1606 category = "regular" 1607 long = "quant-epr" 1608 type = "bool" 1609 default = "false" 1610 help = "infer whether in effectively propositional fragment, use for cbqi" 1611 1612[[option]] 1613 name = "quantEprMatching" 1614 category = "regular" 1615 long = "quant-epr-match" 1616 type = "bool" 1617 default = "true" 1618 read_only = true 1619 help = "use matching heuristics for EPR instantiation" 1620 1621# CEGQI for BV 1622 1623[[option]] 1624 name = "cbqiBv" 1625 category = "regular" 1626 long = "cbqi-bv" 1627 type = "bool" 1628 default = "true" 1629 help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors" 1630 1631[[option]] 1632 name = "cbqiBvInterleaveValue" 1633 category = "regular" 1634 long = "cbqi-bv-interleave-value" 1635 type = "bool" 1636 default = "false" 1637 help = "interleave model value instantiation with word-level inversion approach" 1638 1639[[option]] 1640 name = "cbqiBvIneqMode" 1641 category = "regular" 1642 long = "cbqi-bv-ineq=MODE" 1643 type = "CVC4::theory::quantifiers::CbqiBvIneqMode" 1644 default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY" 1645 handler = "stringToCbqiBvIneqMode" 1646 includes = ["options/quantifiers_modes.h"] 1647 help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation" 1648 1649[[option]] 1650 name = "cbqiBvRmExtract" 1651 category = "regular" 1652 long = "cbqi-bv-rm-extract" 1653 type = "bool" 1654 default = "true" 1655 help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors" 1656 1657[[option]] 1658 name = "cbqiBvLinearize" 1659 category = "regular" 1660 long = "cbqi-bv-linear" 1661 type = "bool" 1662 default = "true" 1663 help = "linearize adder chains for variables" 1664 1665[[option]] 1666 name = "cbqiBvSolveNl" 1667 category = "regular" 1668 long = "cbqi-bv-solve-nl" 1669 type = "bool" 1670 default = "false" 1671 help = "try to solve non-linear bv literals using model value projections" 1672 1673[[option]] 1674 name = "cbqiBvConcInv" 1675 category = "regular" 1676 long = "cbqi-bv-concat-inv" 1677 type = "bool" 1678 default = "true" 1679 help = "compute inverse for concat over equalities rather than producing an invertibility condition" 1680 1681### Local theory extensions options 1682 1683[[option]] 1684 name = "localTheoryExt" 1685 category = "regular" 1686 long = "local-t-ext" 1687 type = "bool" 1688 default = "false" 1689 read_only = true 1690 help = "do instantiation based on local theory extensions" 1691 1692[[option]] 1693 name = "ltePartialInst" 1694 category = "regular" 1695 long = "lte-partial-inst" 1696 type = "bool" 1697 default = "false" 1698 read_only = true 1699 help = "partially instantiate local theory quantifiers" 1700 1701[[option]] 1702 name = "lteRestrictInstClosure" 1703 category = "regular" 1704 long = "lte-restrict-inst-closure" 1705 type = "bool" 1706 default = "false" 1707 read_only = true 1708 help = "treat arguments of inst closure as restricted terms for instantiation" 1709 1710### Reduction options 1711 1712[[option]] 1713 name = "quantAlphaEquiv" 1714 category = "regular" 1715 long = "quant-alpha-equiv" 1716 type = "bool" 1717 default = "true" 1718 read_only = true 1719 help = "infer alpha equivalence between quantified formulas" 1720 1721[[option]] 1722 name = "macrosQuant" 1723 category = "regular" 1724 long = "macros-quant" 1725 type = "bool" 1726 default = "false" 1727 help = "perform quantifiers macro expansion" 1728 1729[[option]] 1730 name = "macrosQuantMode" 1731 category = "regular" 1732 long = "macros-quant-mode=MODE" 1733 type = "CVC4::theory::quantifiers::MacrosQuantMode" 1734 default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF" 1735 handler = "stringToMacrosQuantMode" 1736 includes = ["options/quantifiers_modes.h"] 1737 read_only = true 1738 help = "mode for quantifiers macro expansion" 1739 1740[[option]] 1741 name = "quantDynamicSplit" 1742 category = "regular" 1743 long = "quant-dsplit-mode=MODE" 1744 type = "CVC4::theory::quantifiers::QuantDSplitMode" 1745 default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE" 1746 handler = "stringToQuantDSplitMode" 1747 includes = ["options/quantifiers_modes.h"] 1748 help = "mode for dynamic quantifiers splitting" 1749 1750[[option]] 1751 name = "quantAntiSkolem" 1752 category = "regular" 1753 long = "quant-anti-skolem" 1754 type = "bool" 1755 default = "false" 1756 help = "perform anti-skolemization for quantified formulas" 1757 1758### Higher-order options 1759 1760[[option]] 1761 name = "hoMatching" 1762 category = "regular" 1763 long = "ho-matching" 1764 type = "bool" 1765 default = "true" 1766 read_only = true 1767 help = "do higher-order matching algorithm for triggers with variable operators" 1768 1769[[option]] 1770 name = "hoMatchingVarArgPriority" 1771 category = "regular" 1772 long = "ho-matching-var-priority" 1773 type = "bool" 1774 default = "true" 1775 read_only = true 1776 help = "give priority to variable arguments over constant arguments" 1777 1778[[option]] 1779 name = "hoMergeTermDb" 1780 category = "regular" 1781 long = "ho-merge-term-db" 1782 type = "bool" 1783 default = "true" 1784 read_only = true 1785 help = "merge term indices modulo equality" 1786 1787### Proof options 1788 1789[[option]] 1790 name = "trackInstLemmas" 1791 category = "regular" 1792 long = "track-inst-lemmas" 1793 type = "bool" 1794 default = "false" 1795 help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)" 1796