src/options/quantifiers_options.toml

   1 id     = "QUANTIFIERS"
   2 name   = "Quantifiers"
   3 header = "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"
 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       = "inferArithTriggerEqExp"
 229   category   = "regular"
 230   long       = "infer-arith-trigger-eq-exp"
 231   type       = "bool"
 232   default    = "false"
 233   read_only  = true
 234   help       = "record explanations for inferArithTriggerEq"
 235
 236 [[option]]
 237   name       = "strictTriggers"
 238   category   = "regular"
 239   long       = "strict-triggers"
 240   type       = "bool"
 241   default    = "false"
 242   read_only  = true
 243   help       = "only instantiate quantifiers with user patterns based on triggers"
 244
 245 [[option]]
 246   name       = "relevantTriggers"
 247   category   = "regular"
 248   long       = "relevant-triggers"
 249   type       = "bool"
 250   default    = "false"
 251   read_only  = true
 252   help       = "prefer triggers that are more relevant based on SInE style analysis"
 253
 254 [[option]]
 255   name       = "relationalTriggers"
 256   category   = "regular"
 257   long       = "relational-triggers"
 258   type       = "bool"
 259   default    = "false"
 260   read_only  = true
 261   help       = "choose relational triggers such as x = f(y), x >= f(y)"
 262
 263 [[option]]
 264   name       = "purifyTriggers"
 265   category   = "regular"
 266   long       = "purify-triggers"
 267   type       = "bool"
 268   default    = "false"
 269   help       = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
 270
 271 [[option]]
 272   name       = "purifyDtTriggers"
 273   category   = "regular"
 274   long       = "purify-dt-triggers"
 275   type       = "bool"
 276   default    = "false"
 277   help       = "purify dt triggers, match all constructors of correct form instead of selectors"
 278
 279 [[option]]
 280   name       = "pureThTriggers"
 281   category   = "regular"
 282   long       = "pure-th-triggers"
 283   type       = "bool"
 284   default    = "false"
 285   help       = "use pure theory terms as single triggers"
 286
 287 [[option]]
 288   name       = "partialTriggers"
 289   category   = "regular"
 290   long       = "partial-triggers"
 291   type       = "bool"
 292   default    = "false"
 293   help       = "use triggers that do not contain all free variables"
 294
 295 [[option]]
 296   name       = "multiTriggerWhenSingle"
 297   category   = "regular"
 298   long       = "multi-trigger-when-single"
 299   type       = "bool"
 300   default    = "false"
 301   read_only  = true
 302   help       = "select multi triggers when single triggers exist"
 303
 304 [[option]]
 305   name       = "multiTriggerPriority"
 306   category   = "regular"
 307   long       = "multi-trigger-priority"
 308   type       = "bool"
 309   default    = "false"
 310   read_only  = true
 311   help       = "only try multi triggers if single triggers give no instantiations"
 312
 313 [[option]]
 314   name       = "multiTriggerCache"
 315   category   = "regular"
 316   long       = "multi-trigger-cache"
 317   type       = "bool"
 318   default    = "false"
 319   read_only  = true
 320   help       = "caching version of multi triggers"
 321
 322 [[option]]
 323   name       = "multiTriggerLinear"
 324   category   = "regular"
 325   long       = "multi-trigger-linear"
 326   type       = "bool"
 327   default    = "true"
 328   read_only  = true
 329   help       = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
 330
 331 [[option]]
 332   name       = "triggerSelMode"
 333   category   = "regular"
 334   long       = "trigger-sel"
 335   type       = "CVC4::theory::quantifiers::TriggerSelMode"
 336   default    = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN"
 337   handler    = "stringToTriggerSelMode"
 338   includes   = ["options/quantifiers_modes.h"]
 339   help       = "selection mode for triggers"
 340
 341 [[option]]
 342   name       = "triggerActiveSelMode"
 343   category   = "regular"
 344   long       = "trigger-active-sel"
 345   type       = "CVC4::theory::quantifiers::TriggerActiveSelMode"
 346   default    = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL"
 347   handler    = "stringToTriggerActiveSelMode"
 348   includes   = ["options/quantifiers_modes.h"]
 349   help       = "selection mode to activate triggers"
 350
 351 [[option]]
 352   name       = "userPatternsQuant"
 353   category   = "regular"
 354   long       = "user-pat=MODE"
 355   type       = "CVC4::theory::quantifiers::UserPatMode"
 356   default    = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST"
 357   handler    = "stringToUserPatMode"
 358   includes   = ["options/quantifiers_modes.h"]
 359   help       = "policy for handling user-provided patterns for quantifier instantiation"
 360
 361 [[option]]
 362   name       = "incrementTriggers"
 363   category   = "regular"
 364   long       = "increment-triggers"
 365   type       = "bool"
 366   default    = "true"
 367   read_only  = true
 368   help       = "generate additional triggers as needed during search"
 369
 370 [[option]]
 371   name       = "instWhenMode"
 372   category   = "regular"
 373   long       = "inst-when=MODE"
 374   type       = "CVC4::theory::quantifiers::InstWhenMode"
 375   default    = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL"
 376   handler    = "stringToInstWhenMode"
 377   predicates = ["checkInstWhenMode"]
 378   includes   = ["options/quantifiers_modes.h"]
 379   help       = "when to apply instantiation"
 380
 381 [[option]]
 382   name       = "instWhenStrictInterleave"
 383   category   = "regular"
 384   long       = "inst-when-strict-interleave"
 385   type       = "bool"
 386   default    = "true"
 387   help       = "ensure theory combination and standard quantifier effort strategies take turns"
 388
 389 [[option]]
 390   name       = "instWhenPhase"
 391   category   = "regular"
 392   long       = "inst-when-phase=N"
 393   type       = "int"
 394   default    = "2"
 395   help       = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
 396
 397 [[option]]
 398   name       = "instWhenTcFirst"
 399   category   = "regular"
 400   long       = "inst-when-tc-first"
 401   type       = "bool"
 402   default    = "true"
 403   help       = "allow theory combination to happen once initially, before quantifier strategies are run"
 404
 405 [[option]]
 406   name       = "quantModelEe"
 407   category   = "regular"
 408   long       = "quant-model-ee"
 409   type       = "bool"
 410   default    = "false"
 411   read_only  = true
 412   help       = "use equality engine of model for last call effort"
 413
 414 [[option]]
 415   name       = "instMaxLevel"
 416   category   = "regular"
 417   long       = "inst-max-level=N"
 418   type       = "int"
 419   default    = "-1"
 420   help       = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
 421
 422 [[option]]
 423   name       = "instLevelInputOnly"
 424   category   = "regular"
 425   long       = "inst-level-input-only"
 426   type       = "bool"
 427   default    = "true"
 428   read_only  = true
 429   help       = "only input terms are assigned instantiation level zero"
 430
 431 [[option]]
 432   name       = "quantRepMode"
 433   category   = "regular"
 434   long       = "quant-rep-mode=MODE"
 435   type       = "CVC4::theory::quantifiers::QuantRepMode"
 436   default    = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST"
 437   handler    = "stringToQuantRepMode"
 438   includes   = ["options/quantifiers_modes.h"]
 439   help       = "selection mode for representatives in quantifiers engine"
 440
 441 [[option]]
 442   name       = "fullSaturateQuant"
 443   category   = "regular"
 444   long       = "full-saturate-quant"
 445   type       = "bool"
 446   default    = "false"
 447   help       = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
 448
 449 [[option]]
 450   name       = "fullSaturateQuantRd"
 451   category   = "regular"
 452   long       = "full-saturate-quant-rd"
 453   type       = "bool"
 454   default    = "true"
 455   read_only  = true
 456   help       = "whether to use relevant domain first for full saturation instantiation strategy"
 457
 458 [[option]]
 459   name       = "fullSaturateInterleave"
 460   category   = "regular"
 461   long       = "fs-interleave"
 462   type       = "bool"
 463   default    = "false"
 464   read_only  = true
 465   help       = "interleave full saturate instantiation with other techniques"
 466
 467 [[option]]
 468   name       = "literalMatchMode"
 469   category   = "regular"
 470   long       = "literal-matching=MODE"
 471   type       = "CVC4::theory::quantifiers::LiteralMatchMode"
 472   default    = "CVC4::theory::quantifiers::LITERAL_MATCH_USE"
 473   handler    = "stringToLiteralMatchMode"
 474   predicates = ["checkLiteralMatchMode"]
 475   includes   = ["options/quantifiers_modes.h"]
 476   read_only  = true
 477   help       = "choose literal matching mode"
 478
 479 ### Finite model finding options
 480
 481 [[option]]
 482   name       = "finiteModelFind"
 483   category   = "regular"
 484   long       = "finite-model-find"
 485   type       = "bool"
 486   default    = "false"
 487   help       = "use finite model finding heuristic for quantifier instantiation"
 488
 489 [[option]]
 490   name       = "quantFunWellDefined"
 491   category   = "regular"
 492   long       = "quant-fun-wd"
 493   type       = "bool"
 494   default    = "false"
 495   read_only  = true
 496   help       = "assume that function defined by quantifiers are well defined"
 497
 498 [[option]]
 499   name       = "fmfFunWellDefined"
 500   category   = "regular"
 501   long       = "fmf-fun"
 502   type       = "bool"
 503   default    = "false"
 504   help       = "find models for recursively defined functions, assumes functions are admissible"
 505
 506 [[option]]
 507   name       = "fmfFunWellDefinedRelevant"
 508   category   = "regular"
 509   long       = "fmf-fun-rlv"
 510   type       = "bool"
 511   default    = "false"
 512   read_only  = true
 513   help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
 514
 515 [[option]]
 516   name       = "fmfEmptySorts"
 517   category   = "regular"
 518   long       = "fmf-empty-sorts"
 519   type       = "bool"
 520   default    = "false"
 521   read_only  = true
 522   help       = "allow finite model finding to assume sorts that do not occur in ground assertions are empty"
 523
 524 [[option]]
 525   name       = "mbqiMode"
 526   category   = "regular"
 527   long       = "mbqi=MODE"
 528   type       = "CVC4::theory::quantifiers::MbqiMode"
 529   default    = "CVC4::theory::quantifiers::MBQI_FMC"
 530   handler    = "stringToMbqiMode"
 531   predicates = ["checkMbqiMode"]
 532   includes   = ["options/quantifiers_modes.h"]
 533   help       = "choose mode for model-based quantifier instantiation"
 534
 535 [[option]]
 536   name       = "fmfOneInstPerRound"
 537   category   = "regular"
 538   long       = "mbqi-one-inst-per-round"
 539   type       = "bool"
 540   default    = "false"
 541   help       = "only add one instantiation per quantifier per round for mbqi"
 542
 543 [[option]]
 544   name       = "fmfOneQuantPerRound"
 545   category   = "regular"
 546   long       = "mbqi-one-quant-per-round"
 547   type       = "bool"
 548   default    = "false"
 549   read_only  = true
 550   help       = "only add instantiations for one quantifier per round for mbqi"
 551
 552 [[option]]
 553   name       = "mbqiInterleave"
 554   category   = "regular"
 555   long       = "mbqi-interleave"
 556   type       = "bool"
 557   default    = "false"
 558   read_only  = true
 559   help       = "interleave model-based quantifier instantiation with other techniques"
 560
 561 [[option]]
 562   name       = "fmfInstEngine"
 563   category   = "regular"
 564   long       = "fmf-inst-engine"
 565   type       = "bool"
 566   default    = "false"
 567   help       = "use instantiation engine in conjunction with finite model finding"
 568
 569 [[option]]
 570   name       = "fmfInstGen"
 571   category   = "regular"
 572   long       = "fmf-inst-gen"
 573   type       = "bool"
 574   default    = "true"
 575   read_only  = true
 576   help       = "enable Inst-Gen instantiation techniques for finite model finding"
 577
 578 [[option]]
 579   name       = "fmfInstGenOneQuantPerRound"
 580   category   = "regular"
 581   long       = "fmf-inst-gen-one-quant-per-round"
 582   type       = "bool"
 583   default    = "false"
 584   read_only  = true
 585   help       = "only perform Inst-Gen instantiation techniques on one quantifier per round"
 586
 587 [[option]]
 588   name       = "fmfFreshDistConst"
 589   category   = "regular"
 590   long       = "fmf-fresh-dc"
 591   type       = "bool"
 592   default    = "false"
 593   read_only  = true
 594   help       = "use fresh distinguished representative when applying Inst-Gen techniques"
 595
 596 [[option]]
 597   name       = "fmfFmcSimple"
 598   category   = "regular"
 599   long       = "fmf-fmc-simple"
 600   type       = "bool"
 601   default    = "true"
 602   read_only  = true
 603   help       = "simple models in full model check for finite model finding"
 604
 605 [[option]]
 606   name       = "fmfBoundInt"
 607   category   = "regular"
 608   long       = "fmf-bound-int"
 609   type       = "bool"
 610   default    = "false"
 611   help       = "finite model finding on bounded integer quantification"
 612
 613 [[option]]
 614   name       = "fmfBound"
 615   category   = "regular"
 616   long       = "fmf-bound"
 617   type       = "bool"
 618   default    = "false"
 619   help       = "finite model finding on bounded quantification"
 620
 621 [[option]]
 622   name       = "fmfBoundLazy"
 623   category   = "regular"
 624   long       = "fmf-bound-lazy"
 625   type       = "bool"
 626   default    = "false"
 627   help       = "enforce bounds for bounded quantification lazily via use of proxy variables"
 628
 629 [[option]]
 630   name       = "fmfBoundMinMode"
 631   category   = "regular"
 632   long       = "fmf-bound-min-mode=MODE"
 633   type       = "CVC4::theory::quantifiers::FmfBoundMinMode"
 634   default    = "CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE"
 635   handler    = "stringToFmfBoundMinMode"
 636   includes   = ["options/quantifiers_modes.h"]
 637   read_only  = true
 638   help       = "mode for which types of bounds to minimize via first decision heuristics"
 639
 640 [[option]]
 641   name       = "quantConflictFind"
 642   category   = "regular"
 643   long       = "quant-cf"
 644   type       = "bool"
 645   default    = "true"
 646   help       = "enable conflict find mechanism for quantifiers"
 647
 648 [[option]]
 649   name       = "qcfMode"
 650   category   = "regular"
 651   long       = "quant-cf-mode=MODE"
 652   type       = "CVC4::theory::quantifiers::QcfMode"
 653   default    = "CVC4::theory::quantifiers::QCF_PROP_EQ"
 654   handler    = "stringToQcfMode"
 655   includes   = ["options/quantifiers_modes.h"]
 656   read_only  = true
 657   help       = "what effort to apply conflict find mechanism"
 658
 659 [[option]]
 660   name       = "qcfWhenMode"
 661   category   = "regular"
 662   long       = "quant-cf-when=MODE"
 663   type       = "CVC4::theory::quantifiers::QcfWhenMode"
 664   default    = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT"
 665   handler    = "stringToQcfWhenMode"
 666   includes   = ["options/quantifiers_modes.h"]
 667   read_only  = true
 668   help       = "when to invoke conflict find mechanism for quantifiers"
 669
 670 [[option]]
 671   name       = "qcfTConstraint"
 672   category   = "regular"
 673   long       = "qcf-tconstraint"
 674   type       = "bool"
 675   default    = "false"
 676   help       = "enable entailment checks for t-constraints in qcf algorithm"
 677
 678 [[option]]
 679   name       = "qcfAllConflict"
 680   category   = "regular"
 681   long       = "qcf-all-conflict"
 682   type       = "bool"
 683   default    = "false"
 684   help       = "add all available conflicting instances during conflict-based instantiation"
 685
 686 [[option]]
 687   name       = "qcfNestedConflict"
 688   category   = "regular"
 689   long       = "qcf-nested-conflict"
 690   type       = "bool"
 691   default    = "false"
 692   read_only  = true
 693   help       = "consider conflicts for nested quantifiers"
 694
 695 [[option]]
 696   name       = "qcfVoExp"
 697   category   = "regular"
 698   long       = "qcf-vo-exp"
 699   type       = "bool"
 700   default    = "false"
 701   read_only  = true
 702   help       = "qcf experimental variable ordering"
 703
 704 [[option]]
 705   name       = "instNoEntail"
 706   category   = "regular"
 707   long       = "inst-no-entail"
 708   type       = "bool"
 709   default    = "true"
 710   help       = "do not consider instances of quantified formulas that are currently entailed"
 711
 712 [[option]]
 713   name       = "instNoModelTrue"
 714   category   = "regular"
 715   long       = "inst-no-model-true"
 716   type       = "bool"
 717   default    = "false"
 718   help       = "do not consider instances of quantified formulas that are currently true in model, if it is available"
 719
 720 [[option]]
 721   name       = "instPropagate"
 722   category   = "regular"
 723   long       = "inst-prop"
 724   type       = "bool"
 725   default    = "false"
 726   help       = "internal propagation for instantiations for selecting relevant instances"
 727
 728 [[option]]
 729   name       = "qcfEagerTest"
 730   category   = "regular"
 731   long       = "qcf-eager-test"
 732   type       = "bool"
 733   default    = "true"
 734   read_only  = true
 735   help       = "optimization, test qcf instances eagerly"
 736
 737 [[option]]
 738   name       = "qcfEagerCheckRd"
 739   category   = "regular"
 740   long       = "qcf-eager-check-rd"
 741   type       = "bool"
 742   default    = "true"
 743   read_only  = true
 744   help       = "optimization, eagerly check relevant domain of matched position"
 745
 746 [[option]]
 747   name       = "qcfSkipRd"
 748   category   = "regular"
 749   long       = "qcf-skip-rd"
 750   type       = "bool"
 751   default    = "false"
 752   read_only  = true
 753   help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 754
 755 ### Rewrite rules options
 756
 757 [[option]]
 758   name       = "quantRewriteRules"
 759   category   = "regular"
 760   long       = "rewrite-rules"
 761   type       = "bool"
 762   default    = "false"
 763   read_only  = true
 764   help       = "use rewrite rules module"
 765
 766 [[option]]
 767   name       = "rrOneInstPerRound"
 768   category   = "regular"
 769   long       = "rr-one-inst-per-round"
 770   type       = "bool"
 771   default    = "false"
 772   read_only  = true
 773   help       = "add one instance of rewrite rule per round"
 774
 775 ### Induction options
 776
 777 [[option]]
 778   name       = "quantInduction"
 779   category   = "regular"
 780   long       = "quant-ind"
 781   type       = "bool"
 782   default    = "false"
 783   read_only  = true
 784   help       = "use all available techniques for inductive reasoning"
 785
 786 [[option]]
 787   name       = "dtStcInduction"
 788   category   = "regular"
 789   long       = "dt-stc-ind"
 790   type       = "bool"
 791   default    = "false"
 792   help       = "apply strengthening for existential quantification over datatypes based on structural induction"
 793
 794 [[option]]
 795   name       = "intWfInduction"
 796   category   = "regular"
 797   long       = "int-wf-ind"
 798   type       = "bool"
 799   default    = "false"
 800   help       = "apply strengthening for integers based on well-founded induction"
 801
 802 [[option]]
 803   name       = "conjectureGen"
 804   category   = "regular"
 805   long       = "conjecture-gen"
 806   type       = "bool"
 807   default    = "false"
 808   help       = "generate candidate conjectures for inductive proofs"
 809
 810 [[option]]
 811   name       = "conjectureGenPerRound"
 812   category   = "regular"
 813   long       = "conjecture-gen-per-round=N"
 814   type       = "int"
 815   default    = "1"
 816   read_only  = true
 817   help       = "number of conjectures to generate per instantiation round"
 818
 819 [[option]]
 820   name       = "conjectureNoFilter"
 821   category   = "regular"
 822   long       = "conjecture-no-filter"
 823   type       = "bool"
 824   default    = "false"
 825   read_only  = true
 826   help       = "do not filter conjectures"
 827
 828 [[option]]
 829   name       = "conjectureFilterActiveTerms"
 830   category   = "regular"
 831   long       = "conjecture-filter-active-terms"
 832   type       = "bool"
 833   default    = "true"
 834   help       = "filter based on active terms"
 835
 836 [[option]]
 837   name       = "conjectureFilterCanonical"
 838   category   = "regular"
 839   long       = "conjecture-filter-canonical"
 840   type       = "bool"
 841   default    = "true"
 842   help       = "filter based on canonicity"
 843
 844 [[option]]
 845   name       = "conjectureFilterModel"
 846   category   = "regular"
 847   long       = "conjecture-filter-model"
 848   type       = "bool"
 849   default    = "true"
 850   help       = "filter based on model"
 851
 852 [[option]]
 853   name       = "conjectureGenGtEnum"
 854   category   = "regular"
 855   long       = "conjecture-gen-gt-enum=N"
 856   type       = "int"
 857   default    = "50"
 858   read_only  = true
 859   help       = "number of ground terms to generate for model filtering"
 860
 861 [[option]]
 862   name       = "conjectureUeeIntro"
 863   category   = "regular"
 864   long       = "conjecture-gen-uee-intro"
 865   type       = "bool"
 866   default    = "false"
 867   read_only  = true
 868   help       = "more aggressive merging for universal equality engine, introduces terms"
 869
 870 [[option]]
 871   name       = "conjectureGenMaxDepth"
 872   category   = "regular"
 873   long       = "conjecture-gen-max-depth=N"
 874   type       = "int"
 875   default    = "3"
 876   read_only  = true
 877   help       = "maximum depth of terms to consider for conjectures"
 878
 879 ### Synthesis options
 880
 881 [[option]]
 882   name       = "sygusInference"
 883   category   = "regular"
 884   long       = "sygus-inference"
 885   type       = "bool"
 886   default    = "false"
 887   read_only  = false
 888   help       = "attempt to preprocess arbitrary inputs to sygus conjectures"
 889
 890 [[option]]
 891   name       = "ceGuidedInst"
 892   category   = "regular"
 893   long       = "cegqi"
 894   type       = "bool"
 895   default    = "false"
 896   help       = "counterexample-guided quantifier instantiation for sygus"
 897
 898 [[option]]
 899   name       = "cegqiSingleInvMode"
 900   category   = "regular"
 901   long       = "cegqi-si=MODE"
 902   type       = "CVC4::theory::quantifiers::CegqiSingleInvMode"
 903   default    = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
 904   handler    = "stringToCegqiSingleInvMode"
 905   includes   = ["options/quantifiers_modes.h"]
 906   help       = "mode for processing single invocation synthesis conjectures"
 907
 908 [[option]]
 909   name       = "cegqiSingleInvPartial"
 910   category   = "regular"
 911   long       = "cegqi-si-partial"
 912   type       = "bool"
 913   default    = "false"
 914   read_only  = true
 915   help       = "combined techniques for synthesis conjectures that are partially single invocation"
 916
 917 [[option]]
 918   name       = "cegqiSingleInvReconstruct"
 919   category   = "regular"
 920   long       = "cegqi-si-reconstruct"
 921   type       = "bool"
 922   default    = "true"
 923   read_only  = true
 924   help       = "reconstruct solutions for single invocation conjectures in original grammar"
 925
 926 [[option]]
 927   name       = "cegqiSolMinCore"
 928   category   = "regular"
 929   long       = "cegqi-si-sol-min-core"
 930   type       = "bool"
 931   default    = "false"
 932   read_only  = true
 933   help       = "minimize solutions for single invocation conjectures based on unsat core"
 934
 935 [[option]]
 936   name       = "cegqiSolMinInst"
 937   category   = "regular"
 938   long       = "cegqi-si-sol-min-inst"
 939   type       = "bool"
 940   default    = "true"
 941   read_only  = true
 942   help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
 943
 944 [[option]]
 945   name       = "cegqiSingleInvReconstructConst"
 946   category   = "regular"
 947   long       = "cegqi-si-reconstruct-const"
 948   type       = "bool"
 949   default    = "true"
 950   read_only  = true
 951   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 952
 953 [[option]]
 954   name       = "cegqiSingleInvAbort"
 955   category   = "regular"
 956   long       = "cegqi-si-abort"
 957   type       = "bool"
 958   default    = "false"
 959   read_only  = true
 960   help       = "abort if synthesis conjecture is not single invocation"
 961
 962 [[option]]
 963   name       = "sygusUnif"
 964   category   = "regular"
 965   long       = "sygus-unif"
 966   type       = "bool"
 967   default    = "false"
 968   help       = "Unification-based function synthesis"
 969
 970 [[option]]
 971   name       = "sygusQePreproc"
 972   category   = "regular"
 973   long       = "sygus-qe-preproc"
 974   type       = "bool"
 975   default    = "false"
 976   read_only  = true
 977   help       = "use quantifier elimination as a preprocessing step for sygus"
 978
 979 [[option]]
 980   name       = "sygusMinGrammar"
 981   category   = "regular"
 982   long       = "sygus-min-grammar"
 983   type       = "bool"
 984   default    = "true"
 985   read_only  = true
 986   help       = "statically minimize sygus grammars"
 987
 988 [[option]]
 989   name       = "sygusAddConstGrammar"
 990   category   = "regular"
 991   long       = "sygus-add-const-grammar"
 992   type       = "bool"
 993   default    = "true"
 994   read_only  = true
 995   help       = "statically add constants appearing in conjecture to grammars"
 996
 997 [[option]]
 998   name       = "sygusGrammarNorm"
 999   category   = "regular"
