fmtools/content
1
0
Fork 0
Code Issues 24 Pull Requests Actions Packages Projects 1 Releases Wiki Activity

add tools

Browse Source
This commit is contained in:
Landon Taylor 2025-06-10 14:13:34 -06:00
parent a454011c40
commit 5c5710ca6a
15 changed files with 301 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
tools/_index.md
View File

@ -2,3 +2,9 @@
title = "All Tools"
layout = "section"
+++
This page lists all of the tools on this site in alphabetical order.
Click a tool name in the first column to view tool details.
Click a colorful item in the second column to view all the tools for which that term applies.
Item colors mean nothing and are intended to make it easy to skim the page.
Colors are generated by hashing each term's name and converting it to RGB color values.

22
tools/glucose.md Normal file
View File

@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'Glucose'
subtitle = 'SAT Solver'
links = [
{ title = "Homepage", url = "https://www.labri.fr/perso/lsimon/research/glucose/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/audemard/glucose", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SAT Solver']
developers = ['Gilles Audemard','Laurent Simon']
licenses = ['MIT']
inputs = ['CNF']
interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['deMoura2008']
+++
<!-- {{<closed-source>}} -->
Glucose is a SAT solver.

22
tools/lingeling.md Normal file
View File

@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'Lingeling'
subtitle = 'SMT Solver'
links = [
{ title = "Homepage", url = "https://fmv.jku.at/lingeling/", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/arminbiere/lingeling", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SAT Solver']
developers = ['Johannes Kepler Universität Linz']
licenses = ['MIT']
# inputs = ['']
interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['deMoura2008']
+++
<!-- {{<closed-source>}} -->
Lingeling is a SAT solver.

22
tools/mathsat.md Normal file
View File

@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'MathSAT'
subtitle = 'SMT Solver'
links = [
{ title = "Homepage", url = "https://mathsat.fbk.eu/", icon = 'fa-solid fa-home' },
# { title = "Source Code", url = "https://github.com/niklasso/minisat", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SMT Solver']
developers = ['Fondazione Bruno Kessler','DISI-University of Trento']
licenses = ['All rights reserved']
# inputs = ['']
interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['deMoura2008']
+++
{{<closed-source>}}
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.

22
tools/minisat.md Normal file
View File

@ -0,0 +1,22 @@
+++
date = 2025-06-07
draft = false
title = 'MiniSat'
subtitle = 'SAT Solver'
links = [
{ title = "Homepage", url = "http://minisat.se/Main.html", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/niklasso/minisat", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SAT Solver']
developers = ['Niklas Eén', 'Niklas Sörensson']
licenses = ['MIT']
# inputs = ['']
interfaces = ['CLI']
maintenance = ['Not Maintained']
# techniques = ['CDCL']
# publications = ['deMoura2008']
+++
{{<inactive year="2013">}}
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.

21
tools/opensmt.md Normal file
View File

@ -0,0 +1,21 @@
+++
date = 2025-06-07
draft = false
title = 'OpenSMT'
subtitle = 'SMT Solver'
links = [
{ title = "Homepage", url = "https://verify.inf.usi.ch/opensmt", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/usi-verification-and-security/opensmt", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SMT Solver']
developers = ['University of Lugano']
licenses = ['GPLv3']
inputs = ['SMTLIB2']
interfaces = ['CLI']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
# publications = ['deMoura2008']
+++
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of [MiniSAT](/tools/minisat).

34
tools/parafrost.md Normal file
View File

@ -0,0 +1,34 @@
+++
date = 2025-06-07
draft = false
title = 'ParaFROST'
subtitle = 'SMT Solver'
links = [
# { title = "Homepage", url = "https://github.com/Z3Prover/z3", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/muhos/ParaFROST", icon = 'fa-brands fa-github' },
# { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SAT Solver']
developers = ['Eindhoven University of Technology', 'Albert-Ludwigs-Universität']
licenses = ['GPLv3']
inputs = ['SMTLIB2']
interfaces = ['CLI']
maintenance = ['Actively Maintained']
techniques = ['CDCL', 'GPU']
publications = ['Osama2024']
+++
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.
## APIs and Bindings
This tool is available through the following interfaces:
- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)
- **.NET API:** [Z3 .NET Namespace Reference](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
- **Java API:** [Z3 Java API Reference](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
- **Python bindings:** [z3-solver PyPI package](https://pypi.org/project/z3-solver/) ([Documentation](https://z3prover.github.io/api/html/z3.html))
- **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3)

25
tools/q3b.md Normal file
View File

@ -0,0 +1,25 @@
+++
date = 2025-06-07
draft = false
title = 'Q3B'
subtitle = 'SMT Solver'
links = [
# { title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/martinjonas/Q3B", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SMT Solver']
developers = ['Masaryk University']
licenses = ['MIT']
inputs = ['SMTLIB2']
interfaces = ['CLI']
maintenance = ['Not Maintained']
publications = ['Jonas2016']
+++
{{<inactive year="2023">}}
Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.

25
tools/riss.md Normal file
View File

@ -0,0 +1,25 @@
+++
date = 2025-06-07
draft = false
title = 'Riss'
subtitle = 'SAT Tool Collection'
links = [
# { title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/nmanthey/riss-solver", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SAT Solver']
developers = ['Norbert Manthey']
licenses = ['LGPLv2']
inputs = []
interfaces = ['CLI']
maintenance = ['Not Maintained']
# publications = ['Henkel2021']
+++
{{<inactive year="2017">}}
Riss is a SAT solving tool collection.

31
tools/smt-rat.md Normal file
View File

@ -0,0 +1,31 @@
+++
date = 2025-06-07
draft = false
title = 'SMT-RAT'
subtitle = 'SMT Toolbox'
links = [
{ title = "Homepage", url = "https://ths-rwth.github.io/smtrat/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/ths-rwth/smtrat", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SMT Solver', 'SAT Solver']
developers = ['RWTH Aachen']
licenses = ['MIT']
inputs = ['SMTLIB2']
interfaces = ['CLI', 'C++']
maintenance = ['Actively Maintained']
publications = ['Corzilius2015']
+++
SMT-RAT is an SMT Real Algebra Toolbox.
## APIs and Bindings
This tool is available through the following interfaces:
- **C++ API:** [C++ API Reference](https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25)

31
tools/smtinterpol.md Normal file
View File

@ -0,0 +1,31 @@
+++
date = 2025-06-07
draft = false
title = 'SMTInterpol'
subtitle = 'Interpolating SMT Solver'
links = [
{ title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/ultimate-pa/smtinterpol", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SMT Solver']
developers = ['University of Freiburg']
licenses = ['GPLv3']
inputs = ['SMTLIB2']
interfaces = ['CLI', 'Java']
maintenance = ['Actively Maintained']
publications = ['Henkel2021']
+++
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
## APIs and Bindings
This tool is available through the following interfaces:
- **Java API:** [Java API Reference](https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html)

32
tools/stp.md Normal file
View File

@ -0,0 +1,32 @@
+++
date = 2025-06-07
draft = false
title = 'STP'
subtitle = 'Simple Theorem Prover'
links = [
{ title = "Homepage", url = "https://stp.github.io/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/stp/stp", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['Constraint Solver', 'SMT Solver', 'Theorem Prover']
developers = ['University of Illinois', 'Stanford University']
licenses = ['MIT']
inputs = ['SMTLIB2']
interfaces = ['CLI', 'C', 'Python']
maintenance = ['Actively Maintained']
publications = ['Ganesh2007', 'Cadar2006']
+++
STP is a constraint solver for quantifier-free bitvectors.
## APIs and Bindings
This tool is available through the following interfaces:
- **C API:** [stp C API Reference](https://stp.readthedocs.io/en/latest/#c-library-usage)
- **Python bindings:** [stp PyPI package](https://stp.readthedocs.io/en/latest/#python-usage)

2
tools/verit.md
View File

@ -7,7 +7,7 @@ subtitle = 'SMT Solver'
links = [
{ title = "Homepage", url = "https://www.verit-solver.org/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/SRI-CSL/yices2", icon = 'fa-brands fa-github' },
# { title = "Source Code", url = "https://github.com/SRI-CSL/yices2", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]

4
tools/yices.md
View File

@ -11,7 +11,7 @@ links = [
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SMT Solver']
applications = ['SMT Solver', 'SAT Solver']
developers = ['SRI International']
licenses = ['GPLv3']
inputs = ['SMTLIB2', 'Yices 2']
@ -24,7 +24,7 @@ publications = ['Dutertre2014']
Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.
## APIs and Bindings
Yices is available through several interfaces, making it a convenient option to build into a project.
This tool is available through the following interfaces:
- **General API:** [Yices API Reference](https://yices.csl.sri.com/doc/index.html)
- **Python bindings:** [yices2 PyPI package](https://pypi.org/project/yices/)

10
tools/z3.md
View File

@ -1,5 +1,5 @@
+++
date = 2024-02-02T04:14:54-08:00
date = 2025-06-07
draft = false
title = 'Z3'
subtitle = 'Theorem Prover'
@ -8,7 +8,7 @@ links = [
{ title = "Source Code", url = "https://github.com/Z3Prover/z3", icon = 'fa-brands fa-github' },
{ title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SMT Solver', 'Theorem Prover']
applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver']
developers = ['Microsoft Research']
licenses = ['MIT']
inputs = ['SMTLIB2', 'DIMACS']
@ -18,11 +18,11 @@ maintenance = ['Actively Maintained']
publications = ['deMoura2008']
+++
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
## APIs and Bindings
Z3 is available through several interfaces, making it a convenient option to build into a project.
This tool is available through the following interfaces:
- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)