id     = "SMT"
name   = "SMT layer"
header = "options/smt_options.h"

[[option]]
  name       = "dumpModeString"
  smt_name   = "dump"
  category   = "common"
  long       = "dump=MODE"
  type       = "std::string"
  notifies   = ["notifyDumpMode"]
  read_only  = true
  help       = "dump preprocessed assertions, etc., see --dump=help"

[[option]]
  name       = "dumpToFileName"
  smt_name   = "dump-to"
  category   = "common"
  long       = "dump-to=FILE"
  type       = "std::string"
  notifies   = ["notifyDumpToFile"]
  read_only  = true
  help       = "all dumping goes to FILE (instead of stdout)"

[[option]]
  name       = "ackermann"
  category   = "regular"
  long       = "ackermann"
  type       = "bool"
  default    = "false"
  help       = "eliminate functions by ackermannization"

[[option]]
  name       = "simplificationMode"
  smt_name   = "simplification-mode"
  category   = "regular"
  long       = "simplification=MODE"
  type       = "SimplificationMode"
  default    = "BATCH"
  help       = "choose simplification mode, see --simplification=help"
  help_mode  = "Simplification modes."
[[option.mode.NONE]]
  name = "none"
  help = "Do not perform nonclausal simplification."
[[option.mode.BATCH]]
  name = "batch"
  help = "Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration)."

[[option]]
  name       = "doStaticLearning"
  category   = "regular"
  long       = "static-learning"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "use static learning (on by default)"

[[option]]
  name       = "expandDefinitions"
  smt_name   = "expand-definitions"
  category   = "regular"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "always expand symbol definitions in output"

[[option]]
  name       = "produceModels"
  category   = "common"
  short      = "m"
  long       = "produce-models"
  type       = "bool"
  default    = "false"
  notifies   = ["notifyBeforeSearch"]
  help       = "support the get-value and get-model commands"

[[option]]
  name       = "checkModels"
  category   = "regular"
  long       = "check-models"
  type       = "bool"
  notifies   = ["notifyBeforeSearch"]
  help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"

[[option]]
  name       = "debugCheckModels"
  category   = "regular"
  long       = "debug-check-models"
  type       = "bool"
  notifies   = ["notifyBeforeSearch"]
  help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"

[[option]]
  name       = "dumpModels"
  category   = "regular"
  long       = "dump-models"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "output models after every SAT/INVALID/UNKNOWN response"

[[option]]
  name       = "modelCoresMode"
  category   = "regular"
  long       = "model-cores=MODE"
  type       = "ModelCoresMode"
  default    = "NONE"
  help       = "mode for producing model cores"
  help_mode  = "Model cores modes."
[[option.mode.NONE]]
  name = "none"
  help = "Do not compute model cores."
[[option.mode.SIMPLE]]
  name = "simple"
  help = "Only include a subset of variables whose values are sufficient to show the input formula is satisfied by the given model."
[[option.mode.NON_IMPLIED]]
  name = "non-implied"
  help = "Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model."

[[option]]
  name       = "blockModelsMode"
  category   = "regular"
  long       = "block-models=MODE"
  type       = "BlockModelsMode"
  default    = "NONE"
  help       = "mode for producing several models"
  help_mode  = "Blocking models modes."
[[option.mode.NONE]]
  name = "none"
  help = "Do not block models."
[[option.mode.LITERALS]]
  name = "literals"
  help = "Block models based on the SAT skeleton."
[[option.mode.VALUES]]
  name = "values"
  help = "Block models based on the concrete model values for the free variables."

[[option]]
  name       = "proof"
  smt_name   = "produce-proofs"
  category   = "regular"
  long       = "proof"
  type       = "bool"
  default    = "false"
  predicates = ["proofEnabledBuild"]
  notifies   = ["notifyBeforeSearch"]
  help       = "turn on proof generation"

[[option]]
  name       = "checkProofs"
  category   = "regular"
  long       = "check-proofs"
  type       = "bool"
  predicates = ["LFSCEnabledBuild"]
  notifies   = ["notifyBeforeSearch"]
  help       = "after UNSAT/VALID, machine-check the generated proof"

[[option]]
  name       = "dumpProofs"
  category   = "regular"
  long       = "dump-proofs"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "output proofs after every UNSAT/VALID response"

[[option]]
  name       = "proofNew"
  category   = "regular"
  long       = "proof-new"
  type       = "bool"
  default    = "false"
  help       = "do proof production using the new infrastructure"

