# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

# Further options for Bitwuzla in addition to the default options. Format: 
# "option_name=value" with ’,’ to separate options. Option names and values
# can be found in the Bitwuzla documentation online:
# https://bitwuzla.github.io/docs/cpp/enums/option.html#_CPPv4N8bitwuzla6OptionE
# Example: "PRODUCE_MODELS=2,SAT_SOLVER=kissat".
solver.bitwuzla.furtherOptions = ""

# The SAT solver used by Bitwuzla.
solver.bitwuzla.satSolver = CADICAL
  enum:     [LINGELING, CMS, CADICAL, KISSAT]

# Further options for Boolector in addition to the default options. Format: 
# "Optionname=value" with ’,’ to separate options. Option names and values
# can be found in BtorOption or Boolector C Api. Example:
# "BTOR_OPT_MODEL_GEN=2,BTOR_OPT_INCREMENTAL=1".
solver.boolector.furtherOptions = ""

# The SAT solver used by Boolector.
solver.boolector.satSolver = CADICAL
  enum:     [LINGELING, PICOSAT, MINISAT, CMS, CADICAL]

# Counts all operations and interactions towards the SMT solver.
solver.collectStatistics = false

# Further options that will be passed to CVC5 in addition to the default
# options. Format is 'key1=value1,key2=value2'
solver.cvc5.furtherOptions = ""

# apply additional validation checks for interpolation results
solver.cvc5.validateInterpolants = false

# Enable assertions that make sure that functions are only used in the
# context that declared them.
solver.debugMode.noSharedDeclarations = false

# Enable assertions that make sure formula terms are only used in the context
# that created them.
solver.debugMode.noSharedFormulas = false

# Enable assertions that make sure that solver instances are only used on the
# thread that created them.
solver.debugMode.threadLocal = false

# Default rounding mode for floating point operations.
solver.floatingPointRoundingMode = NEAREST_TIES_TO_EVEN
  enum:     [NEAREST_TIES_TO_EVEN, NEAREST_TIES_AWAY, TOWARD_POSITIVE, TOWARD_NEGATIVE,
             TOWARD_ZERO]

# Export solver queries in SmtLib format into a file.
solver.logAllQueries = false
solver.logfile = no default value

# If used together with solver.mathsat5.useExtendedSMTLIB2Output, SMTLIB2
# output will contain let-bindings instead of define-fun based bindings.
solver.mathsat5.dumpSMTLIB2LetExpressions = false

# Further options that will be passed to Mathsat in addition to the default
# options. Format is 'key1=value1,key2=value2'
solver.mathsat5.furtherOptions = ""

# Load less stable optimizing version of mathsat5 solver.
solver.mathsat5.loadOptimathsat5 = false

# If enabled, SMTLIB2 output of MathSAT5 will be generated using the extended
# dumping function msat_to_smtlib2_ext(), instead of the regular dumping
# function msat_to_smtlib2(). This extended dump might allow the exporting of
# features to SMTLIB2 that can't be solved using MathSAT5, e.g. quantified
# formulas. The output will contain define-fun based bindings instead of
# let-expressions per default. If you want to use let bindings, enable option
# solver.mathsat5.dumpSMTLIB2LetExpressions as well.
solver.mathsat5.useExtendedSMTLIB2Output = false

# Use non-linear arithmetic of the solver if supported and throw exception
# otherwise, approximate non-linear arithmetic with UFs if unsupported, or
# always approximate non-linear arithmetic. This affects only the theories of
# integer and rational arithmetic.
solver.nonLinearArithmetic = USE
  enum:     [USE, APPROXIMATE_FALLBACK, APPROXIMATE_ALWAYS]

# deprecated name for solver.opensmt.interpolation.algorithm.booleanTheory
solver.opensmt.algBool = MCMILLAN
  enum:     [MCMILLAN, PUDLAK, MCMILLAN_PRIME, PROOF_SENSITIVE, PROOF_SENSITIVE_WEAK,
             PROOF_SENSITIVE_STRONG]

# deprecated name for solver.opensmt.interpolation.algorithm.lraTheory
solver.opensmt.algLra = STRONG
  enum:     [STRONG, WEAK, FACTOR, DECOMPOSING_STRONG, DECOMPOSING_WEAK]

