fmtools/public
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Ready to deploy in beta more

Browse Source
This commit is contained in:
Landon Taylor
2025-06-13 13:09:07 -06:00
parent ad8d224db4
commit fb51f11cd4
189 changed files with 9460 additions and 3385 deletions
Download Patch File Download Diff File Expand all files Collapse all files

135
tools/sat-smt/bitwuzla/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Bitwuzla">
<meta property="og:description" content="Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/bitwuzla/">
<meta property="og:url" content="https://example.org/tools/sat-smt/bitwuzla/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/bitwuzla/">
<link rel="canonical" href="https://example.org/tools/sat-smt/bitwuzla/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -105,6 +113,23 @@
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
<a
class="term-link"
id="applications_smt-solver"
@@ -131,23 +156,6 @@
</a>
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
</td>
</tr>
@@ -348,6 +356,34 @@
<li>
<strong>Bitwuzla</strong>
@@ -377,50 +413,6 @@
</ul>
</section>
@@ -429,8 +421,8 @@
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Bitwuzla">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Bitwuzla" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -447,6 +439,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

141
tools/sat-smt/boolector/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/boolector/">
<meta property="og:url" content="https://example.org/tools/sat-smt/boolector/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/boolector/">
<link rel="canonical" href="https://example.org/tools/sat-smt/boolector/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -115,6 +123,23 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
<a
class="term-link"
id="applications_smt-solver"
@@ -141,23 +166,6 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
</a>
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
</td>
</tr>
@@ -184,10 +192,10 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
<a
class="term-link"
id="developers_stanford-university"
style="background:rgba(38,159,198,0.4)"
href="/developers/stanford-university">
Stanford University
id="developers_johannes-kepler-universit%C3%A4t-linz"
style="background:rgba(78,0,50,0.4)"
href="/developers/johannes-kepler-universit%C3%A4t-linz">
Johannes Kepler Universität Linz
</a>
@@ -201,10 +209,10 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
<a
class="term-link"
id="developers_johannes-kepler-universit%C3%A4t-linz"
style="background:rgba(78,0,50,0.4)"
href="/developers/johannes-kepler-universit%C3%A4t-linz">
Johannes Kepler Universität Linz
id="developers_stanford-university"
style="background:rgba(38,159,198,0.4)"
href="/developers/stanford-university">
Stanford University
</a>
@@ -368,7 +376,7 @@ Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of f
<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>
Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p>
</section>
@@ -390,6 +398,28 @@ Succeeded by <a href="../bitwuzla">Bitwuzla</a></p>
<li>
<strong>Boolector 2.0</strong>
@@ -421,44 +451,6 @@ Succeeded by <a href="../bitwuzla">Bitwuzla</a></p>
</ul>
</section>
@@ -466,7 +458,9 @@ Succeeded by <a href="../bitwuzla">Bitwuzla</a></p>
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Boolector&body=Describe+your+problem+or+suggested+update+for+the+page+%22Boolector%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Boolector" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -483,6 +477,7 @@ Succeeded by <a href="../bitwuzla">Bitwuzla</a></p>
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

29
tools/sat-smt/colibri/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Colibri">
<meta property="og:description" content="Colibri is an SMT solver.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/colibri/">
<meta property="og:url" content="https://example.org/tools/sat-smt/colibri/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/colibri/">
<link rel="canonical" href="https://example.org/tools/sat-smt/colibri/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -306,7 +314,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Colibri&body=Describe+your+problem+or+suggested+update+for+the+page+%22Colibri%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Colibri" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -323,6 +333,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