[[option]]
  name       = "proofNewPedantic"
  category   = "regular"
  long       = "proof-new-pedantic"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "assertion failure for any incorrect rule application or untrusted lemma for fully supported portions with proof-new"

[[option]]
  name       = "dumpInstantiations"
  category   = "regular"
  long       = "dump-instantiations"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "output instantiations of quantified formulas after every UNSAT/VALID response"

[[option]]
  name       = "sygusOut"
  category   = "regular"
  long       = "sygus-out=MODE"
  type       = "SygusSolutionOutMode"
  default    = "STATUS_AND_DEF"
  help       = "output mode for sygus"
  help_mode  = "Modes for sygus solution output."
[[option.mode.STATUS]]
  name = "status"
  help = "Print only status for check-synth calls."
[[option.mode.STATUS_AND_DEF]]
  name = "status-and-def"
  help = "Print status followed by definition corresponding to solution."
[[option.mode.STATUS_OR_DEF]]
  name = "status-or-def"
  help = "Print status if infeasible, or definition corresponding to solution if feasible."
[[option.mode.STANDARD]]
  name = "sygus-standard"
  help = "Print based on SyGuS standard."

[[option]]
  name       = "sygusPrintCallbacks"
  category   = "regular"
  long       = "sygus-print-callbacks"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)"

[[option]]
  name       = "dumpSynth"
  category   = "regular"
  long       = "dump-synth"
  type       = "bool"
  default    = "false"
  help       = "output solution for synthesis conjectures after every UNSAT/VALID response"

[[option]]
  name       = "unsatCores"
  category   = "regular"
  long       = "produce-unsat-cores"
  type       = "bool"
  predicates = ["proofEnabledBuild"]
  notifies   = ["notifyBeforeSearch"]
  help       = "turn on unsat core generation"

[[option]]
  name       = "checkUnsatCores"
  category   = "regular"
  long       = "check-unsat-cores"
  type       = "bool"
  help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"

[[option]]
  name       = "dumpUnsatCores"
  category   = "regular"
  long       = "dump-unsat-cores"
  type       = "bool"
  default    = "false"
  notifies   = ["notifyBeforeSearch"]
  help       = "output unsat cores after every UNSAT/VALID response"

[[option]]
  name       = "dumpUnsatCoresFull"
  category   = "regular"
  long       = "dump-unsat-cores-full"
  type       = "bool"
  default    = "false"
  notifies   = ["notifyBeforeSearch"]
  read_only  = true
  help       = "dump the full unsat core, including unlabeled assertions"

[[option]]
  name       = "unsatAssumptions"
  category   = "regular"
  long       = "produce-unsat-assumptions"
  type       = "bool"
  default    = "false"
  predicates = ["proofEnabledBuild"]
  notifies   = ["notifyBeforeSearch"]
  read_only  = true
  help       = "turn on unsat assumptions generation"

[[option]]
  name       = "checkSynthSol"
  category   = "regular"
  long       = "check-synth-sol"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "checks whether produced solutions to functions-to-synthesize satisfy the conjecture"

[[option]]
  name       = "produceAssignments"
  category   = "regular"
  long       = "produce-assignments"
  type       = "bool"
  default    = "false"
  notifies   = ["notifyBeforeSearch"]
  help       = "support the get-assignment command"

[[option]]
  name       = "interactiveMode"
  smt_name   = "interactive-mode"
  category   = "undocumented"
  type       = "bool"
  predicates = ["setProduceAssertions"]
  notifies   = ["notifyBeforeSearch"]
  help       = "deprecated name for produce-assertions"

[[option]]
  name       = "produceAssertions"
  category   = "common"
  long       = "produce-assertions"
  type       = "bool"
  predicates = ["setProduceAssertions"]
  notifies   = ["notifyBeforeSearch"]
  help       = "keep an assertions list (enables get-assertions command)"

[[option]]
  name       = "doITESimp"
  category   = "regular"
  long       = "ite-simp"
  type       = "bool"
  help       = "turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)"

[[option]]
  name       = "doITESimpOnRepeat"
  category   = "regular"
  long       = "on-repeat-ite-simp"
  type       = "bool"
  default    = "false"
  help       = "do the ite simplification pass again if repeating simplification"

[[option]]
  name       = "extRewPrep"
  category   = "regular"
  long       = "ext-rew-prep"
  type       = "bool"
  default    = "false"
  help       = "use extended rewriter as a preprocessing pass"

[[option]]
  name       = "extRewPrepAgg"
  category   = "regular"
  long       = "ext-rew-prep-agg"
  type       = "bool"
  default    = "false"
  help       = "use aggressive extended rewriter as a preprocessing pass"

