Wrap up SAT/SMT
This commit is contained in:
452
tools/sat-smt/bitwuzla/index.html
Normal file
452
tools/sat-smt/bitwuzla/index.html
Normal file
@@ -0,0 +1,452 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Bitwuzla | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/bitwuzla/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/bitwuzla/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Bitwuzla</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://bitwuzla.github.io" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/bitwuzla/bitwuzla" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_stanford-university"
|
||||
style="background:rgba(38,159,198,0.4)"
|
||||
href="/developers/stanford-university">
|
||||
Stanford University
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>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.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Bitwuzla</strong>
|
||||
|
||||
|
||||
(2023)
|
||||
|
||||
|
||||
by Aina Niemetz et. al.
|
||||
| Appears in <em>CAV 2023</em>
|
||||
(3-17)
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-031-37703-7_1" target="_blank" rel="noopener">10.1007/978-3-031-37703-7_1</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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+Bitwuzla&body=Describe+your+problem+or+suggested+update+for+the+page+%22Bitwuzla%22.">issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork">pull request</a>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
490
tools/sat-smt/boolector/index.html
Normal file
490
tools/sat-smt/boolector/index.html
Normal file
@@ -0,0 +1,490 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Boolector | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Boolector">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2024
|
||||
|
||||
]
|
||||
|
||||
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/boolector/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/boolector/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Boolector</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://boolector.github.io/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/boolector/boolector" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_stanford-university"
|
||||
style="background:rgba(38,159,198,0.4)"
|
||||
href="/developers/stanford-university">
|
||||
Stanford University
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span>
|
||||
|
||||
<span style="display:none">]</span>
|
||||
</div>
|
||||
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
|
||||
Succeeded by <a href="../bitwuzla">Bitwuzla</a></p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Boolector 2.0</strong>
|
||||
|
||||
|
||||
(2014)
|
||||
|
||||
|
||||
|
||||
|
||||
(53-58)
|
||||
| Appears in <em>J. Satisf. Boolean Model. Comput.</em>
|
||||
| Volume 9
|
||||
|
||||
| <a href="https://doi.org/10.3233/sat190101" target="_blank" rel="noopener">10.3233/sat190101</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
330
tools/sat-smt/colibri/index.html
Normal file
330
tools/sat-smt/colibri/index.html
Normal file
@@ -0,0 +1,330 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Colibri | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/colibri/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/colibri/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Colibri</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://colibri.frama-c.com/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://git.frama-c.com/pub/colibrics/-/tree/master" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_cea"
|
||||
style="background:rgba(69,53,67,0.4)"
|
||||
href="/developers/cea">
|
||||
CEA
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Colibri is an SMT solver.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
497
tools/sat-smt/cryptominisat/index.html
Normal file
497
tools/sat-smt/cryptominisat/index.html
Normal file
@@ -0,0 +1,497 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>CryptoMiniSat | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="CryptoMiniSat">
|
||||
<meta property="og:description" content="CryptoMiniSat is a SAT solver.
|
||||
APIs and Bindings
|
||||
This tool is available through the following interfaces:
|
||||
|
||||
C++ Namespace: Documentation on homepage
|
||||
Python">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/cryptominisat/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/cryptominisat/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>CryptoMiniSat</h1>
|
||||
|
||||
<span class="subtitle">SAT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://www.msoos.org/cryptominisat5/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/msoos/cryptominisat" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_inria-rh%C3%B4ne-alpes"
|
||||
style="background:rgba(20,228,136,0.4)"
|
||||
href="/developers/inria-rh%C3%B4ne-alpes">
|
||||
INRIA Rhône-Alpes
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-virginia"
|
||||
style="background:rgba(207,199,132,0.4)"
|
||||
href="/developers/university-of-virginia">
|
||||
University of Virginia
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_cnf"
|
||||
style="background:rgba(168,102,205,0.4)"
|
||||
href="/inputs/cnf">
|
||||
CNF
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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_c++"
|
||||
style="background:rgba(246,248,124,0.4)"
|
||||
href="/interfaces/c++">
|
||||
C++
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv2"
|
||||
style="background:rgba(220,234,19,0.4)"
|
||||
href="/licenses/gplv2">
|
||||
GPLv2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>CryptoMiniSat is a SAT solver.</p>
|
||||
<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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Extending SAT Solvers to Cryptographic Problems</strong>
|
||||
|
||||
|
||||
(2009)
|
||||
|
||||
|
||||
by Mate Soos et. al.
|
||||
| Appears in <em>SAT 2009</em>
|
||||
(244-257)
|
||||
|
||||
| Volume 5584
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-642-02777-2_24" target="_blank" rel="noopener">10.1007/978-3-642-02777-2_24</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
491
tools/sat-smt/cvc4/index.html
Normal file
491
tools/sat-smt/cvc4/index.html
Normal file
@@ -0,0 +1,491 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>cvc4 | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="cvc4">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2021
|
||||
|
||||
]
|
||||
|
||||
cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/cvc4/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/cvc4/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>cvc4</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://cvc4.github.io/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/CVC4/CVC4-archived" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
<li><a href="https://cvc4.github.io/app/" target="_blank" rel="noopener"><i class="fa-solid fa-gamepad"></i> Playground</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_stanford-university"
|
||||
style="background:rgba(38,159,198,0.4)"
|
||||
href="/developers/stanford-university">
|
||||
Stanford University
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-iowa"
|
||||
style="background:rgba(81,243,205,0.4)"
|
||||
href="/developers/university-of-iowa">
|
||||
University of Iowa
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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_online"
|
||||
style="background:rgba(84,246,100,0.4)"
|
||||
href="/interfaces/online">
|
||||
Online
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span>
|
||||
|
||||
<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>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>CVC4</strong>
|
||||
|
||||
|
||||
(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>
|
||||
(171-177)
|
||||
|
||||
| Volume 6806
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-642-22110-1_14" target="_blank" rel="noopener">10.1007/978-3-642-22110-1_14</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
471
tools/sat-smt/cvc5/index.html
Normal file
471
tools/sat-smt/cvc5/index.html
Normal file
@@ -0,0 +1,471 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>cvc5 | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/cvc5/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/cvc5/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>cvc5</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://cvc5.github.io/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/cvc5/cvc5" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
<li><a href="https://cvc5.github.io/app/" target="_blank" rel="noopener"><i class="fa-solid fa-gamepad"></i> Playground</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_stanford-university"
|
||||
style="background:rgba(38,159,198,0.4)"
|
||||
href="/developers/stanford-university">
|
||||
Stanford University
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-iowa"
|
||||
style="background:rgba(81,243,205,0.4)"
|
||||
href="/developers/university-of-iowa">
|
||||
University of Iowa
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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_online"
|
||||
style="background:rgba(84,246,100,0.4)"
|
||||
href="/interfaces/online">
|
||||
Online
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>cvc5 is an automatic theorem prover for SMT problems.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>cvc5: A Versatile and Industrial-Strength SMT Solver</strong>
|
||||
|
||||
|
||||
(2022)
|
||||
|
||||
|
||||
by Barbosa, Haniel et. al.
|
||||
| Appears in <em>TACAS 2022</em>
|
||||
(415-442)
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-030-99524-9_24" target="_blank" rel="noopener">10.1007/978-3-030-99524-9_24</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
290
tools/sat-smt/dreal/index.html
Normal file
290
tools/sat-smt/dreal/index.html
Normal file
@@ -0,0 +1,290 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>dReal | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="dReal">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2023
|
||||
|
||||
]
|
||||
|
||||
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/dreal/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/dreal/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>dReal</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://dreal.github.io/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/dreal/dreal4" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_apache-2.0"
|
||||
style="background:rgba(242,244,241,0.4)"
|
||||
href="/licenses/apache-2.0">
|
||||
Apache-2.0
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
|
||||
|
||||
<span style="display:none">]</span>
|
||||
</div>
|
||||
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
347
tools/sat-smt/glucose/index.html
Normal file
347
tools/sat-smt/glucose/index.html
Normal file
@@ -0,0 +1,347 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Glucose | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/glucose/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/glucose/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Glucose</h1>
|
||||
|
||||
<span class="subtitle">SAT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://www.labri.fr/perso/lsimon/research/glucose/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/audemard/glucose" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_gilles-audemard"
|
||||
style="background:rgba(114,89,108,0.4)"
|
||||
href="/developers/gilles-audemard">
|
||||
Gilles Audemard
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_laurent-simon"
|
||||
style="background:rgba(152,167,32,0.4)"
|
||||
href="/developers/laurent-simon">
|
||||
Laurent Simon
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_cnf"
|
||||
style="background:rgba(168,102,205,0.4)"
|
||||
href="/inputs/cnf">
|
||||
CNF
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Glucose is a SAT solver.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
2925
tools/sat-smt/index.html
Normal file
2925
tools/sat-smt/index.html
Normal file
File diff suppressed because it is too large
Load Diff
159
tools/sat-smt/index.xml
Normal file
159
tools/sat-smt/index.xml
Normal file
@@ -0,0 +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 & SMT Tools on Formal Methods Tools</title>
|
||||
<link>https://example.org/tools/sat-smt/</link>
|
||||
<description>Recent content in All SAT & 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="https://example.org/tools/sat-smt/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Bitwuzla</title>
|
||||
<link>https://example.org/tools/sat-smt/bitwuzla/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/bitwuzla/</guid>
|
||||
<description><p>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.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Boolector</title>
|
||||
<link>https://example.org/tools/sat-smt/boolector/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/boolector/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span>
 
 <span style="display:none">]</span>