151
tools/sat-smt/cryptominisat/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -19,16 +19,16 @@ This tool is available through the following interfaces:
C&#43;&#43; Namespace: Documentation on homepage
Python">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/cryptominisat/">
<meta property="og:url" content="https://example.org/tools/sat-smt/cryptominisat/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/cryptominisat/">
<link rel="canonical" href="https://example.org/tools/sat-smt/cryptominisat/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -40,6 +40,14 @@ Python">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -229,6 +237,23 @@ Python">
<a
class="term-link"
id="interfaces_c&#43;&#43;"
style="background:rgba(246,248,124,0.4)"
href="/interfaces/c&#43;&#43;">
C&#43;&#43;
</a>
<a
class="term-link"
id="interfaces_cli"
@@ -255,23 +280,6 @@ Python">
</a>
<a
class="term-link"
id="interfaces_c&#43;&#43;"
style="background:rgba(246,248,124,0.4)"
href="/interfaces/c&#43;&#43;">
C&#43;&#43;
</a>
</td>
</tr>
@@ -298,10 +306,10 @@ Python">
<a
class="term-link"
id="licenses_mit"
style="background:rgba(122,188,26,0.4)"
href="/licenses/mit">
MIT
id="licenses_gplv2"
style="background:rgba(220,234,19,0.4)"
href="/licenses/gplv2">
GPLv2
</a>
@@ -315,10 +323,10 @@ Python">
<a
class="term-link"
id="licenses_gplv2"
style="background:rgba(220,234,19,0.4)"
href="/licenses/gplv2">
GPLv2
id="licenses_mit"
style="background:rgba(122,188,26,0.4)"
href="/licenses/mit">
MIT
</a>
@@ -373,8 +381,8 @@ Python">
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/">homepage</a></li>
<li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li>
<li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li>
<li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li>
</ul>
</section>
@@ -401,6 +409,32 @@ Python">
<li>
<strong>Extending SAT Solvers to Cryptographic Problems</strong>
@@ -424,48 +458,6 @@ Python">
</ul>
</section>
@@ -473,7 +465,9 @@ Python">
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+CryptoMiniSat&body=Describe+your+problem+or+suggested+update+for+the+page+%22CryptoMiniSat%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20CryptoMiniSat" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -490,6 +484,7 @@ Python">
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

51
tools/sat-smt/cvc4/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/cvc4/">
<meta property="og:url" content="https://example.org/tools/sat-smt/cvc4/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/cvc4/">
<link rel="canonical" href="https://example.org/tools/sat-smt/cvc4/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -369,7 +377,7 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5">
<span style="display:none">]</span>
</div>
cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5">cvc5</a></p>
cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p>
</section>
@@ -392,12 +400,6 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href
@@ -405,11 +407,11 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href
<strong>CVC4</strong>
(2011)
(July 2011)
by Barrett, Clark W. et. al.
| Appears in <em>Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings</em>
| Appears in <em>CAV 2011</em>
(171-177)
| Volume 6806
@@ -439,16 +441,6 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href
@@ -467,7 +459,9 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+cvc4&body=Describe+your+problem+or+suggested+update+for+the+page+%22cvc4%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20cvc4" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -484,6 +478,7 @@ cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

45
tools/sat-smt/cvc5/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="cvc5">
<meta property="og:description" content="cvc5 is an automatic theorem prover for SMT problems.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/cvc5/">
<meta property="og:url" content="https://example.org/tools/sat-smt/cvc5/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/cvc5/">
<link rel="canonical" href="https://example.org/tools/sat-smt/cvc5/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -376,8 +384,6 @@
<li>
<strong>cvc5: A Versatile and Industrial-Strength SMT Solver</strong>
@@ -415,20 +421,6 @@
@@ -447,7 +439,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+cvc5&body=Describe+your+problem+or+suggested+update+for+the+page+%22cvc5%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20cvc5" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -464,6 +458,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

29
tools/sat-smt/dreal/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/dreal/">
<meta property="og:url" content="https://example.org/tools/sat-smt/dreal/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/dreal/">
<link rel="canonical" href="https://example.org/tools/sat-smt/dreal/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ dReal is an automated reasoning tool. It focuses on solving problems that can be
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -266,7 +274,9 @@ dReal is an automated reasoning tool. It focuses on solving problems that can be
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+dReal&body=Describe+your+problem+or+suggested+update+for+the+page+%22dReal%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20dReal" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -283,6 +293,7 @@ dReal is an automated reasoning tool. It focuses on solving problems that can be
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

29
tools/sat-smt/glucose/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Glucose">
<meta property="og:description" content="Glucose is a SAT solver.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/glucose/">
<meta property="og:url" content="https://example.org/tools/sat-smt/glucose/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/glucose/">
<link rel="canonical" href="https://example.org/tools/sat-smt/glucose/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -323,7 +331,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Glucose&body=Describe+your+problem+or+suggested+update+for+the+page+%22Glucose%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Glucose" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -340,6 +350,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

936
tools/sat-smt/index.html
View File

File diff suppressed because it is too large Load Diff

112
tools/sat-smt/index.xml
View File

