Deploy to GitHub Pages

Author: 🤖 SoSy-Bot 🤖

ConfigurationOptions.txt

@@ -0,0 +1,158 @@
+# 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
+
+# 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 = MCMILLAN
+  enum:     [MCMILLAN, PUDLAK, MCMILLAN_PRIME, PROOF_SENSITIVE, PROOF_SENSITIVE_WEAK,
+             PROOF_SENSITIVE_STRONG]
+
+# Algorithm for LRA interpolation
+solver.opensmt.algLra = STRONG
+  enum:     [STRONG, WEAK, FACTOR, DECOMPOSING_STRONG, DECOMPOSING_WEAK]
+
+# Algorithm for UF interpolation
+solver.opensmt.algUf = STRONG
+  enum:     [STRONG, WEAK, RANDOM]
+
+# 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]
+
+# Level of simplification for interpolants,ranging from 0 (no simplification)
+# to 4 (maximum simplification).
+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, 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