</div>
Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
Succeeded by <a href="../bitwuzla">Bitwuzla</a></p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Colibri</title>
|
||||
<link>https://example.org/tools/sat-smt/colibri/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/colibri/</guid>
|
||||
<description><p>Colibri is an SMT solver.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>CryptoMiniSat</title>
|
||||
<link>https://example.org/tools/sat-smt/cryptominisat/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/cryptominisat/</guid>
|
||||
<description><p>CryptoMiniSat is a SAT solver.</p>
<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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>cvc4</title>
|
||||
<link>https://example.org/tools/sat-smt/cvc4/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/cvc4/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span>
 
 <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></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>cvc5</title>
|
||||
<link>https://example.org/tools/sat-smt/cvc5/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/cvc5/</guid>
|
||||
<description><p>cvc5 is an automatic theorem prover for SMT problems.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>dReal</title>
|
||||
<link>https://example.org/tools/sat-smt/dreal/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/dreal/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
 
 <span style="display:none">]</span>
</div>
dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Glucose</title>
|
||||
<link>https://example.org/tools/sat-smt/glucose/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/glucose/</guid>
|
||||
<description><p>Glucose is a SAT solver.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Lingeling</title>
|
||||
<link>https://example.org/tools/sat-smt/lingeling/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/lingeling/</guid>
|
||||
<description><p>Lingeling is a SAT solver.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>MathSAT</title>
|
||||
<link>https://example.org/tools/sat-smt/mathsat/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/mathsat/</guid>
|
||||
<description><p><div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
 <span style="display:none">[</span>
 <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
 <span style="display:none">]&nbsp;</span>