@@ -1,159 +1,159 @@
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>All SAT &amp; SMT Tools on Formal Methods Tools</title>
<link>http://localhost:1313/tools/sat-smt/</link>
<description>Recent content in All SAT &amp; SMT Tools on Formal Methods Tools</description>
<title>SAT &amp; SMT Tools on Formal Methods Tools</title>
<link>https://example.org/tools/sat-smt/</link>
<description>Recent content in SAT &amp; SMT Tools on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="http://localhost:1313/tools/sat-smt/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="https://example.org/tools/sat-smt/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>Bitwuzla</title>
<link>http://localhost:1313/tools/sat-smt/bitwuzla/</link>
<link>https://example.org/tools/sat-smt/bitwuzla/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/bitwuzla/</guid>
<guid>https://example.org/tools/sat-smt/bitwuzla/</guid>
<description>&lt;p&gt;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.&lt;/p&gt;</description>
</item>
<item>
<title>Boolector</title>
<link>http://localhost:1313/tools/sat-smt/boolector/</link>
<link>https://example.org/tools/sat-smt/boolector/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/boolector/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2024&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.&#xA;Succeeded by &lt;a href=&#34;../bitwuzla&#34;&gt;Bitwuzla&lt;/a&gt;&lt;/p&gt;</description>
<guid>https://example.org/tools/sat-smt/boolector/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2024&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.&#xA;Succeeded by &lt;a href=&#34;../bitwuzla&#34; &gt;Bitwuzla&lt;/a&gt;&lt;/p&gt;</description>
</item>
<item>
<title>Colibri</title>
<link>http://localhost:1313/tools/sat-smt/colibri/</link>
<link>https://example.org/tools/sat-smt/colibri/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/colibri/</guid>
<guid>https://example.org/tools/sat-smt/colibri/</guid>
<description>&lt;p&gt;Colibri is an SMT solver.&lt;/p&gt;</description>
</item>
<item>
<title>CryptoMiniSat</title>
<link>http://localhost:1313/tools/sat-smt/cryptominisat/</link>
<link>https://example.org/tools/sat-smt/cryptominisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/cryptominisat/</guid>
<description>&lt;p&gt;CryptoMiniSat is a SAT solver.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ Namespace:&lt;/strong&gt; Documentation on &lt;a href=&#34;https://www.msoos.org/cryptominisat5/&#34;&gt;homepage&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python package:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/pycryptosat/&#34;&gt;PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/cryptominisat/</guid>
<description>&lt;p&gt;CryptoMiniSat is a SAT solver.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ Namespace:&lt;/strong&gt; Documentation on &lt;a href=&#34;https://www.msoos.org/cryptominisat5/&#34; target=&#34;_blank&#34; &gt;homepage&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python package:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/pycryptosat/&#34; target=&#34;_blank&#34; &gt;PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>cvc4</title>
<link>http://localhost:1313/tools/sat-smt/cvc4/</link>
<link>https://example.org/tools/sat-smt/cvc4/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/cvc4/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2021&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;cvc4 is an automatic theorem prover for SMT problems. It is succeeded by &lt;a href=&#34;../cvc5&#34;&gt;cvc5&lt;/a&gt;&lt;/p&gt;</description>
<guid>https://example.org/tools/sat-smt/cvc4/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2021&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;cvc4 is an automatic theorem prover for SMT problems. It is succeeded by &lt;a href=&#34;../cvc5&#34; &gt;cvc5&lt;/a&gt;&lt;/p&gt;</description>
</item>
<item>
<title>cvc5</title>
<link>http://localhost:1313/tools/sat-smt/cvc5/</link>
<link>https://example.org/tools/sat-smt/cvc5/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/cvc5/</guid>
<guid>https://example.org/tools/sat-smt/cvc5/</guid>
<description>&lt;p&gt;cvc5 is an automatic theorem prover for SMT problems.&lt;/p&gt;</description>
</item>
<item>
<title>dReal</title>
<link>http://localhost:1313/tools/sat-smt/dreal/</link>
<link>https://example.org/tools/sat-smt/dreal/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/dreal/</guid>
<guid>https://example.org/tools/sat-smt/dreal/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2023&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;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.&lt;/p&gt;</description>
</item>
<item>
<title>Glucose</title>
<link>http://localhost:1313/tools/sat-smt/glucose/</link>
<link>https://example.org/tools/sat-smt/glucose/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/glucose/</guid>
<guid>https://example.org/tools/sat-smt/glucose/</guid>
<description>&lt;p&gt;Glucose is a SAT solver.&lt;/p&gt;</description>
</item>
<item>
<title>Lingeling</title>
<link>http://localhost:1313/tools/sat-smt/lingeling/</link>
<link>https://example.org/tools/sat-smt/lingeling/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/lingeling/</guid>
<guid>https://example.org/tools/sat-smt/lingeling/</guid>
<description>&lt;p&gt;Lingeling is a SAT solver.&lt;/p&gt;</description>
</item>
<item>
<title>MathSAT</title>
<link>http://localhost:1313/tools/sat-smt/mathsat/</link>
<link>https://example.org/tools/sat-smt/mathsat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/mathsat/</guid>
<guid>https://example.org/tools/sat-smt/mathsat/</guid>
<description>&lt;p&gt;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &lt;span style=&#34;color: rgb(226, 181, 59); font-size: 1rem;&#34;&gt;Closed-Source Tool&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;]&amp;nbsp;&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.&lt;/p&gt;</description>
</item>
<item>
<title>MiniSat</title>
<link>http://localhost:1313/tools/sat-smt/minisat/</link>
<link>https://example.org/tools/sat-smt/minisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/minisat/</guid>
<guid>https://example.org/tools/sat-smt/minisat/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2013&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.&lt;/p&gt;</description>
</item>
<item>
<title>OpenSMT</title>
<link>http://localhost:1313/tools/sat-smt/opensmt/</link>
<link>https://example.org/tools/sat-smt/opensmt/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/opensmt/</guid>
<description>&lt;p&gt;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 &lt;a href=&#34;http://localhost:1313/tools/minisat&#34;&gt;MiniSAT&lt;/a&gt;.&lt;/p&gt;</description>
<guid>https://example.org/tools/sat-smt/opensmt/</guid>
<description>&lt;p&gt;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 &lt;a href=&#34;https://example.org/tools/minisat&#34; &gt;MiniSAT&lt;/a&gt;.&lt;/p&gt;</description>
</item>
<item>
<title>ParaFROST</title>
<link>http://localhost:1313/tools/sat-smt/parafrost/</link>
<link>https://example.org/tools/sat-smt/parafrost/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/parafrost/</guid>
<description>&lt;p&gt;ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34;&gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34;&gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34;&gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34;&gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34;&gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34;&gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34;&gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/parafrost/</guid>
<description>&lt;p&gt;ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Q3B</title>
<link>http://localhost:1313/tools/sat-smt/q3b/</link>
<link>https://example.org/tools/sat-smt/q3b/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/q3b/</guid>
<guid>https://example.org/tools/sat-smt/q3b/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2023&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.&lt;/p&gt;</description>
</item>
<item>
<title>Riss</title>
<link>http://localhost:1313/tools/sat-smt/riss/</link>
<link>https://example.org/tools/sat-smt/riss/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/riss/</guid>
<guid>https://example.org/tools/sat-smt/riss/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2017&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Riss is a SAT solving tool collection.&lt;/p&gt;</description>
</item>
<item>
<title>SMT-RAT</title>
<link>http://localhost:1313/tools/sat-smt/smt-rat/</link>
<link>https://example.org/tools/sat-smt/smt-rat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/smt-rat/</guid>
<description>&lt;p&gt;SMT-RAT is an SMT Real Algebra Toolbox.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25&#34;&gt;C++ API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/smt-rat/</guid>
<description>&lt;p&gt;SMT-RAT is an SMT Real Algebra Toolbox.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25&#34; target=&#34;_blank&#34; &gt;C++ API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>SMTInterpol</title>
<link>http://localhost:1313/tools/sat-smt/smtinterpol/</link>
<link>https://example.org/tools/sat-smt/smtinterpol/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/smtinterpol/</guid>
<description>&lt;p&gt;SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html&#34;&gt;Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/smtinterpol/</guid>
<description>&lt;p&gt;SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html&#34; target=&#34;_blank&#34; &gt;Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>STP</title>
<link>http://localhost:1313/tools/sat-smt/stp/</link>
<link>https://example.org/tools/sat-smt/stp/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/stp/</guid>
<description>&lt;p&gt;STP is a constraint solver for quantifier-free bitvectors.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#c-library-usage&#34;&gt;stp C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#python-usage&#34;&gt;stp PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/stp/</guid>
<description>&lt;p&gt;STP is a constraint solver for quantifier-free bitvectors.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#c-library-usage&#34; target=&#34;_blank&#34; &gt;stp C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#python-usage&#34; target=&#34;_blank&#34; &gt;stp PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>veriT</title>
<link>http://localhost:1313/tools/sat-smt/verit/</link>
<link>https://example.org/tools/sat-smt/verit/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/verit/</guid>
<guid>https://example.org/tools/sat-smt/verit/</guid>
<description>&lt;p&gt;veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.&lt;/p&gt;</description>
</item>
<item>
<title>Yices 2</title>
<link>http://localhost:1313/tools/sat-smt/yices/</link>
<link>https://example.org/tools/sat-smt/yices/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/yices/</guid>
<description>&lt;p&gt;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.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;General API:&lt;/strong&gt; &lt;a href=&#34;https://yices.csl.sri.com/doc/index.html&#34;&gt;Yices API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/yices/&#34;&gt;yices2 PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/yices2&#34;&gt;yices2 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/yices/</guid>
<description>&lt;p&gt;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.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;General API:&lt;/strong&gt; &lt;a href=&#34;https://yices.csl.sri.com/doc/index.html&#34; target=&#34;_blank&#34; &gt;Yices API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/yices/&#34; target=&#34;_blank&#34; &gt;yices2 PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/yices2&#34; target=&#34;_blank&#34; &gt;yices2 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<link>https://example.org/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34;&gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34;&gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34;&gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34;&gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34;&gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34;&gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34;&gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
<guid>https://example.org/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>
</rss>