[[option]]
  name       = "simplifyWithCareEnabled"
  category   = "regular"
  long       = "simp-with-care"
  type       = "bool"
  default    = "false"
  help       = "enables simplifyWithCare in ite simplificiation"

[[option]]
  name       = "compressItes"
  category   = "regular"
  long       = "simp-ite-compress"
  type       = "bool"
  default    = "false"
  help       = "enables compressing ites after ite simplification"

[[option]]
  name       = "unconstrainedSimp"
  category   = "regular"
  long       = "unconstrained-simp"
  type       = "bool"
  default    = "false"
  help       = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV."

[[option]]
  name       = "repeatSimp"
  category   = "regular"
  long       = "repeat-simp"
  type       = "bool"
  help       = "make multiple passes with nonclausal simplifier"

[[option]]
  name       = "zombieHuntThreshold"
  category   = "regular"
  long       = "simp-ite-hunt-zombies=N"
  type       = "uint32_t"
  default    = "524288"
  read_only  = true
  help       = "post ite compression enables zombie removal while the number of nodes is above this threshold"

[[option]]
  name       = "sortInference"
  category   = "regular"
  long       = "sort-inference"
  type       = "bool"
  default    = "false"
  help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
  
[[option]]
  name       = "incrementalSolving"
  category   = "common"
  short      = "i"
  long       = "incremental"
  type       = "bool"
  default    = "true"
  read_only  = true
  help       = "enable incremental solving"

[[option]]
  name       = "abstractValues"
  category   = "regular"
  long       = "abstract-values"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard"

[[option]]
  name       = "modelUninterpDtEnum"
  category   = "regular"
  long       = "model-u-dt-enum"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "in models, output uninterpreted sorts as datatype enumerations"

[[option]]
  name       = "modelWitnessValue"
  category   = "regular"
  long       = "model-witness-value"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "in models, use a witness constant for choice functions"

[[option]]
  name       = "regularChannelName"
  smt_name   = "regular-output-channel"
  category   = "regular"
  type       = "std::string"
  notifies   = ["notifySetRegularOutputChannel"]
  read_only  = true
  help       = "set the regular output channel of the solver"

[[option]]
  name       = "diagnosticChannelName"
  smt_name   = "diagnostic-output-channel"
  category   = "regular"
  type       = "std::string"
  notifies   = ["notifySetDiagnosticOutputChannel"]
  read_only  = true
  help       = "set the diagnostic output channel of the solver"

[[option]]
  name       = "cumulativeMillisecondLimit"
  smt_name   = "tlimit"
  category   = "common"
  long       = "tlimit=MS"
  type       = "unsigned long"
  handler    = "limitHandler"
  notifies   = ["notifyTlimit"]
  read_only  = true
  help       = "enable time limiting (give milliseconds)"

[[option]]
  name       = "perCallMillisecondLimit"
  smt_name   = "tlimit-per"
  category   = "common"
  long       = "tlimit-per=MS"
  type       = "unsigned long"
  handler    = "limitHandler"
  notifies   = ["notifyTlimitPer"]
  read_only  = true
  help       = "enable time limiting per query (give milliseconds)"

[[option]]
  name       = "cumulativeResourceLimit"
  smt_name   = "rlimit"
  category   = "common"
  long       = "rlimit=N"
  type       = "unsigned long"
  handler    = "limitHandler"
  notifies   = ["notifyRlimit"]
  read_only  = true
  help       = "enable resource limiting (currently, roughly the number of SAT conflicts)"

[[option]]
  name       = "perCallResourceLimit"
  smt_name   = "reproducible-resource-limit"
  category   = "common"
  long       = "rlimit-per=N"
  type       = "unsigned long"
  handler    = "limitHandler"
  notifies   = ["notifyRlimitPer"]
  read_only  = true
  help       = "enable resource limiting per query"

[[option]]
  name       = "hardLimit"
  category   = "common"
  long       = "hard-limit"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)"

[[option]]
  name       = "cpuTime"
  category   = "common"
  long       = "cpu-time"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "measures CPU time if set to true and wall time if false (default false)"

[[option]]
  name       = "rewriteStep"
  category   = "expert"
  long       = "rewrite-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each rewrite step"

[[option]]
  name       = "theoryCheckStep"
  category   = "expert"
  long       = "theory-check-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each theory check call"

[[option]]
  name       = "decisionStep"
  category   = "expert"
  long       = "decision-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of getNext decision calls in the decision engine"

