SMT-RAT
SMT-RAT is an SMT Real Algebra Toolbox.
diff --git a/developers/rwth-aachen/index.xml b/developers/rwth-aachen/index.xml
index 127bd39..fb855c7 100644
--- a/developers/rwth-aachen/index.xml
+++ b/developers/rwth-aachen/index.xml
@@ -8,6 +8,13 @@
en-us
Sat, 07 Jun 2025 00:00:00 +0000
+ -
+
COMICS
+ http://localhost:1313/tools/prob/comics/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/prob/comics/
+ <p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p>
+
-
SMT-RAT
http://localhost:1313/tools/sat-smt/smt-rat/
diff --git a/developers/sri-international/index.html b/developers/sri-international/index.html
index c189b01..eda635c 100644
--- a/developers/sri-international/index.html
+++ b/developers/sri-international/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/stanford-university/index.html b/developers/stanford-university/index.html
index 10e7ece..1ba4919 100644
--- a/developers/stanford-university/index.html
+++ b/developers/stanford-university/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/tu-wien/index.html b/developers/tu-wien/index.html
new file mode 100644
index 0000000..a23925f
--- /dev/null
+++ b/developers/tu-wien/index.html
@@ -0,0 +1,140 @@
+
+
+
+
+
+
+
+
+TU Wien | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 🚧 This site is a work in progress. Don’t be shy to submit an issue or pull request 🚧
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ TU Wien
+
+
+
+
+
+
+
diff --git a/developers/tu-wien/index.xml b/developers/tu-wien/index.xml
new file mode 100644
index 0000000..422ec05
--- /dev/null
+++ b/developers/tu-wien/index.xml
@@ -0,0 +1,26 @@
+
+
+
+ TU Wien on Formal Methods Tools
+ http://localhost:1313/developers/tu-wien/
+ Recent content in TU Wien on Formal Methods Tools
+ Hugo
+ en-us
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+ -
+
Vampire
+ http://localhost:1313/tools/sat-smt/vampire/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/vampire/
+ <p>Vampire is a theorem prover.</p>
+
+ -
+
Zipperposition
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ <p>Zipperposition is an automated theorem prover for first-order logic with equality and theories.</p>
+
+
+
diff --git a/developers/uliege/index.html b/developers/uliege/index.html
index 1d4cb04..02e9944 100644
--- a/developers/uliege/index.html
+++ b/developers/uliege/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/university-of-freiburg/index.html b/developers/university-of-freiburg/index.html
index 7bdb183..c8508c9 100644
--- a/developers/university-of-freiburg/index.html
+++ b/developers/university-of-freiburg/index.html
@@ -23,7 +23,7 @@
-
+
@@ -107,6 +107,15 @@
+
+ CaDiCaL
+ CaDiCaL is a simplified satisfiability solver.
+
+
+
+
+
+
SMTInterpol
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
diff --git a/developers/university-of-freiburg/index.xml b/developers/university-of-freiburg/index.xml
index e659c8d..83498d9 100644
--- a/developers/university-of-freiburg/index.xml
+++ b/developers/university-of-freiburg/index.xml
@@ -8,6 +8,13 @@
en-us
Sat, 07 Jun 2025 00:00:00 +0000
+ -
+
CaDiCaL
+ http://localhost:1313/tools/sat-smt/cadical/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/cadical/
+ <p>CaDiCaL is a simplified satisfiability solver.</p>
+
-
SMTInterpol
http://localhost:1313/tools/sat-smt/smtinterpol/
diff --git a/developers/university-of-illinois/index.html b/developers/university-of-illinois/index.html
index ae28329..a0515d3 100644
--- a/developers/university-of-illinois/index.html
+++ b/developers/university-of-illinois/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/university-of-iowa/index.html b/developers/university-of-iowa/index.html
index c78bbac..400141c 100644
--- a/developers/university-of-iowa/index.html
+++ b/developers/university-of-iowa/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/university-of-lugano/index.html b/developers/university-of-lugano/index.html
index ff41290..94f0c3e 100644
--- a/developers/university-of-lugano/index.html
+++ b/developers/university-of-lugano/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/university-of-virginia/index.html b/developers/university-of-virginia/index.html
index 5d44ad3..5291835 100644
--- a/developers/university-of-virginia/index.html
+++ b/developers/university-of-virginia/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/developers/utah-state-university/index.html b/developers/utah-state-university/index.html
index b5c52ec..ed19e21 100644
--- a/developers/utah-state-university/index.html
+++ b/developers/utah-state-university/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/domains/index.html b/domains/index.html
index e639737..b3f3807 100644
--- a/domains/index.html
+++ b/domains/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/index.html b/index.html
index 9e79c06..ab92f05 100644
--- a/index.html
+++ b/index.html
@@ -24,7 +24,7 @@
-
+
@@ -118,6 +118,31 @@ Contribute
Try Something New
This list shows a selection of 20 random tools, refreshed every time this site is updated.
+
+
+
+
+ STP
+
+ Simple Theorem Prover
+
+
+ STP is a constraint solver for quantifier-free bitvectors.
+APIs and Bindings This tool is available …
+ STP
+
+
+
+
+ Storm
+
+ Probabilistic Model Checker
+
+
+ Storm is a tool for the analysis of systems involving random or probabilistic phenomena.
+
+ Storm
+
@@ -127,43 +152,43 @@ Contribute
CryptoMiniSat is a SAT solver.
-APIs and Bindings This tool is available through the following interfaces:
-C++ Namespace: …
+APIs and Bindings This tool is available through the following …
CryptoMiniSat
- Sally
-
- Probabilistic Model Checker
-
-
- Sally is a model checker for infinite state systems described as transition systems.
-
- Sally
-
-
-
-
- STAMINA
-
- Probabilistic Model Checker
-
-
- A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM. …
- STAMINA
-
-
-
-
- veriT
+ MathSAT
SMT Solver
- veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …
- veriT
+ [ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help …
+ MathSAT
+
+
+
+
+ Lingeling
+
+ SAT Solver
+
+
+ Lingeling is a SAT solver.
+
+ Lingeling
+
+
+
+
+ Zipperposition
+
+ Theorem Prover
+
+
+ Zipperposition is an automated theorem prover for first-order logic with equality and theories.
+
+ Zipperposition
@@ -173,7 +198,7 @@ C++ Namespace: …
SMT Solver
- Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, …
+ Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools …
Alt-Ergo
@@ -191,14 +216,127 @@ C++ Namespace: …
- cvc5
+ Boolector
- Theorem Prover
+ SMT Solver
- cvc5 is an automatic theorem prover for SMT problems.
+
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the …
+ Boolector
+
+
+
+
+ Yices 2
+
+ SMT Solver
+
+
+ Yices is an SMT solver developed by SRI International. It is widely used for checking the …
+ Yices 2
+
+
+
+
+ SMT-RAT
+
+ SMT Toolbox
+
+
+ SMT-RAT is an SMT Real Algebra Toolbox.
+APIs and Bindings This tool is available through the …
+ SMT-RAT
+
+
+
+
+ dReal
+
+ SMT Solver
+
+
+ [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems …
+ dReal
+
+
+
+
+ SMTInterpol
+
+ Interpolating SMT Solver
+
+
+ SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
+APIs and …
+ SMTInterpol
+
+
+
+
+ Q3B
+
+ SMT Solver
+
+
+ [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which …
+ Q3B
+
+
+
+
+ CaDiCaL
+
+ SAT Solver
+
+
+ CaDiCaL is a simplified satisfiability solver.
- cvc5
+ CaDiCaL
+
+
+
+
+ ParaFROST
+
+ SMT Solver
+
+
+ ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA …
+ ParaFROST
+
+
+
+
+ OpenSMT
+
+ SMT Solver
+
+
+ OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making …
+ OpenSMT
+
+
+
+
+ MiniSat
+
+ SAT Solver
+
+
+ [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help …
+ MiniSat
+
+
+
+
+ Sally
+
+ Probabilistic Model Checker
+
+
+ Sally is a model checker for infinite state systems described as transition systems.
+
+ Sally
@@ -213,145 +351,27 @@ C++ Namespace: …
Riss
-
-
- Boolector
-
- SMT Solver
-
-
- [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …
- Boolector
-
-
-
-
- SMTInterpol
-
- Interpolating SMT Solver
-
-
- SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
-APIs and Bindings This tool is …
- SMTInterpol
-
-
-
-
- MathSAT
-
- SMT Solver
-
-
- [ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers …
- MathSAT
-
-
-
-
- Z3
-
- Theorem Prover
-
-
- Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
-APIs and Bindings This tool is available …
- Z3
-
-
-
-
- Bitwuzla
-
- SMT Solver
-
-
- Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point …
- Bitwuzla
-
-
-
-
- Yices 2
-
- SMT Solver
-
-
- Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …
- Yices 2
-
-
-
-
- Lingeling
-
- SAT Solver
-
-
- Lingeling is a SAT solver.
-
- Lingeling
-
-
-
-
- dReal
-
- SMT Solver
-
-
- [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as …
- dReal
-
-
-
-
- MiniSat
-
- SAT Solver
-
-
- [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …
- MiniSat
-
-
-
-
- OpenSMT
-
- SMT Solver
-
-
- OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand …
- OpenSMT
-
-
-
-
- cvc4
-
- Theorem Prover
-
-
- [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5
-
- cvc4
-
-
-
-
- STP
-
- Simple Theorem Prover
-
-
- STP is a constraint solver for quantifier-free bitvectors.
-APIs and Bindings This tool is available through the following …
- STP
-
-
+
+
+
+
+
+
+
+
+
+ -
+
CaDiCaL
+ http://localhost:1313/tools/sat-smt/cadical/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/cadical/
+ <p>CaDiCaL is a simplified satisfiability solver.</p>
+
-
Colibri
http://localhost:1313/tools/sat-smt/colibri/
@@ -36,6 +43,13 @@
http://localhost:1313/tools/sat-smt/colibri/
<p>Colibri is an SMT solver.</p>
+ -
+
COMICS
+ http://localhost:1313/tools/prob/comics/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/prob/comics/
+ <p>COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).</p>
+
-
CryptoMiniSat
http://localhost:1313/tools/sat-smt/cryptominisat/
@@ -64,6 +78,13 @@
http://localhost:1313/tools/sat-smt/dreal/
<p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
<span style="display:none">]</span>
</div>
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p>
+ -
+
E
+ http://localhost:1313/tools/sat-smt/e/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/e/
+ <p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
+
-
Glucose
http://localhost:1313/tools/sat-smt/glucose/
@@ -169,6 +190,13 @@
http://localhost:1313/tools/sat-smt/stp/
<p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li>
</ul>
+ -
+
Vampire
+ http://localhost:1313/tools/sat-smt/vampire/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/vampire/
+ <p>Vampire is a theorem prover.</p>
+
-
veriT
http://localhost:1313/tools/sat-smt/verit/
@@ -190,6 +218,13 @@
http://localhost:1313/tools/sat-smt/z3/
<p>Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li>
</ul>
+ -
+
Zipperposition
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ <p>Zipperposition is an automated theorem prover for first-order logic with equality and theories.</p>
+
-
About
http://localhost:1313/about/
diff --git a/inputs/alt-ergo/index.html b/inputs/alt-ergo/index.html
index 636c159..55f0d71 100644
--- a/inputs/alt-ergo/index.html
+++ b/inputs/alt-ergo/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/cnf/index.html b/inputs/cnf/index.html
index eba2209..f413806 100644
--- a/inputs/cnf/index.html
+++ b/inputs/cnf/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/dimacs/index.html b/inputs/dimacs/index.html
index a4dd8e7..73a62ae 100644
--- a/inputs/dimacs/index.html
+++ b/inputs/dimacs/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/galileo/index.html b/inputs/galileo/index.html
index 750d01d..87e7ad8 100644
--- a/inputs/galileo/index.html
+++ b/inputs/galileo/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/greatspn/index.html b/inputs/greatspn/index.html
index b74602b..cc33ef9 100644
--- a/inputs/greatspn/index.html
+++ b/inputs/greatspn/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/index.html b/inputs/index.html
index 80cd46f..98da698 100644
--- a/inputs/index.html
+++ b/inputs/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/jani/index.html b/inputs/jani/index.html
index 323f2c5..841902f 100644
--- a/inputs/jani/index.html
+++ b/inputs/jani/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/mrmc/index.html b/inputs/mrmc/index.html
index ca5d681..95d9736 100644
--- a/inputs/mrmc/index.html
+++ b/inputs/mrmc/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/pnml/index.html b/inputs/pnml/index.html
index ee800d4..f0ae43e 100644
--- a/inputs/pnml/index.html
+++ b/inputs/pnml/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/prism/index.html b/inputs/prism/index.html
index 01b8e67..ad04328 100644
--- a/inputs/prism/index.html
+++ b/inputs/prism/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/sally/index.html b/inputs/sally/index.html
index 475ec1b..b0baba7 100644
--- a/inputs/sally/index.html
+++ b/inputs/sally/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/smtlib2/index.html b/inputs/smtlib2/index.html
index d033fcb..ebb7791 100644
--- a/inputs/smtlib2/index.html
+++ b/inputs/smtlib2/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/inputs/yices-2/index.html b/inputs/yices-2/index.html
index 5f5574e..faee39b 100644
--- a/inputs/yices-2/index.html
+++ b/inputs/yices-2/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/.net/index.html b/interfaces/.net/index.html
index d6198bc..a3d5199 100644
--- a/interfaces/.net/index.html
+++ b/interfaces/.net/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/c++/index.html b/interfaces/c++/index.html
index dc0327e..dec3b23 100644
--- a/interfaces/c++/index.html
+++ b/interfaces/c++/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/c/index.html b/interfaces/c/index.html
index c7ca055..df70337 100644
--- a/interfaces/c/index.html
+++ b/interfaces/c/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/cli/index.html b/interfaces/cli/index.html
index 3671617..62cdd8b 100644
--- a/interfaces/cli/index.html
+++ b/interfaces/cli/index.html
@@ -23,7 +23,7 @@
-
+
@@ -129,6 +129,15 @@
+
+
+
+ CaDiCaL
+ CaDiCaL is a simplified satisfiability solver.
+
+
+
+
@@ -172,6 +181,14 @@ APIs and Bindings This tool is available through the following …
+
+
+
+ E
+ E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with …
+
+
+
@@ -300,6 +317,15 @@ APIs and Bindings This tool is available …
+
+
+
+ Vampire
+ Vampire is a theorem prover.
+
+
+
+
@@ -325,6 +351,15 @@ APIs and Bindings This …
+
+
+
+ Zipperposition
+ Zipperposition is an automated theorem prover for first-order logic with equality and theories.
+
+
+
+
diff --git a/interfaces/cli/index.xml b/interfaces/cli/index.xml
index 2be35d0..5f17352 100644
--- a/interfaces/cli/index.xml
+++ b/interfaces/cli/index.xml
@@ -29,6 +29,13 @@
http://localhost:1313/tools/sat-smt/boolector/
<p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span>
<span style="display:none">]</span>
</div>
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p>
+ -
+
CaDiCaL
+ http://localhost:1313/tools/sat-smt/cadical/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/cadical/
+ <p>CaDiCaL is a simplified satisfiability solver.</p>
+
-
Colibri
http://localhost:1313/tools/sat-smt/colibri/
@@ -64,6 +71,13 @@
http://localhost:1313/tools/sat-smt/dreal/
<p>
<div style="display: flex; align-items: center; gap: 8px;">
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
<span style="display:none">[</span>
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
<span style="display:none">]</span>
</div>
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p>
+ -
+
E
+ http://localhost:1313/tools/sat-smt/e/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/e/
+ <p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.</p>
+
-
Glucose
http://localhost:1313/tools/sat-smt/glucose/
@@ -169,6 +183,13 @@
http://localhost:1313/tools/sat-smt/stp/
<p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li>
</ul>
+ -
+
Vampire
+ http://localhost:1313/tools/sat-smt/vampire/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/vampire/
+ <p>Vampire is a theorem prover.</p>
+
-
veriT
http://localhost:1313/tools/sat-smt/verit/
@@ -190,5 +211,12 @@
http://localhost:1313/tools/sat-smt/z3/
<p>Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li>
</ul>
+ -
+
Zipperposition
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/sat-smt/zipperposition/
+ <p>Zipperposition is an automated theorem prover for first-order logic with equality and theories.</p>
+
diff --git a/interfaces/index.html b/interfaces/index.html
index 768a248..016be92 100644
--- a/interfaces/index.html
+++ b/interfaces/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/java/index.html b/interfaces/java/index.html
index 355f488..bac98f6 100644
--- a/interfaces/java/index.html
+++ b/interfaces/java/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/online/index.html b/interfaces/online/index.html
index 6197598..7883152 100644
--- a/interfaces/online/index.html
+++ b/interfaces/online/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/python/index.html b/interfaces/python/index.html
index 922f6f6..0dd8433 100644
--- a/interfaces/python/index.html
+++ b/interfaces/python/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/interfaces/rust/index.html b/interfaces/rust/index.html
index ca23e77..1dc6317 100644
--- a/interfaces/rust/index.html
+++ b/interfaces/rust/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/license/index.html b/license/index.html
index 10f9bb5..1baf034 100644
--- a/license/index.html
+++ b/license/index.html
@@ -25,7 +25,7 @@ Permission is hereby granted, free of charge, to any person obtaining a copy of
-
+
diff --git a/licenses/all-rights-reserved/index.html b/licenses/all-rights-reserved/index.html
index 843edaf..1e8b6ab 100644
--- a/licenses/all-rights-reserved/index.html
+++ b/licenses/all-rights-reserved/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/licenses/apache-2.0/index.html b/licenses/apache-2.0/index.html
index 70c7b91..eac6c24 100644
--- a/licenses/apache-2.0/index.html
+++ b/licenses/apache-2.0/index.html
@@ -23,7 +23,7 @@
-
+
diff --git a/licenses/bsd/index.html b/licenses/bsd/index.html
index 4db885f..6d66c4a 100644
--- a/licenses/bsd/index.html
+++ b/licenses/bsd/index.html
@@ -23,7 +23,7 @@
-
+
@@ -122,6 +122,15 @@
+
+
+