31
tools/sat-smt/lingeling/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Lingeling">
<meta property="og:description" content="Lingeling is a SAT solver.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/lingeling/">
<meta property="og:url" content="https://example.org/tools/sat-smt/lingeling/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/lingeling/">
<link rel="canonical" href="https://example.org/tools/sat-smt/lingeling/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -60,7 +68,7 @@
<div id="page-header">
<h1>Lingeling</h1>
<span class="subtitle">SMT Solver</span>
<span class="subtitle">SAT Solver</span>
@@ -276,7 +284,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Lingeling&body=Describe+your+problem+or+suggested+update+for+the+page+%22Lingeling%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Lingeling" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -293,6 +303,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

45
tools/sat-smt/mathsat/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -20,16 +20,16 @@
]&nbsp;
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/mathsat/">
<meta property="og:url" content="https://example.org/tools/sat-smt/mathsat/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/mathsat/">
<link rel="canonical" href="https://example.org/tools/sat-smt/mathsat/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -41,6 +41,14 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -144,10 +152,10 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<a
class="term-link"
id="developers_fondazione-bruno-kessler"
style="background:rgba(8,170,192,0.4)"
href="/developers/fondazione-bruno-kessler">
Fondazione Bruno Kessler
id="developers_disi-university-of-trento"
style="background:rgba(225,19,233,0.4)"
href="/developers/disi-university-of-trento">
DISI-University of Trento
</a>
@@ -161,10 +169,10 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<a
class="term-link"
id="developers_disi-university-of-trento"
style="background:rgba(225,19,233,0.4)"
href="/developers/disi-university-of-trento">
DISI-University of Trento
id="developers_fondazione-bruno-kessler"
style="background:rgba(8,170,192,0.4)"
href="/developers/fondazione-bruno-kessler">
Fondazione Bruno Kessler
</a>
@@ -303,7 +311,9 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+MathSAT&body=Describe+your+problem+or+suggested+update+for+the+page+%22MathSAT%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20MathSAT" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -320,6 +330,7 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

