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       = "sygusAbduct"
 881   category   = "regular"
 882   long       = "sygus-abduct"
 883   type       = "bool"
 884   default    = "false"
 885   read_only  = false
 886   help       = "compute abductions using sygus"
 887
 888 [[option]]
 889   name       = "ceGuidedInst"
 890   category   = "regular"
 891   long       = "cegqi"
 892   type       = "bool"
 893   default    = "false"
 894   help       = "counterexample-guided quantifier instantiation for sygus"
 895
 896 [[option]]
 897   name       = "cegqiSingleInvMode"
 898   category   = "regular"
 899   long       = "cegqi-si=MODE"
 900   type       = "CVC4::theory::quantifiers::CegqiSingleInvMode"
 901   default    = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
 902   handler    = "stringToCegqiSingleInvMode"
 903   includes   = ["options/quantifiers_modes.h"]
 904   help       = "mode for processing single invocation synthesis conjectures"
 905
 906 [[option]]
 907   name       = "cegqiSingleInvPartial"
 908   category   = "regular"
 909   long       = "cegqi-si-partial"
 910   type       = "bool"
 911   default    = "false"
 912   read_only  = true
 913   help       = "combined techniques for synthesis conjectures that are partially single invocation"
 914
 915 [[option]]
 916   name       = "cegqiSingleInvReconstruct"
 917   category   = "regular"
 918   long       = "cegqi-si-rcons=MODE"
 919   type       = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode"
 920   default    = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT"
 921   handler    = "stringToCegqiSingleInvRconsMode"
 922   includes   = ["options/quantifiers_modes.h"]
 923   help       = "policy for reconstructing solutions for single invocation conjectures"
 924
 925 [[option]]
 926   name       = "cegqiSingleInvReconstructLimit"
 927   category   = "regular"
 928   long       = "cegqi-si-rcons-limit=N"
 929   type       = "int"
 930   default    = "10000"
 931   read_only  = true
 932   help       = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
 933
 934 [[option]]
 935   name       = "cegqiSingleInvReconstructConst"
 936   category   = "regular"
 937   long       = "cegqi-si-reconstruct-const"
 938   type       = "bool"
 939   default    = "true"
 940   read_only  = true
 941   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 942
 943 [[option]]
 944   name       = "cegqiSolMinCore"
 945   category   = "regular"
 946   long       = "cegqi-si-sol-min-core"
 947   type       = "bool"
 948   default    = "false"
 949   read_only  = true
 950   help       = "minimize solutions for single invocation conjectures based on unsat core"
 951
 952 [[option]]
 953   name       = "cegqiSolMinInst"
 954   category   = "regular"
 955   long       = "cegqi-si-sol-min-inst"
 956   type       = "bool"
 957   default    = "true"
 958   read_only  = true
 959   help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
 960
 961 [[option]]
 962   name       = "cegqiSingleInvAbort"
 963   category   = "regular"
 964   long       = "cegqi-si-abort"
 965   type       = "bool"
 966   default    = "false"
 967   read_only  = true
 968   help       = "abort if synthesis conjecture is not single invocation"
 969
 970 [[option]]
 971   name       = "sygusConstRepairAbort"
 972   category   = "regular"
 973   long       = "sygus-crepair-abort"
 974   type       = "bool"
 975   default    = "false"
 976   read_only  = true
 977   help       = "abort if constant repair techniques are not applicable"
 978
 979 [[option]]
 980   name       = "sygusUnif"
 981   category   = "regular"
 982   long       = "sygus-unif"
 983   type       = "bool"
 984   default    = "false"
 985   help       = "Unification-based function synthesis"
 986
 987 [[option]]
 988   name       = "sygusUnifCondIndependent"
 989   category   = "regular"
 990   long       = "sygus-unif-cond-independent"
 991   type       = "bool"
 992   default    = "false"
 993   help       = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
 994
 995 [[option]]
 996   name       = "sygusUnifShuffleCond"
 997   category   = "regular"
 998   long       = "sygus-unif-shuffle-cond"
 999   type       = "bool"