# deprecated name for solver.opensmt.interpolation.algorithm.ufTheory
solver.opensmt.algUf = STRONG
  enum:     [STRONG, WEAK, RANDOM]

# Interpolation algorithm for boolean theory
solver.opensmt.interpolation.algorithm.booleanTheory = MCMILLAN
  enum:     [MCMILLAN, PUDLAK, MCMILLAN_PRIME, PROOF_SENSITIVE, PROOF_SENSITIVE_WEAK,
             PROOF_SENSITIVE_STRONG]

# Interpolation algorithm for LRA theory
solver.opensmt.interpolation.algorithm.lraTheory = STRONG
  enum:     [STRONG, WEAK, FACTOR, DECOMPOSING_STRONG, DECOMPOSING_WEAK]

# Interpolation algorithm for UF theory
solver.opensmt.interpolation.algorithm.ufTheory = STRONG
  enum:     [STRONG, WEAK, RANDOM]

# Level of simplification for interpolants,ranging from 0 (no simplification)
# to 4 (maximum simplification).
solver.opensmt.interpolation.simplificationLevel = 0

# SMT-LIB2 name of the logic to be used by the solver.
solver.opensmt.logic = QF_AUFLIRA
  enum:     [CORE, QF_AX, QF_UF, QF_IDL, QF_RDL, QF_LIA, QF_LRA, QF_ALIA, QF_ALRA,
             QF_UFLIA, QF_UFLRA, QF_AUFLIA, QF_AUFLRA, QF_AUFLIRA]

# deprecated name for solver.opensmt.interpolation.simplificationLevel
solver.opensmt.simplifyInterpolants = 0

# Enable additional assertion checks within Princess. The main usage is
# debugging. This option can cause a performance overhead.
solver.princess.enableAssertions = false

# log all queries as Princess-specific Scala code
solver.princess.logAllQueriesAsScala = false

# file for Princess-specific dump of queries as Scala code
solver.princess.logAllQueriesAsScalaFile = "princess-query-%03d-"

# The number of atoms a term has to have before it gets abbreviated if there
# are more identical terms.
solver.princess.minAtomsForAbbreviation = 100

# Random seed for SMT solver.
solver.randomSeed = 42

# If logging from the same application, avoid conflicting logfile names.
solver.renameLogfileToAvoidConflicts = true

# Double check generated results like interpolants and models whether they
# are correct
solver.smtinterpol.checkResults = false

# Further options that will be set to true for SMTInterpol in addition to the
# default options. Format is 'option1,option2,option3'
solver.smtinterpol.furtherOptions = []

# Which SMT solver to use.
solver.solver = SMTINTERPOL
  enum:     [OPENSMT, MATHSAT5, SMTINTERPOL, Z3, Z3_WITH_INTERPOLATION, PRINCESS,
             BOOLECTOR, CVC4, CVC5, YICES2, BITWUZLA]

# Sequentialize all solver actions to allow concurrent access!
solver.synchronize = false

# Use provers from a seperate context to solve queries. This allows more
# parallelity when solving larger queries.
solver.synchronized.useSeperateProvers = false

# Apply additional checks to catch common user errors.
solver.useDebugMode = false

# Log solver actions, this may be slow!
solver.useLogger = false

# Activate replayable logging in Z3. The log can be given as an input to the
# solver and replayed.
solver.z3.legacy.log = no default value

# Require proofs from SMT solver
solver.z3.legacy.requireProofs = true
  allowed values: [true, false]

# Activate replayable logging in Z3. The log can be given as an input to the
# solver and replayed.
solver.z3.log = no default value

# Ordering for objectives in the optimization context
solver.z3.objectivePrioritizationMode = "box"
  allowed values: [lex, pareto, box]

# Engine to use for the optimization
solver.z3.optimizationEngine = "basic"
  allowed values: [basic, farkas, symba]

# Require proofs from SMT solver
solver.z3.requireProofs = false

# Whether to use PhantomReferences for discarding Z3 AST
solver.z3.usePhantomReferences = false