29
tools/sat-smt/minisat/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/minisat/">
<meta property="og:url" content="https://example.org/tools/sat-smt/minisat/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/minisat/">
<link rel="canonical" href="https://example.org/tools/sat-smt/minisat/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -313,7 +321,9 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+MiniSat&body=Describe+your+problem+or+suggested+update+for+the+page+%22MiniSat%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20MiniSat" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -330,6 +340,7 @@ MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

31
tools/sat-smt/opensmt/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="OpenSMT">
<meta property="og:description" content="OpenSMT is a compact and open-source SMT-solver written in C&#43;&#43;, with the main goal of making SMT-Solvers easy to understand and use as a computational engine">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/opensmt/">
<meta property="og:url" content="https://example.org/tools/sat-smt/opensmt/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/opensmt/">
<link rel="canonical" href="https://example.org/tools/sat-smt/opensmt/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -296,7 +304,7 @@
<section>
<h2>Description</h2>
<p>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 <a href="/tools/minisat">MiniSAT</a>.</p>
<p>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 <a href="/tools/minisat" >MiniSAT</a>.</p>
</section>
@@ -306,7 +314,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+OpenSMT&body=Describe+your+problem+or+suggested+update+for+the+page+%22OpenSMT%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20OpenSMT" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -323,6 +333,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