</div>
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>MiniSat</title>
|
||||
<link>https://example.org/tools/sat-smt/minisat/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/minisat/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span>
 
 <span style="display:none">]</span>
</div>
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>OpenSMT</title>
|
||||
<link>https://example.org/tools/sat-smt/opensmt/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/opensmt/</guid>
|
||||
<description><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="https://example.org/tools/minisat">MiniSAT</a>.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>ParaFROST</title>
|
||||
<link>https://example.org/tools/sat-smt/parafrost/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/parafrost/</guid>
|
||||
<description><p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Q3B</title>
|
||||
<link>https://example.org/tools/sat-smt/q3b/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/q3b/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
 
 <span style="display:none">]</span>
</div>
Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Riss</title>
|
||||
<link>https://example.org/tools/sat-smt/riss/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/riss/</guid>
|
||||
<description><p>

<div style="display: flex; align-items: center; gap: 8px;">
 <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
 <span style="display:none">[</span>
 
 <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span>
 
 <span style="display:none">]</span>
</div>
Riss is a SAT solving tool collection.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>SMT-RAT</title>
|
||||
<link>https://example.org/tools/sat-smt/smt-rat/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/smt-rat/</guid>
|
||||
<description><p>SMT-RAT is an SMT Real Algebra Toolbox.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C++ API:</strong> <a href="https://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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>SMTInterpol</title>
|
||||
<link>https://example.org/tools/sat-smt/smtinterpol/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/smtinterpol/</guid>
|
||||
<description><p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p>
<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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>STP</title>
|
||||
<link>https://example.org/tools/sat-smt/stp/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/stp/</guid>
|
||||
<description><p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>veriT</title>
|
||||
<link>https://example.org/tools/sat-smt/verit/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/verit/</guid>
|
||||
<description><p>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.</p></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>https://example.org/tools/sat-smt/yices/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/yices/</guid>
|
||||
<description><p>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.</p>
<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>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>https://example.org/tools/sat-smt/z3/</link>
|
||||
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
|
||||
<guid>https://example.org/tools/sat-smt/z3/</guid>
|
||||
<description><p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">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>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
300
tools/sat-smt/lingeling/index.html
Normal file
300
tools/sat-smt/lingeling/index.html
Normal file
@@ -0,0 +1,300 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Lingeling | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/lingeling/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/lingeling/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Lingeling</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://fmv.jku.at/lingeling/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/arminbiere/lingeling" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Lingeling is a SAT solver.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
327
tools/sat-smt/mathsat/index.html
Normal file
327
tools/sat-smt/mathsat/index.html
Normal file
@@ -0,0 +1,327 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>MathSAT | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="MathSAT">
|
||||
<meta property="og:description" content="
|
||||
|
||||
[
|
||||
Closed-Source Tool
|
||||
]
|
||||
|
||||
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/mathsat/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/mathsat/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>MathSAT</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://mathsat.fbk.eu/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_all-rights-reserved"
|
||||
style="background:rgba(157,39,42,0.4)"
|
||||
href="/licenses/all-rights-reserved">
|
||||
All Rights Reserved
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p><div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span>
|
||||
<span style="display:none">[</span>
|
||||
<span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span>
|
||||
<span style="display:none">] </span>
|
||||
</div>
|
||||
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
337
tools/sat-smt/minisat/index.html
Normal file
337
tools/sat-smt/minisat/index.html
Normal file
@@ -0,0 +1,337 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>MiniSat | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="MiniSat">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2013
|
||||
|
||||
]
|
||||
|
||||
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/minisat/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/minisat/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>MiniSat</h1>
|
||||
|
||||
<span class="subtitle">SAT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="http://minisat.se/Main.html" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/niklasso/minisat" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_niklas-e%C3%A9n"
|
||||
style="background:rgba(29,131,44,0.4)"
|
||||
href="/developers/niklas-e%C3%A9n">
|
||||
Niklas Eén
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_niklas-s%C3%B6rensson"
|
||||
style="background:rgba(143,73,134,0.4)"
|
||||
href="/developers/niklas-s%C3%B6rensson">
|
||||
Niklas Sörensson
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span>
|
||||
|
||||
<span style="display:none">]</span>
|
||||
</div>
|
||||
MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
330
tools/sat-smt/opensmt/index.html
Normal file
330
tools/sat-smt/opensmt/index.html
Normal file
@@ -0,0 +1,330 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>OpenSMT | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/opensmt/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/opensmt/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>OpenSMT</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://verify.inf.usi.ch/opensmt" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/usi-verification-and-security/opensmt" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-lugano"
|
||||
style="background:rgba(92,207,196,0.4)"
|
||||
href="/developers/university-of-lugano">
|
||||
University of Lugano
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv3"
|
||||
style="background:rgba(182,14,173,0.4)"
|
||||
href="/licenses/gplv3">
|
||||
GPLv3
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
490
tools/sat-smt/parafrost/index.html
Normal file
490
tools/sat-smt/parafrost/index.html
Normal file
@@ -0,0 +1,490 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>ParaFROST | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/parafrost/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/parafrost/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>ParaFROST</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://github.com/muhos/ParaFROST" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv3"
|
||||
style="background:rgba(182,14,173,0.4)"
|
||||
href="/licenses/gplv3">
|
||||
GPLv3
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/techniques">
|
||||
Techniques
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="techniques_cdcl"
|
||||
style="background:rgba(227,216,97,0.4)"
|
||||
href="/techniques/cdcl">
|
||||
CDCL
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="techniques_gpu"
|
||||
style="background:rgba(82,249,236,0.4)"
|
||||
href="/techniques/gpu">
|
||||
GPU
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p>
|
||||
<h2 id="apis-and-bindings">APIs and Bindings</h2>
|
||||
<p>This tool is available through the following interfaces:</p>
|
||||
<ul>
|
||||
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Certified SAT solving with GPU accelerated inprocessing</strong>
|
||||
|
||||
|
||||
(2024)
|
||||
|
||||
|
||||
by Osama, Muhammad et. al.
|
||||
| Appears in <em>FMSD 2024</em>
|
||||
(79-118)
|
||||
|
||||
| Volume 62
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/s10703-023-00432-z" target="_blank" rel="noopener">10.1007/s10703-023-00432-z</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
436
tools/sat-smt/q3b/index.html
Normal file
436
tools/sat-smt/q3b/index.html
Normal file
@@ -0,0 +1,436 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Q3B | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Q3B">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2023
|
||||
|
||||
]
|
||||
|
||||
Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/q3b/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/q3b/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Q3B</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://github.com/martinjonas/Q3B" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_masaryk-university"
|
||||
style="background:rgba(17,222,208,0.4)"
|
||||
href="/developers/masaryk-university">
|
||||
Masaryk University
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span>
|
||||
|
||||
<span style="display:none">]</span>
|
||||
</div>
|
||||
Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams</strong>
|
||||
|
||||
|
||||
(2016)
|
||||
|
||||
|
||||
by Jonáš, Martin et. al.
|
||||
| Appears in <em>SAT 2016</em>
|
||||
(267-283)
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-319-40970-2_17" target="_blank" rel="noopener">10.1007/978-3-319-40970-2_17</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
318
tools/sat-smt/riss/index.html
Normal file
318
tools/sat-smt/riss/index.html
Normal file
@@ -0,0 +1,318 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Riss | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Riss">
|
||||
<meta property="og:description" content="
|
||||
|
||||
|
||||
|
||||
[
|
||||
|
||||
Not Maintained Since 2017
|
||||
|
||||
]
|
||||
|
||||
Riss is a SAT solving tool collection.">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/riss/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/riss/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Riss</h1>
|
||||
|
||||
<span class="subtitle">SAT Tool Collection</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://github.com/nmanthey/riss-solver" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_norbert-manthey"
|
||||
style="background:rgba(33,162,222,0.4)"
|
||||
href="/developers/norbert-manthey">
|
||||
Norbert Manthey
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_lgplv2"
|
||||
style="background:rgba(62,13,168,0.4)"
|
||||
href="/licenses/lgplv2">
|
||||
LGPLv2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_not-maintained"
|
||||
style="background:rgba(61,68,67,0.4)"
|
||||
href="/maintenance/not-maintained">
|
||||
Not Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>
|
||||
|
||||
<div style="display: flex; align-items: center; gap: 8px;">
|
||||
<span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span>
|
||||
<span style="display:none">[</span>
|
||||
|
||||
<span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span>
|
||||
|
||||
<span style="display:none">]</span>
|
||||
</div>
|
||||
Riss is a SAT solving tool collection.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
462
tools/sat-smt/smt-rat/index.html
Normal file
462
tools/sat-smt/smt-rat/index.html
Normal file
@@ -0,0 +1,462 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>SMT-RAT | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="SMT-RAT">
|
||||
<meta property="og:description" content="SMT-RAT is an SMT Real Algebra Toolbox.
|
||||
APIs and Bindings
|
||||
This tool is available through the following interfaces:
|
||||
|
||||
C++ API: C++ API Reference
|
||||
">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/smt-rat/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/smt-rat/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>SMT-RAT</h1>
|
||||
|
||||
<span class="subtitle">SMT Toolbox</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://ths-rwth.github.io/smtrat/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/ths-rwth/smtrat" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_rwth-aachen"
|
||||
style="background:rgba(3,239,109,0.4)"
|
||||
href="/developers/rwth-aachen">
|
||||
RWTH Aachen
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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_c++"
|
||||
style="background:rgba(246,248,124,0.4)"
|
||||
href="/interfaces/c++">
|
||||
C++
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>SMT-RAT is an SMT Real Algebra Toolbox.</p>
|
||||
<h2 id="apis-and-bindings">APIs and Bindings</h2>
|
||||
<p>This tool is available through the following interfaces:</p>
|
||||
<ul>
|
||||
<li><strong>C++ API:</strong> <a href="https://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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving</strong>
|
||||
|
||||
|
||||
(2015)
|
||||
|
||||
|
||||
by Corzilius, Florian et. al.
|
||||
| Appears in <em>SAT 2015</em>
|
||||
(360-368)
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-319-24318-4_26" target="_blank" rel="noopener">10.1007/978-3-319-24318-4_26</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
441
tools/sat-smt/smtinterpol/index.html
Normal file
441
tools/sat-smt/smtinterpol/index.html
Normal file
@@ -0,0 +1,441 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>SMTInterpol | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="SMTInterpol">
|
||||
<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="https://example.org/tools/sat-smt/smtinterpol/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/smtinterpol/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>SMTInterpol</h1>
|
||||
|
||||
<span class="subtitle">Interpolating SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/ultimate-pa/smtinterpol" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_university-of-freiburg"
|
||||
style="background:rgba(134,74,190,0.4)"
|
||||
href="/developers/university-of-freiburg">
|
||||
University of Freiburg
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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"
|
||||
style="background:rgba(213,35,135,0.4)"
|
||||
href="/interfaces/java">
|
||||
Java
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv3"
|
||||
style="background:rgba(182,14,173,0.4)"
|
||||
href="/licenses/gplv3">
|
||||
GPLv3
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p>
|
||||
<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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality</strong>
|
||||
|
||||
|
||||
(2021)
|
||||
|
||||
|
||||
by Henkel, Elisabeth et. al.
|
||||
| Appears in <em>SMT 2021</em>
|
||||
|
||||
|
||||
|
||||
|
||||
| <a href="#ZgotmplZ" target="_blank" rel="noopener">https://ceur-ws.org/Vol-2908/short12.pdf</a>
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
530
tools/sat-smt/stp/index.html
Normal file
530
tools/sat-smt/stp/index.html
Normal file
@@ -0,0 +1,530 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>STP | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="STP">
|
||||
<meta property="og:description" content="STP is a constraint solver for quantifier-free bitvectors.
|
||||
APIs and Bindings
|
||||
This tool is available through the following interfaces:
|
||||
|
||||
C API: stp C API">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/stp/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/stp/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>STP</h1>
|
||||
|
||||
<span class="subtitle">Simple Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://stp.github.io/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/stp/stp" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_constraint-solver"
|
||||
style="background:rgba(223,220,236,0.4)"
|
||||
href="/applications/constraint-solver">
|
||||
Constraint Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_stanford-university"
|
||||
style="background:rgba(38,159,198,0.4)"
|
||||
href="/developers/stanford-university">
|
||||
Stanford University
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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_c"
|
||||
style="background:rgba(13,97,248,0.4)"
|
||||
href="/interfaces/c">
|
||||
C
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_python"
|
||||
style="background:rgba(167,245,243,0.4)"
|
||||
href="/interfaces/python">
|
||||
Python
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>STP is a constraint solver for quantifier-free bitvectors.</p>
|
||||
<h2 id="apis-and-bindings">APIs and Bindings</h2>
|
||||
<p>This tool is available through the following interfaces:</p>
|
||||
<ul>
|
||||
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>A Decision Procedure for Bit-Vectors and Arrays</strong>
|
||||
|
||||
|
||||
(July 2007)
|
||||
|
||||
|
||||
by Ganesh, Vijay et. al.
|
||||
| Appears in <em>CAV 2007</em>
|
||||
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-540-73368-3_52" target="_blank" rel="noopener">10.1007/978-3-540-73368-3_52</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
450
tools/sat-smt/verit/index.html
Normal file
450
tools/sat-smt/verit/index.html
Normal file
@@ -0,0 +1,450 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>veriT | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/verit/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/verit/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>veriT</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://www.verit-solver.org/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_loria"
|
||||
style="background:rgba(127,59,149,0.4)"
|
||||
href="/developers/loria">
|
||||
LORIA
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_uliege"
|
||||
style="background:rgba(30,16,221,0.4)"
|
||||
href="/developers/uliege">
|
||||
ULiege
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_dimacs"
|
||||
style="background:rgba(190,57,177,0.4)"
|
||||
href="/inputs/dimacs">
|
||||
DIMACS
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interfaces/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_bsd"
|
||||
style="background:rgba(197,57,224,0.4)"
|
||||
href="/licenses/bsd">
|
||||
BSD
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>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.</p>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant</strong>
|
||||
|
||||
|
||||
(2021)
|
||||
|
||||
|
||||
by Schurr, Hans-Jörg et. al.
|
||||
| Appears in <em>CADE 2021</em>
|
||||
|
||||
|
||||
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-030-79876-5_26" target="_blank" rel="noopener">10.1007/978-3-030-79876-5_26</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
493
tools/sat-smt/yices/index.html
Normal file
493
tools/sat-smt/yices/index.html
Normal file
@@ -0,0 +1,493 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Yices 2 | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<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="https://example.org/tools/sat-smt/yices/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/yices/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Yices 2</h1>
|
||||
|
||||
<span class="subtitle">SMT Solver</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://yices.csl.sri.com/" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/SRI-CSL/yices2" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_sri-international"
|
||||
style="background:rgba(97,35,218,0.4)"
|
||||
href="/developers/sri-international">
|
||||
SRI International
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_yices-2"
|
||||
style="background:rgba(244,95,143,0.4)"
|
||||
href="/inputs/yices-2">
|
||||
Yices 2
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_gplv3"
|
||||
style="background:rgba(182,14,173,0.4)"
|
||||
href="/licenses/gplv3">
|
||||
GPLv3
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>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.</p>
|
||||
<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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Yices 2.2</strong>
|
||||
|
||||
|
||||
(July 2014)
|
||||
|
||||
|
||||
by Dutertre, Bruno
|
||||
| Appears in <em>Computer-Aided Verification</em>
|
||||
(737-744)
|
||||
|
||||
| Volume 8559
|
||||
| Published by Springer
|
||||
| <a href="https://doi.org/10.1007/978-3-319-08867-9_49" target="_blank" rel="noopener">10.1007/978-3-319-08867-9_49</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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+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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
604
tools/sat-smt/z3/index.html
Normal file
604
tools/sat-smt/z3/index.html
Normal file
@@ -0,0 +1,604 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
|
||||
<title>Z3 | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Z3">
|
||||
<meta property="og:description" content="Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
|
||||
APIs and Bindings
|
||||
This tool is available through the following interfaces:
|
||||
|
||||
C API:">
|
||||
<meta property="og:url" content="https://example.org/tools/sat-smt/z3/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/tools/sat-smt/z3/">
|
||||
|
||||
<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="https://example.org/css/styles.e5b470edf89c3e1b9498ce83a3fd0a2e73e9d06958e2c3a1af8d89781f9f2bf612b21d5e45ab8f4aef773661de2529437838673a136797a6a8aaab7759f94ded.css" integrity="sha512-5bRw7ficPhuUmM6Do/0KLnPp0GlY4sOhr42JeB+fK/YSsh1eRauPSu93NmHeJSlDeDhnOhNnl6aoqqt3WflN7Q==">
|
||||
|
||||
<link href="/css/fontawesome.css" rel="stylesheet" />
|
||||
<link href="/css/brands.css" rel="stylesheet" />
|
||||
<link href="/css/solid.css" rel="stylesheet" />
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Data</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
|
||||
<div id="page-header">
|
||||
<h1>Z3</h1>
|
||||
|
||||
<span class="subtitle">Theorem Prover</span>
|
||||
|
||||
|
||||
|
||||
|
||||
<div id="link-list">
|
||||
<ul>
|
||||
|
||||
<li><a href="https://github.com/Z3Prover/z3" target="_blank" rel="noopener"><i class="fa-solid fa-home"></i> Homepage</a></li>
|
||||
|
||||
<li><a href="https://github.com/Z3Prover/z3" target="_blank" rel="noopener"><i class="fa-brands fa-github"></i> Source Code</a></li>
|
||||
|
||||
<li><a href="https://jfmc.github.io/z3-play/" target="_blank" rel="noopener"><i class="fa-solid fa-gamepad"></i> Playground</a></li>
|
||||
|
||||
</ul>
|
||||
</div>
|
||||
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
<section id="taxonomies">
|
||||
<h2>At a Glance</h2>
|
||||
<table id="taxonomy-table">
|
||||
<tbody>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/applications">
|
||||
Applications
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_smt-solver"
|
||||
style="background:rgba(190,107,118,0.4)"
|
||||
href="/applications/smt-solver">
|
||||
SMT Solver
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="applications_theorem-prover"
|
||||
style="background:rgba(190,35,109,0.4)"
|
||||
href="/applications/theorem-prover">
|
||||
Theorem Prover
|
||||
</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>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/developers">
|
||||
Developers
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_microsoft-research"
|
||||
style="background:rgba(38,15,27,0.4)"
|
||||
href="/developers/microsoft-research">
|
||||
Microsoft Research
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/inputs">
|
||||
Inputs
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_smtlib2"
|
||||
style="background:rgba(108,44,180,0.4)"
|
||||
href="/inputs/smtlib2">
|
||||
SMTLIB2
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="inputs_dimacs"
|
||||
style="background:rgba(190,57,177,0.4)"
|
||||
href="/inputs/dimacs">
|
||||
DIMACS
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/interfaces">
|
||||
Interfaces
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<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
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_c"
|
||||
style="background:rgba(13,97,248,0.4)"
|
||||
href="/interfaces/c">
|
||||
C
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_c++"
|
||||
style="background:rgba(246,248,124,0.4)"
|
||||
href="/interfaces/c++">
|
||||
C++
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_java"
|
||||
style="background:rgba(213,35,135,0.4)"
|
||||
href="/interfaces/java">
|
||||
Java
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_.net"
|
||||
style="background:rgba(48,60,176,0.4)"
|
||||
href="/interfaces/.net">
|
||||
.NET
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interfaces_online"
|
||||
style="background:rgba(84,246,100,0.4)"
|
||||
href="/interfaces/online">
|
||||
Online
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/licenses">
|
||||
Licenses
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="licenses_mit"
|
||||
style="background:rgba(122,188,26,0.4)"
|
||||
href="/licenses/mit">
|
||||
MIT
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
<tr>
|
||||
<td>
|
||||
<a
|
||||
class="taxonomy-name"
|
||||
href="/maintenance">
|
||||
Maintenance
|
||||
</a>
|
||||
</td>
|
||||
<td>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="maintenance_actively-maintained"
|
||||
style="background:rgba(177,86,105,0.4)"
|
||||
href="/maintenance/actively-maintained">
|
||||
Actively Maintained
|
||||
</a>
|
||||
|
||||
|
||||
</td>
|
||||
</tr>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</tbody>
|
||||
</table>
|
||||
</section>
|
||||
|
||||
|
||||
<section>
|
||||
<h2>Description</h2>
|
||||
<p>Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.</p>
|
||||
<h2 id="apis-and-bindings">APIs and Bindings</h2>
|
||||
<p>This tool is available through the following interfaces:</p>
|
||||
<ul>
|
||||
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">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>
|
||||
</ul>
|
||||
|
||||
</section>
|
||||
|
||||
|
||||
|
||||
<section id="publications">
|
||||
<h2>Publications</h2>
|
||||
<ul>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<li>
|
||||
<strong>Z3: An Efficient SMT Solver</strong>
|
||||
|
||||
|
||||
(March 2008)
|
||||
|
||||
|
||||
by de Moura, Leonardo et. al.
|
||||
| Appears in <em>TACAS 2008</em>
|
||||
|
||||
|
||||
|
||||
| Published by Springer, Berlin, Heidelberg
|
||||
| <a href="https://doi.org/10.1007/978-3-540-78800-3_24" target="_blank" rel="noopener">10.1007/978-3-540-78800-3_24</a>
|
||||
|
||||
</li>
|
||||
|
||||
|
||||
|
||||
</ul>
|
||||
</section>
|
||||
|
||||
|
||||
<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>.
|
||||
</div>
|
||||
|
||||
<div class="footer-date" style="text-align: right;">
|
||||
|
||||
|
||||
Updated <time datetime="2025-06-07T00:00:00+00:00">7 June 2025</time>
|
||||
</div>
|
||||
|
||||
</div>
|
||||
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p><a href="/contribute">Contribute</a> | <a href="/about">About</a> | <a href="/license">License</a> | <a href="/privacy">Privacy</a> </p>
|
||||
|
||||
<p>© Copyright 2025. An open-source project.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
Reference in New Issue
Block a user