src/options/smt_options.toml

   1 id     = "SMT"
   2 name   = "SMT layer"
   3 header = "options/smt_options.h"
   4
   5 [[option]]
   6   name       = "dumpModeString"
   7   smt_name   = "dump"
   8   category   = "common"
   9   long       = "dump=MODE"
  10   type       = "std::string"
  11   notifies   = ["notifyDumpMode"]
  12   read_only  = true
  13   help       = "dump preprocessed assertions, etc., see --dump=help"
  14
  15 [[option]]
  16   name       = "dumpToFileName"
  17   smt_name   = "dump-to"
  18   category   = "common"
  19   long       = "dump-to=FILE"
  20   type       = "std::string"
  21   notifies   = ["notifyDumpToFile"]
  22   read_only  = true
  23   help       = "all dumping goes to FILE (instead of stdout)"
  24
  25 [[option]]
  26   name       = "simplificationMode"
  27   smt_name   = "simplification-mode"
  28   category   = "regular"
  29   long       = "simplification=MODE"
  30   type       = "SimplificationMode"
  31   default    = "SIMPLIFICATION_MODE_BATCH"
  32   handler    = "stringToSimplificationMode"
  33   includes   = ["options/smt_modes.h"]
  34   help       = "choose simplification mode, see --simplification=help"
  35
  36 [[alias]]
  37   category   = "regular"
  38   long       = "no-simplification"
  39   links      = ["--simplification=none"]
  40   help       = "turn off all simplification (same as --simplification=none)"
  41
  42 [[option]]
  43   name       = "doStaticLearning"
  44   category   = "regular"
  45   long       = "static-learning"
  46   type       = "bool"
  47   default    = "true"
  48   read_only  = true
  49   help       = "use static learning (on by default)"
  50
  51 [[option]]
  52   name       = "expandDefinitions"
  53   smt_name   = "expand-definitions"
  54   category   = "regular"
  55   type       = "bool"
  56   default    = "false"
  57   read_only  = true
  58   help       = "always expand symbol definitions in output"
  59
  60 [[option]]
  61   name       = "produceModels"
  62   category   = "common"
  63   short      = "m"
  64   long       = "produce-models"
  65   type       = "bool"
  66   default    = "false"
  67   notifies   = ["notifyBeforeSearch"]
  68   read_only  = true
  69   help       = "support the get-value and get-model commands"
  70
  71 [[option]]
  72   name       = "checkModels"
  73   category   = "regular"
  74   long       = "check-models"
  75   type       = "bool"
  76   notifies   = ["notifyBeforeSearch"]
  77   links      = ["--produce-models", "--produce-assertions"]
  78   read_only  = true
  79   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
  80
  81 [[option]]
  82   name       = "dumpModels"
  83   category   = "regular"
  84   long       = "dump-models"
  85   type       = "bool"
  86   default    = "false"
  87   links      = ["--produce-models"]
  88   read_only  = true
  89   help       = "output models after every SAT/INVALID/UNKNOWN response"
  90
  91 [[option]]
  92   name       = "modelCoresMode"
  93   category   = "regular"
  94   long       = "model-cores=MODE"
  95   type       = "ModelCoresMode"
  96   default    = "MODEL_CORES_NONE"
  97   handler    = "stringToModelCoresMode"
  98   includes   = ["options/smt_modes.h"]
  99   help       = "mode for producing model cores"
 100
 101 [[option]]
 102   name       = "proof"
 103   smt_name   = "produce-proofs"
 104   category   = "regular"
 105   long       = "proof"
 106   type       = "bool"
 107   default    = "false"
 108   predicates = ["proofEnabledBuild"]
 109   notifies   = ["notifyBeforeSearch"]
 110   read_only  = true
 111   help       = "turn on proof generation"
 112
 113 [[option]]
 114   name       = "checkProofs"
 115   category   = "regular"
 116   long       = "check-proofs"
 117   type       = "bool"
 118   predicates = ["LFSCEnabledBuild"]
 119   notifies   = ["notifyBeforeSearch"]
 120   links      = ["--proof"]
 121   help       = "after UNSAT/VALID, machine-check the generated proof"
 122
 123 [[option]]
 124   name       = "dumpProofs"
 125   category   = "regular"
 126   long       = "dump-proofs"
 127   type       = "bool"
 128   default    = "false"
 129   links      = ["--proof"]
 130   read_only  = true
 131   help       = "output proofs after every UNSAT/VALID response"
 132
 133 [[option]]
 134   name       = "dumpInstantiations"
 135   category   = "regular"
 136   long       = "dump-instantiations"
 137   type       = "bool"
 138   default    = "false"
 139   read_only  = true
 140   help       = "output instantiations of quantified formulas after every UNSAT/VALID response"
 141
 142 [[option]]
 143   name       = "sygusOut"
 144   category   = "regular"
 145   long       = "sygus-out=MODE"
 146   type       = "SygusSolutionOutMode"
 147   default    = "SYGUS_SOL_OUT_STATUS_AND_DEF"
 148   handler    = "stringToSygusSolutionOutMode"
 149   includes   = ["options/sygus_out_mode.h"]
 150   help       = "output mode for sygus"
 151
 152 [[option]]
 153   name       = "sygusPrintCallbacks"
 154   category   = "regular"
 155   long       = "sygus-print-callbacks"
 156   type       = "bool"
 157   default    = "true"
 158   read_only  = true
 159   help       = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)"
 160
 161 [[option]]
 162   name       = "dumpSynth"
 163   category   = "regular"
 164   long       = "dump-synth"
 165   type       = "bool"
 166   default    = "false"
 167   help       = "output solution for synthesis conjectures after every UNSAT/VALID response"
 168
 169 [[option]]
 170   name       = "unsatCores"
 171   category   = "regular"
 172   long       = "produce-unsat-cores"
 173   type       = "bool"
 174   predicates = ["proofEnabledBuild"]
 175   notifies   = ["notifyBeforeSearch"]
 176   read_only  = true
 177   help       = "turn on unsat core generation"
 178
 179 [[option]]
 180   name       = "checkUnsatCores"
 181   category   = "regular"
 182   long       = "check-unsat-cores"
 183   type       = "bool"
 184   links      = ["--produce-unsat-cores"]
 185   help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
 186
 187 [[option]]
 188   name       = "dumpUnsatCores"
 189   category   = "regular"
 190   long       = "dump-unsat-cores"
 191   type       = "bool"
 192   default    = "false"
 193   notifies   = ["notifyBeforeSearch"]
 194   links      = ["--produce-unsat-cores"]
 195   read_only  = true
 196   help       = "output unsat cores after every UNSAT/VALID response"
 197
 198 [[option]]
 199   name       = "dumpUnsatCoresFull"
 200   category   = "regular"
 201   long       = "dump-unsat-cores-full"
 202   type       = "bool"
 203   default    = "false"
 204   notifies   = ["notifyBeforeSearch"]
 205   links      = ["--dump-unsat-cores"]
 206   read_only  = true
 207   help       = "dump the full unsat core, including unlabeled assertions"
 208
 209 [[option]]
 210   name       = "unsatAssumptions"
 211   category   = "regular"
 212   long       = "produce-unsat-assumptions"
 213   type       = "bool"
 214   default    = "false"
 215   links      = ["--produce-unsat-cores"]
 216   predicates = ["proofEnabledBuild"]
 217   notifies   = ["notifyBeforeSearch"]
 218   read_only  = true
 219   help       = "turn on unsat assumptions generation"
 220
 221 [[option]]
 222   name       = "checkSynthSol"
 223   category   = "regular"
 224   long       = "check-synth-sol"
 225   type       = "bool"
 226   default    = "false"
 227   read_only  = true
 228   help       = "checks whether produced solutions to functions-to-synthesize satisfy the conjecture"
 229
 230 [[option]]
 231   name       = "produceAssignments"
 232   category   = "regular"
 233   long       = "produce-assignments"
 234   type       = "bool"
 235   default    = "false"
 236   notifies   = ["notifyBeforeSearch"]
 237   read_only  = true
 238   help       = "support the get-assignment command"
 239
 240 [[option]]
 241   name       = "interactiveMode"
 242   smt_name   = "interactive-mode"
 243   category   = "undocumented"
 244   type       = "bool"
 245   predicates = ["setProduceAssertions"]
 246   notifies   = ["notifyBeforeSearch"]
 247   help       = "deprecated name for produce-assertions"
 248
 249 [[option]]
 250   name       = "produceAssertions"
 251   category   = "common"
 252   long       = "produce-assertions"
 253   type       = "bool"
 254   predicates = ["setProduceAssertions"]
 255   notifies   = ["notifyBeforeSearch"]
 256   help       = "keep an assertions list (enables get-assertions command)"
 257
 258 [[option]]
 259   name       = "doITESimp"
 260   category   = "regular"
 261   long       = "ite-simp"
 262   type       = "bool"
 263   help       = "turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)"
 264
 265 [[option]]
 266   name       = "doITESimpOnRepeat"
 267   category   = "regular"
 268   long       = "on-repeat-ite-simp"
 269   type       = "bool"
 270   default    = "false"
 271   help       = "do the ite simplification pass again if repeating simplification"
 272
 273 [[option]]
 274   name       = "extRewPrep"
 275   category   = "regular"
 276   long       = "ext-rew-prep"
 277   type       = "bool"
 278   default    = "false"
 279   help       = "use extended rewriter as a preprocessing pass"
 280
 281 [[option]]
 282   name       = "extRewPrepAgg"
 283   category   = "regular"
 284   long       = "ext-rew-prep-agg"
 285   type       = "bool"
 286   default    = "false"
 287   help       = "use aggressive extended rewriter as a preprocessing pass"
 288
 289 [[option]]
 290   name       = "simplifyWithCareEnabled"
 291   category   = "regular"
 292   long       = "simp-with-care"
 293   type       = "bool"
 294   default    = "false"
 295   help       = "enables simplifyWithCare in ite simplificiation"
 296
 297 [[option]]
 298   name       = "compressItes"
 299   category   = "regular"
 300   long       = "simp-ite-compress"
 301   type       = "bool"
 302   default    = "false"
 303   help       = "enables compressing ites after ite simplification"
 304
 305 [[option]]
 306   name       = "unconstrainedSimp"
 307   category   = "regular"
 308   long       = "unconstrained-simp"
 309   type       = "bool"
 310   default    = "false"
 311   help       = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)"
 312
 313 [[option]]
 314   name       = "repeatSimp"
 315   category   = "regular"
 316   long       = "repeat-simp"
 317   type       = "bool"
 318   help       = "make multiple passes with nonclausal simplifier"
 319
 320 [[option]]
 321   name       = "zombieHuntThreshold"
 322   category   = "regular"
 323   long       = "simp-ite-hunt-zombies=N"
 324   type       = "uint32_t"
 325   default    = "524288"
 326   read_only  = true
 327   help       = "post ite compression enables zombie removal while the number of nodes is above this threshold"
 328
 329 [[option]]
 330   name       = "sortInference"
 331   category   = "regular"
 332   long       = "sort-inference"
 333   type       = "bool"
 334   default    = "false"
 335   help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
 336
 337 [[option]]
 338   name       = "symmetryBreakerExp"
 339   category   = "regular"
 340   long       = "symmetry-breaker-exp"
 341   type       = "bool"
 342   default    = "false"
 343   help       = "generate symmetry breaking constraints after symmetry detection"
 344
 345 [[option]]
 346   name       = "incrementalSolving"
 347   category   = "common"
 348   short      = "i"
 349   long       = "incremental"
 350   type       = "bool"
 351   default    = "true"
 352   read_only  = true
 353   help       = "enable incremental solving"
 354
 355 [[option]]
 356   name       = "abstractValues"
 357   category   = "regular"
 358   long       = "abstract-values"
 359   type       = "bool"
 360   default    = "false"
 361   read_only  = true
 362   help       = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard"
 363
 364 [[option]]
 365   name       = "modelUninterpDtEnum"
 366   category   = "regular"
 367   long       = "model-u-dt-enum"
 368   type       = "bool"
 369   default    = "false"
 370   read_only  = true
 371   help       = "in models, output uninterpreted sorts as datatype enumerations"
 372
 373 [[option]]
 374   name       = "regularChannelName"
 375   smt_name   = "regular-output-channel"
 376   category   = "regular"
 377   type       = "std::string"
 378   notifies   = ["notifySetRegularOutputChannel"]
 379   read_only  = true
 380   help       = "set the regular output channel of the solver"
 381
 382 [[option]]
 383   name       = "diagnosticChannelName"
 384   smt_name   = "diagnostic-output-channel"
 385   category   = "regular"
 386   type       = "std::string"
 387   notifies   = ["notifySetDiagnosticOutputChannel"]
 388   read_only  = true
 389   help       = "set the diagnostic output channel of the solver"
 390
 391 [[option]]
 392   name       = "cumulativeMillisecondLimit"
 393   smt_name   = "tlimit"
 394   category   = "common"
 395   long       = "tlimit=MS"
 396   type       = "unsigned long"
 397   handler    = "limitHandler"
 398   notifies   = ["notifyTlimit"]
 399   read_only  = true
 400   help       = "enable time limiting (give milliseconds)"
 401
 402 [[option]]
 403   name       = "perCallMillisecondLimit"
 404   smt_name   = "tlimit-per"
 405   category   = "common"
 406   long       = "tlimit-per=MS"
 407   type       = "unsigned long"
 408   handler    = "limitHandler"
 409   notifies   = ["notifyTlimitPer"]
 410   read_only  = true
 411   help       = "enable time limiting per query (give milliseconds)"
 412
 413 [[option]]
 414   name       = "cumulativeResourceLimit"
 415   smt_name   = "rlimit"
 416   category   = "common"
 417   long       = "rlimit=N"
 418   type       = "unsigned long"
 419   handler    = "limitHandler"
 420   notifies   = ["notifyRlimit"]
 421   read_only  = true
 422   help       = "enable resource limiting (currently, roughly the number of SAT conflicts)"
 423
 424 [[option]]
 425   name       = "perCallResourceLimit"
 426   smt_name   = "reproducible-resource-limit"
 427   category   = "common"
 428   long       = "rlimit-per=N"
 429   type       = "unsigned long"
 430   handler    = "limitHandler"
 431   notifies   = ["notifyRlimitPer"]
 432   read_only  = true
 433   help       = "enable resource limiting per query"
 434
 435 [[option]]
 436   name       = "hardLimit"
 437   category   = "common"
 438   long       = "hard-limit"
 439   type       = "bool"
 440   default    = "false"
 441   read_only  = true
 442   help       = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)"
 443
 444 [[option]]
 445   name       = "cpuTime"
 446   category   = "common"
 447   long       = "cpu-time"
 448   type       = "bool"
 449   default    = "false"
 450   read_only  = true
 451   help       = "measures CPU time if set to true and wall time if false (default false)"
 452
 453 [[option]]
 454   name       = "rewriteStep"
 455   category   = "expert"
 456   long       = "rewrite-step=N"
 457   type       = "unsigned"
 458   default    = "1"
 459   read_only  = true
 460   help       = "amount of resources spent for each rewrite step"
 461
 462 [[option]]
 463   name       = "theoryCheckStep"
 464   category   = "expert"
 465   long       = "theory-check-step=N"
 466   type       = "unsigned"
 467   default    = "1"
 468   read_only  = true
 469   help       = "amount of resources spent for each theory check call"
 470
 471 [[option]]
 472   name       = "decisionStep"
 473   category   = "expert"
 474   long       = "decision-step=N"
 475   type       = "unsigned"
 476   default    = "1"
 477   read_only  = true
 478   help       = "amount of getNext decision calls in the decision engine"
 479
 480 [[option]]
 481   name       = "bitblastStep"
 482   category   = "expert"
 483   long       = "bitblast-step=N"
 484   type       = "unsigned"
 485   default    = "1"
 486   read_only  = true
 487   help       = "amount of resources spent for each bitblast step"
 488
 489 [[option]]
 490   name       = "parseStep"
 491   category   = "expert"
 492   long       = "parse-step=N"
 493   type       = "unsigned"
 494   default    = "1"
 495   read_only  = true
 496   help       = "amount of resources spent for each command/expression parsing"
 497
 498 [[option]]
 499   name       = "lemmaStep"
 500   category   = "expert"
 501   long       = "lemma-step=N"
 502   type       = "unsigned"
 503   default    = "1"
 504   read_only  = true
 505   help       = "amount of resources spent when adding lemmas"
 506
 507 [[option]]
 508   name       = "restartStep"
 509   category   = "expert"
 510   long       = "restart-step=N"
 511   type       = "unsigned"
 512   default    = "1"
 513   read_only  = true
 514   help       = "amount of resources spent for each theory restart"
 515
 516 [[option]]
 517   name       = "cnfStep"
 518   category   = "expert"
 519   long       = "cnf-step=N"
 520   type       = "unsigned"
 521   default    = "1"
 522   read_only  = true
 523   help       = "amount of resources spent for each call to cnf conversion"
 524
 525 [[option]]
 526   name       = "preprocessStep"
 527   category   = "expert"
 528   long       = "preprocess-step=N"
 529   type       = "unsigned"
 530   default    = "1"
 531   read_only  = true
 532   help       = "amount of resources spent for each preprocessing step in SmtEngine"
 533
 534 [[option]]
 535   name       = "quantifierStep"
 536   category   = "expert"
 537   long       = "quantifier-step=N"
 538   type       = "unsigned"
 539   default    = "1"
 540   read_only  = true
 541   help       = "amount of resources spent for quantifier instantiations"
 542
 543 [[option]]
 544   name       = "satConflictStep"
 545   category   = "expert"
 546   long       = "sat-conflict-step=N"
 547   type       = "unsigned"
 548   default    = "1"
 549   read_only  = true
 550   help       = "amount of resources spent for each sat conflict (main sat solver)"
 551
 552 [[option]]
 553   name       = "bvSatConflictStep"
 554   category   = "expert"
 555   long       = "bv-sat-conflict-step=N"
 556   type       = "unsigned"
 557   default    = "1"
 558   read_only  = true
 559   help       = "amount of resources spent for each sat conflict (bitvectors)"
 560
 561 [[option]]
 562   name       = "rewriteApplyToConst"
 563   category   = "expert"
 564   long       = "rewrite-apply-to-const"
 565   type       = "bool"
 566   default    = "false"
 567   read_only  = true
 568   help       = "eliminate function applications, rewriting e.g. f(5) to a new symbol f_5"
 569
 570 # --replay is currently broken; don't document it for 1.0
 571 [[option]]
 572   name       = "replayInputFilename"
 573   category   = "undocumented"
 574   long       = "replay=FILE"
 575   type       = "std::string"
 576   handler    = "checkReplayFilename"
 577   read_only  = true
 578   help       = "replay decisions from file"
 579
 580 # --replay is currently broken; don't document it for 1.0
 581 [[option]]
 582   name       = "replayLogFilename"
 583   category   = "undocumented"
 584   long       = "replay-log=FILE"
 585   type       = "std::string"
 586   handler    = "checkReplayFilename"
 587   notifies   = ["notifySetReplayLogFilename", "notifyBeforeSearch"]
 588   read_only  = true
 589   help       = "replay decisions from file"
 590
 591 [[option]]
 592   name       = "forceNoLimitCpuWhileDump"
 593   category   = "regular"
 594   long       = "force-no-limit-cpu-while-dump"
 595   type       = "bool"
 596   default    = "false"
 597   read_only  = true
 598   help       = "Force no CPU limit when dumping models and proofs"
 599
 600 [[option]]
 601   name       = "solveIntAsBV"
 602   category   = "undocumented"
 603   long       = "solve-int-as-bv=N"
 604   type       = "uint32_t"
 605   default    = "0"
 606   read_only  = true
 607   help       = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)"
 608
 609 [[option]]
 610   name       = "solveRealAsInt"
 611   category   = "undocumented"
 612   long       = "solve-real-as-int"
 613   type       = "bool"
 614   default    = "false"
 615   read_only  = true
 616   help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
 617
 618 [[option]]
 619   name       = "produceAbducts"
 620   category   = "undocumented"
 621   long       = "produce-abducts"
 622   type       = "bool"
 623   default    = "false"
 624   read_only  = true
 625   help       = "support the get-abduct command"