93
tools/sat-smt/parafrost/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="ParaFROST">
<meta property="og:description" content="ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/parafrost/">
<meta property="og:url" content="https://example.org/tools/sat-smt/parafrost/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/parafrost/">
<link rel="canonical" href="https://example.org/tools/sat-smt/parafrost/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -138,10 +146,10 @@
<a
class="term-link"
id="developers_eindhoven-university-of-technology"
style="background:rgba(171,15,81,0.4)"
href="/developers/eindhoven-university-of-technology">
Eindhoven University of Technology
id="developers_albert-ludwigs-universit%C3%A4t"
style="background:rgba(15,60,110,0.4)"
href="/developers/albert-ludwigs-universit%C3%A4t">
Albert-Ludwigs-Universität
</a>
@@ -155,10 +163,10 @@
<a
class="term-link"
id="developers_albert-ludwigs-universit%C3%A4t"
style="background:rgba(15,60,110,0.4)"
href="/developers/albert-ludwigs-universit%C3%A4t">
Albert-Ludwigs-Universität
id="developers_eindhoven-university-of-technology"
style="background:rgba(171,15,81,0.4)"
href="/developers/eindhoven-university-of-technology">
Eindhoven University of Technology
</a>
@@ -362,12 +370,12 @@
<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">Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li>
<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>
</section>
@@ -395,6 +403,16 @@
@@ -433,32 +451,6 @@
</ul>
</section>
@@ -466,7 +458,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+ParaFROST&body=Describe+your+problem+or+suggested+update+for+the+page+%22ParaFROST%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20ParaFROST" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -483,6 +477,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

45
tools/sat-smt/q3b/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/q3b/">
<meta property="og:url" content="https://example.org/tools/sat-smt/q3b/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/q3b/">
<link rel="canonical" href="https://example.org/tools/sat-smt/q3b/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -384,22 +392,6 @@ Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p>
@@ -412,7 +404,9 @@ Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p>
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Q3B&body=Describe+your+problem+or+suggested+update+for+the+page+%22Q3B%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Q3B" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -429,6 +423,7 @@ Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p>
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

29
tools/sat-smt/riss/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -24,16 +24,16 @@
]
Riss is a SAT solving tool collection.">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/riss/">
<meta property="og:url" content="https://example.org/tools/sat-smt/riss/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/riss/">
<link rel="canonical" href="https://example.org/tools/sat-smt/riss/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -45,6 +45,14 @@ Riss is a SAT solving tool collection.">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -294,7 +302,9 @@ Riss is a SAT solving tool collection.</p>
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Riss&body=Describe+your+problem+or+suggested+update+for+the+page+%22Riss%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Riss" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -311,6 +321,7 @@ Riss is a SAT solving tool collection.</p>
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

79
tools/sat-smt/smt-rat/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -19,16 +19,16 @@ This tool is available through the following interfaces:
C&#43;&#43; API: C&#43;&#43; API Reference
">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/smt-rat/">
<meta property="og:url" content="https://example.org/tools/sat-smt/smt-rat/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/smt-rat/">
<link rel="canonical" href="https://example.org/tools/sat-smt/smt-rat/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -40,6 +40,14 @@ C&#43;&#43; API: C&#43;&#43; API Reference
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -112,10 +120,10 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<a
class="term-link"
id="applications_smt-solver"
style="background:rgba(190,107,118,0.4)"
href="/applications/smt-solver">
SMT Solver
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
@@ -129,10 +137,10 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
id="applications_smt-solver"
style="background:rgba(190,107,118,0.4)"
href="/applications/smt-solver">
SMT Solver
</a>
@@ -231,10 +239,10 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<a
class="term-link"
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
id="interfaces_c&#43;&#43;"
style="background:rgba(246,248,124,0.4)"
href="/interfaces/c&#43;&#43;">
C&#43;&#43;
</a>
@@ -248,10 +256,10 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<a
class="term-link"
id="interfaces_c&#43;&#43;"
style="background:rgba(246,248,124,0.4)"
href="/interfaces/c&#43;&#43;">
C&#43;&#43;
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
</a>
@@ -339,7 +347,7 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<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://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25">C++ API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li>
</ul>
</section>
@@ -365,20 +373,6 @@ C&#43;&#43; API: C&#43;&#43; API Reference
@@ -426,8 +420,6 @@ C&#43;&#43; API: C&#43;&#43; API Reference
@@ -438,7 +430,9 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+SMT-RAT&body=Describe+your+problem+or+suggested+update+for+the+page+%22SMT-RAT%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20SMT-RAT" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -455,6 +449,7 @@ C&#43;&#43; API: C&#43;&#43; API Reference
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

47
tools/sat-smt/smtinterpol/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -16,16 +16,16 @@
<meta property="og:description" content="SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
APIs and Bindings
This tool is available through the following">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/smtinterpol/">
<meta property="og:url" content="https://example.org/tools/sat-smt/smtinterpol/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/smtinterpol/">
<link rel="canonical" href="https://example.org/tools/sat-smt/smtinterpol/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -37,6 +37,14 @@ This tool is available through the following">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -319,7 +327,7 @@ This tool is available through the following">
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html">Java API Reference</a></li>
<li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li>
</ul>
</section>
@@ -349,16 +357,6 @@ This tool is available through the following">
@@ -399,12 +397,6 @@ This tool is available through the following">
@@ -417,7 +409,9 @@ This tool is available through the following">
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+SMTInterpol&body=Describe+your+problem+or+suggested+update+for+the+page+%22SMTInterpol%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20SMTInterpol" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -434,6 +428,7 @@ This tool is available through the following">
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

