Wrap up SAT/SMT

privacy.md

@@ -3,10 +3,10 @@ title = 'Privacy'
 subtitle = "tl;dr: I won't know you were here."
 +++
 
-This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and 
+This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and there is no money to be made from this project.
 
-If you choose to contribute content (such as submitting an article or comment), any information you voluntarily provide will be stored as part of the website's content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website's owner. Any information you voluntarily provide as part of a code contribution becomes public information and may be used by the general public as allowed by respective laws and policies.
+If you choose to contribute content (including emails, issues, and pull requests), any information you voluntarily provide may be stored as part of the website's content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website's owner. Due to the public nature of its disclosure, this information is not considered private and may be used by the general public as allowed by respective laws and policies. Your privacy is respected, and no unnecessary data is collected or shared. 
 
-Your privacy is respected, and no unnecessary data is collected or shared. If you or your tool is listed on this page and you would like to remove it, please contact `fmtools@mossbiscuits.com` with the subject `Please remove my data`.
+If your information (e.g., your name, a tool you developed, or an attribution) is listed on this website and you would like to remove it, please contact `fmtools@mossbiscuits.com` with the subject `Please remove my data`. I cannot make guarantees, but I will make a reasonable effort to remove or redact your information within 1-3 business days.
 
-*Look at you, reading privacy policies. Thanks for being a responsible internet user.*
+*Look at you, reading privacy policies. Thanks for being a responsible internet user. Now go do something more interesting* :slightly_smiling_face:

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.

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']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.

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.

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']
++++
+
+<!-- {{<inactive year="2024">}} -->
+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.

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']
++++
+
+{{<inactive year="2024">}}
+Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
+Succeeded by [Bitwuzla](../bitwuzla)

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.

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']
++++
+
+<!-- {{<inactive year="2021">}} -->
+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/)
+<!-- - **.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) -->
+<!-- - **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3) -->
+
+

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']
++++
+
+{{<inactive year="2021">}}
+cvc4 is an automatic theorem prover for SMT problems. It is succeeded by [cvc5](../cvc5)

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']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.

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']
++++
+
+{{<inactive year="2023">}}
+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. 

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']

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.

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']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.