-
Notifications
You must be signed in to change notification settings - Fork 46
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit 19d9e43
Showing
219 changed files
with
118,579 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,146 @@ | ||
# 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 | ||
|
||
# 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 | ||
|
||
# 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 | ||
|
||
# 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.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 |
Oops, something went wrong.