From 589a55d8cde8dc713b9e36061cad05eefb339e6c Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 12 Jun 2025 15:13:07 -0600 Subject: [PATCH] Wrap up SAT/SMT --- tools/pmc/_index.md | 10 +++++++++ tools/pmc/stamina.md | 22 ++++++++++++++++++++ tools/sat-smt/_index.md | 10 +++++++++ tools/sat-smt/bitwuzla.md | 22 ++++++++++++++++++++ tools/sat-smt/boolector.md | 23 +++++++++++++++++++++ tools/sat-smt/colibri.md | 21 +++++++++++++++++++ tools/sat-smt/cryptominisat.md | 33 ++++++++++++++++++++++++++++++ tools/sat-smt/cvc4.md | 22 ++++++++++++++++++++ tools/sat-smt/cvc5.md | 22 ++++++++++++++++++++ tools/sat-smt/dreal.md | 22 ++++++++++++++++++++ tools/{ => sat-smt}/glucose.md | 0 tools/{ => sat-smt}/lingeling.md | 0 tools/{ => sat-smt}/mathsat.md | 2 +- tools/{ => sat-smt}/minisat.md | 0 tools/{ => sat-smt}/opensmt.md | 0 tools/{ => sat-smt}/parafrost.md | 0 tools/{ => sat-smt}/q3b.md | 0 tools/{ => sat-smt}/riss.md | 0 tools/{ => sat-smt}/smt-rat.md | 0 tools/{ => sat-smt}/smtinterpol.md | 0 tools/{ => sat-smt}/stp.md | 0 tools/{ => sat-smt}/verit.md | 0 tools/{ => sat-smt}/yices.md | 0 tools/{ => sat-smt}/z3.md | 0 tools/termination/_index.md | 10 +++++++++ tools/termination/approve.md | 22 ++++++++++++++++++++ 26 files changed, 240 insertions(+), 1 deletion(-) create mode 100644 tools/pmc/_index.md create mode 100644 tools/pmc/stamina.md create mode 100644 tools/sat-smt/_index.md create mode 100644 tools/sat-smt/bitwuzla.md create mode 100644 tools/sat-smt/boolector.md create mode 100644 tools/sat-smt/colibri.md create mode 100644 tools/sat-smt/cryptominisat.md create mode 100644 tools/sat-smt/cvc4.md create mode 100644 tools/sat-smt/cvc5.md create mode 100644 tools/sat-smt/dreal.md rename tools/{ => sat-smt}/glucose.md (100%) rename tools/{ => sat-smt}/lingeling.md (100%) rename tools/{ => sat-smt}/mathsat.md (95%) rename tools/{ => sat-smt}/minisat.md (100%) rename tools/{ => sat-smt}/opensmt.md (100%) rename tools/{ => sat-smt}/parafrost.md (100%) rename tools/{ => sat-smt}/q3b.md (100%) rename tools/{ => sat-smt}/riss.md (100%) rename tools/{ => sat-smt}/smt-rat.md (100%) rename tools/{ => sat-smt}/smtinterpol.md (100%) rename tools/{ => sat-smt}/stp.md (100%) rename tools/{ => sat-smt}/verit.md (100%) rename tools/{ => sat-smt}/yices.md (100%) rename tools/{ => sat-smt}/z3.md (100%) create mode 100644 tools/termination/_index.md create mode 100644 tools/termination/approve.md diff --git a/tools/pmc/_index.md b/tools/pmc/_index.md new file mode 100644 index 0000000..e9cbb12 --- /dev/null +++ b/tools/pmc/_index.md @@ -0,0 +1,10 @@ ++++ +title = "All PMC Tools" +layout = "section" ++++ + +This page lists all of the SAT & SMT 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. \ No newline at end of file diff --git a/tools/pmc/stamina.md b/tools/pmc/stamina.md new file mode 100644 index 0000000..687636a --- /dev/null +++ b/tools/pmc/stamina.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = true +title = 'STAMINA TODO' +subtitle = 'Probabilistic Model Checker' +links = [ + { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github' }, + { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Probabilistic Model Checker', 'Rare Events'] +developers = ['Utah State University'] +licenses = ['BSD'] +inputs = ['SMTLIB2'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +publications = ['Barbosa2022'] ++++ + + +cvc5 is an automatic theorem prover for SMT problems. \ No newline at end of file diff --git a/tools/sat-smt/_index.md b/tools/sat-smt/_index.md new file mode 100644 index 0000000..89d3e3b --- /dev/null +++ b/tools/sat-smt/_index.md @@ -0,0 +1,10 @@ ++++ +title = "All SAT & SMT Tools" +layout = "section" ++++ + +This page lists all of the SAT & SMT 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. \ No newline at end of file diff --git a/tools/sat-smt/bitwuzla.md b/tools/sat-smt/bitwuzla.md new file mode 100644 index 0000000..d0b3335 --- /dev/null +++ b/tools/sat-smt/bitwuzla.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Bitwuzla' +subtitle = 'SMT Solver' +links = [ + { title = "Homepage", url = "https://bitwuzla.github.io", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/bitwuzla/bitwuzla", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Stanford University'] +licenses = ['MIT'] +inputs = ['SMTLIB2'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +publications = ['Niemetz2023'] ++++ + + +Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations. \ No newline at end of file diff --git a/tools/sat-smt/boolector.md b/tools/sat-smt/boolector.md new file mode 100644 index 0000000..c95c42a --- /dev/null +++ b/tools/sat-smt/boolector.md @@ -0,0 +1,23 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Boolector' +subtitle = 'SMT Solver' +links = [ + { title = "Homepage", url = "https://boolector.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/boolector/boolector", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Stanford University', 'Johannes Kepler Universität Linz'] +licenses = ['MIT'] +inputs = ['SMTLIB2'] +interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +publications = ['Niemetz2014'] ++++ + +{{}} +Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. +Succeeded by [Bitwuzla](../bitwuzla) \ No newline at end of file diff --git a/tools/sat-smt/colibri.md b/tools/sat-smt/colibri.md new file mode 100644 index 0000000..515794c --- /dev/null +++ b/tools/sat-smt/colibri.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Colibri' +subtitle = 'SMT Solver' +links = [ + { title = "Homepage", url = "https://colibri.frama-c.com/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://git.frama-c.com/pub/colibrics/-/tree/master", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver'] +developers = ['CEA'] +licenses = ['MIT'] +inputs = ['SMTLIB2'] +interfaces = ['CLI'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +Colibri is an SMT solver. \ No newline at end of file diff --git a/tools/sat-smt/cryptominisat.md b/tools/sat-smt/cryptominisat.md new file mode 100644 index 0000000..add2fe1 --- /dev/null +++ b/tools/sat-smt/cryptominisat.md @@ -0,0 +1,33 @@ ++++ +date = 2025-06-07 +draft = false +title = 'CryptoMiniSat' +subtitle = 'SAT Solver' +links = [ + { title = "Homepage", url = "https://www.msoos.org/cryptominisat5/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/msoos/cryptominisat", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc4.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SAT Solver'] +developers = ['INRIA Rhône-Alpes', 'University of Virginia'] +licenses = ['MIT', 'GPLv2'] +inputs = ['CNF'] +interfaces = ['CLI', 'Python', 'C++', ] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +publications = ['Soos2009'] ++++ + + +CryptoMiniSat is a SAT solver. + +## APIs and Bindings +This tool is available through the following interfaces: + +- **C++ Namespace:** Documentation on [homepage](https://www.msoos.org/cryptominisat5/) +- **Python package:** [PyPI package](https://pypi.org/project/pycryptosat/) + + + + + diff --git a/tools/sat-smt/cvc4.md b/tools/sat-smt/cvc4.md new file mode 100644 index 0000000..38cb479 --- /dev/null +++ b/tools/sat-smt/cvc4.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'cvc4' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://cvc4.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/CVC4/CVC4-archived", icon = 'fa-brands fa-github' }, + { title = "Playground", url = "https://cvc4.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover'] +developers = ['Stanford University', 'University of Iowa'] +licenses = ['BSD'] +inputs = ['SMTLIB2'] +interfaces = ['CLI', 'Online'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +publications = ['Barrett2011'] ++++ + +{{}} +cvc4 is an automatic theorem prover for SMT problems. It is succeeded by [cvc5](../cvc5) \ No newline at end of file diff --git a/tools/sat-smt/cvc5.md b/tools/sat-smt/cvc5.md new file mode 100644 index 0000000..4b342bb --- /dev/null +++ b/tools/sat-smt/cvc5.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'cvc5' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/cvc5/cvc5", icon = 'fa-brands fa-github' }, + { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover'] +developers = ['Stanford University', 'University of Iowa'] +licenses = ['BSD'] +inputs = ['SMTLIB2'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +publications = ['Barbosa2022'] ++++ + + +cvc5 is an automatic theorem prover for SMT problems. \ No newline at end of file diff --git a/tools/sat-smt/dreal.md b/tools/sat-smt/dreal.md new file mode 100644 index 0000000..5700ff5 --- /dev/null +++ b/tools/sat-smt/dreal.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'dReal' +subtitle = 'SMT Solver' +links = [ + { title = "Homepage", url = "https://dreal.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver'] +# developers = ['Johannes Kepler Universität Linz'] +licenses = ['Apache-2.0'] +# inputs = [''] +interfaces = ['CLI'] +maintenance = ['Not Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +{{}} +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. \ No newline at end of file diff --git a/tools/glucose.md b/tools/sat-smt/glucose.md similarity index 100% rename from tools/glucose.md rename to tools/sat-smt/glucose.md diff --git a/tools/lingeling.md b/tools/sat-smt/lingeling.md similarity index 100% rename from tools/lingeling.md rename to tools/sat-smt/lingeling.md diff --git a/tools/mathsat.md b/tools/sat-smt/mathsat.md similarity index 95% rename from tools/mathsat.md rename to tools/sat-smt/mathsat.md index 398cb9d..3728a15 100644 --- a/tools/mathsat.md +++ b/tools/sat-smt/mathsat.md @@ -10,7 +10,7 @@ links = [ ] applications = ['SMT Solver'] developers = ['Fondazione Bruno Kessler','DISI-University of Trento'] -licenses = ['All rights reserved'] +licenses = ['All Rights Reserved'] # inputs = [''] interfaces = ['CLI'] maintenance = ['Actively Maintained'] diff --git a/tools/minisat.md b/tools/sat-smt/minisat.md similarity index 100% rename from tools/minisat.md rename to tools/sat-smt/minisat.md diff --git a/tools/opensmt.md b/tools/sat-smt/opensmt.md similarity index 100% rename from tools/opensmt.md rename to tools/sat-smt/opensmt.md diff --git a/tools/parafrost.md b/tools/sat-smt/parafrost.md similarity index 100% rename from tools/parafrost.md rename to tools/sat-smt/parafrost.md diff --git a/tools/q3b.md b/tools/sat-smt/q3b.md similarity index 100% rename from tools/q3b.md rename to tools/sat-smt/q3b.md diff --git a/tools/riss.md b/tools/sat-smt/riss.md similarity index 100% rename from tools/riss.md rename to tools/sat-smt/riss.md diff --git a/tools/smt-rat.md b/tools/sat-smt/smt-rat.md similarity index 100% rename from tools/smt-rat.md rename to tools/sat-smt/smt-rat.md diff --git a/tools/smtinterpol.md b/tools/sat-smt/smtinterpol.md similarity index 100% rename from tools/smtinterpol.md rename to tools/sat-smt/smtinterpol.md diff --git a/tools/stp.md b/tools/sat-smt/stp.md similarity index 100% rename from tools/stp.md rename to tools/sat-smt/stp.md diff --git a/tools/verit.md b/tools/sat-smt/verit.md similarity index 100% rename from tools/verit.md rename to tools/sat-smt/verit.md diff --git a/tools/yices.md b/tools/sat-smt/yices.md similarity index 100% rename from tools/yices.md rename to tools/sat-smt/yices.md diff --git a/tools/z3.md b/tools/sat-smt/z3.md similarity index 100% rename from tools/z3.md rename to tools/sat-smt/z3.md diff --git a/tools/termination/_index.md b/tools/termination/_index.md new file mode 100644 index 0000000..85d4237 --- /dev/null +++ b/tools/termination/_index.md @@ -0,0 +1,10 @@ ++++ +title = "All Termination Tools" +layout = "section" ++++ + +This page lists all of the termination 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. \ No newline at end of file diff --git a/tools/termination/approve.md b/tools/termination/approve.md new file mode 100644 index 0000000..9ff6092 --- /dev/null +++ b/tools/termination/approve.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = true +title = 'AProVE TODO' +subtitle = 'Probabilistic Model Checker' +links = [ + { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github' }, + { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Probabilistic Model Checker', 'Rare Events'] +developers = ['Utah State University'] +licenses = ['BSD'] +inputs = ['SMTLIB2'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +publications = ['Barbosa2022'] ++++ + + +cvc5 is an automatic theorem prover for SMT problems. \ No newline at end of file