1000   long       = "sygus-grammar-norm"
1001   type       = "bool"
1002   default    = "false"
1003   read_only  = true
1004   help       = "statically normalize sygus grammars based on flattening (linearization)"
1005
1006 [[option]]
1007   name       = "sygusTemplEmbedGrammar"
1008   category   = "regular"
1009   long       = "sygus-templ-embed-grammar"
1010   type       = "bool"
1011   default    = "false"
1012   read_only  = true
1013   help       = "embed sygus templates into grammars"
1014
1015 [[option]]
1016   name       = "sygusInvTemplMode"
1017   category   = "regular"
1018   long       = "sygus-inv-templ=MODE"
1019   type       = "CVC4::theory::quantifiers::SygusInvTemplMode"
1020   default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1021   handler    = "stringToSygusInvTemplMode"
1022   includes   = ["options/quantifiers_modes.h"]
1023   read_only  = true
1024   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1025
1026 [[option]]
1027   name       = "sygusInvTemplWhenSyntax"
1028   category   = "regular"
1029   long       = "sygus-inv-templ-when-sg"
1030   type       = "bool"
1031   default    = "false"
1032   read_only  = false
1033   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1034
1035 [[option]]
1036   name       = "sygusInvAutoUnfold"
1037   category   = "regular"
1038   long       = "sygus-auto-unfold"
1039   type       = "bool"
1040   default    = "true"
1041   read_only  = true
1042   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1043
1044 [[option]]
1045   name       = "sygusUnifPbe"
1046   category   = "regular"
1047   long       = "sygus-pbe"
1048   type       = "bool"
1049   default    = "true"
1050   help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1051
1052 [[option]]
1053   name       = "sygusDirectEval"
1054   category   = "regular"
1055   long       = "sygus-direct-eval"
1056   type       = "bool"
1057   default    = "true"
1058   read_only  = true
1059   help       = "direct unfolding of evaluation functions"
1060
1061 [[option]]
1062   name       = "sygusUnfoldBool"
1063   category   = "regular"
1064   long       = "sygus-unfold-bool"
1065   type       = "bool"
1066   default    = "true"
1067   read_only  = true
1068   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1069
1070 [[option]]
1071   name       = "sygusCRefEval"
1072   category   = "regular"
1073   long       = "sygus-cref-eval"
1074   type       = "bool"
1075   default    = "true"
1076   read_only  = true
1077   help       = "direct evaluation of refinement lemmas for conflict analysis"
1078
1079 [[option]]
1080   name       = "sygusCRefEvalMinExp"
1081   category   = "regular"
1082   long       = "sygus-cref-eval-min-exp"
1083   type       = "bool"
1084   default    = "true"
1085   read_only  = true
1086   help       = "use min explain for direct evaluation of refinement lemmas for conflict analysis"
1087
1088 [[option]]
1089   name       = "sygusStream"
1090   category   = "regular"
1091   long       = "sygus-stream"
1092   type       = "bool"
1093   default    = "false"
1094   help       = "enumerate a stream of solutions instead of terminating after the first one"
1095
1096 [[option]]
1097   name       = "sygusExtRew"
1098   category   = "regular"
1099   long       = "sygus-ext-rew"
1100   type       = "bool"
1101   default    = "true"
1102   help       = "use extended rewriter for sygus"
1103
1104 [[option]]
1105   name       = "cegisSample"
1106   category   = "regular"
1107   long       = "cegis-sample=MODE"
1108   type       = "CVC4::theory::quantifiers::CegisSampleMode"
1109   default    = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1110   handler    = "stringToCegisSampleMode"
1111   includes   = ["options/quantifiers_modes.h"]
1112   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
1113
1114 # Internal uses of sygus
1115
1116 [[option]]
1117   name       = "sygusRew"
1118   category   = "regular"
1119   long       = "sygus-rr"
1120   type       = "bool"
1121   default    = "false"
1122   read_only  = true
1123   help       = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
1124
1125 [[option]]
1126   name       = "sygusRewSynth"
1127   category   = "regular"
1128   long       = "sygus-rr-synth"
1129   type       = "bool"
1130   default    = "false"
1131   help       = "use sygus to enumerate candidate rewrite rules via sampling"
1132
1133 [[option]]
1134   name       = "sygusRewSynthFilterOrder"
1135   category   = "regular"
1136   long       = "sygus-rr-synth-filter-order"
1137   type       = "bool"
1138   default    = "true"
1139   help       = "filter candidate rewrites based on variable ordering"
1140
1141 [[option]]
1142   name       = "sygusRewSynthFilterMatch"
1143   category   = "regular"
1144   long       = "sygus-rr-synth-filter-match"
1145   type       = "bool"
1146   default    = "true"
1147   help       = "filter candidate rewrites based on matching"
1148
1149 [[option]]
1150   name       = "sygusRewSynthFilterCong"
1151   category   = "regular"
1152   long       = "sygus-rr-synth-filter-cong"
1153   type       = "bool"
1154   default    = "true"
1155   help       = "filter candidate rewrites based on congruence"
1156
1157 [[option]]
1158   name       = "sygusRewVerify"
1159   category   = "regular"
1160   long       = "sygus-rr-verify"
1161   type       = "bool"
1162   default    = "false"
1163   help       = "use sygus to verify the correctness of rewrite rules via sampling"
1164
1165 [[option]]
1166   name       = "sygusRewVerifyAbort"
1167   category   = "regular"
1168   long       = "sygus-rr-verify-abort"
1169   type       = "bool"
1170   default    = "true"
1171   help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1172
1173 [[option]]
1174   name       = "sygusSamples"
1175   category   = "regular"
1176   long       = "sygus-samples=N"
1177   type       = "int"
1178   default    = "1000"
1179   help       = "number of points to consider when doing sygus rewriter sample testing"
1180
1181 [[option]]
1182   name       = "sygusSampleGrammar"
1183   category   = "regular"
1184   long       = "sygus-sample-grammar"
1185   type       = "bool"
1186   default    = "true"
1187   read_only  = true
1188   help       = "when applicable, use grammar for choosing sample points"
1189
1190 [[option]]
1191   name       = "sygusRewSynthAccel"
1192   category   = "regular"
1193   long       = "sygus-rr-synth-accel"
1194   type       = "bool"
1195   default    = "false"
1196   help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
1197
1198 [[option]]
1199   name       = "sygusRewSynthCheck"
1200   category   = "regular"
1201   long       = "sygus-rr-synth-check"
1202   type       = "bool"
1203   default    = "false"
1204   help       = "use satisfiability check to verify correctness of candidate rewrites"
1205
1206 # CEGQI applied to general quantified formulas
1207
1208 [[option]]
1209   name       = "cbqi"
1210   category   = "regular"
1211   long       = "cbqi"
1212   type       = "bool"
1213   default    = "false"
1214   help       = "turns on counterexample-based quantifier instantiation"
1215
1216 [[option]]
1217   name       = "cbqiFullEffort"
1218   category   = "regular"
1219   long       = "cbqi-full"
1220   type       = "bool"
1221   default    = "false"
1222   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1223
1224 [[option]]
1225   name       = "recurseCbqi"
1226   category   = "regular"
1227   long       = "cbqi-recurse"
1228   type       = "bool"
1229   default    = "true"
1230   read_only  = true
1231   help       = "turns on recursive counterexample-based quantifier instantiation"
1232
1233 [[option]]
1234   name       = "cbqiSat"
1235   category   = "regular"
1236   long       = "cbqi-sat"
1237   type       = "bool"
1238   default    = "true"
1239   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1240
1241 [[option]]
1242   name       = "cbqiModel"
1243   category   = "regular"
1244   long       = "cbqi-model"
1245   type       = "bool"
1246   default    = "true"
1247   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1248
1249 [[option]]
1250   name       = "cbqiAll"
1251   category   = "regular"
1252   long       = "cbqi-all"
1253   type       = "bool"
1254   default    = "false"
1255   help       = "apply counterexample-based instantiation to all quantified formulas"
1256
1257 [[option]]
1258   name       = "cbqiMultiInst"
1259   category   = "regular"
1260   long       = "cbqi-multi-inst"
1261   type       = "bool"
1262   default    = "false"
1263   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1264
1265 [[option]]
1266   name       = "cbqiRepeatLit"
1267   category   = "regular"
1268   long       = "cbqi-repeat-lit"
1269   type       = "bool"
1270   default    = "false"
1271   help       = "solve literals more than once in counterexample-based quantifier instantiation"
1272
1273 [[option]]
1274   name       = "cbqiInnermost"
1275   category   = "regular"
1276   long       = "cbqi-innermost"
1277   type       = "bool"
1278   default    = "true"
1279   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1280
1281 [[option]]
1282   name       = "cbqiNestedQE"
1283   category   = "regular"
1284   long       = "cbqi-nested-qe"
1285   type       = "bool"
1286   default    = "false"
1287   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1288
1289 # CEGQI for arithmetic
1290
1291 [[option]]
1292   name       = "cbqiUseInfInt"
1293   category   = "regular"
1294   long       = "cbqi-use-inf-int"
1295   type       = "bool"
1296   default    = "false"
1297   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1298
1299 [[option]]
1300   name       = "cbqiUseInfReal"
1301   category   = "regular"
1302   long       = "cbqi-use-inf-real"
1303   type       = "bool"
1304   default    = "false"
1305   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1306
1307 [[option]]
1308   name       = "cbqiPreRegInst"
1309   category   = "regular"
1310   long       = "cbqi-prereg-inst"
1311   type       = "bool"
1312   default    = "false"
1313   help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
1314
1315 [[option]]
1316   name       = "cbqiMinBounds"
1317   category   = "regular"
1318   long       = "cbqi-min-bounds"
1319   type       = "bool"
1320   default    = "false"
1321   read_only  = true
1322   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1323
1324 [[option]]
1325   name       = "cbqiRoundUpLowerLia"
1326   category   = "regular"
1327   long       = "cbqi-round-up-lia"
1328   type       = "bool"
1329   default    = "false"
1330   read_only  = true
1331   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1332
1333 [[option]]
1334   name       = "cbqiMidpoint"
1335   category   = "regular"
1336   long       = "cbqi-midpoint"
1337   type       = "bool"
1338   default    = "false"
1339   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1340
1341 [[option]]
1342   name       = "cbqiNopt"
1343   category   = "regular"
1344   long       = "cbqi-nopt"
1345   type       = "bool"
1346   default    = "true"
1347   read_only  = true
1348   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1349
1350 [[option]]
1351   name       = "cbqiLitDepend"
1352   category   = "regular"
1353   long       = "cbqi-lit-dep"
1354   type       = "bool"
1355   default    = "true"
1356   read_only  = true
1357   help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1358
1359 # CEGQI for EPR
1360
1361 [[option]]
1362   name       = "quantEpr"
1363   category   = "regular"
1364   long       = "quant-epr"
1365   type       = "bool"
1366   default    = "false"
1367   help       = "infer whether in effectively propositional fragment, use for cbqi"
1368
1369 [[option]]
1370   name       = "quantEprMatching"
1371   category   = "regular"
1372   long       = "quant-epr-match"
1373   type       = "bool"
1374   default    = "true"
1375   read_only  = true
1376   help       = "use matching heuristics for EPR instantiation"
1377
1378 # CEGQI for BV
1379
1380 [[option]]
1381   name       = "cbqiBv"
1382   category   = "regular"
1383   long       = "cbqi-bv"
1384   type       = "bool"
1385   default    = "true"
1386   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1387
1388 [[option]]
1389   name       = "cbqiBvInterleaveValue"
1390   category   = "regular"
1391   long       = "cbqi-bv-interleave-value"
1392   type       = "bool"
1393   default    = "false"
1394   help       = "interleave model value instantiation with word-level inversion approach"
1395
1396 [[option]]
1397   name       = "cbqiBvIneqMode"
1398   category   = "regular"
1399   long       = "cbqi-bv-ineq=MODE"
1400   type       = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1401   default    = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1402   handler    = "stringToCbqiBvIneqMode"
1403   includes   = ["options/quantifiers_modes.h"]
1404   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1405
1406 [[option]]
1407   name       = "cbqiBvRmExtract"
1408   category   = "regular"
1409   long       = "cbqi-bv-rm-extract"
1410   type       = "bool"
1411   default    = "true"
1412   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1413
1414 [[option]]
1415   name       = "cbqiBvLinearize"
1416   category   = "regular"
1417   long       = "cbqi-bv-linear"
1418   type       = "bool"
1419   default    = "true"
1420   help       = "linearize adder chains for variables"
1421
1422 [[option]]
1423   name       = "cbqiBvConcInv"
1424   category   = "regular"
1425   long       = "cbqi-bv-concat-inv"
1426   type       = "bool"
1427   default    = "true"
1428   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1429
1430 ### Local theory extensions options
1431
1432 [[option]]
1433   name       = "localTheoryExt"
1434   category   = "regular"
1435   long       = "local-t-ext"
1436   type       = "bool"
1437   default    = "false"
1438   read_only  = true
1439   help       = "do instantiation based on local theory extensions"
1440
1441 [[option]]
1442   name       = "ltePartialInst"
1443   category   = "regular"
1444   long       = "lte-partial-inst"
1445   type       = "bool"
1446   default    = "false"
1447   read_only  = true
1448   help       = "partially instantiate local theory quantifiers"
1449
1450 [[option]]
1451   name       = "lteRestrictInstClosure"
1452   category   = "regular"
1453   long       = "lte-restrict-inst-closure"
1454   type       = "bool"
1455   default    = "false"
1456   read_only  = true
1457   help       = "treat arguments of inst closure as restricted terms for instantiation"
1458
1459 ### Reduction options
1460
1461 [[option]]
1462   name       = "quantAlphaEquiv"
1463   category   = "regular"
1464   long       = "quant-alpha-equiv"
1465   type       = "bool"
1466   default    = "true"
1467   read_only  = true
1468   help       = "infer alpha equivalence between quantified formulas"
1469
1470 [[option]]
1471   name       = "macrosQuant"
1472   category   = "regular"
1473   long       = "macros-quant"
1474   type       = "bool"
1475   default    = "false"
1476   help       = "perform quantifiers macro expansion"
1477
1478 [[option]]
1479   name       = "macrosQuantMode"
1480   category   = "regular"
1481   long       = "macros-quant-mode=MODE"
1482   type       = "CVC4::theory::quantifiers::MacrosQuantMode"
1483   default    = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1484   handler    = "stringToMacrosQuantMode"
1485   includes   = ["options/quantifiers_modes.h"]
1486   read_only  = true
1487   help       = "mode for quantifiers macro expansion"
1488
1489 [[option]]
1490   name       = "quantDynamicSplit"
1491   category   = "regular"
1492   long       = "quant-dsplit-mode=MODE"
1493   type       = "CVC4::theory::quantifiers::QuantDSplitMode"
1494   default    = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1495   handler    = "stringToQuantDSplitMode"
1496   includes   = ["options/quantifiers_modes.h"]
1497   help       = "mode for dynamic quantifiers splitting"
1498
1499 [[option]]
1500   name       = "quantAntiSkolem"
1501   category   = "regular"
1502   long       = "quant-anti-skolem"
1503   type       = "bool"
1504   default    = "false"
1505   help       = "perform anti-skolemization for quantified formulas"
1506
1507 ### Higher-order options
1508
1509 [[option]]
1510   name       = "hoMatching"
1511   category   = "regular"
1512   long       = "ho-matching"
1513   type       = "bool"
1514   default    = "true"
1515   read_only  = true
1516   help       = "do higher-order matching algorithm for triggers with variable operators"
1517
1518 [[option]]
1519   name       = "hoMatchingVarArgPriority"
1520   category   = "regular"
1521   long       = "ho-matching-var-priority"
1522   type       = "bool"
1523   default    = "true"
1524   read_only  = true
1525   help       = "give priority to variable arguments over constant arguments"
1526
1527 [[option]]
1528   name       = "hoMergeTermDb"
1529   category   = "regular"
1530   long       = "ho-merge-term-db"
1531   type       = "bool"
1532   default    = "true"
1533   read_only  = true
1534   help       = "merge term indices modulo equality"
1535
1536 ### Proof options
1537
1538 [[option]]
1539   name       = "trackInstLemmas"
1540   category   = "regular"
1541   long       = "track-inst-lemmas"
1542   type       = "bool"
1543   default    = "false"
1544   help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"