113
tools/sat-smt/stp/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -18,16 +18,16 @@ APIs and Bindings
This tool is available through the following interfaces:
C API: stp C API">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/stp/">
<meta property="og:url" content="https://example.org/tools/sat-smt/stp/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/stp/">
<link rel="canonical" href="https://example.org/tools/sat-smt/stp/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -39,6 +39,14 @@ C API: stp C API">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -178,10 +186,10 @@ C API: stp C API">
<a
class="term-link"
id="developers_university-of-illinois"
style="background:rgba(92,216,117,0.4)"
href="/developers/university-of-illinois">
University of Illinois
id="developers_stanford-university"
style="background:rgba(38,159,198,0.4)"
href="/developers/stanford-university">
Stanford University
</a>
@@ -195,10 +203,10 @@ C API: stp C API">
<a
class="term-link"
id="developers_stanford-university"
style="background:rgba(38,159,198,0.4)"
href="/developers/stanford-university">
Stanford University
id="developers_university-of-illinois"
style="background:rgba(92,216,117,0.4)"
href="/developers/university-of-illinois">
University of Illinois
</a>
@@ -264,10 +272,10 @@ C API: stp C API">
<a
class="term-link"
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
id="interfaces_c"
style="background:rgba(13,97,248,0.4)"
href="/interfaces/c">
C
</a>
@@ -281,10 +289,10 @@ C API: stp C API">
<a
class="term-link"
id="interfaces_c"
style="background:rgba(13,97,248,0.4)"
href="/interfaces/c">
C
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
</a>
@@ -389,8 +397,8 @@ C API: stp C API">
<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">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
<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>
</section>
@@ -421,21 +429,22 @@ C API: stp C API">
<li>
<strong>EXE: Automatically Generating Inputs of Death</strong>
(October 2006)
by Cadar, Cristian et. al.
| Appears in <em>CCS 2006</em>
| Published by ACM
| <a href="https://doi.org/10.1145/1455518.1455522" target="_blank" rel="noopener">10.1145/1455518.1455522</a>
</li>
@@ -464,23 +473,6 @@ C API: stp C API">
<li>
<strong>EXE: Automatically Generating Inputs of Death</strong>
(October 2006)
by Cadar, Cristian et. al.
| Appears in <em>CCS 2006</em>
| Published by ACM
| <a href="https://doi.org/10.1145/1455518.1455522" target="_blank" rel="noopener">10.1145/1455518.1455522</a>
</li>
@@ -506,7 +498,9 @@ C API: stp C API">
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+STP&body=Describe+your+problem+or+suggested+update+for+the+page+%22STP%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20STP" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -523,6 +517,7 @@ C API: stp C API">
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

61
tools/sat-smt/verit/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="veriT">
<meta property="og:description" content="veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning,">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/verit/">
<meta property="og:url" content="https://example.org/tools/sat-smt/verit/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/verit/">
<link rel="canonical" href="https://example.org/tools/sat-smt/verit/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -191,10 +199,10 @@
<a
class="term-link"
id="inputs_smtlib2"
style="background:rgba(108,44,180,0.4)"
href="/inputs/smtlib2">
SMTLIB2
id="inputs_dimacs"
style="background:rgba(190,57,177,0.4)"
href="/inputs/dimacs">
DIMACS
</a>
@@ -208,10 +216,10 @@
<a
class="term-link"
id="inputs_dimacs"
style="background:rgba(190,57,177,0.4)"
href="/inputs/dimacs">
DIMACS
id="inputs_smtlib2"
style="background:rgba(108,44,180,0.4)"
href="/inputs/smtlib2">
SMTLIB2
</a>
@@ -363,20 +371,6 @@
@@ -417,8 +411,6 @@
</ul>
</section>
@@ -426,7 +418,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+veriT&body=Describe+your+problem+or+suggested+update+for+the+page+%22veriT%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20veriT" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -443,6 +437,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

