id     = "SMT"
name   = "SMT Layer"

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

[[option]]
  name       = "dumpToFileName"
  category   = "common"
  long       = "dump-to=FILE"
  type       = "std::string"
  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"
  alias      = ["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"
  help       = "use static learning (on by default)"

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

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

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

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

[[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       = "produceProofs"
  category   = "regular"
  long       = "produce-proofs"
  type       = "bool"
  default    = "false"
  help       = "produce proofs, support check-proofs and get-proof"

[[option]]
  name       = "checkProofs"
  category   = "regular"
  long       = "check-proofs"
  type       = "bool"
  help       = "after UNSAT/VALID, check the generated proof (with proof)"

[[option]]
  name       = "sygusOut"
  category   = "regular"
  long       = "sygus-out=MODE"
  type       = "SygusSolutionOutMode"
  default    = "STANDARD"
  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"
  help       = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)"

[[option]]
  name       = "unsatCores"
  category   = "regular"
  long       = "produce-unsat-cores"
  type       = "bool"
  help       = "turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs."

[[option]]
  name       = "unsatCoresMode"
  category   = "regular"
  long       = "unsat-cores-mode=MODE"
  type       = "UnsatCoresMode"
  default    = "OFF"
  help       = "choose unsat core mode, see --unsat-cores-mode=help"
  help_mode  = "unsat cores modes."
[[option.mode.OFF]]
  name = "off"
  help = "Do not produce unsat cores."
[[option.mode.SAT_PROOF]]
  name = "sat-proof"
  help = "Produce unsat cores from SAT and preprocessing proofs."
[[option.mode.FULL_PROOF]]
  name = "full-proof"
  help = "Produce unsat cores from full proofs."
[[option.mode.ASSUMPTIONS]]
  name = "assumptions"
  help = "Produce unsat cores using solving under assumptions and preprocessing proofs."

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

[[option]]
  name       = "unsatAssumptions"
  category   = "regular"
  long       = "produce-unsat-assumptions"
  type       = "bool"
  default    = "false"
  help       = "turn on unsat assumptions generation"

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

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

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

[[option]]
  name       = "produceAssertions"
  category   = "common"
  long       = "produce-assertions"
  type       = "bool"
  predicates = ["setProduceAssertions"]
  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       = "earlyIteRemoval"
  category   = "experimental"
  long       = "early-ite-removal"
  type       = "bool"
  default    = "false"
  help       = "remove ITEs early in preprocessing"

[[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"
  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       = "abstractValues"
  category   = "regular"
  long       = "abstract-values"
  type       = "bool"
  default    = "false"
  help       = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard"

[[option]]
  name       = "modelUninterpPrint"
  alias      = ["model-uninterp-print"]
  category   = "regular"
  long       = "model-u-print=MODE"
  type       = "ModelUninterpPrintMode"
  default    = "None"
  help       = "determines how to print uninterpreted elements in models"
  help_mode  = "uninterpreted elements in models printing  modes."
[[option.mode.DtEnum]]
  name = "dtenum"
  help = "print uninterpreted elements as datatype enumerations, where the sort is the datatype"
[[option.mode.DeclSortAndFun]]
  name = "decl-sort-and-fun"
  help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort"
[[option.mode.DeclFun]]
  name = "decl-fun"
  help = "print uninterpreted elements declare-fun, but don't include a declare-sort for the sort"
[[option.mode.None]]
  name = "none"
  help = "(default) do not print declarations of uninterpreted elements in models."


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

[[option]]
  name       = "regularChannelName"
  long       = "regular-output-channel=CHANNEL"
  category   = "regular"
  type       = "std::string"
  help       = "set the regular output channel of the solver"

[[option]]
  name       = "diagnosticChannelName"
  long       = "diagnostic-output-channel=CHANNEL"
  category   = "regular"
  type       = "std::string"
  help       = "set the diagnostic output channel of the solver"

[[option]]
  name       = "foreignTheoryRewrite"
  category   = "regular"
  long       = "foreign-theory-rewrite"
  type       = "bool"
  default    = "false"
  help       = "Cross-theory rewrites"

[[option]]
  name       = "solveBVAsInt"
  category   = "undocumented"
  long       = "solve-bv-as-int=MODE"
  type       = "SolveBVAsIntMode"
  default    = "OFF"
  help       = "mode for translating BVAnd to integer"
  help_mode  = "solve-bv-as-int modes."
[[option.mode.OFF]]
  name = "off"
  help = "Do not translate bit-vectors to integers"
[[option.mode.SUM]]
  name = "sum"
  help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
[[option.mode.IAND]]
  name = "iand"
  help = "Translate bvand to the iand operator (experimental)"
[[option.mode.BV]]
  name = "bv"
  help = "Translate bvand back to bit-vectors"

[[option]]
  name       = "BVAndIntegerGranularity"
  category   = "undocumented"
  long       = "bvand-integer-granularity=N"
  type       = "uint32_t"
  default    = "1"
  help       = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)"

[[option]]
  name       = "iandMode"
  category   = "undocumented"
  long       = "iand-mode=mode"
  type       = "IandMode"
  default    = "VALUE"
  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"
  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"
  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"
  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"
  help       = "support the get-abduct command"

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

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