# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
# SPDX-FileCopyrightText: 2022 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-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#_CPPv4N8bitwuzla6OptionEExample:
# "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 seperate options. Optionname and value 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

# apply additional validation checks for interpolation results
solver.cvc5.validateInterpolants = 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

# 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

# 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]

# Algorithm for boolean interpolation
solver.opensmt.algBool = 0

# Algorithm for LRA interpolation
solver.opensmt.algLra = 0

# Algorithm for UF interpolation
solver.opensmt.algUf = 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]

# 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, 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

# 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.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