-
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 bded4ef
Showing
189 changed files
with
102,188 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,120 @@ | ||
# 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 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] | ||
|
||
# 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 |
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
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,241 @@ | ||
<!DOCTYPE HTML> | ||
<!-- NewPage --> | ||
<html lang="en"> | ||
<head> | ||
<!-- Generated by javadoc (11.0.19) on Mon Apr 15 08:17:09 UTC 2024 --> | ||
<title>All Packages (JavaSMT Solver Library)</title> | ||
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"> | ||
<meta name="dc.created" content="2024-04-15"> | ||
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="Style"> | ||
<link rel="stylesheet" type="text/css" href="jquery/jquery-ui.min.css" title="Style"> | ||
<link rel="stylesheet" type="text/css" href="jquery-ui.overrides.css" title="Style"> | ||
<script type="text/javascript" src="script.js"></script> | ||
<script type="text/javascript" src="jquery/jszip/dist/jszip.min.js"></script> | ||
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils.min.js"></script> | ||
<!--[if IE]> | ||
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils-ie.min.js"></script> | ||
<![endif]--> | ||
<script type="text/javascript" src="jquery/jquery-3.6.1.min.js"></script> | ||
<script type="text/javascript" src="jquery/jquery-ui.min.js"></script> | ||
</head> | ||
<body> | ||
<script type="text/javascript"><!-- | ||
try { | ||
if (location.href.indexOf('is-external=true') == -1) { | ||
parent.document.title="All Packages (JavaSMT Solver Library)"; | ||
} | ||
} | ||
catch(err) { | ||
} | ||
//--> | ||
var pathtoroot = "./"; | ||
var useModuleDirectories = true; | ||
loadScripts(document, 'script');</script> | ||
<noscript> | ||
<div>JavaScript is disabled on your browser.</div> | ||
</noscript> | ||
<header role="banner"> | ||
<nav role="navigation"> | ||
<div class="fixedNav"> | ||
<!-- ========= START OF TOP NAVBAR ======= --> | ||
<div class="topNav"><a id="navbar.top"> | ||
<!-- --> | ||
</a> | ||
<div class="skipNav"><a href="#skip.navbar.top" title="Skip navigation links">Skip navigation links</a></div> | ||
<a id="navbar.top.firstrow"> | ||
<!-- --> | ||
</a> | ||
<ul class="navList" title="Navigation"> | ||
<li><a href="index.html">Overview</a></li> | ||
<li>Package</li> | ||
<li>Class</li> | ||
<li><a href="overview-tree.html">Tree</a></li> | ||
<li><a href="deprecated-list.html">Deprecated</a></li> | ||
<li><a href="index-all.html">Index</a></li> | ||
<li><a href="help-doc.html">Help</a></li> | ||
</ul> | ||
</div> | ||
<div class="subNav"> | ||
<ul class="navList" id="allclasses_navbar_top"> | ||
<li><a href="allclasses.html">All Classes</a></li> | ||
</ul> | ||
<ul class="navListSearch"> | ||
<li><label for="search">SEARCH:</label> | ||
<input type="text" id="search" value="search" disabled="disabled"> | ||
<input type="reset" id="reset" value="reset" disabled="disabled"> | ||
</li> | ||
</ul> | ||
<div> | ||
<script type="text/javascript"><!-- | ||
allClassesLink = document.getElementById("allclasses_navbar_top"); | ||
if(window==top) { | ||
allClassesLink.style.display = "block"; | ||
} | ||
else { | ||
allClassesLink.style.display = "none"; | ||
} | ||
//--> | ||
</script> | ||
<noscript> | ||
<div>JavaScript is disabled on your browser.</div> | ||
</noscript> | ||
</div> | ||
<a id="skip.navbar.top"> | ||
<!-- --> | ||
</a></div> | ||
<!-- ========= END OF TOP NAVBAR ========= --> | ||
</div> | ||
<div class="navPadding"> </div> | ||
<script type="text/javascript"><!-- | ||
$('.navPadding').css('padding-top', $('.fixedNav').css("height")); | ||
//--> | ||
</script> | ||
</nav> | ||
</header> | ||
<main role="main"> | ||
<div class="header"> | ||
<h1 title="All&nbsp;Packages" class="title">All Packages</h1> | ||
</div> | ||
<div class="allPackagesContainer"> | ||
<ul class="blockList"> | ||
<li class="blockList"> | ||
<table class="packagesSummary"> | ||
<caption><span>Package Summary</span><span class="tabEnd"> </span></caption> | ||
<tr> | ||
<th class="colFirst" scope="col">Package</th> | ||
<th class="colLast" scope="col">Description</th> | ||
</tr> | ||
<tbody> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/package-summary.html">org.sosy_lab.java_smt</a></th> | ||
<td class="colLast"> | ||
<div class="block">JavaSMT: a generic SMT solver API.</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/api/package-summary.html">org.sosy_lab.java_smt.api</a></th> | ||
<td class="colLast"> | ||
<div class="block">The core interfaces for abstracting from SMT solvers and providing a common API for all solvers.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/api/visitors/package-summary.html">org.sosy_lab.java_smt.api.visitors</a></th> | ||
<td class="colLast"> | ||
<div class="block">The visitors of this package allow for efficient traversal, manipulation and transformation of | ||
formulas.</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/basicimpl/package-summary.html">org.sosy_lab.java_smt.basicimpl</a></th> | ||
<td class="colLast"> | ||
<div class="block">Abstract base classes for easier implementation of a solver backend.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/basicimpl/tactics/package-summary.html">org.sosy_lab.java_smt.basicimpl.tactics</a></th> | ||
<td class="colLast"> | ||
<div class="block">Default tactics implementations (formula-to-formula transformations).</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/package-summary.html">org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper</a></th> | ||
<td class="colLast"> | ||
<div class="block">Wrapper-classes to guarantee identical behavior for all solvers.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/delegate/logging/package-summary.html">org.sosy_lab.java_smt.delegate.logging</a></th> | ||
<td class="colLast"> | ||
<div class="block">Wraps the proving environment with loggers.</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/delegate/statistics/package-summary.html">org.sosy_lab.java_smt.delegate.statistics</a></th> | ||
<td class="colLast"> | ||
<div class="block">The classes of this package wrap the whole proving environment and measure all accesses to it.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/delegate/synchronize/package-summary.html">org.sosy_lab.java_smt.delegate.synchronize</a></th> | ||
<td class="colLast"> | ||
<div class="block">The classes of this package wrap the whole solver context and all corresponding proving | ||
environment and synchronize all accesses to it.</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/example/package-summary.html">org.sosy_lab.java_smt.example</a></th> | ||
<td class="colLast"> | ||
<div class="block">Some basic examples for using Java-SMT.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/example/nqueens_user_propagator/package-summary.html">org.sosy_lab.java_smt.example.nqueens_user_propagator</a></th> | ||
<td class="colLast"> | ||
<div class="block">Some basic examples for using Java-SMT.</div> | ||
</td> | ||
</tr> | ||
<tr class="rowColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/test/package-summary.html">org.sosy_lab.java_smt.test</a></th> | ||
<td class="colLast"> | ||
<div class="block">Solver-independent tests and test utilities for the solver API.</div> | ||
</td> | ||
</tr> | ||
<tr class="altColor"> | ||
<th class="colFirst" scope="row"><a href="org/sosy_lab/java_smt/utils/package-summary.html">org.sosy_lab.java_smt.utils</a></th> | ||
<td class="colLast"> | ||
<div class="block">Utility classes implementing algorithms based on the API of JavaSMT.</div> | ||
</td> | ||
</tr> | ||
</tbody> | ||
</table> | ||
</li> | ||
</ul> | ||
</div> | ||
</main> | ||
<footer role="contentinfo"> | ||
<nav role="navigation"> | ||
<!-- ======= START OF BOTTOM NAVBAR ====== --> | ||
<div class="bottomNav"><a id="navbar.bottom"> | ||
<!-- --> | ||
</a> | ||
<div class="skipNav"><a href="#skip.navbar.bottom" title="Skip navigation links">Skip navigation links</a></div> | ||
<a id="navbar.bottom.firstrow"> | ||
<!-- --> | ||
</a> | ||
<ul class="navList" title="Navigation"> | ||
<li><a href="index.html">Overview</a></li> | ||
<li>Package</li> | ||
<li>Class</li> | ||
<li><a href="overview-tree.html">Tree</a></li> | ||
<li><a href="deprecated-list.html">Deprecated</a></li> | ||
<li><a href="index-all.html">Index</a></li> | ||
<li><a href="help-doc.html">Help</a></li> | ||
</ul> | ||
</div> | ||
<div class="subNav"> | ||
<ul class="navList" id="allclasses_navbar_bottom"> | ||
<li><a href="allclasses.html">All Classes</a></li> | ||
</ul> | ||
<div> | ||
<script type="text/javascript"><!-- | ||
allClassesLink = document.getElementById("allclasses_navbar_bottom"); | ||
if(window==top) { | ||
allClassesLink.style.display = "block"; | ||
} | ||
else { | ||
allClassesLink.style.display = "none"; | ||
} | ||
//--> | ||
</script> | ||
<noscript> | ||
<div>JavaScript is disabled on your browser.</div> | ||
</noscript> | ||
</div> | ||
<a id="skip.navbar.bottom"> | ||
<!-- --> | ||
</a></div> | ||
<!-- ======== END OF BOTTOM NAVBAR ======= --> | ||
</nav> | ||
</footer> | ||
</body> | ||
</html> |
Oops, something went wrong.