[[option]]
  name       = "bitblastStep"
  category   = "expert"
  long       = "bitblast-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each bitblast step"

[[option]]
  name       = "bvPropagationStep"
  category   = "expert"
  long       = "bv-propagation-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each BV propagation step"

[[option]]
  name       = "bvEagerAssertStep"
  category   = "expert"
  long       = "bv-eager-assert-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each eager BV assert step"

[[option]]
  name       = "parseStep"
  category   = "expert"
  long       = "parse-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each command/expression parsing"

[[option]]
  name       = "lemmaStep"
  category   = "expert"
  long       = "lemma-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent when adding lemmas"

[[option]]
  name       = "restartStep"
  category   = "expert"
  long       = "restart-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each theory restart"

[[option]]
  name       = "cnfStep"
  category   = "expert"
  long       = "cnf-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each call to cnf conversion"

[[option]]
  name       = "preprocessStep"
  category   = "expert"
  long       = "preprocess-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each preprocessing step in SmtEngine"

[[option]]
  name       = "quantifierStep"
  category   = "expert"
  long       = "quantifier-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for quantifier instantiations"

[[option]]
  name       = "satConflictStep"
  category   = "expert"
  long       = "sat-conflict-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each sat conflict (main sat solver)"

[[option]]
  name       = "bvSatConflictStep"
  category   = "expert"
  long       = "bv-sat-conflict-step=N"
  type       = "unsigned"
  default    = "1"
  read_only  = true
  help       = "amount of resources spent for each sat conflict (bitvectors)"

[[option]]
  name       = "forceNoLimitCpuWhileDump"
  category   = "regular"
  long       = "force-no-limit-cpu-while-dump"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "Force no CPU limit when dumping models and proofs"

[[option]]
  name       = "solveBVAsInt"
  category   = "undocumented"
  long       = "solve-bv-as-int=N"
  type       = "uint32_t"
  default    = "0"
  read_only  = true
  help       = "attempt to solve BV formulas by translation to integer arithmetic (experimental)"

[[option]]
  name       = "iandMode"
  category   = "undocumented"
  long       = "iand-mode=mode"
  type       = "IandMode"
  default    = "VALUE"
  read_only  = true
  help       = "Set the refinement scheme for integer AND"
  help_mode  = "Refinement modes for integer AND"
  [[option.mode.VALUE]]
  name = "value"
  help = "value-based refinement"
  [[option.mode.SUM]]
  name = "sum"
  help = "use sum to represent integer AND in refinement"
  [[option.mode.BITWISE]]
  name = "bitwise"
  help = "use bitwise comparisons on binary representation of integer for refinement (experimental)"
  
[[option]]
  name       = "solveIntAsBV"
  category   = "undocumented"
  long       = "solve-int-as-bv=N"
  type       = "uint32_t"
  default    = "0"
  read_only  = true
  help       = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)"

[[option]]
  name       = "solveRealAsInt"
  category   = "undocumented"
  long       = "solve-real-as-int"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"

[[option]]
  name       = "produceInterpols"
  category   = "undocumented"
  long       = "produce-interpols=MODE"
  type       = "ProduceInterpols"
  default    = "NONE"
  read_only  = true
  help       = "support the get-interpol command"
  help_mode  = "Interpolants grammar mode"
[[option.mode.NONE]]
  name = "none"
  help = "don't compute interpolants"
[[option.mode.DEFAULT]]
  name = "default"
  help = "use the default grammar for the theory or the user-defined grammar if given"
[[option.mode.ASSUMPTIONS]]
  name = "assumptions"
  help = "use only operators that occur in the assumptions"
[[option.mode.CONJECTURE]]
  name = "conjecture"
  help = "use only operators that occur in the conjecture"
[[option.mode.SHARED]]
  name = "shared"
  help = "use only operators that occur both in the assumptions and the conjecture"
[[option.mode.ALL]]
  name = "all"
  help = "use only operators that occur either in the assumptions or the conjecture"

[[option]]
  name       = "produceAbducts"
  category   = "undocumented"
  long       = "produce-abducts"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "support the get-abduct command"

[[option]]
  name       = "checkInterpols"
  category   = "regular"
  long       = "check-interpols"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "checks whether produced solutions to get-interpol are correct"

[[option]]
  name       = "checkAbducts"
  category   = "regular"
  long       = "check-abducts"
  type       = "bool"
  default    = "false"
  read_only  = true
  help       = "checks whether produced solutions to get-abduct are correct"