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       = "ceGuidedInst"
 883   category   = "regular"
 884   long       = "cegqi"
 885   type       = "bool"
 886   default    = "false"
 887   help       = "counterexample-guided quantifier instantiation for sygus"
 888
 889 [[option]]
 890   name       = "cegqiSingleInvMode"
 891   category   = "regular"
 892   long       = "cegqi-si=MODE"
 893   type       = "CVC4::theory::quantifiers::CegqiSingleInvMode"
 894   default    = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
 895   handler    = "stringToCegqiSingleInvMode"
 896   includes   = ["options/quantifiers_modes.h"]
 897   help       = "mode for processing single invocation synthesis conjectures"
 898
 899 [[option]]
 900   name       = "cegqiSingleInvPartial"
 901   category   = "regular"
 902   long       = "cegqi-si-partial"
 903   type       = "bool"
 904   default    = "false"
 905   read_only  = true
 906   help       = "combined techniques for synthesis conjectures that are partially single invocation"
 907
 908 [[option]]
 909   name       = "cegqiSingleInvReconstruct"
 910   category   = "regular"
 911   long       = "cegqi-si-reconstruct"
 912   type       = "bool"
 913   default    = "true"
 914   read_only  = true
 915   help       = "reconstruct solutions for single invocation conjectures in original grammar"
 916
 917 [[option]]
 918   name       = "cegqiSolMinCore"
 919   category   = "regular"
 920   long       = "cegqi-si-sol-min-core"
 921   type       = "bool"
 922   default    = "false"
 923   read_only  = true
 924   help       = "minimize solutions for single invocation conjectures based on unsat core"
 925
 926 [[option]]
 927   name       = "cegqiSolMinInst"
 928   category   = "regular"
 929   long       = "cegqi-si-sol-min-inst"
 930   type       = "bool"
 931   default    = "true"
 932   read_only  = true
 933   help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
 934
 935 [[option]]
 936   name       = "cegqiSingleInvReconstructConst"
 937   category   = "regular"
 938   long       = "cegqi-si-reconstruct-const"
 939   type       = "bool"
 940   default    = "true"
 941   read_only  = true
 942   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 943
 944 [[option]]
 945   name       = "cegqiSingleInvAbort"
 946   category   = "regular"
 947   long       = "cegqi-si-abort"
 948   type       = "bool"
 949   default    = "false"
 950   read_only  = true
 951   help       = "abort if synthesis conjecture is not single invocation"
 952
 953 [[option]]
 954   name       = "sygusPbe"
 955   category   = "regular"
 956   long       = "sygus-pbe"
 957   type       = "bool"
 958   default    = "true"
 959   help       = "sygus advanced pruning based on examples"
 960
 961 [[option]]
 962   name       = "sygusQePreproc"
 963   category   = "regular"
 964   long       = "sygus-qe-preproc"
 965   type       = "bool"
 966   default    = "false"
 967   read_only  = true
 968   help       = "use quantifier elimination as a preprocessing step for sygus"
 969
 970 [[option]]
 971   name       = "sygusMinGrammar"
 972   category   = "regular"
 973   long       = "sygus-min-grammar"
 974   type       = "bool"
 975   default    = "true"
 976   read_only  = true
 977   help       = "statically minimize sygus grammars"
 978
 979 [[option]]
 980   name       = "sygusAddConstGrammar"
 981   category   = "regular"
 982   long       = "sygus-add-const-grammar"
 983   type       = "bool"
 984   default    = "true"
 985   read_only  = true
 986   help       = "statically add constants appearing in conjecture to grammars"
 987
 988 [[option]]
 989   name       = "sygusGrammarNorm"
 990   category   = "regular"
 991   long       = "sygus-grammar-norm"
 992   type       = "bool"
 993   default    = "false"
 994   read_only  = true
 995   help       = "statically normalize sygus grammars based on flattening (linearization)"
 996
 997 [[option]]
 998   name       = "sygusTemplEmbedGrammar"
 999   category   = "regular"