99
tools/sat-smt/yices/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -14,16 +14,16 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Yices 2">
<meta property="og:description" content="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">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/yices/">
<meta property="og:url" content="https://example.org/tools/sat-smt/yices/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/yices/">
<link rel="canonical" href="https://example.org/tools/sat-smt/yices/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -35,6 +35,14 @@
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -107,10 +115,10 @@
<a
class="term-link"
id="applications_smt-solver"
style="background:rgba(190,107,118,0.4)"
href="/applications/smt-solver">
SMT Solver
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
@@ -124,10 +132,10 @@
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
id="applications_smt-solver"
style="background:rgba(190,107,118,0.4)"
href="/applications/smt-solver">
SMT Solver
</a>
@@ -368,9 +376,9 @@
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li>
</ul>
</section>
@@ -400,38 +408,6 @@
@@ -457,6 +433,22 @@
</li>
@@ -469,7 +461,9 @@
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Yices&#43;2&body=Describe+your+problem+or+suggested+update+for+the+page+%22Yices%202%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Yices&#43;2" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -486,6 +480,7 @@
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>

243
tools/sat-smt/z3/index.html
View File

@@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<head>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@@ -18,16 +18,16 @@ APIs and Bindings
This tool is available through the following interfaces:
C API:">
<meta property="og:url" content="http://localhost:1313/tools/sat-smt/z3/">
<meta property="og:url" content="https://example.org/tools/sat-smt/z3/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="http://localhost:1313/tools/sat-smt/z3/">
<link rel="canonical" href="https://example.org/tools/sat-smt/z3/">
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
<link rel="manifest" href='https://example.org/site.webmanifest'>
<link rel="stylesheet" href="http://localhost:1313/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB&#43;fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
<link rel="stylesheet" href="https://example.org/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
@@ -39,6 +39,14 @@ C API:">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
@@ -111,6 +119,23 @@ C API:">
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
<a
class="term-link"
id="applications_smt-solver"
@@ -137,23 +162,6 @@ C API:">
</a>
<a
class="term-link"
id="applications_sat-solver"
style="background:rgba(197,220,18,0.4)"
href="/applications/sat-solver">
SAT Solver
</a>
</td>
</tr>
@@ -216,10 +224,10 @@ C API:">
<a
class="term-link"
id="inputs_smtlib2"
style="background:rgba(108,44,180,0.4)"
href="/inputs/smtlib2">
SMTLIB2
id="inputs_dimacs"
style="background:rgba(190,57,177,0.4)"
href="/inputs/dimacs">
DIMACS
</a>
@@ -233,10 +241,10 @@ C API:">
<a
class="term-link"
id="inputs_dimacs"
style="background:rgba(190,57,177,0.4)"
href="/inputs/dimacs">
DIMACS
id="inputs_smtlib2"
style="background:rgba(108,44,180,0.4)"
href="/inputs/smtlib2">
SMTLIB2
</a>
@@ -266,44 +274,10 @@ C API:">
<a
class="term-link"
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
</a>
<a
class="term-link"
id="interfaces_python"
style="background:rgba(167,245,243,0.4)"
href="/interfaces/python">
Python
</a>
<a
class="term-link"
id="interfaces_rust"
style="background:rgba(245,226,101,0.4)"
href="/interfaces/rust">
Rust
id="interfaces_.net"
style="background:rgba(48,60,176,0.4)"
href="/interfaces/.net">
.NET
</a>
@@ -349,6 +323,23 @@ C API:">
<a
class="term-link"
id="interfaces_cli"
style="background:rgba(145,175,87,0.4)"
href="/interfaces/cli">
CLI
</a>
<a
class="term-link"
id="interfaces_java"
@@ -368,10 +359,10 @@ C API:">
<a
class="term-link"
id="interfaces_.net"
style="background:rgba(48,60,176,0.4)"
href="/interfaces/.net">
.NET
id="interfaces_online"
style="background:rgba(84,246,100,0.4)"
href="/interfaces/online">
Online
</a>
@@ -385,10 +376,27 @@ C API:">
<a
class="term-link"
id="interfaces_online"
style="background:rgba(84,246,100,0.4)"
href="/interfaces/online">
Online
id="interfaces_python"
style="background:rgba(167,245,243,0.4)"
href="/interfaces/python">
Python
</a>
<a
class="term-link"
id="interfaces_rust"
style="background:rgba(245,226,101,0.4)"
href="/interfaces/rust">
Rust
</a>
@@ -476,12 +484,12 @@ C API:">
<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">Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li>
<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>
</section>
@@ -511,44 +519,6 @@ C API:">
@@ -573,6 +543,28 @@ C API:">
</ul>
</section>
@@ -580,7 +572,9 @@ C API:">
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new?title=Update+Page+For+Z3&body=Describe+your+problem+or+suggested+update+for+the+page+%22Z3%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20Z3" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
@@ -597,6 +591,7 @@ C API:">
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>