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       = "PrenexQuantMode"
  40   default    = "SIMPLE"
  41   help       = "prenex mode for quantified formulas"
  42   help_mode  = "Prenex quantifiers modes."
  43 [[option.mode.NONE]]
  44   name = "none"
  45   help = "Do no prenex nested quantifiers."
  46 [[option.mode.SIMPLE]]
  47   name = "simple"
  48   help = "Do simple prenexing of same sign quantifiers."
  49 [[option.mode.NORMAL]]
  50   name = "norm"
  51   help = "Prenex to prenex normal form."
  52
  53 [[option]]
  54   name       = "prenexQuantUser"
  55   category   = "regular"
  56   long       = "prenex-quant-user"
  57   type       = "bool"
  58   default    = "false"
  59   help       = "prenex quantified formulas with user patterns"
  60
  61 # Whether to variable-eliminate quantifiers.
  62 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
  63 #   forall y. P( c, y )
  64 [[option]]
  65   name       = "varElimQuant"
  66   category   = "regular"
  67   long       = "var-elim-quant"
  68   type       = "bool"
  69   default    = "true"
  70   help       = "enable simple variable elimination for quantified formulas"
  71
  72 [[option]]
  73   name       = "varIneqElimQuant"
  74   category   = "regular"
  75   long       = "var-ineq-elim-quant"
  76   type       = "bool"
  77   default    = "true"
  78   help       = "enable variable elimination based on infinite projection of unbound arithmetic variables"
  79
  80 [[option]]
  81   name       = "dtVarExpandQuant"
  82   category   = "regular"
  83   long       = "dt-var-exp-quant"
  84   type       = "bool"
  85   default    = "true"
  86   help       = "expand datatype variables bound to one constructor in quantifiers"
  87
  88 [[option]]
  89   name       = "iteLiftQuant"
  90   category   = "regular"
  91   long       = "ite-lift-quant=MODE"
  92   type       = "IteLiftQuantMode"
  93   default    = "SIMPLE"
  94   help       = "ite lifting mode for quantified formulas"
  95   help_mode  = "ITE lifting modes for quantified formulas."
  96 [[option.mode.NONE]]
  97   name = "none"
  98   help = "Do not lift if-then-else in quantified formulas."
  99 [[option.mode.SIMPLE]]
 100   name = "simple"
 101   help = "Lift if-then-else in quantified formulas if results in smaller term size."
 102 [[option.mode.ALL]]
 103   name = "all"
 104   help = "Lift if-then-else in quantified formulas."
 105
 106 [[option]]
 107   name       = "condVarSplitQuant"
 108   category   = "regular"
 109   long       = "cond-var-split-quant"
 110   type       = "bool"
 111   default    = "true"
 112   help       = "split quantified formulas that lead to variable eliminations"
 113
 114 [[option]]
 115   name       = "condVarSplitQuantAgg"
 116   category   = "regular"
 117   long       = "cond-var-split-agg-quant"
 118   type       = "bool"
 119   default    = "false"
 120   help       = "aggressive split quantified formulas that lead to variable eliminations"
 121
 122 [[option]]
 123   name       = "iteDtTesterSplitQuant"
 124   category   = "regular"
 125   long       = "ite-dtt-split-quant"
 126   type       = "bool"
 127   default    = "false"
 128   help       = "split ites with dt testers as conditions"
 129
 130 # Whether to pre-skolemize quantifier bodies.
 131 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 132 #   forall x. P( x ) => f( S( x ) ) = x
 133 [[option]]
 134   name       = "preSkolemQuant"
 135   category   = "regular"
 136   long       = "pre-skolem-quant"
 137   type       = "bool"
 138   default    = "false"
 139   help       = "apply skolemization eagerly to bodies of quantified formulas"
 140
 141 [[option]]
 142   name       = "preSkolemQuantNested"
 143   category   = "regular"
 144   long       = "pre-skolem-quant-nested"
 145   type       = "bool"
 146   default    = "true"
 147   help       = "apply skolemization to nested quantified formulas"
 148
 149 [[option]]
 150   name       = "preSkolemQuantAgg"
 151   category   = "regular"
 152   long       = "pre-skolem-quant-agg"
 153   type       = "bool"
 154   default    = "true"
 155   help       = "apply skolemization to quantified formulas aggressively"
 156
 157 [[option]]
 158   name       = "aggressiveMiniscopeQuant"
 159   category   = "regular"
 160   long       = "ag-miniscope-quant"
 161   type       = "bool"
 162   default    = "false"
 163   help       = "perform aggressive miniscoping for quantifiers"
 164
 165 [[option]]
 166   name       = "elimTautQuant"
 167   category   = "regular"
 168   long       = "elim-taut-quant"
 169   type       = "bool"
 170   default    = "true"
 171   help       = "eliminate tautological disjuncts of quantified formulas"
 172
 173 [[option]]
 174   name       = "extRewriteQuant"
 175   category   = "regular"
 176   long       = "ext-rewrite-quant"
 177   type       = "bool"
 178   default    = "false"
 179   help       = "apply extended rewriting to bodies 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       = "TermDbMode"
 204   default    = "ALL"
 205   help       = "which ground terms to consider for instantiation"
 206   help_mode  = "Modes for terms included in the quantifiers term database."
 207 [[option.mode.ALL]]
 208   name = "all"
 209   help = "Quantifiers module considers all ground terms."
 210 [[option.mode.RELEVANT]]
 211   name = "relevant"
 212   help = "Quantifiers module considers only ground terms connected to current assertions."
 213
 214 [[option]]
 215   name       = "termDbCd"
 216   category   = "regular"
 217   long       = "term-db-cd"
 218   type       = "bool"
 219   default    = "true"
 220   help       = "register terms in term database based on the SAT context"
 221
 222 [[option]]
 223   name       = "registerQuantBodyTerms"
 224   category   = "regular"
 225   long       = "register-quant-body-terms"
 226   type       = "bool"
 227   default    = "false"
 228   help       = "consider ground terms within bodies of quantified formulas for matching"
 229
 230 [[option]]
 231   name       = "strictTriggers"
 232   category   = "regular"
 233   long       = "strict-triggers"
 234   type       = "bool"
 235   default    = "false"
 236   help       = "only instantiate quantifiers with user patterns based on triggers"
 237
 238 [[option]]
 239   name       = "relevantTriggers"
 240   category   = "regular"
 241   long       = "relevant-triggers"
 242   type       = "bool"
 243   default    = "false"
 244   help       = "prefer triggers that are more relevant based on SInE style analysis"
 245
 246 [[option]]
 247   name       = "relationalTriggers"
 248   category   = "regular"
 249   long       = "relational-triggers"
 250   type       = "bool"
 251   default    = "false"
 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       = "partialTriggers"
 264   category   = "regular"
 265   long       = "partial-triggers"
 266   type       = "bool"
 267   default    = "false"
 268   help       = "use triggers that do not contain all free variables"
 269
 270 [[option]]
 271   name       = "multiTriggerWhenSingle"
 272   category   = "regular"
 273   long       = "multi-trigger-when-single"
 274   type       = "bool"
 275   default    = "false"
 276   help       = "select multi triggers when single triggers exist"
 277
 278 [[option]]
 279   name       = "multiTriggerPriority"
 280   category   = "regular"
 281   long       = "multi-trigger-priority"
 282   type       = "bool"
 283   default    = "false"
 284   help       = "only try multi triggers if single triggers give no instantiations"
 285
 286 [[option]]
 287   name       = "multiTriggerCache"
 288   category   = "regular"
 289   long       = "multi-trigger-cache"
 290   type       = "bool"
 291   default    = "false"
 292   help       = "caching version of multi triggers"
 293
 294 [[option]]
 295   name       = "multiTriggerLinear"
 296   category   = "regular"
 297   long       = "multi-trigger-linear"
 298   type       = "bool"
 299   default    = "true"
 300   help       = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
 301
 302 # Trigger selection mode.
 303 #
 304 # These modes are used for determining which terms to select
 305 # as triggers for quantified formulas, when necessary, during E-matching.
 306 # In the following, note the following terminology. A trigger is a set of terms,
 307 # where a single trigger is a singleton set and a multi-trigger is a set of more
 308 # than one term.
 309 #
 310 # MIN selects single triggers of minimal term size.
 311 # MAX selects single triggers of maximal term size.
 312 #
 313 # For example, consider the quantified formula :
 314 #   forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y )
 315 #
 316 # MIN will select g( x, y ) and Q( f( x ), y ).
 317 # MAX will select P( f( g( x ) ) ) and Q( f( x ), y ).
 318 #
 319 # The remaining three trigger selections make a difference for multi-triggers
 320 # only. For quantified formulas that require multi-triggers, we build a set of
 321 # partial triggers that don't contain all variables, call this set S. Then,
 322 # multi-triggers are built by taking a random subset of S that collectively
 323 # contains all variables.
 324 #
 325 # Consider the quantified formula :
 326 #   forall xyz. P( h( x ), y ) V Q( y, z )
 327 #
 328 # For ALL and MIN_SINGLE_ALL,
 329 #   S = { h( x ), P( h( x ), y ), Q( y, z ) }.
 330 # For MIN_SINGLE_MAX,
 331 #   S = { P( h( x ), y ), Q( y, z ) }.
 332 #
 333 # Furthermore, MIN_SINGLE_ALL and MIN_SINGLE_MAX, when
 334 # selecting single triggers, only select terms of minimal size.
 335 #
 336 [[option]]
 337   name       = "triggerSelMode"
 338   category   = "regular"
 339   long       = "trigger-sel=MODE"
 340   type       = "TriggerSelMode"
 341   default    = "MIN"
 342   help       = "selection mode for triggers"
 343   help_mode  = "Trigger selection modes."
 344 [[option.mode.MIN]]
 345   name = "min"
 346   help = "Consider only minimal subterms that meet criteria for triggers."
 347 [[option.mode.MAX]]
 348   name = "max"
 349   help = "Consider only maximal subterms that meet criteria for triggers."
 350 [[option.mode.MIN_SINGLE_MAX]]
 351   name = "min-s-max"
 352   help = "Consider only minimal subterms that meet criteria for single triggers, maximal otherwise."
 353 [[option.mode.MIN_SINGLE_ALL]]
 354   name = "min-s-all"
 355   help = "Consider only minimal subterms that meet criteria for single triggers, all otherwise."
 356 [[option.mode.ALL]]
 357   name = "all"
 358   help = "Consider all subterms that meet criteria for triggers."
 359
 360 [[option]]
 361   name       = "triggerActiveSelMode"
 362   category   = "regular"
 363   long       = "trigger-active-sel=MODE"
 364   type       = "TriggerActiveSelMode"
 365   default    = "ALL"
 366   help       = "selection mode to activate triggers"
 367   help_mode  = "Trigger active selection modes."
 368 [[option.mode.ALL]]
 369   name = "all"
 370   help = "Make all triggers active."
 371 [[option.mode.MIN]]
 372   name = "min"
 373   help = "Activate triggers with minimal ground terms."
 374 [[option.mode.MAX]]
 375   name = "max"
 376   help = "Activate triggers with maximal ground terms."
 377
 378 [[option]]
 379   name       = "userPatternsQuant"
 380   category   = "regular"
 381   long       = "user-pat=MODE"
 382   type       = "UserPatMode"
 383   default    = "TRUST"
 384   help       = "policy for handling user-provided patterns for quantifier instantiation"
 385   help_mode  = "These modes determine how user provided patterns (triggers) are used during E-matching. The modes vary on when instantiation based on user-provided triggers is combined with instantiation based on automatically selected triggers."
 386 [[option.mode.USE]]
 387   name = "use"
 388   help = "Use both user-provided and auto-generated patterns when patterns are provided for a quantified formula."
 389 [[option.mode.TRUST]]
 390   name = "trust"
 391   help = "When provided, use only user-provided patterns for a quantified formula."
 392 [[option.mode.RESORT]]
 393   name = "resort"
 394   help = "Use user-provided patterns only after auto-generated patterns saturate."
 395 [[option.mode.IGNORE]]
 396   name = "ignore"
 397   help = "Ignore user-provided patterns."
 398 [[option.mode.INTERLEAVE]]
 399   name = "interleave"
 400   help = "Alternate between use/resort."
 401
 402 [[option]]
 403   name       = "incrementTriggers"
 404   category   = "regular"
 405   long       = "increment-triggers"
 406   type       = "bool"
 407   default    = "true"
 408   help       = "generate additional triggers as needed during search"
 409
 410 [[option]]
 411   name       = "instWhenMode"
 412   category   = "regular"
 413   long       = "inst-when=MODE"
 414   type       = "InstWhenMode"
 415   default    = "FULL_LAST_CALL"
 416   predicates = ["checkInstWhenMode"]
 417   help       = "when to apply instantiation"
 418   help_mode  = "Instantiation modes."
 419 [[option.mode.PRE_FULL]]
 420   name = "pre-full"
 421   help = "Run instantiation round before full effort (possibly at standard effort)."
 422 [[option.mode.FULL]]
 423   name = "full"
 424   help = "Run instantiation round at full effort, before theory combination."
 425 [[option.mode.FULL_DELAY]]
 426   name = "full-delay"
 427   help = "Run instantiation round at full effort, before theory combination, after all other theories have finished."
 428 [[option.mode.FULL_LAST_CALL]]
 429   name = "full-last-call"
 430   help = "Alternate running instantiation rounds at full effort and last call.  In other words, interleave instantiation and theory combination."
 431 [[option.mode.FULL_DELAY_LAST_CALL]]
 432   name = "full-delay-last-call"
 433   help = "Alternate running instantiation rounds at full effort after all other theories have finished, and last call."
 434 [[option.mode.LAST_CALL]]
 435   name = "last-call"
 436   help = "Run instantiation at last call effort, after theory combination and and theories report sat."
 437
 438 [[option]]
 439   name       = "instWhenStrictInterleave"
 440   category   = "regular"
 441   long       = "inst-when-strict-interleave"
 442   type       = "bool"
 443   default    = "true"
 444   help       = "ensure theory combination and standard quantifier effort strategies take turns"
 445
 446 [[option]]
 447   name       = "instWhenPhase"
 448   category   = "regular"
 449   long       = "inst-when-phase=N"
 450   type       = "int"
 451   default    = "2"
 452   help       = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
 453
 454 [[option]]
 455   name       = "instWhenTcFirst"
 456   category   = "regular"
 457   long       = "inst-when-tc-first"
 458   type       = "bool"
 459   default    = "true"
 460   help       = "allow theory combination to happen once initially, before quantifier strategies are run"
 461
 462 [[option]]
 463   name       = "instMaxLevel"
 464   category   = "regular"
 465   long       = "inst-max-level=N"
 466   type       = "int"
 467   default    = "-1"
 468   help       = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
 469
 470 [[option]]
 471   name       = "instLevelInputOnly"
 472   category   = "regular"
 473   long       = "inst-level-input-only"
 474   type       = "bool"
 475   default    = "true"
 476   help       = "only input terms are assigned instantiation level zero"
 477
 478 [[option]]
 479   name       = "quantRepMode"
 480   category   = "regular"
 481   long       = "quant-rep-mode=MODE"
 482   type       = "QuantRepMode"
 483   default    = "FIRST"
 484   help       = "selection mode for representatives in quantifiers engine"
 485   help_mode  = "Modes for quantifiers representative selection."
 486 [[option.mode.EE]]
 487   name = "ee"
 488   help = "Let equality engine choose representatives."
 489 [[option.mode.FIRST]]
 490   name = "first"
 491   help = "Choose terms that appear first."
 492 [[option.mode.DEPTH]]
 493   name = "depth"
 494   help = "Choose terms that are of minimal depth."
 495
 496 [[option]]
 497   name       = "fullSaturateQuant"
 498   category   = "regular"
 499   long       = "full-saturate-quant"
 500   type       = "bool"
 501   default    = "false"
 502   help       = "enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
 503
 504 [[option]]
 505   name       = "fullSaturateQuantRd"
 506   category   = "regular"
 507   long       = "full-saturate-quant-rd"
 508   type       = "bool"
 509   default    = "true"
 510   help       = "whether to use relevant domain first for enumerative instantiation strategy"
 511
 512 [[option]]
 513   name       = "fullSaturateLimit"
 514   category   = "regular"
 515   long       = "full-saturate-quant-limit=N"
 516   type       = "int"
 517   default    = "-1"
 518   help       = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)"
 519
 520 [[option]]
 521   name       = "fullSaturateInterleave"
 522   category   = "regular"
 523   long       = "fs-interleave"
 524   type       = "bool"
 525   default    = "false"
 526   help       = "interleave enumerative instantiation with other techniques"
 527
 528 [[option]]
 529   name       = "fullSaturateStratify"
 530   category   = "regular"
 531   long       = "fs-stratify"
 532   type       = "bool"
 533   default    = "false"
 534   help       = "stratify effort levels in enumerative instantiation, which favors speed over fairness"
 535
 536 [[option]]
 537   name       = "fullSaturateSum"
 538   category   = "regular"
 539   long       = "fs-sum"
 540   type       = "bool"
 541   default    = "false"
 542   help       = "enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum"
 543
 544 [[option]]
 545   name       = "literalMatchMode"
 546   category   = "regular"
 547   long       = "literal-matching=MODE"
 548   type       = "LiteralMatchMode"
 549   default    = "USE"
 550   help       = "choose literal matching mode"
 551   help_mode  = "Literal match modes."
 552 [[option.mode.NONE]]
 553   name = "none"
 554   help = "Do not use literal matching."
 555 [[option.mode.USE]]
 556   name = "use"
 557   help = "Consider phase requirements of triggers conservatively. For example, the trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with terms in the equivalence class of true, and likewise Q( x ) will not be matched terms in the equivalence class of false. Extends to equality."
 558 [[option.mode.AGG_PREDICATE]]
 559   name = "agg-predicate"
 560   help = "Consider phase requirements aggressively for predicates. In the above example, only match P( x ) with terms that are in the equivalence class of false."
 561 [[option.mode.AGG]]
 562   name = "agg"
 563   help = "Consider the phase requirements aggressively for all triggers."
 564
 565 [[option]]
 566   name       = "poolInst"
 567   category   = "regular"
 568   long       = "pool-inst"
 569   type       = "bool"
 570   default    = "true"
 571   help       = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools"
 572
 573 ### Finite model finding options
 574
 575 [[option]]
 576   name       = "finiteModelFind"
 577   category   = "regular"
 578   long       = "finite-model-find"
 579   type       = "bool"
 580   default    = "false"
 581   help       = "use finite model finding heuristic for quantifier instantiation"
 582
 583 [[option]]
 584   name       = "quantFunWellDefined"
 585   category   = "regular"
 586   long       = "quant-fun-wd"
 587   type       = "bool"
 588   default    = "false"
 589   help       = "assume that function defined by quantifiers are well defined"
 590
 591 [[option]]
 592   name       = "fmfFunWellDefined"
 593   category   = "regular"
 594   long       = "fmf-fun"
 595   type       = "bool"
 596   default    = "false"
 597   help       = "find models for recursively defined functions, assumes functions are admissible"
 598
 599 [[option]]
 600   name       = "fmfFunWellDefinedRelevant"
 601   category   = "regular"
 602   long       = "fmf-fun-rlv"
 603   type       = "bool"
 604   default    = "false"
 605   help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
 606
 607 [[option]]
 608   name       = "mbqiMode"
 609   category   = "regular"
 610   long       = "mbqi=MODE"
 611   type       = "MbqiMode"
 612   default    = "FMC"
 613   help       = "choose mode for model-based quantifier instantiation"
 614   help_mode  = "Model-based quantifier instantiation modes."
 615 [[option.mode.NONE]]
 616   name = "none"
 617   help = "Disable model-based quantifier instantiation."
 618 [[option.mode.FMC]]
 619   name = "fmc"
 620   help = "Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability Modulo Theories."
 621 [[option.mode.TRUST]]
 622   name = "trust"
 623   help = "Do not instantiate quantified formulas (incomplete technique)."
 624
 625 [[option]]
 626   name       = "fmfOneInstPerRound"
 627   category   = "regular"
 628   long       = "mbqi-one-inst-per-round"
 629   type       = "bool"
 630   default    = "false"
 631   help       = "only add one instantiation per quantifier per round for mbqi"
 632
 633 [[option]]
 634   name       = "mbqiInterleave"
 635   category   = "regular"
 636   long       = "mbqi-interleave"
 637   type       = "bool"
 638   default    = "false"
 639   help       = "interleave model-based quantifier instantiation with other techniques"
 640
 641 [[option]]
 642   name       = "fmfInstEngine"
 643   category   = "regular"
 644   long       = "fmf-inst-engine"
 645   type       = "bool"
 646   default    = "false"
 647   help       = "use instantiation engine in conjunction with finite model finding"
 648
 649 [[option]]
 650   name       = "fmfFreshDistConst"
 651   category   = "regular"
 652   long       = "fmf-fresh-dc"
 653   type       = "bool"
 654   default    = "false"
 655   help       = "use fresh distinguished representative when applying Inst-Gen techniques"
 656
 657 [[option]]
 658   name       = "fmfFmcSimple"
 659   category   = "regular"
 660   long       = "fmf-fmc-simple"
 661   type       = "bool"
 662   default    = "true"
 663   help       = "simple models in full model check for finite model finding"
 664
 665 [[option]]
 666   name       = "fmfBoundInt"
 667   category   = "regular"
 668   long       = "fmf-bound-int"
 669   type       = "bool"
 670   default    = "false"
 671   help       = "finite model finding on bounded integer quantification"
 672
 673 [[option]]
 674   name       = "fmfBound"
 675   category   = "regular"
 676   long       = "fmf-bound"
 677   type       = "bool"
 678   default    = "false"
 679   help       = "finite model finding on bounded quantification"
 680
 681 [[option]]
 682   name       = "fmfBoundLazy"
 683   category   = "regular"
 684   long       = "fmf-bound-lazy"
 685   type       = "bool"
 686   default    = "false"
 687   help       = "enforce bounds for bounded quantification lazily via use of proxy variables"
 688
 689 [[option]]
 690   name       = "fmfTypeCompletionThresh"
 691   category   = "regular"
 692   long       = "fmf-type-completion-thresh=N"
 693   type       = "int"
 694   default    = "1000"
 695   help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
 696
 697 [[option]]
 698   name       = "quantConflictFind"
 699   category   = "regular"
 700   long       = "quant-cf"
 701   type       = "bool"
 702   default    = "true"
 703   help       = "enable conflict find mechanism for quantifiers"
 704
 705 [[option]]
 706   name       = "qcfMode"
 707   category   = "regular"
 708   long       = "quant-cf-mode=MODE"
 709   type       = "QcfMode"
 710   default    = "PROP_EQ"
 711   help       = "what effort to apply conflict find mechanism"
 712   help_mode  = "Quantifier conflict find modes."
 713 [[option.mode.CONFLICT_ONLY]]
 714   name = "conflict"
 715   help = "Apply QCF algorithm to find conflicts only."
 716 [[option.mode.PROP_EQ]]
 717   name = "prop-eq"
 718   help = "Apply QCF algorithm to propagate equalities as well as conflicts."
 719 [[option.mode.PARTIAL]]
 720   name = "partial"
 721   help = "Use QCF for conflicts, propagations and heuristic instantiations."
 722
 723 [[option]]
 724   name       = "qcfWhenMode"
 725   category   = "regular"
 726   long       = "quant-cf-when=MODE"
 727   type       = "QcfWhenMode"
 728   default    = "DEFAULT"
 729   help       = "when to invoke conflict find mechanism for quantifiers"
 730   help_mode  = "Quantifier conflict find modes."
 731 [[option.mode.DEFAULT]]
 732   name = "default"
 733   help = "Default, apply conflict finding at full effort."
 734 [[option.mode.LAST_CALL]]
 735   name = "last-call"
 736   help = "Apply conflict finding at last call, after theory combination and and all theories report sat."
 737 [[option.mode.STD]]
 738   name = "std"
 739   help = "Apply conflict finding at standard effort."
 740 [[option.mode.STD_H]]
 741   name = "std-h"
 742   help = "Apply conflict finding at standard effort when heuristic says to."
 743
 744 [[option]]
 745   name       = "qcfTConstraint"
 746   category   = "regular"
 747   long       = "qcf-tconstraint"
 748   type       = "bool"
 749   default    = "false"
 750   help       = "enable entailment checks for t-constraints in qcf algorithm"
 751
 752 [[option]]
 753   name       = "qcfAllConflict"
 754   category   = "regular"
 755   long       = "qcf-all-conflict"
 756   type       = "bool"
 757   default    = "false"
 758   help       = "add all available conflicting instances during conflict-based instantiation"
 759
 760 [[option]]
 761   name       = "qcfNestedConflict"
 762   category   = "regular"
 763   long       = "qcf-nested-conflict"
 764   type       = "bool"
 765   default    = "false"
 766   help       = "consider conflicts for nested quantifiers"
 767
 768 [[option]]
 769   name       = "qcfVoExp"
 770   category   = "regular"
 771   long       = "qcf-vo-exp"
 772   type       = "bool"
 773   default    = "false"
 774   help       = "qcf experimental variable ordering"
 775
 776 [[option]]
 777   name       = "instNoEntail"
 778   category   = "regular"
 779   long       = "inst-no-entail"
 780   type       = "bool"
 781   default    = "true"
 782   help       = "do not consider instances of quantified formulas that are currently entailed"
 783
 784 [[option]]
 785   name       = "qcfEagerTest"
 786   category   = "regular"
 787   long       = "qcf-eager-test"
 788   type       = "bool"
 789   default    = "true"
 790   help       = "optimization, test qcf instances eagerly"
 791
 792 [[option]]
 793   name       = "qcfEagerCheckRd"
 794   category   = "regular"
 795   long       = "qcf-eager-check-rd"
 796   type       = "bool"
 797   default    = "true"
 798   help       = "optimization, eagerly check relevant domain of matched position"
 799
 800 [[option]]
 801   name       = "qcfSkipRd"
 802   category   = "regular"
 803   long       = "qcf-skip-rd"
 804   type       = "bool"
 805   default    = "false"
 806   help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 807
 808 ### Induction options
 809
 810 [[option]]
 811   name       = "quantInduction"
 812   category   = "regular"
 813   long       = "quant-ind"
 814   type       = "bool"
 815   default    = "false"
 816   help       = "use all available techniques for inductive reasoning"
 817
 818 [[option]]
 819   name       = "dtStcInduction"
 820   category   = "regular"
 821   long       = "dt-stc-ind"
 822   type       = "bool"
 823   default    = "false"
 824   help       = "apply strengthening for existential quantification over datatypes based on structural induction"
 825
 826 [[option]]
 827   name       = "intWfInduction"
 828   category   = "regular"
 829   long       = "int-wf-ind"
 830   type       = "bool"
 831   default    = "false"
 832   help       = "apply strengthening for integers based on well-founded induction"
 833
 834 [[option]]
 835   name       = "conjectureGen"
 836   category   = "regular"
 837   long       = "conjecture-gen"
 838   type       = "bool"
 839   default    = "false"
 840   help       = "generate candidate conjectures for inductive proofs"
 841
 842 [[option]]
 843   name       = "conjectureGenPerRound"
 844   category   = "regular"
 845   long       = "conjecture-gen-per-round=N"
 846   type       = "int"
 847   default    = "1"
 848   help       = "number of conjectures to generate per instantiation round"
 849
 850 [[option]]
 851   name       = "conjectureNoFilter"
 852   category   = "regular"
 853   long       = "conjecture-no-filter"
 854   type       = "bool"
 855   default    = "false"
 856   help       = "do not filter conjectures"
 857
 858 [[option]]
 859   name       = "conjectureFilterActiveTerms"
 860   category   = "regular"
 861   long       = "conjecture-filter-active-terms"
 862   type       = "bool"
 863   default    = "true"
 864   help       = "filter based on active terms"
 865
 866 [[option]]
 867   name       = "conjectureFilterCanonical"
 868   category   = "regular"
 869   long       = "conjecture-filter-canonical"
 870   type       = "bool"
 871   default    = "true"
 872   help       = "filter based on canonicity"
 873
 874 [[option]]
 875   name       = "conjectureFilterModel"
 876   category   = "regular"
 877   long       = "conjecture-filter-model"
 878   type       = "bool"
 879   default    = "true"
 880   help       = "filter based on model"
 881
 882 [[option]]
 883   name       = "conjectureGenGtEnum"
 884   category   = "regular"
 885   long       = "conjecture-gen-gt-enum=N"
 886   type       = "int"
 887   default    = "50"
 888   help       = "number of ground terms to generate for model filtering"
 889
 890 [[option]]
 891   name       = "conjectureUeeIntro"
 892   category   = "regular"
 893   long       = "conjecture-gen-uee-intro"
 894   type       = "bool"
 895   default    = "false"
 896   help       = "more aggressive merging for universal equality engine, introduces terms"
 897
 898 [[option]]
 899   name       = "conjectureGenMaxDepth"
 900   category   = "regular"
 901   long       = "conjecture-gen-max-depth=N"
 902   type       = "int"
 903   default    = "3"
 904   help       = "maximum depth of terms to consider for conjectures"
 905
 906 ### Synthesis options
 907
 908 [[option]]
 909   name       = "sygusInference"
 910   category   = "regular"
 911   long       = "sygus-inference"
 912   type       = "bool"
 913   default    = "false"
 914   help       = "attempt to preprocess arbitrary inputs to sygus conjectures"
 915
 916 [[option]]
 917   name       = "sygus"
 918   category   = "regular"
 919   long       = "sygus"
 920   type       = "bool"
 921   default    = "false"
 922   help       = "use sygus solver (default is true for sygus inputs)"
 923
 924 [[option]]
 925   name       = "cegqiSingleInvMode"
 926   category   = "regular"
 927   long       = "sygus-si=MODE"
 928   type       = "CegqiSingleInvMode"
 929   default    = "NONE"
 930   help       = "mode for processing single invocation synthesis conjectures"
 931   help_mode  = "Modes for single invocation techniques."
 932 [[option.mode.NONE]]
 933   name = "none"
 934   help = "Do not use single invocation techniques."
 935 [[option.mode.USE]]
 936   name = "use"
 937   help = "Use single invocation techniques only if grammar is not restrictive."
 938 [[option.mode.ALL]]
 939   name = "all"
 940   help = "Always use single invocation techniques."
 941
 942 [[option]]
 943   name       = "cegqiSingleInvPartial"
 944   category   = "regular"
 945   long       = "sygus-si-partial"
 946   type       = "bool"
 947   default    = "false"
 948   help       = "combined techniques for synthesis conjectures that are partially single invocation"
 949
 950 # Solution reconstruction modes for single invocation conjectures
 951 #
 952 # These modes indicate the policy when cvc5 solves a synthesis conjecture using
 953 # single invocation techniques for a sygus problem with a user-specified
 954 # grammar.
 955 #
 956 [[option]]
 957   name       = "cegqiSingleInvReconstruct"
 958   category   = "regular"
 959   long       = "sygus-si-rcons=MODE"
 960   type       = "CegqiSingleInvRconsMode"
 961   default    = "ALL_LIMIT"
 962   help       = "policy for reconstructing solutions for single invocation conjectures"
 963   help_mode  = "Modes for reconstruction solutions while using single invocation techniques."
 964 [[option.mode.NONE]]
 965   name = "none"
 966   help = "Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by cvc5 may violate grammar restrictions."
 967 [[option.mode.TRY]]
 968   name = "try"
 969   help = "Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner."
 970 [[option.mode.ALL_LIMIT]]
 971   name = "all-limit"
 972   help = "Try to reconstruct solutions in the original grammar, but termintate if a maximum number of rounds for reconstruction is exceeded."
 973 [[option.mode.ALL]]
 974   name = "all"
 975   help = "Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed."
 976
 977 [[option]]
 978   name       = "cegqiSingleInvReconstructLimit"
 979   category   = "regular"
 980   long       = "sygus-si-rcons-limit=N"
 981   type       = "int"
 982   default    = "10000"
 983   help       = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
 984
 985 [[option]]
 986   name       = "cegqiSingleInvReconstructConst"
 987   category   = "regular"
 988   long       = "sygus-si-reconstruct-const"
 989   type       = "bool"
 990   default    = "true"
 991   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 992
 993 [[option]]
 994   name       = "cegqiSingleInvAbort"
 995   category   = "regular"
 996   long       = "sygus-si-abort"
 997   type       = "bool"
 998   default    = "false"
 999   help       = "abort if synthesis conjecture is not single invocation"