1000   long       = "sygus-templ-embed-grammar"
1001   type       = "bool"
1002   default    = "false"
1003   read_only  = true
1004   help       = "embed sygus templates into grammars"
1005
1006 [[option]]
1007   name       = "sygusInvTemplMode"
1008   category   = "regular"
1009   long       = "sygus-inv-templ=MODE"
1010   type       = "CVC4::theory::quantifiers::SygusInvTemplMode"
1011   default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1012   handler    = "stringToSygusInvTemplMode"
1013   includes   = ["options/quantifiers_modes.h"]
1014   read_only  = true
1015   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1016
1017 [[option]]
1018   name       = "sygusInvTemplWhenSyntax"
1019   category   = "regular"
1020   long       = "sygus-inv-templ-when-sg"
1021   type       = "bool"
1022   default    = "false"
1023   read_only  = false
1024   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1025
1026 [[option]]
1027   name       = "sygusInvAutoUnfold"
1028   category   = "regular"
1029   long       = "sygus-auto-unfold"
1030   type       = "bool"
1031   default    = "true"
1032   read_only  = true
1033   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1034
1035 [[option]]
1036   name       = "sygusUnifCondSol"
1037   category   = "regular"
1038   long       = "sygus-unif-csol"
1039   type       = "bool"
1040   default    = "true"
1041   read_only  = true
1042   help       = "enable new approach which unifies conditional solutions"
1043
1044 [[option]]
1045   name       = "sygusDirectEval"
1046   category   = "regular"
1047   long       = "sygus-direct-eval"
1048   type       = "bool"
1049   default    = "true"
1050   read_only  = true
1051   help       = "direct unfolding of evaluation functions"
1052
1053 [[option]]
1054   name       = "sygusUnfoldBool"
1055   category   = "regular"
1056   long       = "sygus-unfold-bool"
1057   type       = "bool"
1058   default    = "true"
1059   read_only  = true
1060   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1061
1062 [[option]]
1063   name       = "sygusCRefEval"
1064   category   = "regular"
1065   long       = "sygus-cref-eval"
1066   type       = "bool"
1067   default    = "true"
1068   read_only  = true
1069   help       = "direct evaluation of refinement lemmas for conflict analysis"
1070
1071 [[option]]
1072   name       = "sygusCRefEvalMinExp"
1073   category   = "regular"
1074   long       = "sygus-cref-eval-min-exp"
1075   type       = "bool"
1076   default    = "true"
1077   read_only  = true
1078   help       = "use min explain for direct evaluation of refinement lemmas for conflict analysis"
1079
1080 [[option]]
1081   name       = "sygusStream"
1082   category   = "regular"
1083   long       = "sygus-stream"
1084   type       = "bool"
1085   default    = "false"
1086   help       = "enumerate a stream of solutions instead of terminating after the first one"
1087
1088 [[option]]
1089   name       = "cegisSample"
1090   category   = "regular"
1091   long       = "cegis-sample=MODE"
1092   type       = "CVC4::theory::quantifiers::CegisSampleMode"
1093   default    = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1094   handler    = "stringToCegisSampleMode"
1095   includes   = ["options/quantifiers_modes.h"]
1096   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
1097
1098 # Internal uses of sygus
1099
1100 [[option]]
1101   name       = "sygusRew"
1102   category   = "regular"
1103   long       = "sygus-rr"
1104   type       = "bool"
1105   default    = "false"
1106   read_only  = true
1107   help       = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
1108
1109 [[option]]
1110   name       = "sygusRewSynth"
1111   category   = "regular"
1112   long       = "sygus-rr-synth"
1113   type       = "bool"
1114   default    = "false"
1115   help       = "use sygus to enumerate candidate rewrite rules via sampling"
1116
1117 [[option]]
1118   name       = "sygusRewVerify"
1119   category   = "regular"
1120   long       = "sygus-rr-verify"
1121   type       = "bool"
1122   default    = "false"
1123   help       = "use sygus to verify the correctness of rewrite rules via sampling"
1124
1125 [[option]]
1126   name       = "sygusRewVerifyAbort"
1127   category   = "regular"
1128   long       = "sygus-rr-verify-abort"
1129   type       = "bool"
1130   default    = "true"
1131   help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1132
1133 [[option]]
1134   name       = "sygusSamples"
1135   category   = "regular"
1136   long       = "sygus-samples=N"
1137   type       = "int"
1138   default    = "1000"
1139   help       = "number of points to consider when doing sygus rewriter sample testing"
1140
1141 [[option]]
1142   name       = "sygusSampleGrammar"
1143   category   = "regular"
1144   long       = "sygus-sample-grammar"
1145   type       = "bool"
1146   default    = "true"
1147   read_only  = true
1148   help       = "when applicable, use grammar for choosing sample points"
1149
1150
1151 # CEGQI applied to general quantified formulas
1152
1153 [[option]]
1154   name       = "cbqi"
1155   category   = "regular"
1156   long       = "cbqi"
1157   type       = "bool"
1158   default    = "false"
1159   help       = "turns on counterexample-based quantifier instantiation"
1160
1161 [[option]]
1162   name       = "cbqiFullEffort"
1163   category   = "regular"
1164   long       = "cbqi-full"
1165   type       = "bool"
1166   default    = "false"
1167   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1168
1169 [[option]]
1170   name       = "recurseCbqi"
1171   category   = "regular"
1172   long       = "cbqi-recurse"
1173   type       = "bool"
1174   default    = "true"
1175   read_only  = true
1176   help       = "turns on recursive counterexample-based quantifier instantiation"
1177
1178 [[option]]
1179   name       = "cbqiSat"
1180   category   = "regular"
1181   long       = "cbqi-sat"
1182   type       = "bool"
1183   default    = "true"
1184   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1185
1186 [[option]]
1187   name       = "cbqiModel"
1188   category   = "regular"
1189   long       = "cbqi-model"
1190   type       = "bool"
1191   default    = "true"
1192   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1193
1194 [[option]]
1195   name       = "cbqiAll"
1196   category   = "regular"
1197   long       = "cbqi-all"
1198   type       = "bool"
1199   default    = "false"
1200   help       = "apply counterexample-based instantiation to all quantified formulas"
1201
1202 [[option]]
1203   name       = "cbqiMultiInst"
1204   category   = "regular"
1205   long       = "cbqi-multi-inst"
1206   type       = "bool"
1207   default    = "false"
1208   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1209
1210 [[option]]
1211   name       = "cbqiRepeatLit"
1212   category   = "regular"
1213   long       = "cbqi-repeat-lit"
1214   type       = "bool"
1215   default    = "false"
1216   help       = "solve literals more than once in counterexample-based quantifier instantiation"
1217
1218 [[option]]
1219   name       = "cbqiInnermost"
1220   category   = "regular"
1221   long       = "cbqi-innermost"
1222   type       = "bool"
1223   default    = "true"
1224   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1225
1226 [[option]]
1227   name       = "cbqiNestedQE"
1228   category   = "regular"
1229   long       = "cbqi-nested-qe"
1230   type       = "bool"
1231   default    = "false"
1232   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1233
1234 # CEGQI for arithmetic
1235
1236 [[option]]
1237   name       = "cbqiUseInfInt"
1238   category   = "regular"
1239   long       = "cbqi-use-inf-int"
1240   type       = "bool"
1241   default    = "false"
1242   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1243
1244 [[option]]
1245   name       = "cbqiUseInfReal"
1246   category   = "regular"
1247   long       = "cbqi-use-inf-real"
1248   type       = "bool"
1249   default    = "false"
1250   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1251
1252 [[option]]
1253   name       = "cbqiPreRegInst"
1254   category   = "regular"
1255   long       = "cbqi-prereg-inst"
1256   type       = "bool"
1257   default    = "false"
1258   help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
1259
1260 [[option]]
1261   name       = "cbqiMinBounds"
1262   category   = "regular"
1263   long       = "cbqi-min-bounds"
1264   type       = "bool"
1265   default    = "false"
1266   read_only  = true
1267   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1268
1269 [[option]]
1270   name       = "cbqiRoundUpLowerLia"
1271   category   = "regular"
1272   long       = "cbqi-round-up-lia"
1273   type       = "bool"
1274   default    = "false"
1275   read_only  = true
1276   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1277
1278 [[option]]
1279   name       = "cbqiMidpoint"
1280   category   = "regular"
1281   long       = "cbqi-midpoint"
1282   type       = "bool"
1283   default    = "false"
1284   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1285
1286 [[option]]
1287   name       = "cbqiNopt"
1288   category   = "regular"
1289   long       = "cbqi-nopt"
1290   type       = "bool"
1291   default    = "true"
1292   read_only  = true
1293   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1294
1295 [[option]]
1296   name       = "cbqiLitDepend"
1297   category   = "regular"
1298   long       = "cbqi-lit-dep"
1299   type       = "bool"
1300   default    = "true"
1301   read_only  = true
1302   help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1303
1304 # CEGQI for EPR
1305
1306 [[option]]
1307   name       = "quantEpr"
1308   category   = "regular"
1309   long       = "quant-epr"
1310   type       = "bool"
1311   default    = "false"
1312   help       = "infer whether in effectively propositional fragment, use for cbqi"
1313
1314 [[option]]
1315   name       = "quantEprMatching"
1316   category   = "regular"
1317   long       = "quant-epr-match"
1318   type       = "bool"
1319   default    = "true"
1320   read_only  = true
1321   help       = "use matching heuristics for EPR instantiation"
1322
1323 # CEGQI for BV
1324
1325 [[option]]
1326   name       = "cbqiBv"
1327   category   = "regular"
1328   long       = "cbqi-bv"
1329   type       = "bool"
1330   default    = "true"
1331   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1332
1333 [[option]]
1334   name       = "cbqiBvInterleaveValue"
1335   category   = "regular"
1336   long       = "cbqi-bv-interleave-value"
1337   type       = "bool"
1338   default    = "false"
1339   help       = "interleave model value instantiation with word-level inversion approach"
1340
1341 [[option]]
1342   name       = "cbqiBvIneqMode"
1343   category   = "regular"
1344   long       = "cbqi-bv-ineq=MODE"
1345   type       = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1346   default    = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1347   handler    = "stringToCbqiBvIneqMode"
1348   includes   = ["options/quantifiers_modes.h"]
1349   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1350
1351 [[option]]
1352   name       = "cbqiBvRmExtract"
1353   category   = "regular"
1354   long       = "cbqi-bv-rm-extract"
1355   type       = "bool"
1356   default    = "true"
1357   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1358
1359 [[option]]
1360   name       = "cbqiBvLinearize"
1361   category   = "regular"
1362   long       = "cbqi-bv-linear"
1363   type       = "bool"
1364   default    = "true"
1365   help       = "linearize adder chains for variables"
1366
1367 [[option]]
1368   name       = "cbqiBvConcInv"
1369   category   = "regular"
1370   long       = "cbqi-bv-concat-inv"
1371   type       = "bool"
1372   default    = "true"
1373   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1374
1375 ### Local theory extensions options
1376
1377 [[option]]
1378   name       = "localTheoryExt"
1379   category   = "regular"
1380   long       = "local-t-ext"
1381   type       = "bool"
1382   default    = "false"
1383   read_only  = true
1384   help       = "do instantiation based on local theory extensions"
1385
1386 [[option]]
1387   name       = "ltePartialInst"
1388   category   = "regular"
1389   long       = "lte-partial-inst"
1390   type       = "bool"
1391   default    = "false"
1392   read_only  = true
1393   help       = "partially instantiate local theory quantifiers"
1394
1395 [[option]]
1396   name       = "lteRestrictInstClosure"
1397   category   = "regular"
1398   long       = "lte-restrict-inst-closure"
1399   type       = "bool"
1400   default    = "false"
1401   read_only  = true
1402   help       = "treat arguments of inst closure as restricted terms for instantiation"
1403
1404 ### Reduction options
1405
1406 [[option]]
1407   name       = "quantAlphaEquiv"
1408   category   = "regular"
1409   long       = "quant-alpha-equiv"
1410   type       = "bool"
1411   default    = "true"
1412   read_only  = true
1413   help       = "infer alpha equivalence between quantified formulas"
1414
1415 [[option]]
1416   name       = "macrosQuant"
1417   category   = "regular"
1418   long       = "macros-quant"
1419   type       = "bool"
1420   default    = "false"
1421   help       = "perform quantifiers macro expansion"
1422
1423 [[option]]
1424   name       = "macrosQuantMode"
1425   category   = "regular"
1426   long       = "macros-quant-mode=MODE"
1427   type       = "CVC4::theory::quantifiers::MacrosQuantMode"
1428   default    = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1429   handler    = "stringToMacrosQuantMode"
1430   includes   = ["options/quantifiers_modes.h"]
1431   read_only  = true
1432   help       = "mode for quantifiers macro expansion"
1433
1434 [[option]]
1435   name       = "quantDynamicSplit"
1436   category   = "regular"
1437   long       = "quant-dsplit-mode=MODE"
1438   type       = "CVC4::theory::quantifiers::QuantDSplitMode"
1439   default    = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1440   handler    = "stringToQuantDSplitMode"
1441   includes   = ["options/quantifiers_modes.h"]
1442   help       = "mode for dynamic quantifiers splitting"
1443
1444 [[option]]
1445   name       = "quantAntiSkolem"
1446   category   = "regular"
1447   long       = "quant-anti-skolem"
1448   type       = "bool"
1449   default    = "false"
1450   help       = "perform anti-skolemization for quantified formulas"
1451
1452 ### Higher-order options
1453
1454 [[option]]
1455   name       = "hoMatching"
1456   category   = "regular"
1457   long       = "ho-matching"
1458   type       = "bool"
1459   default    = "true"
1460   read_only  = true
1461   help       = "do higher-order matching algorithm for triggers with variable operators"
1462
1463 [[option]]
1464   name       = "hoMatchingVarArgPriority"
1465   category   = "regular"
1466   long       = "ho-matching-var-priority"
1467   type       = "bool"
1468   default    = "true"
1469   read_only  = true
1470   help       = "give priority to variable arguments over constant arguments"
1471
1472 [[option]]
1473   name       = "hoMergeTermDb"
1474   category   = "regular"
1475   long       = "ho-merge-term-db"
1476   type       = "bool"
1477   default    = "true"
1478   read_only  = true
1479   help       = "merge term indices modulo equality"
1480
1481 ### Proof options
1482
1483 [[option]]
1484   name       = "trackInstLemmas"
1485   category   = "regular"
1486   long       = "track-inst-lemmas"
1487   type       = "bool"
1488   default    = "false"
1489   help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"