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-independent-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    = "false"
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       = "sygusActiveGenMode"
1036   category   = "regular"
1037   long       = "sygus-active-gen=MODE"
1038   type       = "CVC4::theory::quantifiers::SygusActiveGenMode"
1039   default    = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE"
1040   handler    = "stringToSygusActiveGenMode"
1041   includes   = ["options/quantifiers_modes.h"]
1042   read_only  = true
1043   help       = "mode for actively-generated sygus enumerators"
1044
1045 [[option]]
1046   name       = "sygusMinGrammar"
1047   category   = "regular"
1048   long       = "sygus-min-grammar"
1049   type       = "bool"
1050   default    = "true"
1051   read_only  = true
1052   help       = "statically minimize sygus grammars"
1053
1054 [[option]]
1055   name       = "sygusAddConstGrammar"
1056   category   = "regular"
1057   long       = "sygus-add-const-grammar"
1058   type       = "bool"
1059   default    = "false"
1060   read_only  = true
1061   help       = "statically add constants appearing in conjecture to grammars"
1062
1063 [[option]]
1064   name       = "sygusGrammarNorm"
1065   category   = "regular"
1066   long       = "sygus-grammar-norm"
1067   type       = "bool"
1068   default    = "false"
1069   read_only  = true
1070   help       = "statically normalize sygus grammars based on flattening (linearization)"
1071
1072 [[option]]
1073   name       = "sygusTemplEmbedGrammar"
1074   category   = "regular"
1075   long       = "sygus-templ-embed-grammar"
1076   type       = "bool"
1077   default    = "false"
1078   read_only  = true
1079   help       = "embed sygus templates into grammars"
1080
1081 [[option]]
1082   name       = "sygusInvTemplMode"
1083   category   = "regular"
1084   long       = "sygus-inv-templ=MODE"
1085   type       = "CVC4::theory::quantifiers::SygusInvTemplMode"
1086   default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1087   handler    = "stringToSygusInvTemplMode"
1088   includes   = ["options/quantifiers_modes.h"]
1089   read_only  = true
1090   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1091
1092 [[option]]
1093   name       = "sygusInvTemplWhenSyntax"
1094   category   = "regular"
1095   long       = "sygus-inv-templ-when-sg"
1096   type       = "bool"
1097   default    = "false"
1098   read_only  = false
1099   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1100
1101 [[option]]
1102   name       = "sygusInvAutoUnfold"
1103   category   = "regular"
1104   long       = "sygus-auto-unfold"
1105   type       = "bool"
1106   default    = "true"
1107   read_only  = true
1108   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1109
1110 [[option]]
1111   name       = "sygusUnifPbe"
1112   category   = "regular"
1113   long       = "sygus-pbe"
1114   type       = "bool"
1115   default    = "true"
1116   help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1117
1118 [[option]]
1119   name       = "sygusPbeMultiFair"
1120   category   = "regular"
1121   long       = "sygus-pbe-multi-fair"
1122   type       = "bool"
1123   default    = "true"
1124   help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
1125
1126 [[option]]
1127   name       = "sygusPbeMultiFairDiff"
1128   category   = "regular"
1129   long       = "sygus-pbe-multi-fair-diff=N"
1130   type       = "int"
1131   default    = "0"
1132   help       = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1133
1134 [[option]]
1135   name       = "sygusEvalUnfold"
1136   category   = "regular"
1137   long       = "sygus-eval-unfold"
1138   type       = "bool"
1139   default    = "true"
1140   read_only  = true
1141   help       = "do unfolding of sygus evaluation functions"
1142
1143 [[option]]
1144   name       = "sygusEvalUnfoldBool"
1145   category   = "regular"
1146   long       = "sygus-eval-unfold-bool"
1147   type       = "bool"
1148   default    = "true"
1149   read_only  = true
1150   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1151
1152 [[option]]
1153   name       = "sygusRefEval"
1154   category   = "regular"
1155   long       = "sygus-ref-eval"
1156   type       = "bool"
1157   default    = "true"
1158   read_only  = true
1159   help       = "direct evaluation of refinement lemmas for conflict analysis"
1160
1161 [[option]]
1162   name       = "sygusStream"
1163   category   = "regular"
1164   long       = "sygus-stream"
1165   type       = "bool"
1166   default    = "false"
1167   help       = "enumerate a stream of solutions instead of terminating after the first one"
1168
1169 [[option]]
1170   name       = "sygusVerifySubcall"
1171   category   = "regular"
1172   long       = "sygus-verify-subcall"
1173   type       = "bool"
1174   default    = "true"
1175   help       = "use separate copy of the SMT solver for verification lemmas in sygus"
1176
1177 [[option]]
1178   name       = "sygusExtRew"
1179   category   = "regular"
1180   long       = "sygus-ext-rew"
1181   type       = "bool"
1182   default    = "true"
1183   help       = "use extended rewriter for sygus"
1184
1185 [[option]]
1186   name       = "cegisSample"
1187   category   = "regular"
1188   long       = "cegis-sample=MODE"
1189   type       = "CVC4::theory::quantifiers::CegisSampleMode"
1190   default    = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1191   handler    = "stringToCegisSampleMode"
1192   includes   = ["options/quantifiers_modes.h"]
1193   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
1194
1195 [[option]]
1196   name       = "minSynthSol"
1197   category   = "regular"
1198   long       = "min-synth-sol"
1199   type       = "bool"
1200   default    = "true"
1201   help       = "Minimize synthesis solutions"
1202
1203 [[option]]
1204   name       = "sygusEvalOpt"
1205   category   = "regular"
1206   long       = "sygus-eval-opt"
1207   type       = "bool"
1208   default    = "true"
1209   help       = "use optimized approach for evaluation in sygus"
1210
1211 [[option]]
1212   name       = "sygusArgRelevant"
1213   category   = "regular"
1214   long       = "sygus-arg-relevant"
1215   type       = "bool"
1216   default    = "false"
1217   help       = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1218
1219 # Internal uses of sygus
1220
1221 [[option]]
1222   name       = "sygusRew"
1223   category   = "regular"
1224   long       = "sygus-rr"
1225   type       = "bool"
1226   default    = "false"
1227   read_only  = true
1228   help       = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
1229
1230 [[option]]
1231   name       = "sygusRewSynth"
1232   category   = "regular"
1233   long       = "sygus-rr-synth"
1234   type       = "bool"
1235   default    = "false"
1236   help       = "use sygus to enumerate candidate rewrite rules via sampling"
1237
1238 [[option]]
1239   name       = "sygusRewSynthFilterOrder"
1240   category   = "regular"
1241   long       = "sygus-rr-synth-filter-order"
1242   type       = "bool"
1243   default    = "true"
1244   help       = "filter candidate rewrites based on variable ordering"
1245
1246 [[option]]
1247   name       = "sygusRewSynthFilterMatch"
1248   category   = "regular"
1249   long       = "sygus-rr-synth-filter-match"
1250   type       = "bool"
1251   default    = "true"
1252   help       = "filter candidate rewrites based on matching"
1253
1254 [[option]]
1255   name       = "sygusRewSynthFilterCong"
1256   category   = "regular"
1257   long       = "sygus-rr-synth-filter-cong"
1258   type       = "bool"
1259   default    = "true"
1260   help       = "filter candidate rewrites based on congruence"
1261
1262 [[option]]
1263   name       = "sygusRewSynthFilterNonLinear"
1264   category   = "regular"
1265   long       = "sygus-rr-synth-filter-nl"
1266   type       = "bool"
1267   default    = "false"
1268   help       = "filter non-linear candidate rewrites"
1269
1270 [[option]]
1271   name       = "sygusRewVerify"
1272   category   = "regular"
1273   long       = "sygus-rr-verify"
1274   type       = "bool"
1275   default    = "false"
1276   help       = "use sygus to verify the correctness of rewrite rules via sampling"
1277
1278 [[option]]
1279   name       = "sygusRewVerifyAbort"
1280   category   = "regular"
1281   long       = "sygus-rr-verify-abort"
1282   type       = "bool"
1283   default    = "true"
1284   help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1285
1286 [[option]]
1287   name       = "sygusSamples"
1288   category   = "regular"
1289   long       = "sygus-samples=N"
1290   type       = "int"
1291   default    = "1000"
1292   help       = "number of points to consider when doing sygus rewriter sample testing"
1293
1294 [[option]]
1295   name       = "sygusSampleGrammar"
1296   category   = "regular"
1297   long       = "sygus-sample-grammar"
1298   type       = "bool"
1299   default    = "true"
1300   read_only  = true
1301   help       = "when applicable, use grammar for choosing sample points"
1302
1303 [[option]]
1304   name       = "sygusSampleFpUniform"
1305   category   = "regular"
1306   long       = "sygus-sample-fp-uniform"
1307   type       = "bool"
1308   default    = "false"
1309   help       = "sample floating-point values uniformly instead of in a biased fashion"
1310
1311 [[option]]
1312   name       = "sygusRewSynthAccel"
1313   category   = "regular"
1314   long       = "sygus-rr-synth-accel"
1315   type       = "bool"
1316   default    = "false"
1317   help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
1318
1319 [[option]]
1320   name       = "sygusRewSynthCheck"
1321   category   = "regular"
1322   long       = "sygus-rr-synth-check"
1323   type       = "bool"
1324   default    = "false"
1325   help       = "use satisfiability check to verify correctness of candidate rewrites"
1326
1327 [[option]]
1328   name       = "sygusRewSynthInput"
1329   category   = "regular"
1330   long       = "sygus-rr-synth-input"
1331   type       = "bool"
1332   default    = "false"
1333   help       = "synthesize rewrite rules based on the input formula"
1334
1335 [[option]]
1336   name       = "sygusRewSynthInputNVars"
1337   category   = "regular"
1338   long       = "sygus-rr-synth-input-nvars=N"
1339   type       = "int"
1340   default    = "3"
1341   help       = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
1342
1343 [[option]]
1344   name       = "sygusRewSynthInputUseBool"
1345   category   = "regular"
1346   long       = "sygus-rr-synth-input-use-bool"
1347   type       = "bool"
1348   default    = "false"
1349   help       = "synthesize Boolean rewrite rules based on the input formula"
1350
1351 [[option]]
1352   name       = "sygusExprMinerCheckTimeout"
1353   category   = "regular"
1354   long       = "sygus-expr-miner-check-timeout=N"
1355   type       = "unsigned long"
1356   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
1357
1358 # CEGQI applied to general quantified formulas
1359
1360 [[option]]
1361   name       = "cbqi"
1362   category   = "regular"
1363   long       = "cbqi"
1364   type       = "bool"
1365   default    = "false"
1366   help       = "turns on counterexample-based quantifier instantiation"
1367
1368 [[option]]
1369   name       = "cbqiFullEffort"
1370   category   = "regular"
1371   long       = "cbqi-full"
1372   type       = "bool"
1373   default    = "false"
1374   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1375
1376 [[option]]
1377   name       = "recurseCbqi"
1378   category   = "regular"
1379   long       = "cbqi-recurse"
1380   type       = "bool"
1381   default    = "true"
1382   read_only  = true
1383   help       = "turns on recursive counterexample-based quantifier instantiation"
1384
1385 [[option]]
1386   name       = "cbqiSat"
1387   category   = "regular"
1388   long       = "cbqi-sat"
1389   type       = "bool"
1390   default    = "true"
1391   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1392
1393 [[option]]
1394   name       = "cbqiModel"
1395   category   = "regular"
1396   long       = "cbqi-model"
1397   type       = "bool"
1398   default    = "true"
1399   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1400
1401 [[option]]
1402   name       = "cbqiAll"
1403   category   = "regular"
1404   long       = "cbqi-all"
1405   type       = "bool"
1406   default    = "false"
1407   help       = "apply counterexample-based instantiation to all quantified formulas"
1408
1409 [[option]]
1410   name       = "cbqiMultiInst"
1411   category   = "regular"
1412   long       = "cbqi-multi-inst"
1413   type       = "bool"
1414   default    = "false"
1415   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1416
1417 [[option]]
1418   name       = "cbqiRepeatLit"
1419   category   = "regular"
1420   long       = "cbqi-repeat-lit"
1421   type       = "bool"
1422   default    = "false"
1423   help       = "solve literals more than once in counterexample-based quantifier instantiation"
1424
1425 [[option]]
1426   name       = "cbqiInnermost"
1427   category   = "regular"
1428   long       = "cbqi-innermost"
1429   type       = "bool"
1430   default    = "true"
1431   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1432
1433 [[option]]
1434   name       = "cbqiNestedQE"
1435   category   = "regular"
1436   long       = "cbqi-nested-qe"
1437   type       = "bool"
1438   default    = "false"
1439   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1440
1441 # CEGQI for arithmetic
1442
1443 [[option]]
1444   name       = "cbqiUseInfInt"
1445   category   = "regular"
1446   long       = "cbqi-use-inf-int"
1447   type       = "bool"
1448   default    = "false"
1449   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1450
1451 [[option]]
1452   name       = "cbqiUseInfReal"
1453   category   = "regular"
1454   long       = "cbqi-use-inf-real"
1455   type       = "bool"
1456   default    = "false"
1457   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1458
1459 [[option]]
1460   name       = "cbqiPreRegInst"
1461   category   = "regular"
1462   long       = "cbqi-prereg-inst"
1463   type       = "bool"
1464   default    = "false"
1465   help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
1466
1467 [[option]]
1468   name       = "cbqiMinBounds"
1469   category   = "regular"
1470   long       = "cbqi-min-bounds"
1471   type       = "bool"
1472   default    = "false"
1473   read_only  = true
1474   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1475
1476 [[option]]
1477   name       = "cbqiRoundUpLowerLia"
1478   category   = "regular"
1479   long       = "cbqi-round-up-lia"
1480   type       = "bool"
1481   default    = "false"
1482   read_only  = true
1483   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1484
1485 [[option]]
1486   name       = "cbqiMidpoint"
1487   category   = "regular"
1488   long       = "cbqi-midpoint"
1489   type       = "bool"
1490   default    = "false"
1491   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1492
1493 [[option]]
1494   name       = "cbqiNopt"
1495   category   = "regular"
1496   long       = "cbqi-nopt"
1497   type       = "bool"
1498   default    = "true"
1499   read_only  = true
1500   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1501
1502 [[option]]
1503   name       = "cbqiLitDepend"
1504   category   = "regular"
1505   long       = "cbqi-lit-dep"
1506   type       = "bool"
1507   default    = "true"
1508   read_only  = true
1509   help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1510
1511 # CEGQI for EPR
1512
1513 [[option]]
1514   name       = "quantEpr"
1515   category   = "regular"
1516   long       = "quant-epr"
1517   type       = "bool"
1518   default    = "false"
1519   help       = "infer whether in effectively propositional fragment, use for cbqi"
1520
1521 [[option]]
1522   name       = "quantEprMatching"
1523   category   = "regular"
1524   long       = "quant-epr-match"
1525   type       = "bool"
1526   default    = "true"
1527   read_only  = true
1528   help       = "use matching heuristics for EPR instantiation"
1529
1530 # CEGQI for BV
1531
1532 [[option]]
1533   name       = "cbqiBv"
1534   category   = "regular"
1535   long       = "cbqi-bv"
1536   type       = "bool"
1537   default    = "true"
1538   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1539
1540 [[option]]
1541   name       = "cbqiBvInterleaveValue"
1542   category   = "regular"
1543   long       = "cbqi-bv-interleave-value"
1544   type       = "bool"
1545   default    = "false"
1546   help       = "interleave model value instantiation with word-level inversion approach"
1547
1548 [[option]]
1549   name       = "cbqiBvIneqMode"
1550   category   = "regular"
1551   long       = "cbqi-bv-ineq=MODE"
1552   type       = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1553   default    = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1554   handler    = "stringToCbqiBvIneqMode"
1555   includes   = ["options/quantifiers_modes.h"]
1556   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1557
1558 [[option]]
1559   name       = "cbqiBvRmExtract"
1560   category   = "regular"
1561   long       = "cbqi-bv-rm-extract"
1562   type       = "bool"
1563   default    = "true"
1564   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1565
1566 [[option]]
1567   name       = "cbqiBvLinearize"
1568   category   = "regular"
1569   long       = "cbqi-bv-linear"
1570   type       = "bool"
1571   default    = "true"
1572   help       = "linearize adder chains for variables"
1573
1574 [[option]]
1575   name       = "cbqiBvSolveNl"
1576   category   = "regular"
1577   long       = "cbqi-bv-solve-nl"
1578   type       = "bool"
1579   default    = "false"
1580   help       = "try to solve non-linear bv literals using model value projections"
1581
1582 [[option]]
1583   name       = "cbqiBvConcInv"
1584   category   = "regular"
1585   long       = "cbqi-bv-concat-inv"
1586   type       = "bool"
1587   default    = "true"
1588   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1589
1590 ### Local theory extensions options
1591
1592 [[option]]
1593   name       = "localTheoryExt"
1594   category   = "regular"
1595   long       = "local-t-ext"
1596   type       = "bool"
1597   default    = "false"
1598   read_only  = true
1599   help       = "do instantiation based on local theory extensions"
1600
1601 [[option]]
1602   name       = "ltePartialInst"
1603   category   = "regular"
1604   long       = "lte-partial-inst"
1605   type       = "bool"
1606   default    = "false"
1607   read_only  = true
1608   help       = "partially instantiate local theory quantifiers"
1609
1610 [[option]]
1611   name       = "lteRestrictInstClosure"
1612   category   = "regular"
1613   long       = "lte-restrict-inst-closure"
1614   type       = "bool"
1615   default    = "false"
1616   read_only  = true
1617   help       = "treat arguments of inst closure as restricted terms for instantiation"
1618
1619 ### Reduction options
1620
1621 [[option]]
1622   name       = "quantAlphaEquiv"
1623   category   = "regular"
1624   long       = "quant-alpha-equiv"
1625   type       = "bool"
1626   default    = "true"
1627   read_only  = true
1628   help       = "infer alpha equivalence between quantified formulas"
1629
1630 [[option]]
1631   name       = "macrosQuant"
1632   category   = "regular"
1633   long       = "macros-quant"
1634   type       = "bool"
1635   default    = "false"
1636   help       = "perform quantifiers macro expansion"
1637
1638 [[option]]
1639   name       = "macrosQuantMode"
1640   category   = "regular"
1641   long       = "macros-quant-mode=MODE"
1642   type       = "CVC4::theory::quantifiers::MacrosQuantMode"
1643   default    = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1644   handler    = "stringToMacrosQuantMode"
1645   includes   = ["options/quantifiers_modes.h"]
1646   read_only  = true
1647   help       = "mode for quantifiers macro expansion"
1648
1649 [[option]]
1650   name       = "quantDynamicSplit"
1651   category   = "regular"
1652   long       = "quant-dsplit-mode=MODE"
1653   type       = "CVC4::theory::quantifiers::QuantDSplitMode"
1654   default    = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1655   handler    = "stringToQuantDSplitMode"
1656   includes   = ["options/quantifiers_modes.h"]
1657   help       = "mode for dynamic quantifiers splitting"
1658
1659 [[option]]
1660   name       = "quantAntiSkolem"
1661   category   = "regular"
1662   long       = "quant-anti-skolem"
1663   type       = "bool"
1664   default    = "false"
1665   help       = "perform anti-skolemization for quantified formulas"
1666
1667 ### Higher-order options
1668
1669 [[option]]
1670   name       = "hoMatching"
1671   category   = "regular"
1672   long       = "ho-matching"
1673   type       = "bool"
1674   default    = "true"
1675   read_only  = true
1676   help       = "do higher-order matching algorithm for triggers with variable operators"
1677
1678 [[option]]
1679   name       = "hoMatchingVarArgPriority"
1680   category   = "regular"
1681   long       = "ho-matching-var-priority"
1682   type       = "bool"
1683   default    = "true"
1684   read_only  = true
1685   help       = "give priority to variable arguments over constant arguments"
1686
1687 [[option]]
1688   name       = "hoMergeTermDb"
1689   category   = "regular"
1690   long       = "ho-merge-term-db"
1691   type       = "bool"
1692   default    = "true"
1693   read_only  = true
1694   help       = "merge term indices modulo equality"
1695
1696 ### Proof options
1697
1698 [[option]]
1699   name       = "trackInstLemmas"
1700   category   = "regular"
1701   long       = "track-inst-lemmas"
1702   type       = "bool"
1703   default    = "false"
1704   help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"