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