1000
1001 [[option]]
1002   name       = "sygusConstRepairAbort"
1003   category   = "regular"
1004   long       = "sygus-crepair-abort"
1005   type       = "bool"
1006   default    = "false"
1007   help       = "abort if constant repair techniques are not applicable"
1008
1009 # Modes for piecewise-independent unification for synthesis (see Barbosa et al
1010 # FMCAD 2019).
1011 #
1012 [[option]]
1013   name       = "sygusUnifPi"
1014   category   = "regular"
1015   long       = "sygus-unif-pi=MODE"
1016   type       = "SygusUnifPiMode"
1017   default    = "NONE"
1018   help       = "mode for synthesis via piecewise-indepedent unification"
1019   help_mode  = "Modes for piecewise-independent unification."
1020 [[option.mode.NONE]]
1021   name = "none"
1022   help = "Do not use piecewise-independent unification."
1023 [[option.mode.COMPLETE]]
1024   name = "complete"
1025   help = "Use complete approach for piecewise-independent unification (see Section 3 of Barbosa et al FMCAD 2019)"
1026 [[option.mode.CENUM]]
1027   name = "cond-enum"
1028   help = "Use unconstrained condition enumeration for piecewise-independent unification (see Section 4 of Barbosa et al FMCAD 2019)."
1029 [[option.mode.CENUM_IGAIN]]
1030   name = "cond-enum-igain"
1031   help = "Same as cond-enum, but additionally uses an information gain heuristic when doing decision tree learning."
1032
1033 [[option]]
1034   name       = "sygusUnifShuffleCond"
1035   category   = "regular"
1036   long       = "sygus-unif-shuffle-cond"
1037   type       = "bool"
1038   default    = "false"
1039   help       = "Shuffle condition pool when building solutions (may change solutions sizes)"
1040
1041 [[option]]
1042   name       = "sygusUnifCondIndNoRepeatSol"
1043   category   = "regular"
1044   long       = "sygus-unif-cond-independent-no-repeat-sol"
1045   type       = "bool"
1046   default    = "true"
1047   help       = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
1048
1049 [[option]]
1050   name       = "sygusBoolIteReturnConst"
1051   category   = "regular"
1052   long       = "sygus-bool-ite-return-const"
1053   type       = "bool"
1054   default    = "true"
1055   help       = "Only use Boolean constants for return values in unification-based function synthesis"
1056
1057 [[option]]
1058   name       = "sygusQePreproc"
1059   category   = "regular"
1060   long       = "sygus-qe-preproc"
1061   type       = "bool"
1062   default    = "false"
1063   help       = "use quantifier elimination as a preprocessing step for sygus"
1064
1065 [[option]]
1066   name       = "sygusRepairConst"
1067   category   = "regular"
1068   long       = "sygus-repair-const"
1069   type       = "bool"
1070   default    = "false"
1071   help       = "use approach to repair constants in sygus candidate solutions"
1072
1073 [[option]]
1074   name       = "sygusCoreConnective"
1075   category   = "regular"
1076   long       = "sygus-core-connective"
1077   type       = "bool"
1078   default    = "false"
1079   help       = "use unsat core analysis to construct Boolean connective to sygus conjectures"
1080
1081 [[option]]
1082   name       = "sygusRepairConstTimeout"
1083   category   = "regular"
1084   long       = "sygus-repair-const-timeout=N"
1085   type       = "unsigned long"
1086   help       = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
1087
1088 [[option]]
1089   name       = "sygusActiveGenMode"
1090   category   = "regular"
1091   long       = "sygus-active-gen=MODE"
1092   type       = "SygusActiveGenMode"
1093   default    = "AUTO"
1094   help       = "mode for actively-generated sygus enumerators"
1095   help_mode  = "Modes for actively-generated sygus enumerators."
1096 [[option.mode.NONE]]
1097   name = "none"
1098   help = "Do not use actively-generated sygus enumerators."
1099 [[option.mode.ENUM_BASIC]]
1100   name = "basic"
1101   help = "Use basic type enumerator for actively-generated sygus enumerators."
1102 [[option.mode.ENUM]]
1103   name = "enum"
1104   help = "Use optimized enumerator for actively-generated sygus enumerators."
1105 [[option.mode.VAR_AGNOSTIC]]
1106   name = "var-agnostic"
1107   help = "Use sygus solver to enumerate terms that are agnostic to variables."
1108 [[option.mode.AUTO]]
1109   name = "auto"
1110   help = "Internally decide the best policy for each enumerator."
1111
1112 [[option]]
1113   name       = "sygusActiveGenEnumConsts"
1114   category   = "regular"
1115   long       = "sygus-active-gen-cfactor=N"
1116   type       = "unsigned long"
1117   default    = "5"
1118   help       = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum"
1119
1120 [[option]]
1121   name       = "sygusMinGrammar"
1122   category   = "regular"
1123   long       = "sygus-min-grammar"
1124   type       = "bool"
1125   default    = "true"
1126   help       = "statically minimize sygus grammars"
1127
1128 [[option]]
1129   name       = "sygusAddConstGrammar"
1130   category   = "regular"
1131   long       = "sygus-add-const-grammar"
1132   type       = "bool"
1133   default    = "false"
1134   help       = "statically add constants appearing in conjecture to grammars"
1135
1136 [[option]]
1137   name       = "sygusGrammarNorm"
1138   category   = "regular"
1139   long       = "sygus-grammar-norm"
1140   type       = "bool"
1141   default    = "false"
1142   help       = "statically normalize sygus grammars based on flattening (linearization)"
1143
1144 [[option]]
1145   name       = "sygusTemplEmbedGrammar"
1146   category   = "regular"
1147   long       = "sygus-templ-embed-grammar"
1148   type       = "bool"
1149   default    = "false"
1150   help       = "embed sygus templates into grammars"
1151
1152 [[option]]
1153   name       = "sygusGrammarConsMode"
1154   category   = "regular"
1155   long       = "sygus-grammar-cons=MODE"
1156   type       = "SygusGrammarConsMode"
1157   default    = "SIMPLE"
1158   help       = "mode for SyGuS grammar construction"
1159   help_mode  = "Modes for default SyGuS grammars."
1160 [[option.mode.SIMPLE]]
1161   name = "simple"
1162   help = "Use simple grammar construction (no symbolic terms or constants)."
1163 [[option.mode.ANY_CONST]]
1164   name = "any-const"
1165   help = "Use symoblic constant constructors."
1166 [[option.mode.ANY_TERM]]
1167   name = "any-term"
1168   help = "When applicable, use constructors corresponding to any symbolic term. This option enables a sum-of-monomials grammar for arithmetic. For all other types, it enables symbolic constant constructors."
1169 [[option.mode.ANY_TERM_CONCISE]]
1170   name = "any-term-concise"
1171   help = "When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to any-term but enables a polynomial grammar for arithmetic when not in a combined theory."
1172
1173 [[option]]
1174   name       = "sygusInvTemplMode"
1175   category   = "regular"
1176   long       = "sygus-inv-templ=MODE"
1177   type       = "SygusInvTemplMode"
1178   default    = "POST"
1179   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1180   help_mode  = "Template modes for sygus invariant synthesis."
1181 [[option.mode.NONE]]
1182   name = "none"
1183   help = "Synthesize invariant directly."
1184 [[option.mode.PRE]]
1185   name = "pre"
1186   help = "Synthesize invariant based on weakening of precondition."
1187 [[option.mode.POST]]
1188   name = "post"
1189   help = "Synthesize invariant based on strengthening of postcondition."
1190
1191 [[option]]
1192   name       = "sygusInvTemplWhenSyntax"
1193   category   = "regular"
1194   long       = "sygus-inv-templ-when-sg"
1195   type       = "bool"
1196   default    = "false"
1197   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1198
1199 [[option]]
1200   name       = "sygusInvAutoUnfold"
1201   category   = "regular"
1202   long       = "sygus-auto-unfold"
1203   type       = "bool"
1204   default    = "true"
1205   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1206
1207 [[option]]
1208   name       = "sygusUnifPbe"
1209   category   = "regular"
1210   long       = "sygus-pbe"
1211   type       = "bool"
1212   default    = "true"
1213   help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1214
1215 [[option]]
1216   name       = "sygusPbeMultiFair"
1217   category   = "regular"
1218   long       = "sygus-pbe-multi-fair"
1219   type       = "bool"
1220   default    = "false"
1221   help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
1222
1223 [[option]]
1224   name       = "sygusPbeMultiFairDiff"
1225   category   = "regular"
1226   long       = "sygus-pbe-multi-fair-diff=N"
1227   type       = "int"
1228   default    = "0"
1229   help       = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1230
1231 [[option]]
1232   name       = "sygusEvalUnfold"
1233   category   = "regular"
1234   long       = "sygus-eval-unfold"
1235   type       = "bool"
1236   default    = "true"
1237   help       = "do unfolding of sygus evaluation functions"
1238
1239 [[option]]
1240   name       = "sygusEvalUnfoldBool"
1241   category   = "regular"
1242   long       = "sygus-eval-unfold-bool"
1243   type       = "bool"
1244   default    = "true"
1245   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1246
1247 [[option]]
1248   name       = "sygusStream"
1249   category   = "regular"
1250   long       = "sygus-stream"
1251   type       = "bool"
1252   default    = "false"
1253   help       = "enumerate a stream of solutions instead of terminating after the first one"
1254
1255 [[option]]
1256   name       = "sygusExtRew"
1257   category   = "regular"
1258   long       = "sygus-ext-rew"
1259   type       = "bool"
1260   default    = "true"
1261   help       = "use extended rewriter for sygus"
1262
1263 [[option]]
1264   name       = "cegisSample"
1265   category   = "regular"
1266   long       = "cegis-sample=MODE"
1267   type       = "CegisSampleMode"
1268   default    = "NONE"
1269   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
1270   help_mode  = "Modes for sampling with counterexample-guided inductive synthesis (CEGIS)."
1271 [[option.mode.NONE]]
1272   name = "none"
1273   help = "Do not use sampling with CEGIS."
1274 [[option.mode.USE]]
1275   name = "use"
1276   help = "Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point."
1277 [[option.mode.TRUST]]
1278   name = "trust"
1279   help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
1280
1281 [[option]]
1282   name       = "sygusEvalOpt"
1283   category   = "regular"
1284   long       = "sygus-eval-opt"
1285   type       = "bool"
1286   default    = "true"
1287   help       = "use optimized approach for evaluation in sygus"
1288
1289 [[option]]
1290   name       = "sygusArgRelevant"
1291   category   = "regular"
1292   long       = "sygus-arg-relevant"
1293   type       = "bool"
1294   default    = "false"
1295   help       = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1296
1297 [[option]]
1298   name       = "sygusRecFun"
1299   category   = "regular"
1300   long       = "sygus-rec-fun"
1301   type       = "bool"
1302   default    = "true"
1303   help       = "enable efficient support for recursive functions in sygus grammars"
1304
1305 [[option]]
1306   name       = "sygusRecFunEvalLimit"
1307   category   = "regular"
1308   long       = "sygus-rec-fun-eval-limit=N"
1309   type       = "unsigned"
1310   default    = "1000"
1311   help       = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
1312
1313 # Internal uses of sygus
1314
1315 [[option]]
1316   name       = "sygusRew"
1317   category   = "regular"
1318   long       = "sygus-rr"
1319   type       = "bool"
1320   default    = "false"
1321   help       = "use sygus to enumerate and verify correctness of rewrite rules"
1322
1323 [[option]]
1324   name       = "sygusRewSynth"
1325   category   = "regular"
1326   long       = "sygus-rr-synth"
1327   type       = "bool"
1328   default    = "false"
1329   help       = "use sygus to enumerate candidate rewrite rules"
1330
1331 [[option]]
1332   name       = "sygusRewSynthFilterOrder"
1333   category   = "regular"
1334   long       = "sygus-rr-synth-filter-order"
1335   type       = "bool"
1336   default    = "true"
1337   help       = "filter candidate rewrites based on variable ordering"
1338
1339 [[option]]
1340   name       = "sygusRewSynthFilterMatch"
1341   category   = "regular"
1342   long       = "sygus-rr-synth-filter-match"
1343   type       = "bool"
1344   default    = "true"
1345   help       = "filter candidate rewrites based on matching"
1346
1347 [[option]]
1348   name       = "sygusRewSynthFilterCong"
1349   category   = "regular"
1350   long       = "sygus-rr-synth-filter-cong"
1351   type       = "bool"
1352   default    = "true"
1353   help       = "filter candidate rewrites based on congruence"
1354
1355 [[option]]
1356   name       = "sygusRewSynthFilterNonLinear"
1357   category   = "regular"
1358   long       = "sygus-rr-synth-filter-nl"
1359   type       = "bool"
1360   default    = "false"
1361   help       = "filter non-linear candidate rewrites"
1362
1363 [[option]]
1364   name       = "sygusRewVerify"
1365   category   = "regular"
1366   long       = "sygus-rr-verify"
1367   type       = "bool"
1368   default    = "false"
1369   help       = "use sygus to verify the correctness of rewrite rules via sampling"
1370
1371 [[option]]
1372   name       = "sygusRewVerifyAbort"
1373   category   = "regular"
1374   long       = "sygus-rr-verify-abort"
1375   type       = "bool"
1376   default    = "true"
1377   help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1378
1379 [[option]]
1380   name       = "sygusSamples"
1381   category   = "regular"
1382   long       = "sygus-samples=N"
1383   type       = "int"
1384   default    = "1000"
1385   help       = "number of points to consider when doing sygus rewriter sample testing"
1386
1387 [[option]]
1388   name       = "sygusSampleGrammar"
1389   category   = "regular"
1390   long       = "sygus-sample-grammar"
1391   type       = "bool"
1392   default    = "true"
1393   help       = "when applicable, use grammar for choosing sample points"
1394
1395 [[option]]
1396   name       = "sygusSampleFpUniform"
1397   category   = "regular"
1398   long       = "sygus-sample-fp-uniform"
1399   type       = "bool"
1400   default    = "false"
1401   help       = "sample floating-point values uniformly instead of in a biased fashion"
1402
1403 [[option]]
1404   name       = "sygusRewSynthAccel"
1405   category   = "regular"
1406   long       = "sygus-rr-synth-accel"
1407   type       = "bool"
1408   default    = "false"
1409   help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
1410
1411 [[option]]
1412   name       = "sygusRewSynthCheck"
1413   category   = "regular"
1414   long       = "sygus-rr-synth-check"
1415   type       = "bool"
1416   default    = "false"
1417   help       = "use satisfiability check to verify correctness of candidate rewrites"
1418
1419 [[option]]
1420   name       = "sygusRewSynthInput"
1421   category   = "regular"
1422   long       = "sygus-rr-synth-input"
1423   type       = "bool"
1424   default    = "false"
1425   help       = "synthesize rewrite rules based on the input formula"
1426
1427 [[option]]
1428   name       = "sygusRewSynthInputNVars"
1429   category   = "regular"
1430   long       = "sygus-rr-synth-input-nvars=N"
1431   type       = "int"
1432   default    = "3"
1433   help       = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
1434
1435 [[option]]
1436   name       = "sygusRewSynthInputUseBool"
1437   category   = "regular"
1438   long       = "sygus-rr-synth-input-use-bool"
1439   type       = "bool"
1440   default    = "false"
1441   help       = "synthesize Boolean rewrite rules based on the input formula"
1442
1443 [[option]]
1444   name       = "sygusExprMinerCheckTimeout"
1445   category   = "regular"
1446   long       = "sygus-expr-miner-check-timeout=N"
1447   type       = "unsigned long"
1448   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
1449
1450 [[option]]
1451   name       = "sygusRewSynthRec"
1452   category   = "regular"
1453   long       = "sygus-rr-synth-rec"
1454   type       = "bool"
1455   default    = "false"
1456   help       = "synthesize rewrite rules over all sygus grammar types recursively"
1457
1458 [[option]]
1459   name       = "sygusQueryGen"
1460   category   = "regular"
1461   long       = "sygus-query-gen"
1462   type       = "bool"
1463   default    = "false"
1464   help       = "use sygus to enumerate interesting satisfiability queries"
1465
1466 [[option]]
1467   name       = "sygusQueryGenThresh"
1468   category   = "regular"
1469   long       = "sygus-query-gen-thresh=N"
1470   type       = "unsigned"
1471   default    = "5"
1472   help       = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
1473
1474 [[option]]
1475   name       = "sygusQueryGenCheck"
1476   category   = "regular"
1477   long       = "sygus-query-gen-check"
1478   type       = "bool"
1479   default    = "true"
1480   help       = "use interesting satisfiability queries to check soundness of cvc5"
1481
1482 [[option]]
1483   name       = "sygusQueryGenDumpFiles"
1484   category   = "regular"
1485   long       = "sygus-query-gen-dump-files=MODE"
1486   type       = "SygusQueryDumpFilesMode"
1487   default    = "NONE"
1488   help       = "mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen"
1489   help_mode  = "Query file options."
1490 [[option.mode.NONE]]
1491   name = "none"
1492   help = "Do not dump query files when using --sygus-query-gen."
1493 [[option.mode.ALL]]
1494   name = "all"
1495   help = "Dump all query files."
1496 [[option.mode.UNSOLVED]]
1497   name = "unsolved"
1498   help = "Dump query files that the subsolver did not solve."
1499
1500 [[option]]
1501   name       = "sygusFilterSolMode"
1502   category   = "regular"
1503   long       = "sygus-filter-sol=MODE"
1504   type       = "SygusFilterSolMode"
1505   default    = "NONE"
1506   help       = "mode for filtering sygus solutions"
1507   help_mode  = "Modes for filtering sygus solutions."
1508 [[option.mode.NONE]]
1509   name = "none"
1510   help = "Do not filter sygus solutions."
1511 [[option.mode.STRONG]]
1512   name = "strong"
1513   help = "Filter solutions that are logically stronger than others."
1514 [[option.mode.WEAK]]
1515   name = "weak"
1516   help = "Filter solutions that are logically weaker than others."
1517
1518 [[option]]
1519   name       = "sygusFilterSolRevSubsume"
1520   category   = "expert"
1521   long       = "sygus-filter-sol-rev"
1522   type       = "bool"
1523   default    = "false"
1524   help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
1525
1526 [[option]]
1527   name       = "debugSygus"
1528   category   = "regular"
1529   long       = "debug-sygus"
1530   type       = "bool"
1531   default    = "false"
1532   help       = "print enumerated terms and candidates generated by the sygus solver (for debugging)"
1533
1534 # CEGQI applied to general quantified formulas
1535
1536 [[option]]
1537   name       = "cegqi"
1538   category   = "regular"
1539   long       = "cegqi"
1540   type       = "bool"
1541   default    = "false"
1542   help       = "turns on counterexample-based quantifier instantiation"
1543
1544 [[option]]
1545   name       = "cegqiFullEffort"
1546   category   = "regular"
1547   long       = "cegqi-full"
1548   type       = "bool"
1549   default    = "false"
1550   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1551
1552 [[option]]
1553   name       = "cegqiSat"
1554   category   = "regular"
1555   long       = "cegqi-sat"
1556   type       = "bool"
1557   default    = "true"
1558   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1559
1560 [[option]]
1561   name       = "cegqiModel"
1562   category   = "regular"
1563   long       = "cegqi-model"
1564   type       = "bool"
1565   default    = "true"
1566   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1567
1568 [[option]]
1569   name       = "cegqiAll"
1570   category   = "regular"
1571   long       = "cegqi-all"
1572   type       = "bool"
1573   default    = "false"
1574   help       = "apply counterexample-based instantiation to all quantified formulas"
1575
1576 [[option]]
1577   name       = "cegqiMultiInst"
1578   category   = "regular"
1579   long       = "cegqi-multi-inst"
1580   type       = "bool"
1581   default    = "false"
1582   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1583
1584 [[option]]
1585   name       = "cegqiRepeatLit"
1586   category   = "regular"
1587   long       = "cegqi-repeat-lit"
1588   type       = "bool"
1589   default    = "false"
1590   help       = "solve literals more than once in counterexample-based quantifier instantiation"
1591
1592 [[option]]
1593   name       = "cegqiInnermost"
1594   category   = "regular"
1595   long       = "cegqi-innermost"
1596   type       = "bool"
1597   default    = "true"
1598   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1599
1600 [[option]]
1601   name       = "cegqiNestedQE"
1602   category   = "regular"
1603   long       = "cegqi-nested-qe"
1604   type       = "bool"
1605   default    = "false"
1606   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1607
1608 # CEGQI for arithmetic
1609
1610 [[option]]
1611   name       = "cegqiUseInfInt"
1612   category   = "regular"
1613   long       = "cegqi-use-inf-int"
1614   type       = "bool"
1615   default    = "false"
1616   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1617
1618 [[option]]
1619   name       = "cegqiUseInfReal"
1620   category   = "regular"
1621   long       = "cegqi-use-inf-real"
1622   type       = "bool"
1623   default    = "false"
1624   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1625
1626 [[option]]
1627   name       = "cegqiMinBounds"
1628   category   = "regular"
1629   long       = "cegqi-min-bounds"
1630   type       = "bool"
1631   default    = "false"
1632   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1633
1634 [[option]]
1635   name       = "cegqiRoundUpLowerLia"
1636   category   = "regular"
1637   long       = "cegqi-round-up-lia"
1638   type       = "bool"
1639   default    = "false"
1640   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1641
1642 [[option]]
1643   name       = "cegqiMidpoint"
1644   category   = "regular"
1645   long       = "cegqi-midpoint"
1646   type       = "bool"
1647   default    = "false"
1648   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1649
1650 [[option]]
1651   name       = "cegqiNopt"
1652   category   = "regular"
1653   long       = "cegqi-nopt"
1654   type       = "bool"
1655   default    = "true"
1656   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1657
1658 # CEGQI for BV
1659
1660 [[option]]
1661   name       = "cegqiBv"
1662   category   = "regular"
1663   long       = "cegqi-bv"
1664   type       = "bool"
1665   default    = "true"
1666   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1667
1668 [[option]]
1669   name       = "cegqiBvInterleaveValue"
1670   category   = "regular"
1671   long       = "cegqi-bv-interleave-value"
1672   type       = "bool"
1673   default    = "false"
1674   help       = "interleave model value instantiation with word-level inversion approach"
1675
1676 [[option]]
1677   name       = "cegqiBvIneqMode"
1678   category   = "regular"
1679   long       = "cegqi-bv-ineq=MODE"
1680   type       = "CegqiBvIneqMode"
1681   default    = "EQ_BOUNDARY"
1682   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1683   help_mode  = "Modes for handling bit-vector inequalities in counterexample-guided instantiation."
1684 [[option.mode.EQ_SLACK]]
1685   name = "eq-slack"
1686   help = "Solve for the inequality using the slack value in the model, e.g., t > s becomes t = s + ( t-s )^M."
1687 [[option.mode.EQ_BOUNDARY]]
1688   name = "eq-boundary"
1689   help = "Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1."
1690 [[option.mode.KEEP]]
1691   name = "keep"
1692   help = "Solve for the inequality directly using side conditions for invertibility."
1693
1694 [[option]]
1695   name       = "cegqiBvRmExtract"
1696   category   = "regular"
1697   long       = "cegqi-bv-rm-extract"
1698   type       = "bool"
1699   default    = "true"
1700   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1701
1702 [[option]]
1703   name       = "cegqiBvLinearize"
1704   category   = "regular"
1705   long       = "cegqi-bv-linear"
1706   type       = "bool"
1707   default    = "true"
1708   help       = "linearize adder chains for variables"
1709
1710 [[option]]
1711   name       = "cegqiBvSolveNl"
1712   category   = "regular"
1713   long       = "cegqi-bv-solve-nl"
1714   type       = "bool"
1715   default    = "false"
1716   help       = "try to solve non-linear bv literals using model value projections"
1717
1718 [[option]]
1719   name       = "cegqiBvConcInv"
1720   category   = "regular"
1721   long       = "cegqi-bv-concat-inv"
1722   type       = "bool"
1723   default    = "true"
1724   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1725
1726 ### Reduction options
1727
1728 [[option]]
1729   name       = "quantAlphaEquiv"
1730   category   = "regular"
1731   long       = "quant-alpha-equiv"
1732   type       = "bool"
1733   default    = "true"
1734   help       = "infer alpha equivalence between quantified formulas"
1735
1736 [[option]]
1737   name       = "macrosQuant"
1738   category   = "regular"
1739   long       = "macros-quant"
1740   type       = "bool"
1741   default    = "false"
1742   help       = "perform quantifiers macro expansion"
1743
1744 [[option]]
1745   name       = "macrosQuantMode"
1746   category   = "regular"
1747   long       = "macros-quant-mode=MODE"
1748   type       = "MacrosQuantMode"
1749   default    = "GROUND_UF"
1750   help       = "mode for quantifiers macro expansion"
1751   help_mode  = "Modes for quantifiers macro expansion."
1752 [[option.mode.ALL]]
1753   name = "all"
1754   help = "Infer definitions for functions, including those containing quantified formulas."
1755 [[option.mode.GROUND]]
1756   name = "ground"
1757   help = "Only infer ground definitions for functions."
1758 [[option.mode.GROUND_UF]]
1759   name = "ground-uf"
1760   help = "Only infer ground definitions for functions that result in triggers for all free variables."
1761
1762 [[option]]
1763   name       = "quantDynamicSplit"
1764   category   = "regular"
1765   long       = "quant-dsplit-mode=MODE"
1766   type       = "QuantDSplitMode"
1767   default    = "DEFAULT"
1768   help       = "mode for dynamic quantifiers splitting"
1769   help_mode  = "Modes for quantifiers splitting."
1770 [[option.mode.NONE]]
1771   name = "none"
1772   help = "Never split quantified formulas."
1773 [[option.mode.DEFAULT]]
1774   name = "default"
1775   help = "Split quantified formulas over some finite datatypes when finite model finding is enabled."
1776 [[option.mode.AGG]]
1777   name = "agg"
1778   help = "Aggressively split quantified formulas."
1779
1780 ### Higher-order options
1781
1782 [[option]]
1783   name       = "hoMatching"
1784   category   = "regular"
1785   long       = "ho-matching"
1786   type       = "bool"
1787   default    = "true"
1788   help       = "do higher-order matching algorithm for triggers with variable operators"
1789
1790 [[option]]
1791   name       = "hoMatchingVarArgPriority"
1792   category   = "regular"
1793   long       = "ho-matching-var-priority"
1794   type       = "bool"
1795   default    = "true"
1796   help       = "give priority to variable arguments over constant arguments"
1797
1798 [[option]]
1799   name       = "hoMergeTermDb"
1800   category   = "regular"
1801   long       = "ho-merge-term-db"
1802   type       = "bool"
1803   default    = "true"
1804   help       = "merge term indices modulo equality"
1805
1806 [[option]]
1807   name       = "hoElim"
1808   category   = "regular"
1809   long       = "ho-elim"
1810   type       = "bool"
1811   default    = "false"
1812   help       = "eagerly eliminate higher-order constraints"
1813
1814 [[option]]
1815   name       = "hoElimStoreAx"
1816   category   = "regular"
1817   long       = "ho-elim-store-ax"
1818   type       = "bool"
1819   default    = "true"
1820   help       = "use store axiom during ho-elim"
1821
1822 ### Output options
1823
1824 [[option]]
1825   name       = "debugInst"
1826   category   = "regular"
1827   long       = "debug-inst"
1828   type       = "bool"
1829   default    = "false"
1830   help       = "print instantiations during solving (for debugging)"
1831
1832 ### SyGuS instantiation options
1833
1834 [[option]]
1835   name       = "sygusInst"
1836   category   = "regular"
1837   long       = "sygus-inst"
1838   type       = "bool"
1839   default    = "false"
1840   help       = "Enable SyGuS instantiation quantifiers module"
1841
1842 [[option]]
1843   name       = "sygusInstScope"
1844   category   = "regular"
1845   long       = "sygus-inst-scope=MODE"
1846   type       = "SygusInstScope"
1847   default    = "IN"
1848   help       = "select scope of ground terms"
1849   help_mode  = "scope for collecting ground terms for the grammar."
1850 [[option.mode.IN]]
1851   name = "in"
1852   help = "use ground terms inside given quantified formula only."
1853 [[option.mode.OUT]]
1854   name = "out"
1855   help = "use ground terms outside of quantified formulas only."
1856 [[option.mode.BOTH]]
1857   name = "both"
1858   help = "combines inside and outside."
1859
1860 [[option]]
1861   name       = "sygusInstTermSel"
1862   category   = "regular"
1863   long       = "sygus-inst-term-sel=MODE"
1864   type       = "SygusInstTermSelMode"
1865   default    = "MIN"
1866   help       = "granularity for ground terms"
1867   help_mode  = "Ground term selection modes."
1868 [[option.mode.MIN]]
1869   name = "min"
1870   help = "collect minimal ground terms only."
1871 [[option.mode.MAX]]
1872   name = "max"
1873   help = "collect maximal ground terms only."
1874 [[option.mode.BOTH]]
1875   name = "both"
1876   help = "combines minimal and maximal ."
1877
1878 [[option]]
1879   name       = "sygusInstMode"
1880   category   = "regular"
1881   long       = "sygus-inst-mode=MODE"
1882   type       = "SygusInstMode"
1883   default    = "PRIORITY_INST"
1884   help       = "select instantiation lemma mode"
1885   help_mode  = "SyGuS instantiation lemma modes."
1886 [[option.mode.PRIORITY_INST]]
1887   name = "priority-inst"
1888   help = "add instantiation lemmas first, add evaluation unfolding if instantiation fails."
1889 [[option.mode.PRIORITY_EVAL]]
1890   name = "priority-eval"
1891   help = "add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added."
1892 [[option.mode.INTERLEAVE]]
1893   name = "interleave"
1894   help = "add instantiation and evaluation unfolding lemmas in the same step."