1000   default    = "false"
1001   help       = "Shuffle condition pool when building solutions (may change solutions sizes)"
1002
1003 [[option]]
1004   name       = "sygusUnifBooleanHeuristicDt"
1005   category   = "regular"
1006   long       = "sygus-unif-boolean-heuristic-dt"
1007   type       = "bool"
1008   default    = "false"
1009   help       = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
1010
1011 [[option]]
1012   name       = "sygusUnifCondIndNoRepeatSol"
1013   category   = "regular"
1014   long       = "sygus-unif-cond-independent-no-repeat-sol"
1015   type       = "bool"
1016   default    = "true"
1017   help       = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
1018
1019 [[option]]
1020   name       = "sygusBoolIteReturnConst"
1021   category   = "regular"
1022   long       = "sygus-bool-ite-return-const"
1023   type       = "bool"
1024   default    = "true"
1025   help       = "Only use Boolean constants for return values in unification-based function synthesis"
1026
1027 [[option]]
1028   name       = "sygusQePreproc"
1029   category   = "regular"
1030   long       = "sygus-qe-preproc"
1031   type       = "bool"
1032   default    = "false"
1033   read_only  = true
1034   help       = "use quantifier elimination as a preprocessing step for sygus"
1035
1036 [[option]]
1037   name       = "sygusRepairConst"
1038   category   = "regular"
1039   long       = "sygus-repair-const"
1040   type       = "bool"
1041   default    = "false"
1042   help       = "use approach to repair constants in sygus candidate solutions"
1043
1044 [[option]]
1045   name       = "sygusRepairConstTimeout"
1046   category   = "regular"
1047   long       = "sygus-repair-const-timeout=N"
1048   type       = "unsigned long"
1049   help       = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
1050
1051 [[option]]
1052   name       = "sygusActiveGenMode"
1053   category   = "regular"
1054   long       = "sygus-active-gen=MODE"
1055   type       = "CVC4::theory::quantifiers::SygusActiveGenMode"
1056   default    = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO"
1057   handler    = "stringToSygusActiveGenMode"
1058   includes   = ["options/quantifiers_modes.h"]
1059   read_only  = true
1060   help       = "mode for actively-generated sygus enumerators"
1061
1062 [[option]]
1063   name       = "sygusActiveGenEnumConsts"
1064   category   = "regular"
1065   long       = "sygus-active-gen-cfactor=N"
1066   type       = "unsigned long"
1067   default    = "5"
1068   help       = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum"
1069
1070 [[option]]
1071   name       = "sygusMinGrammar"
1072   category   = "regular"
1073   long       = "sygus-min-grammar"
1074   type       = "bool"
1075   default    = "true"
1076   read_only  = true
1077   help       = "statically minimize sygus grammars"
1078
1079 [[option]]
1080   name       = "sygusAddConstGrammar"
1081   category   = "regular"
1082   long       = "sygus-add-const-grammar"
1083   type       = "bool"
1084   default    = "false"
1085   read_only  = true
1086   help       = "statically add constants appearing in conjecture to grammars"
1087
1088 [[option]]
1089   name       = "sygusGrammarNorm"
1090   category   = "regular"
1091   long       = "sygus-grammar-norm"
1092   type       = "bool"
1093   default    = "false"
1094   read_only  = true
1095   help       = "statically normalize sygus grammars based on flattening (linearization)"
1096
1097 [[option]]
1098   name       = "sygusTemplEmbedGrammar"
1099   category   = "regular"
1100   long       = "sygus-templ-embed-grammar"
1101   type       = "bool"
1102   default    = "false"
1103   read_only  = true
1104   help       = "embed sygus templates into grammars"
1105
1106 [[option]]
1107   name       = "sygusInvTemplMode"
1108   category   = "regular"
1109   long       = "sygus-inv-templ=MODE"
1110   type       = "CVC4::theory::quantifiers::SygusInvTemplMode"
1111   default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1112   handler    = "stringToSygusInvTemplMode"
1113   includes   = ["options/quantifiers_modes.h"]
1114   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1115
1116 [[option]]
1117   name       = "sygusInvTemplWhenSyntax"
1118   category   = "regular"
1119   long       = "sygus-inv-templ-when-sg"
1120   type       = "bool"
1121   default    = "false"
1122   read_only  = false
1123   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1124
1125 [[option]]
1126   name       = "sygusInvAutoUnfold"
1127   category   = "regular"
1128   long       = "sygus-auto-unfold"
1129   type       = "bool"
1130   default    = "true"
1131   read_only  = true
1132   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1133
1134 [[option]]
1135   name       = "sygusUnifPbe"
1136   category   = "regular"
1137   long       = "sygus-pbe"
1138   type       = "bool"
1139   default    = "true"
1140   help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1141
1142 [[option]]
1143   name       = "sygusPbeMultiFair"
1144   category   = "regular"
1145   long       = "sygus-pbe-multi-fair"
1146   type       = "bool"
1147   default    = "false"
1148   help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
1149
1150 [[option]]
1151   name       = "sygusPbeMultiFairDiff"
1152   category   = "regular"
1153   long       = "sygus-pbe-multi-fair-diff=N"
1154   type       = "int"
1155   default    = "0"
1156   help       = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1157
1158 [[option]]
1159   name       = "sygusEvalUnfold"
1160   category   = "regular"
1161   long       = "sygus-eval-unfold"
1162   type       = "bool"
1163   default    = "true"
1164   read_only  = true
1165   help       = "do unfolding of sygus evaluation functions"
1166
1167 [[option]]
1168   name       = "sygusEvalUnfoldBool"
1169   category   = "regular"
1170   long       = "sygus-eval-unfold-bool"
1171   type       = "bool"
1172   default    = "true"
1173   read_only  = true
1174   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1175
1176 [[option]]
1177   name       = "sygusRefEval"
1178   category   = "regular"
1179   long       = "sygus-ref-eval"
1180   type       = "bool"
1181   default    = "true"
1182   read_only  = true
1183   help       = "direct evaluation of refinement lemmas for conflict analysis"
1184
1185 [[option]]
1186   name       = "sygusStream"
1187   category   = "regular"
1188   long       = "sygus-stream"
1189   type       = "bool"
1190   default    = "false"
1191   help       = "enumerate a stream of solutions instead of terminating after the first one"
1192
1193 [[option]]
1194   name       = "sygusVerifySubcall"
1195   category   = "regular"
1196   long       = "sygus-verify-subcall"
1197   type       = "bool"
1198   default    = "true"
1199   help       = "use separate copy of the SMT solver for verification lemmas in sygus"
1200
1201 [[option]]
1202   name       = "sygusExtRew"
1203   category   = "regular"
1204   long       = "sygus-ext-rew"
1205   type       = "bool"
1206   default    = "true"
1207   help       = "use extended rewriter for sygus"
1208
1209 [[option]]
1210   name       = "cegisSample"
1211   category   = "regular"
1212   long       = "cegis-sample=MODE"
1213   type       = "CVC4::theory::quantifiers::CegisSampleMode"
1214   default    = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1215   handler    = "stringToCegisSampleMode"
1216   includes   = ["options/quantifiers_modes.h"]
1217   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
1218
1219 [[option]]
1220   name       = "minSynthSol"
1221   category   = "regular"
1222   long       = "min-synth-sol"
1223   type       = "bool"
1224   default    = "true"
1225   help       = "Minimize synthesis solutions"
1226
1227 [[option]]
1228   name       = "sygusEvalOpt"
1229   category   = "regular"
1230   long       = "sygus-eval-opt"
1231   type       = "bool"
1232   default    = "true"
1233   help       = "use optimized approach for evaluation in sygus"
1234
1235 [[option]]
1236   name       = "sygusArgRelevant"
1237   category   = "regular"
1238   long       = "sygus-arg-relevant"
1239   type       = "bool"
1240   default    = "false"
1241   help       = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1242
1243 # Internal uses of sygus
1244
1245 [[option]]
1246   name       = "sygusRew"
1247   category   = "regular"
1248   long       = "sygus-rr"
1249   type       = "bool"
1250   default    = "false"
1251   read_only  = true
1252   help       = "use sygus to enumerate and verify correctness of rewrite rules"
1253
1254 [[option]]
1255   name       = "sygusRewSynth"
1256   category   = "regular"
1257   long       = "sygus-rr-synth"
1258   type       = "bool"
1259   default    = "false"
1260   help       = "use sygus to enumerate candidate rewrite rules"
1261
1262 [[option]]
1263   name       = "sygusRewSynthFilterOrder"
1264   category   = "regular"
1265   long       = "sygus-rr-synth-filter-order"
1266   type       = "bool"
1267   default    = "true"
1268   help       = "filter candidate rewrites based on variable ordering"
1269
1270 [[option]]
1271   name       = "sygusRewSynthFilterMatch"
1272   category   = "regular"
1273   long       = "sygus-rr-synth-filter-match"
1274   type       = "bool"
1275   default    = "true"
1276   help       = "filter candidate rewrites based on matching"
1277
1278 [[option]]
1279   name       = "sygusRewSynthFilterCong"
1280   category   = "regular"
1281   long       = "sygus-rr-synth-filter-cong"
1282   type       = "bool"
1283   default    = "true"
1284   help       = "filter candidate rewrites based on congruence"
1285
1286 [[option]]
1287   name       = "sygusRewSynthFilterNonLinear"
1288   category   = "regular"
1289   long       = "sygus-rr-synth-filter-nl"
1290   type       = "bool"
1291   default    = "false"
1292   help       = "filter non-linear candidate rewrites"
1293
1294 [[option]]
1295   name       = "sygusRewVerify"
1296   category   = "regular"
1297   long       = "sygus-rr-verify"
1298   type       = "bool"
1299   default    = "false"
1300   help       = "use sygus to verify the correctness of rewrite rules via sampling"
1301
1302 [[option]]
1303   name       = "sygusRewVerifyAbort"
1304   category   = "regular"
1305   long       = "sygus-rr-verify-abort"
1306   type       = "bool"
1307   default    = "true"
1308   help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1309
1310 [[option]]
1311   name       = "sygusSamples"
1312   category   = "regular"
1313   long       = "sygus-samples=N"
1314   type       = "int"
1315   default    = "1000"
1316   help       = "number of points to consider when doing sygus rewriter sample testing"
1317
1318 [[option]]
1319   name       = "sygusSampleGrammar"
1320   category   = "regular"
1321   long       = "sygus-sample-grammar"
1322   type       = "bool"
1323   default    = "true"
1324   read_only  = true
1325   help       = "when applicable, use grammar for choosing sample points"
1326
1327 [[option]]
1328   name       = "sygusSampleFpUniform"
1329   category   = "regular"
1330   long       = "sygus-sample-fp-uniform"
1331   type       = "bool"
1332   default    = "false"
1333   help       = "sample floating-point values uniformly instead of in a biased fashion"
1334
1335 [[option]]
1336   name       = "sygusRewSynthAccel"
1337   category   = "regular"
1338   long       = "sygus-rr-synth-accel"
1339   type       = "bool"
1340   default    = "false"
1341   help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
1342
1343 [[option]]
1344   name       = "sygusRewSynthCheck"
1345   category   = "regular"
1346   long       = "sygus-rr-synth-check"
1347   type       = "bool"
1348   default    = "false"
1349   help       = "use satisfiability check to verify correctness of candidate rewrites"
1350
1351 [[option]]
1352   name       = "sygusRewSynthInput"
1353   category   = "regular"
1354   long       = "sygus-rr-synth-input"
1355   type       = "bool"
1356   default    = "false"
1357   help       = "synthesize rewrite rules based on the input formula"
1358
1359 [[option]]
1360   name       = "sygusRewSynthInputNVars"
1361   category   = "regular"
1362   long       = "sygus-rr-synth-input-nvars=N"
1363   type       = "int"
1364   default    = "3"
1365   help       = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
1366
1367 [[option]]
1368   name       = "sygusRewSynthInputUseBool"
1369   category   = "regular"
1370   long       = "sygus-rr-synth-input-use-bool"
1371   type       = "bool"
1372   default    = "false"
1373   help       = "synthesize Boolean rewrite rules based on the input formula"
1374
1375 [[option]]
1376   name       = "sygusExprMinerCheckTimeout"
1377   category   = "regular"
1378   long       = "sygus-expr-miner-check-timeout=N"
1379   type       = "unsigned long"
1380   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
1381
1382 [[option]]
1383   name       = "sygusRewSynthRec"
1384   category   = "regular"
1385   long       = "sygus-rr-synth-rec"
1386   type       = "bool"
1387   default    = "false"
1388   help       = "synthesize rewrite rules over all sygus grammar types recursively"
1389
1390 [[option]]
1391   name       = "sygusQueryGen"
1392   category   = "regular"
1393   long       = "sygus-query-gen"
1394   type       = "bool"
1395   default    = "false"
1396   help       = "use sygus to enumerate interesting satisfiability queries"
1397
1398 [[option]]
1399   name       = "sygusQueryGenThresh"
1400   category   = "regular"
1401   long       = "sygus-query-gen-thresh=N"
1402   type       = "unsigned"
1403   default    = "5"
1404   help       = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
1405
1406 [[option]]
1407   name       = "sygusQueryGenCheck"
1408   category   = "regular"
1409   long       = "sygus-query-gen-check"
1410   type       = "bool"
1411   default    = "true"
1412   help       = "use interesting satisfiability queries to check soundness of CVC4"
1413
1414 [[option]]
1415   name       = "sygusQueryGenDumpFiles"
1416   category   = "regular"
1417   long       = "sygus-query-gen-dump-files"
1418   type       = "bool"
1419   default    = "false"
1420   help       = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
1421
1422 [[option]]
1423   name       = "sygusFilterSolMode"
1424   category   = "regular"
1425   long       = "sygus-filter-sol=MODE"
1426   type       = "CVC4::theory::quantifiers::SygusFilterSolMode"
1427   default    = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE"
1428   handler    = "stringToSygusFilterSolMode"
1429   includes   = ["options/quantifiers_modes.h"]
1430   help       = "mode for filtering sygus solutions"
1431
1432 [[option]]
1433   name       = "sygusFilterSolRevSubsume"
1434   category   = "expert"
1435   long       = "sygus-filter-sol-rev"
1436   type       = "bool"
1437   default    = "false"
1438   help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
1439
1440
1441 [[option]]
1442   name       = "sygusExprMinerCheckUseExport"
1443   category   = "expert"
1444   long       = "sygus-expr-miner-check-use-export"
1445   type       = "bool"
1446   default    = "true"
1447   help       = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
1448
1449 # CEGQI applied to general quantified formulas
1450
1451 [[option]]
1452   name       = "cbqi"
1453   category   = "regular"
1454   long       = "cbqi"
1455   type       = "bool"
1456   default    = "false"
1457   help       = "turns on counterexample-based quantifier instantiation"
1458
1459 [[option]]
1460   name       = "cbqiFullEffort"
1461   category   = "regular"
1462   long       = "cbqi-full"
1463   type       = "bool"
1464   default    = "false"
1465   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1466
1467 [[option]]
1468   name       = "cbqiSat"
1469   category   = "regular"
1470   long       = "cbqi-sat"
1471   type       = "bool"
1472   default    = "true"
1473   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1474
1475 [[option]]
1476   name       = "cbqiModel"
1477   category   = "regular"
1478   long       = "cbqi-model"
1479   type       = "bool"
1480   default    = "true"
1481   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1482
1483 [[option]]
1484   name       = "cbqiAll"
1485   category   = "regular"
1486   long       = "cbqi-all"
1487   type       = "bool"
1488   default    = "false"
1489   help       = "apply counterexample-based instantiation to all quantified formulas"
1490
1491 [[option]]
1492   name       = "cbqiMultiInst"
1493   category   = "regular"
1494   long       = "cbqi-multi-inst"
1495   type       = "bool"
1496   default    = "false"
1497   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1498
1499 [[option]]
1500   name       = "cbqiRepeatLit"
1501   category   = "regular"
1502   long       = "cbqi-repeat-lit"
1503   type       = "bool"
1504   default    = "false"
1505   help       = "solve literals more than once in counterexample-based quantifier instantiation"
1506
1507 [[option]]
1508   name       = "cbqiInnermost"
1509   category   = "regular"
1510   long       = "cbqi-innermost"
1511   type       = "bool"
1512   default    = "true"
1513   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1514
1515 [[option]]
1516   name       = "cbqiNestedQE"
1517   category   = "regular"
1518   long       = "cbqi-nested-qe"
1519   type       = "bool"
1520   default    = "false"
1521   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1522
1523 # CEGQI for arithmetic
1524
1525 [[option]]
1526   name       = "cbqiUseInfInt"
1527   category   = "regular"
1528   long       = "cbqi-use-inf-int"
1529   type       = "bool"
1530   default    = "false"
1531   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1532
1533 [[option]]
1534   name       = "cbqiUseInfReal"
1535   category   = "regular"
1536   long       = "cbqi-use-inf-real"
1537   type       = "bool"
1538   default    = "false"
1539   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1540
1541 [[option]]
1542   name       = "cbqiPreRegInst"
1543   category   = "regular"
1544   long       = "cbqi-prereg-inst"
1545   type       = "bool"
1546   default    = "false"
1547   help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
1548
1549 [[option]]
1550   name       = "cbqiMinBounds"
1551   category   = "regular"
1552   long       = "cbqi-min-bounds"
1553   type       = "bool"
1554   default    = "false"
1555   read_only  = true
1556   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1557
1558 [[option]]
1559   name       = "cbqiRoundUpLowerLia"
1560   category   = "regular"
1561   long       = "cbqi-round-up-lia"
1562   type       = "bool"
1563   default    = "false"
1564   read_only  = true
1565   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1566
1567 [[option]]
1568   name       = "cbqiMidpoint"
1569   category   = "regular"
1570   long       = "cbqi-midpoint"
1571   type       = "bool"
1572   default    = "false"
1573   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1574
1575 [[option]]
1576   name       = "cbqiNopt"
1577   category   = "regular"
1578   long       = "cbqi-nopt"
1579   type       = "bool"
1580   default    = "true"
1581   read_only  = true
1582   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1583
1584 [[option]]
1585   name       = "cbqiLitDepend"
1586   category   = "regular"
1587   long       = "cbqi-lit-dep"
1588   type       = "bool"
1589   default    = "true"
1590   read_only  = true
1591   help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1592
1593 # CEGQI for EPR
1594
1595 [[option]]
1596   name       = "quantEpr"
1597   category   = "regular"
1598   long       = "quant-epr"
1599   type       = "bool"
1600   default    = "false"
1601   help       = "infer whether in effectively propositional fragment, use for cbqi"
1602
1603 [[option]]
1604   name       = "quantEprMatching"
1605   category   = "regular"
1606   long       = "quant-epr-match"
1607   type       = "bool"
1608   default    = "true"
1609   read_only  = true
1610   help       = "use matching heuristics for EPR instantiation"
1611
1612 # CEGQI for BV
1613
1614 [[option]]
1615   name       = "cbqiBv"
1616   category   = "regular"
1617   long       = "cbqi-bv"
1618   type       = "bool"
1619   default    = "true"
1620   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1621
1622 [[option]]
1623   name       = "cbqiBvInterleaveValue"
1624   category   = "regular"
1625   long       = "cbqi-bv-interleave-value"
1626   type       = "bool"
1627   default    = "false"
1628   help       = "interleave model value instantiation with word-level inversion approach"
1629
1630 [[option]]
1631   name       = "cbqiBvIneqMode"
1632   category   = "regular"
1633   long       = "cbqi-bv-ineq=MODE"
1634   type       = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1635   default    = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1636   handler    = "stringToCbqiBvIneqMode"
1637   includes   = ["options/quantifiers_modes.h"]
1638   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1639
1640 [[option]]
1641   name       = "cbqiBvRmExtract"
1642   category   = "regular"
1643   long       = "cbqi-bv-rm-extract"
1644   type       = "bool"
1645   default    = "true"
1646   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1647
1648 [[option]]
1649   name       = "cbqiBvLinearize"
1650   category   = "regular"
1651   long       = "cbqi-bv-linear"
1652   type       = "bool"
1653   default    = "true"
1654   help       = "linearize adder chains for variables"
1655
1656 [[option]]
1657   name       = "cbqiBvSolveNl"
1658   category   = "regular"
1659   long       = "cbqi-bv-solve-nl"
1660   type       = "bool"
1661   default    = "false"
1662   help       = "try to solve non-linear bv literals using model value projections"
1663
1664 [[option]]
1665   name       = "cbqiBvConcInv"
1666   category   = "regular"
1667   long       = "cbqi-bv-concat-inv"
1668   type       = "bool"
1669   default    = "true"
1670   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1671
1672 ### Local theory extensions options
1673
1674 [[option]]
1675   name       = "localTheoryExt"
1676   category   = "regular"
1677   long       = "local-t-ext"
1678   type       = "bool"
1679   default    = "false"
1680   read_only  = true
1681   help       = "do instantiation based on local theory extensions"
1682
1683 [[option]]
1684   name       = "ltePartialInst"
1685   category   = "regular"
1686   long       = "lte-partial-inst"
1687   type       = "bool"
1688   default    = "false"
1689   read_only  = true
1690   help       = "partially instantiate local theory quantifiers"
1691
1692 [[option]]
1693   name       = "lteRestrictInstClosure"
1694   category   = "regular"
1695   long       = "lte-restrict-inst-closure"
1696   type       = "bool"
1697   default    = "false"
1698   read_only  = true
1699   help       = "treat arguments of inst closure as restricted terms for instantiation"
1700
1701 ### Reduction options
1702
1703 [[option]]
1704   name       = "quantAlphaEquiv"
1705   category   = "regular"
1706   long       = "quant-alpha-equiv"
1707   type       = "bool"
1708   default    = "true"
1709   read_only  = true
1710   help       = "infer alpha equivalence between quantified formulas"
1711
1712 [[option]]
1713   name       = "macrosQuant"
1714   category   = "regular"
1715   long       = "macros-quant"
1716   type       = "bool"
1717   default    = "false"
1718   help       = "perform quantifiers macro expansion"
1719
1720 [[option]]
1721   name       = "macrosQuantMode"
1722   category   = "regular"
1723   long       = "macros-quant-mode=MODE"
1724   type       = "CVC4::theory::quantifiers::MacrosQuantMode"
1725   default    = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1726   handler    = "stringToMacrosQuantMode"
1727   includes   = ["options/quantifiers_modes.h"]
1728   read_only  = true
1729   help       = "mode for quantifiers macro expansion"
1730
1731 [[option]]
1732   name       = "quantDynamicSplit"
1733   category   = "regular"
1734   long       = "quant-dsplit-mode=MODE"
1735   type       = "CVC4::theory::quantifiers::QuantDSplitMode"
1736   default    = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1737   handler    = "stringToQuantDSplitMode"
1738   includes   = ["options/quantifiers_modes.h"]
1739   help       = "mode for dynamic quantifiers splitting"
1740
1741 [[option]]
1742   name       = "quantAntiSkolem"
1743   category   = "regular"
1744   long       = "quant-anti-skolem"
1745   type       = "bool"
1746   default    = "false"
1747   help       = "perform anti-skolemization for quantified formulas"
1748
1749 ### Higher-order options
1750
1751 [[option]]
1752   name       = "hoMatching"
1753   category   = "regular"
1754   long       = "ho-matching"
1755   type       = "bool"
1756   default    = "true"
1757   read_only  = true
1758   help       = "do higher-order matching algorithm for triggers with variable operators"
1759
1760 [[option]]
1761   name       = "hoMatchingVarArgPriority"
1762   category   = "regular"
1763   long       = "ho-matching-var-priority"
1764   type       = "bool"
1765   default    = "true"
1766   read_only  = true
1767   help       = "give priority to variable arguments over constant arguments"
1768
1769 [[option]]
1770   name       = "hoMergeTermDb"
1771   category   = "regular"
1772   long       = "ho-merge-term-db"
1773   type       = "bool"
1774   default    = "true"
1775   read_only  = true
1776   help       = "merge term indices modulo equality"
1777
1778 ### Proof options
1779
1780 [[option]]
1781   name       = "trackInstLemmas"
1782   category   = "regular"
1783   long       = "track-inst-lemmas"
1784   type       = "bool"
1785   default    = "false"
1786   help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"