Skip to content

Commit

Permalink
Deploy to GitHub Pages
Browse files Browse the repository at this point in the history
  • Loading branch information
@dbeyer
dbeyer committed Apr 25, 2024
0 parents commit 779e392
Show file tree
Hide file tree
Showing 191 changed files with 102,909 additions and 0 deletions.
120 changes: 120 additions & 0 deletions ConfigurationOptions.txt
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, DREAL4]

# 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
865 changes: 865 additions & 0 deletions api/allclasses-index.html

Large diffs are not rendered by default.

158 changes: 158 additions & 0 deletions api/allclasses.html

Large diffs are not rendered by default.

241 changes: 241 additions & 0 deletions api/allpackages-index.html
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 Thu Apr 25 11:26:47 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-25">
<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&nbsp;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">&nbsp;</div>
<script type="text/javascript"><!--
$('.navPadding').css('padding-top', $('.fixedNav').css("height"));
//-->
</script>
</nav>
</header>
<main role="main">
<div class="header">
<h1 title="All&amp;nbsp;Packages" class="title">All&nbsp;Packages</h1>
</div>
<div class="allPackagesContainer">
<ul class="blockList">
<li class="blockList">
<table class="packagesSummary">
<caption><span>Package Summary</span><span class="tabEnd">&nbsp;</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&nbsp;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>
Loading

0 comments on commit 779e392

Please sign in to comment.