Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update docs for pr11501
Browse files Browse the repository at this point in the history
DocBot committed Jan 17, 2025
1 parent 83347b4 commit 405bf31
Showing 576 changed files with 869,195 additions and 6 deletions.
10 changes: 5 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@


* [Documentation for PR #11533](docs-pr11533/) (built from [fc66318](https://github.com/cvc5/cvc5/commit/fc66318) @ [PR #11533](https://github.com/cvc5/cvc5/pull/11533), Jan Fri 17, 20:05 UTC)
* [Documentation for PR #11501](docs-pr11501/) (built from [0654581](https://github.com/cvc5/cvc5/commit/0654581) @ [PR #11501](https://github.com/cvc5/cvc5/pull/11501), Jan Fri 17, 20:13 UTC)

***


* [Documentation for main](docs-main/) (built from [ca078a5](https://github.com/cvc5/cvc5/commit/ca078a5) @ [main](https://github.com/cvc5/cvc5/tree/main), 29 hours ago)
* [Documentation for PR #11536](docs-pr11536/) (built from [c4049d4](https://github.com/cvc5/cvc5/commit/c4049d4) @ [PR #11536](https://github.com/cvc5/cvc5/pull/11536), 27 hours ago)
* [Documentation for PR #11534](docs-pr11534/) (built from [4191eb8](https://github.com/cvc5/cvc5/commit/4191eb8) @ [PR #11534](https://github.com/cvc5/cvc5/pull/11534), 2 days ago)
* [Documentation for PR #11533](docs-pr11533/) (built from [fc66318](https://github.com/cvc5/cvc5/commit/fc66318) @ [PR #11533](https://github.com/cvc5/cvc5/pull/11533), now)
* [Documentation for PR #11533](docs-pr11533/) (built from [fc66318](https://github.com/cvc5/cvc5/commit/fc66318) @ [PR #11533](https://github.com/cvc5/cvc5/pull/11533), 8 minutes ago)
* [Documentation for PR #11532](docs-pr11532/) (built from [a53c29c](https://github.com/cvc5/cvc5/commit/a53c29c) @ [PR #11532](https://github.com/cvc5/cvc5/pull/11532), 2 days ago)
* [Documentation for PR #11531](docs-pr11531/) (built from [40c838c](https://github.com/cvc5/cvc5/commit/40c838c) @ [PR #11531](https://github.com/cvc5/cvc5/pull/11531), 2 days ago)
* [Documentation for PR #11530](docs-pr11530/) (built from [ee5e154](https://github.com/cvc5/cvc5/commit/ee5e154) @ [PR #11530](https://github.com/cvc5/cvc5/pull/11530), 2 days ago)
@@ -26,7 +26,7 @@
* [Documentation for PR #11516](docs-pr11516/) (built from [1a1407f](https://github.com/cvc5/cvc5/commit/1a1407f) @ [PR #11516](https://github.com/cvc5/cvc5/pull/11516), 7 days ago)
* [Documentation for PR #11515](docs-pr11515/) (built from [08b9f6b](https://github.com/cvc5/cvc5/commit/08b9f6b) @ [PR #11515](https://github.com/cvc5/cvc5/pull/11515), 6 days ago)
* [Documentation for PR #11514](docs-pr11514/) (built from [435a1dc](https://github.com/cvc5/cvc5/commit/435a1dc) @ [PR #11514](https://github.com/cvc5/cvc5/pull/11514), 5 days ago)
* [Documentation for PR #11513](docs-pr11513/) (built from [7d9f3c2](https://github.com/cvc5/cvc5/commit/7d9f3c2) @ [PR #11513](https://github.com/cvc5/cvc5/pull/11513), 71 minutes ago)
* [Documentation for PR #11513](docs-pr11513/) (built from [7d9f3c2](https://github.com/cvc5/cvc5/commit/7d9f3c2) @ [PR #11513](https://github.com/cvc5/cvc5/pull/11513), 79 minutes ago)
* [Documentation for PR #11512](docs-pr11512/) (built from [443f9b2](https://github.com/cvc5/cvc5/commit/443f9b2) @ [PR #11512](https://github.com/cvc5/cvc5/pull/11512), 6 days ago)
* [Documentation for PR #11511](docs-pr11511/) (built from [4ceb6df](https://github.com/cvc5/cvc5/commit/4ceb6df) @ [PR #11511](https://github.com/cvc5/cvc5/pull/11511), 7 days ago)
* [Documentation for PR #11510](docs-pr11510/) (built from [fb49845](https://github.com/cvc5/cvc5/commit/fb49845) @ [PR #11510](https://github.com/cvc5/cvc5/pull/11510), 7 days ago)
@@ -37,15 +37,15 @@
* [Documentation for PR #11505](docs-pr11505/) (built from [335f92f](https://github.com/cvc5/cvc5/commit/335f92f) @ [PR #11505](https://github.com/cvc5/cvc5/pull/11505), 8 days ago)
* [Documentation for PR #11504](docs-pr11504/) (built from [6f33b91](https://github.com/cvc5/cvc5/commit/6f33b91) @ [PR #11504](https://github.com/cvc5/cvc5/pull/11504), 8 days ago)
* [Documentation for PR #11503](docs-pr11503/) (built from [3469599](https://github.com/cvc5/cvc5/commit/3469599) @ [PR #11503](https://github.com/cvc5/cvc5/pull/11503), 8 days ago)
* [Documentation for PR #11501](docs-pr11501/) (built from [51a9523](https://github.com/cvc5/cvc5/commit/51a9523) @ [PR #11501](https://github.com/cvc5/cvc5/pull/11501), 7 days ago)
* [Documentation for PR #11501](docs-pr11501/) (built from [0654581](https://github.com/cvc5/cvc5/commit/0654581) @ [PR #11501](https://github.com/cvc5/cvc5/pull/11501), now)
* [Documentation for PR #11494](docs-pr11494/) (built from [70ae2e9](https://github.com/cvc5/cvc5/commit/70ae2e9) @ [PR #11494](https://github.com/cvc5/cvc5/pull/11494), 8 days ago)
* [Documentation for PR #11493](docs-pr11493/) (built from [b0938e6](https://github.com/cvc5/cvc5/commit/b0938e6) @ [PR #11493](https://github.com/cvc5/cvc5/pull/11493), 7 days ago)
* [Documentation for PR #11491](docs-pr11491/) (built from [3f84a11](https://github.com/cvc5/cvc5/commit/3f84a11) @ [PR #11491](https://github.com/cvc5/cvc5/pull/11491), 5 days ago)
* [Documentation for PR #11483](docs-pr11483/) (built from [8dd6613](https://github.com/cvc5/cvc5/commit/8dd6613) @ [PR #11483](https://github.com/cvc5/cvc5/pull/11483), 4 days ago)
* [Documentation for PR #11479](docs-pr11479/) (built from [d3059a1](https://github.com/cvc5/cvc5/commit/d3059a1) @ [PR #11479](https://github.com/cvc5/cvc5/pull/11479), 7 days ago)
* [Documentation for PR #11473](docs-pr11473/) (built from [34d05a0](https://github.com/cvc5/cvc5/commit/34d05a0) @ [PR #11473](https://github.com/cvc5/cvc5/pull/11473), 6 days ago)
* [Documentation for PR #11467](docs-pr11467/) (built from [320e3f0](https://github.com/cvc5/cvc5/commit/320e3f0) @ [PR #11467](https://github.com/cvc5/cvc5/pull/11467), 4 days ago)
* [Documentation for PR #11461](docs-pr11461/) (built from [6740322](https://github.com/cvc5/cvc5/commit/6740322) @ [PR #11461](https://github.com/cvc5/cvc5/pull/11461), 28 hours ago)
* [Documentation for PR #11461](docs-pr11461/) (built from [6740322](https://github.com/cvc5/cvc5/commit/6740322) @ [PR #11461](https://github.com/cvc5/cvc5/pull/11461), 29 hours ago)
* [Documentation for PR #11452](docs-pr11452/) (built from [7f6d7b1](https://github.com/cvc5/cvc5/commit/7f6d7b1) @ [PR #11452](https://github.com/cvc5/cvc5/pull/11452), 8 days ago)
* [Documentation for PR #11445](docs-pr11445/) (built from [c32baea](https://github.com/cvc5/cvc5/commit/c32baea) @ [PR #11445](https://github.com/cvc5/cvc5/pull/11445), 7 days ago)
* [Documentation for PR #11429](docs-pr11429/) (built from [2aa4fb4](https://github.com/cvc5/cvc5/commit/2aa4fb4) @ [PR #11429](https://github.com/cvc5/cvc5/pull/11429), 2 days ago)
2 changes: 1 addition & 1 deletion docs-pr11501
154 changes: 154 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/api.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,154 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>API Documentation &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../static/custom.css?v=b9602cbe" />


<script src="../static/jquery.js?v=5d32c60e"></script>
<script src="../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../" id="documentation_options" src="../static/documentation_options.js?v=b3ba4146"></script>
<script src="../static/doctools.js?v=888ff710"></script>
<script src="../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../static/js/theme.js"></script>
<link rel="index" title="Index" href="../genindex.html" />
<link rel="search" title="Search" href="../search.html" />
<link rel="next" title="C++ API" href="cpp/cpp.html" />
<link rel="prev" title="Quickstart Guide" href="../binary/quickstart.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">API Documentation</a><ul>
<li class="toctree-l2"><a class="reference internal" href="cpp/cpp.html">C++ API</a></li>
<li class="toctree-l2"><a class="reference internal" href="c/c.html">C API</a></li>
<li class="toctree-l2"><a class="reference internal" href="java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item active">API Documentation</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="api-documentation">
<h1>API Documentation<a class="headerlink" href="#api-documentation" title="Permalink to this heading"></a></h1>
<p>Alternatively to using cvc5 <a class="reference internal" href="../binary/binary.html"><span class="doc">as a binary</span></a>, cvc5 can be
integrated at the back end of other tools via one of its rich and comprehensive
APIs.</p>
<p>The primary interface of cvc5 is its <a class="reference internal" href="cpp/cpp.html"><span class="doc">C++ API</span></a>.
Its <a class="reference internal" href="c/c.html"><span class="doc">C API</span></a>, <a class="reference internal" href="java/java.html"><span class="doc">Java API</span></a> and
<a class="reference internal" href="python/base/python.html"><span class="doc">base Python API</span></a> implement a thin wrapper around
the C++ API.
In addition to the base Python API, cvc5 also provides a more <a class="reference internal" href="python/pythonic/pythonic.html"><span class="doc">pythonic
Python API</span></a> at
<a class="reference external" href="https://github.com/cvc5/cvc5_pythonic_api">https://github.com/cvc5/cvc5_pythonic_api</a>,
documented <a class="reference internal" href="python/pythonic/pythonic.html"><span class="doc">here</span></a>.</p>
<div class="toctree-wrapper compound">
<ul>
<li class="toctree-l1"><a class="reference internal" href="cpp/cpp.html">C++ API</a></li>
<li class="toctree-l1"><a class="reference internal" href="c/c.html">C API</a></li>
<li class="toctree-l1"><a class="reference internal" href="java/java.html">Java API</a></li>
<li class="toctree-l1"><a class="reference internal" href="python/python.html">Python API</a></li>
</ul>
</div>
</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="../binary/quickstart.html" class="btn btn-neutral float-left" title="Quickstart Guide" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="cpp/cpp.html" class="btn btn-neutral float-right" title="C++ API" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>
371 changes: 371 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/c.html

Large diffs are not rendered by default.

7,337 changes: 7,337 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/enums/cvc5kind.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

1,434 changes: 1,434 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/quickstart.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

2,103 changes: 2,103 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/types/cvc5.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,193 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Cvc5DatatypeConstructorDecl &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../../../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../../../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../../../static/custom.css?v=b9602cbe" />


<script src="../../../static/jquery.js?v=5d32c60e"></script>
<script src="../../../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../../../" id="documentation_options" src="../../../static/documentation_options.js?v=b3ba4146"></script>
<script src="../../../static/doctools.js?v=888ff710"></script>
<script src="../../../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../../../static/js/theme.js"></script>
<link rel="index" title="Index" href="../../../genindex.html" />
<link rel="search" title="Search" href="../../../search.html" />
<link rel="next" title="Cvc5DatatypeSelector" href="cvc5datatypeselector.html" />
<link rel="prev" title="Cvc5DatatypeConstructor" href="cvc5datatypeconstructor.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../../../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../../../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../../../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="../../api.html">API Documentation</a><ul class="current">
<li class="toctree-l2"><a class="reference internal" href="../../cpp/cpp.html">C++ API</a></li>
<li class="toctree-l2 current"><a class="reference internal" href="../c.html">C API</a><ul class="current">
<li class="toctree-l3"><a class="reference internal" href="../quickstart.html">Quickstart Guide</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5.html">Cvc5</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5command.html">Cvc5Command</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatype.html">Cvc5Datatype</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypedecl.html">Cvc5DatatypeDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructor.html">Cvc5DatatypeConstructor</a></li>
<li class="toctree-l3 current"><a class="current reference internal" href="#">Cvc5DatatypeConstructorDecl</a><ul class="simple">
</ul>
</li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeselector.html">Cvc5DatatypeSelector</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5grammar.html">Cvc5Grammar</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5inputparser.html">Cvc5InputParser</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5op.html">Cvc5Op</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5proof.html">Cvc5Proof</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5result.html">Cvc5Result</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5sort.html">Cvc5Sort</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5statistics.html">Cvc5Statistics</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5symbolmanager.html">Cvc5SymbolManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5synthresult.html">Cvc5SynthResult</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5term.html">Cvc5Term</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5termmanager.html">Cvc5TermManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5optioninfo.html">Cvc5OptionInfo</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5plugin.html">Cvc5Plugin</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5kind.html">Cvc5Kind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5proofrule.html">Cvc5ProofRule and Cvc5ProofRewriteRule</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5sortkind.html">Cvc5SortKind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5roundingmode.html">Cvc5RoundingMode</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5unknownexplanation.html">Cvc5UnknownExplanation</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/modes.html">Modes</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#types">Types</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#structs">Structs</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#enums">Enums</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="../../java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../../../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../../../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../../../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item"><a href="../../api.html">API Documentation</a></li>
<li class="breadcrumb-item"><a href="../c.html">C API</a></li>
<li class="breadcrumb-item active">Cvc5DatatypeConstructorDecl</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="cvc5datatypeconstructordecl">
<h1>Cvc5DatatypeConstructorDecl<a class="headerlink" href="#cvc5datatypeconstructordecl" title="Permalink to this heading"></a></h1>
<p>This struct encapsulates a datatype constructor declaration.
A <a class="reference internal" href="#_CPPv427Cvc5DatatypeConstructorDecl" title="Cvc5DatatypeConstructorDecl"><code class="xref cpp cpp-type docutils literal notranslate"><span class="pre">Cvc5DatatypeConstructorDecl</span></code></a>
is constructed via <code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">cvc5_mk_dt_cons_decl()</span></code>.
This is not yet a datatype constructor <a class="reference internal" href="cvc5datatypeconstructor.html"><span class="doc">datatype constructor itself</span></a>, but the representation of the specification
for creating a datatype constructor of a datatype <a class="reference internal" href="cvc5sort.html#_CPPv48Cvc5Sort" title="Cvc5Sort"><code class="xref cpp cpp-type docutils literal notranslate"><span class="pre">sort</span></code></a>
via <code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">cvc5_mk_dt_sort()</span></code> and <code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">cvc5_mk_dt_sorts()</span></code>.</p>
<div class="hide-toctree docutils container">
<div class="toctree-wrapper compound">
</div>
</div>
<hr class="docutils" />
<dl class="cpp type">
<dt class="sig sig-object cpp" id="_CPPv427Cvc5DatatypeConstructorDecl">
<span id="_CPPv327Cvc5DatatypeConstructorDecl"></span><span id="_CPPv227Cvc5DatatypeConstructorDecl"></span><span id="Cvc5DatatypeConstructorDecl"></span><span class="target" id="cvc5_8h_1af95e0c79b95068ad3149be8ee156f6b7"></span><span class="k"><span class="pre">typedef</span></span><span class="w"> </span><span class="k"><span class="pre">struct</span></span><span class="w"> </span><span class="n"><span class="pre">cvc5_dt_cons_decl_t</span></span><span class="w"> </span><span class="p"><span class="pre">*</span></span><span class="sig-name descname"><span class="n"><span class="pre">Cvc5DatatypeConstructorDecl</span></span></span><a class="headerlink" href="#_CPPv427Cvc5DatatypeConstructorDecl" title="Permalink to this definition"></a><br /></dt>
<dd><p>A cvc5 datatype constructor declaration. A datatype constructor declaration is a specification used for creating a datatype constructor. </p>
</dd></dl>

<hr class="docutils" />
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>doxygengroup: Cannot find group “c_cvc5dtconsdecl” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml</p>
</div>
</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="cvc5datatypeconstructor.html" class="btn btn-neutral float-left" title="Cvc5DatatypeConstructor" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="cvc5datatypeselector.html" class="btn btn-neutral float-right" title="Cvc5DatatypeSelector" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,192 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Cvc5InputParser &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../../../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../../../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../../../static/custom.css?v=b9602cbe" />


<script src="../../../static/jquery.js?v=5d32c60e"></script>
<script src="../../../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../../../" id="documentation_options" src="../../../static/documentation_options.js?v=b3ba4146"></script>
<script src="../../../static/doctools.js?v=888ff710"></script>
<script src="../../../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../../../static/js/theme.js"></script>
<link rel="index" title="Index" href="../../../genindex.html" />
<link rel="search" title="Search" href="../../../search.html" />
<link rel="next" title="Cvc5Op" href="cvc5op.html" />
<link rel="prev" title="Cvc5Grammar" href="cvc5grammar.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../../../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../../../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../../../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="../../api.html">API Documentation</a><ul class="current">
<li class="toctree-l2"><a class="reference internal" href="../../cpp/cpp.html">C++ API</a></li>
<li class="toctree-l2 current"><a class="reference internal" href="../c.html">C API</a><ul class="current">
<li class="toctree-l3"><a class="reference internal" href="../quickstart.html">Quickstart Guide</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5.html">Cvc5</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5command.html">Cvc5Command</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatype.html">Cvc5Datatype</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypedecl.html">Cvc5DatatypeDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructor.html">Cvc5DatatypeConstructor</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructordecl.html">Cvc5DatatypeConstructorDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeselector.html">Cvc5DatatypeSelector</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5grammar.html">Cvc5Grammar</a></li>
<li class="toctree-l3 current"><a class="current reference internal" href="#">Cvc5InputParser</a><ul class="simple">
</ul>
</li>
<li class="toctree-l3"><a class="reference internal" href="cvc5op.html">Cvc5Op</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5proof.html">Cvc5Proof</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5result.html">Cvc5Result</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5sort.html">Cvc5Sort</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5statistics.html">Cvc5Statistics</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5symbolmanager.html">Cvc5SymbolManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5synthresult.html">Cvc5SynthResult</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5term.html">Cvc5Term</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5termmanager.html">Cvc5TermManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5optioninfo.html">Cvc5OptionInfo</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5plugin.html">Cvc5Plugin</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5kind.html">Cvc5Kind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5proofrule.html">Cvc5ProofRule and Cvc5ProofRewriteRule</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5sortkind.html">Cvc5SortKind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5roundingmode.html">Cvc5RoundingMode</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5unknownexplanation.html">Cvc5UnknownExplanation</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/modes.html">Modes</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#types">Types</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#structs">Structs</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#enums">Enums</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="../../java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../../../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../../../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../../../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item"><a href="../../api.html">API Documentation</a></li>
<li class="breadcrumb-item"><a href="../c.html">C API</a></li>
<li class="breadcrumb-item active">Cvc5InputParser</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="cvc5inputparser">
<h1>Cvc5InputParser<a class="headerlink" href="#cvc5inputparser" title="Permalink to this heading"></a></h1>
<p>This struct is the main interface for retrieving <a class="reference internal" href="cvc5command.html#_CPPv411Cvc5Command" title="Cvc5Command"><code class="xref cpp cpp-type docutils literal notranslate"><span class="pre">commands</span></code></a> and <a class="reference internal" href="cvc5term.html#_CPPv48Cvc5Term" title="Cvc5Term"><code class="xref cpp cpp-type docutils literal notranslate"><span class="pre">expressions</span></code></a> from an input.</p>
<div class="hide-toctree docutils container">
<div class="toctree-wrapper compound">
</div>
</div>
<hr class="docutils" />
<dl class="cpp type">
<dt class="sig sig-object cpp" id="_CPPv415Cvc5InputParser">
<span id="_CPPv315Cvc5InputParser"></span><span id="_CPPv215Cvc5InputParser"></span><span id="Cvc5InputParser"></span><span class="target" id="cvc5__parser_8h_1a4fdc3394e8b956baa43d7d44950f1003"></span><span class="k"><span class="pre">typedef</span></span><span class="w"> </span><span class="k"><span class="pre">struct</span></span><span class="w"> </span><a class="reference internal" href="#_CPPv415Cvc5InputParser" title="Cvc5InputParser"><span class="n"><span class="pre">Cvc5InputParser</span></span></a><span class="w"> </span><span class="sig-name descname"><span class="n"><span class="pre">Cvc5InputParser</span></span></span><a class="headerlink" href="#_CPPv415Cvc5InputParser" title="Permalink to this definition"></a><br /></dt>
<dd><p>This struct is the main interface for retrieving commands and expressions from an input using a parser.</p>
<p>After construction, it is expected that an input is first configure via, e.g., <code class="docutils literal notranslate"><span class="pre">cvc5_parser_set_file_input()</span></code>, <code class="docutils literal notranslate"><span class="pre">cvc5_parser_set_str_input()</span></code> or <code class="docutils literal notranslate"><span class="pre">cvc5_parser_set_inc_str_input()</span></code> and <code class="docutils literal notranslate"><span class="pre">cvc5_parser_append_inc_str_input()</span></code>. Then, functions <code class="docutils literal notranslate"><span class="pre">cvc5_parser_next_command()</span></code> and <code class="docutils literal notranslate"><span class="pre">cvc5_parser_next_term()</span></code> can be invoked to parse the input.</p>
<p>The input parser interacts with a symbol manager, which determines which symbols are defined in the current context, based on the background logic and user-defined symbols. If no symbol manager is provided, then the input parser will construct (an initially empty) one.</p>
<p>If provided, the symbol manager must have a logic that is compatible with the provided solver. That is, if both the solver and symbol manager have their logics set (<code class="docutils literal notranslate"><span class="pre">cvc5_sm_is_logic_set()</span></code> and <code class="docutils literal notranslate"><a class="reference internal" href="cvc5.html#group__c__cvc5_1gae57a55ccea9da97769deabd644a9cce5"><span class="std std-ref"><span class="pre">cvc5_is_logic_set()</span></span></a></code>), then their logics must be the same.</p>
<p>Upon setting an input source, if either the solver (resp. symbol manager) has its logic set, then the symbol manager (resp. solver) is set to use that logic, if its logic is not already set. </p>
</dd></dl>

<hr class="docutils" />
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>doxygengroup: Cannot find group “c_cvc5inputparser” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml</p>
</div>
</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="cvc5grammar.html" class="btn btn-neutral float-left" title="Cvc5Grammar" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="cvc5op.html" class="btn btn-neutral float-right" title="Cvc5Op" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

1,255 changes: 1,255 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/types/cvc5sort.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,192 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Cvc5SymbolManager &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../../../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../../../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../../../static/custom.css?v=b9602cbe" />


<script src="../../../static/jquery.js?v=5d32c60e"></script>
<script src="../../../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../../../" id="documentation_options" src="../../../static/documentation_options.js?v=b3ba4146"></script>
<script src="../../../static/doctools.js?v=888ff710"></script>
<script src="../../../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../../../static/js/theme.js"></script>
<link rel="index" title="Index" href="../../../genindex.html" />
<link rel="search" title="Search" href="../../../search.html" />
<link rel="next" title="Cvc5SynthResult" href="cvc5synthresult.html" />
<link rel="prev" title="Cvc5Statistics" href="cvc5statistics.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../../../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../../../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../../../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="../../api.html">API Documentation</a><ul class="current">
<li class="toctree-l2"><a class="reference internal" href="../../cpp/cpp.html">C++ API</a></li>
<li class="toctree-l2 current"><a class="reference internal" href="../c.html">C API</a><ul class="current">
<li class="toctree-l3"><a class="reference internal" href="../quickstart.html">Quickstart Guide</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5.html">Cvc5</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5command.html">Cvc5Command</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatype.html">Cvc5Datatype</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypedecl.html">Cvc5DatatypeDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructor.html">Cvc5DatatypeConstructor</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructordecl.html">Cvc5DatatypeConstructorDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeselector.html">Cvc5DatatypeSelector</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5grammar.html">Cvc5Grammar</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5inputparser.html">Cvc5InputParser</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5op.html">Cvc5Op</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5proof.html">Cvc5Proof</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5result.html">Cvc5Result</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5sort.html">Cvc5Sort</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5statistics.html">Cvc5Statistics</a></li>
<li class="toctree-l3 current"><a class="current reference internal" href="#">Cvc5SymbolManager</a><ul class="simple">
</ul>
</li>
<li class="toctree-l3"><a class="reference internal" href="cvc5synthresult.html">Cvc5SynthResult</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5term.html">Cvc5Term</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5termmanager.html">Cvc5TermManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5optioninfo.html">Cvc5OptionInfo</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5plugin.html">Cvc5Plugin</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5kind.html">Cvc5Kind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5proofrule.html">Cvc5ProofRule and Cvc5ProofRewriteRule</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5sortkind.html">Cvc5SortKind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5roundingmode.html">Cvc5RoundingMode</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5unknownexplanation.html">Cvc5UnknownExplanation</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/modes.html">Modes</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#types">Types</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#structs">Structs</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#enums">Enums</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="../../java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../../../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../../../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../../../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item"><a href="../../api.html">API Documentation</a></li>
<li class="breadcrumb-item"><a href="../c.html">C API</a></li>
<li class="breadcrumb-item active">Cvc5SymbolManager</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="cvc5symbolmanager">
<h1>Cvc5SymbolManager<a class="headerlink" href="#cvc5symbolmanager" title="Permalink to this heading"></a></h1>
<p>This class manages a symbol table and other meta-information pertaining to
SMT-LIB v2 inputs (e.g., named assertions, declared functions, etc.).</p>
<div class="hide-toctree docutils container">
<div class="toctree-wrapper compound">
</div>
</div>
<hr class="docutils" />
<dl class="cpp type">
<dt class="sig sig-object cpp" id="_CPPv417Cvc5SymbolManager">
<span id="_CPPv317Cvc5SymbolManager"></span><span id="_CPPv217Cvc5SymbolManager"></span><span id="Cvc5SymbolManager"></span><span class="target" id="cvc5__parser_8h_1adb57adada5df1bc92998400de488e70b"></span><span class="k"><span class="pre">typedef</span></span><span class="w"> </span><span class="k"><span class="pre">struct</span></span><span class="w"> </span><a class="reference internal" href="#_CPPv417Cvc5SymbolManager" title="Cvc5SymbolManager"><span class="n"><span class="pre">Cvc5SymbolManager</span></span></a><span class="w"> </span><span class="sig-name descname"><span class="n"><span class="pre">Cvc5SymbolManager</span></span></span><a class="headerlink" href="#_CPPv417Cvc5SymbolManager" title="Permalink to this definition"></a><br /></dt>
<dd><p>Symbol manager. Internally, the symbol manager manages a symbol table and other meta-information pertaining to SMT2 file inputs (e.g. named assertions, declared functions, etc.).</p>
<p>A symbol manager can be modified by invoking commands, see <code class="docutils literal notranslate"><a class="reference internal" href="cvc5command.html#group__c__cvc5command_1ga77819a12ff434c85fa619bd99a7e5fb5"><span class="std std-ref"><span class="pre">cvc5_cmd_invoke()</span></span></a></code>.</p>
<p>A symbol manager can be provided when constructing a Cvc5InputParser, in which case that input parser has symbols of this symbol manager preloaded.</p>
<p>The symbol manager’s interface is otherwise not publicly available. </p>
</dd></dl>

<hr class="docutils" />
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>doxygengroup: Cannot find group “c_cvc5symbolmanager” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml</p>
</div>
</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="cvc5statistics.html" class="btn btn-neutral float-left" title="Cvc5Statistics" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="cvc5synthresult.html" class="btn btn-neutral float-right" title="Cvc5SynthResult" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>
Original file line number Diff line number Diff line change
@@ -0,0 +1,194 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Cvc5SynthResult &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../../../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../../../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../../../static/custom.css?v=b9602cbe" />


<script src="../../../static/jquery.js?v=5d32c60e"></script>
<script src="../../../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../../../" id="documentation_options" src="../../../static/documentation_options.js?v=b3ba4146"></script>
<script src="../../../static/doctools.js?v=888ff710"></script>
<script src="../../../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../../../static/js/theme.js"></script>
<link rel="index" title="Index" href="../../../genindex.html" />
<link rel="search" title="Search" href="../../../search.html" />
<link rel="next" title="Cvc5Term" href="cvc5term.html" />
<link rel="prev" title="Cvc5SymbolManager" href="cvc5symbolmanager.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../../../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../../../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../../../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="../../api.html">API Documentation</a><ul class="current">
<li class="toctree-l2"><a class="reference internal" href="../../cpp/cpp.html">C++ API</a></li>
<li class="toctree-l2 current"><a class="reference internal" href="../c.html">C API</a><ul class="current">
<li class="toctree-l3"><a class="reference internal" href="../quickstart.html">Quickstart Guide</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5.html">Cvc5</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5command.html">Cvc5Command</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatype.html">Cvc5Datatype</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypedecl.html">Cvc5DatatypeDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructor.html">Cvc5DatatypeConstructor</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeconstructordecl.html">Cvc5DatatypeConstructorDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5datatypeselector.html">Cvc5DatatypeSelector</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5grammar.html">Cvc5Grammar</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5inputparser.html">Cvc5InputParser</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5op.html">Cvc5Op</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5proof.html">Cvc5Proof</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5result.html">Cvc5Result</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5sort.html">Cvc5Sort</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5statistics.html">Cvc5Statistics</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5symbolmanager.html">Cvc5SymbolManager</a></li>
<li class="toctree-l3 current"><a class="current reference internal" href="#">Cvc5SynthResult</a><ul class="simple">
</ul>
</li>
<li class="toctree-l3"><a class="reference internal" href="cvc5term.html">Cvc5Term</a></li>
<li class="toctree-l3"><a class="reference internal" href="cvc5termmanager.html">Cvc5TermManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5optioninfo.html">Cvc5OptionInfo</a></li>
<li class="toctree-l3"><a class="reference internal" href="../structs/cvc5plugin.html">Cvc5Plugin</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5kind.html">Cvc5Kind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5proofrule.html">Cvc5ProofRule and Cvc5ProofRewriteRule</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5sortkind.html">Cvc5SortKind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5roundingmode.html">Cvc5RoundingMode</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/cvc5unknownexplanation.html">Cvc5UnknownExplanation</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/modes.html">Modes</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#types">Types</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#structs">Structs</a></li>
<li class="toctree-l3"><a class="reference internal" href="../c.html#enums">Enums</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="../../java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../../../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../../../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../../../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item"><a href="../../api.html">API Documentation</a></li>
<li class="breadcrumb-item"><a href="../c.html">C API</a></li>
<li class="breadcrumb-item active">Cvc5SynthResult</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="cvc5synthresult">
<h1>Cvc5SynthResult<a class="headerlink" href="#cvc5synthresult" title="Permalink to this heading"></a></h1>
<p>This struct represents a <a class="reference internal" href="cvc5.html#_CPPv44Cvc5" title="Cvc5"><code class="xref cpp cpp-type docutils literal notranslate"><span class="pre">Cvc5</span></code></a> SyGus synthesis result.</p>
<div class="hide-toctree docutils container">
<div class="toctree-wrapper compound">
</div>
</div>
<hr class="docutils" />
<dl class="cpp type">
<dt class="sig sig-object cpp" id="_CPPv415Cvc5SynthResult">
<span id="_CPPv315Cvc5SynthResult"></span><span id="_CPPv215Cvc5SynthResult"></span><span id="Cvc5SynthResult"></span><span class="target" id="cvc5_8h_1a8053f1348d98369d24dcfb41e47d5d12"></span><span class="k"><span class="pre">typedef</span></span><span class="w"> </span><span class="k"><span class="pre">struct</span></span><span class="w"> </span><span class="n"><span class="pre">cvc5_synth_result_t</span></span><span class="w"> </span><span class="p"><span class="pre">*</span></span><span class="sig-name descname"><span class="n"><span class="pre">Cvc5SynthResult</span></span></span><a class="headerlink" href="#_CPPv415Cvc5SynthResult" title="Permalink to this definition"></a><br /></dt>
<dd><p>Encapsulation of a solver synth result.</p>
<p>This is the return value of the API functions:<ul class="simple">
<li><p><a class="reference internal" href="cvc5.html#group__c__cvc5_1ga6ad682e5dca663fb80edfd94eaf5d35c"><span class="std std-ref">cvc5_check_synth()</span></a></p></li>
<li><p><a class="reference internal" href="cvc5.html#group__c__cvc5_1gaaf9ac9b731c0e7927b923f90061b2164"><span class="std std-ref">cvc5_check_synth_next()</span></a></p></li>
</ul>
</p>
<p>which we call “synthesis queries”. This class indicates whether the synthesis query has a solution, has no solution, or is unknown. </p>
</dd></dl>

<hr class="docutils" />
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>doxygengroup: Cannot find group “c_cvc5synthresult” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml</p>
</div>
</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="cvc5symbolmanager.html" class="btn btn-neutral float-left" title="Cvc5SymbolManager" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="cvc5term.html" class="btn btn-neutral float-right" title="Cvc5Term" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>
1,469 changes: 1,469 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/c/types/cvc5term.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,204 @@


<!DOCTYPE html>
<html class="writer-html5" lang="en">
<head>
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-ML12X2V35B"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-ML12X2V35B');
</script>

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>DriverOptions &mdash; cvc5 documentation</title>
<link rel="stylesheet" type="text/css" href="../../../static/pygments.css?v=b86133f3" />
<link rel="stylesheet" type="text/css" href="../../../static/css/theme.css?v=e59714d7" />
<link rel="stylesheet" type="text/css" href="../../../static/custom.css?v=b9602cbe" />


<script src="../../../static/jquery.js?v=5d32c60e"></script>
<script src="../../../static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script data-url_root="../../../" id="documentation_options" src="../../../static/documentation_options.js?v=b3ba4146"></script>
<script src="../../../static/doctools.js?v=888ff710"></script>
<script src="../../../static/sphinx_highlight.js?v=4825356b"></script>
<script src="../../../static/js/theme.js"></script>
<link rel="index" title="Index" href="../../../genindex.html" />
<link rel="search" title="Search" href="../../../search.html" />
<link rel="next" title="Grammar" href="grammar.html" />
<link rel="prev" title="DatatypeSelector" href="datatypeselector.html" />
</head>

<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >



<a href="../../../index.html" class="icon icon-home">
cvc5
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="../../../search.html" method="get">
<input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="../../../installation/installation.html">Installation</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../binary/binary.html">Binary Documentation</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="../../api.html">API Documentation</a><ul class="current">
<li class="toctree-l2 current"><a class="reference internal" href="../cpp.html">C++ API</a><ul class="current">
<li class="toctree-l3"><a class="reference internal" href="../quickstart.html">Quickstart Guide</a></li>
<li class="toctree-l3"><a class="reference internal" href="../exceptions/exceptions.html">Exceptions</a></li>
<li class="toctree-l3"><a class="reference internal" href="command.html">Command</a></li>
<li class="toctree-l3"><a class="reference internal" href="datatype.html">Datatype</a></li>
<li class="toctree-l3"><a class="reference internal" href="datatypeconstructor.html">DatatypeConstructor</a></li>
<li class="toctree-l3"><a class="reference internal" href="datatypeconstructordecl.html">DatatypeConstructorDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="datatypedecl.html">DatatypeDecl</a></li>
<li class="toctree-l3"><a class="reference internal" href="datatypeselector.html">DatatypeSelector</a></li>
<li class="toctree-l3 current"><a class="current reference internal" href="#">DriverOptions</a></li>
<li class="toctree-l3"><a class="reference internal" href="grammar.html">Grammar</a></li>
<li class="toctree-l3"><a class="reference internal" href="inputparser.html">InputParser</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/kind.html">Kind</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/modes.html">Modes</a></li>
<li class="toctree-l3"><a class="reference internal" href="op.html">Op</a></li>
<li class="toctree-l3"><a class="reference internal" href="optioninfo.html">OptionInfo</a></li>
<li class="toctree-l3"><a class="reference internal" href="plugin.html">Plugin</a></li>
<li class="toctree-l3"><a class="reference internal" href="proof.html">Proof</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/proofrule.html">ProofRule and ProofRewriteRule</a></li>
<li class="toctree-l3"><a class="reference internal" href="result.html">Result</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/roundingmode.html">RoundingMode</a></li>
<li class="toctree-l3"><a class="reference internal" href="solver.html">Solver</a></li>
<li class="toctree-l3"><a class="reference internal" href="sort.html">Sort</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/sortkind.html">SortKind</a></li>
<li class="toctree-l3"><a class="reference internal" href="statistics.html">Statistics</a></li>
<li class="toctree-l3"><a class="reference internal" href="symbolmanager.html">SymbolManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="synthresult.html">SynthResult</a></li>
<li class="toctree-l3"><a class="reference internal" href="term.html">Term</a></li>
<li class="toctree-l3"><a class="reference internal" href="termmanager.html">TermManager</a></li>
<li class="toctree-l3"><a class="reference internal" href="../enums/unknownexplanation.html">UnknownExplanation</a></li>
<li class="toctree-l3"><a class="reference internal" href="../cpp.html#class-hierarchy">Class hierarchy</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="../../c/c.html">C API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../java/java.html">Java API</a></li>
<li class="toctree-l2"><a class="reference internal" href="../../python/python.html">Python API</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="../../../options.html">Options</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../output-tags.html">Output tags</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../proofs/proofs.html">Proof Production</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../resource-limits.html">Resource limits</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../skolem-ids.html">Skolem Identifiers</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../statistics.html">Statistics</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../examples/examples.html">Examples</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../theories/theories.html">Theory References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../references.html">References</a></li>
<li class="toctree-l1"><a class="reference internal" href="../../../genindex.html">Index</a></li>
</ul>

</div>
</div>
</nav>

<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="../../../index.html">cvc5</a>
</nav>

<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="../../../index.html" class="icon icon-home" aria-label="Home"></a></li>
<li class="breadcrumb-item"><a href="../../api.html">API Documentation</a></li>
<li class="breadcrumb-item"><a href="../cpp.html">C++ API</a></li>
<li class="breadcrumb-item active">DriverOptions</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">

<section id="driveroptions">
<h1>DriverOptions<a class="headerlink" href="#driveroptions" title="Permalink to this heading"></a></h1>
<dl class="cpp class">
<dt class="sig sig-object cpp" id="_CPPv4N4cvc513DriverOptionsE">
<span id="_CPPv3N4cvc513DriverOptionsE"></span><span id="_CPPv2N4cvc513DriverOptionsE"></span><span id="cvc5::DriverOptions"></span><span class="target" id="classcvc5_1_1DriverOptions"></span><span class="k"><span class="pre">class</span></span><span class="w"> </span><span class="sig-name descname"><span class="n"><span class="pre">DriverOptions</span></span></span><a class="headerlink" href="#_CPPv4N4cvc513DriverOptionsE" title="Permalink to this definition"></a><br /></dt>
<dd><p>This class provides type-safe access to a few options that frontends are
likely to use, but can not be not be communicated appropriately via the
regular <a class="reference internal" href="solver.html#_CPPv4NK4cvc56Solver9getOptionERKNSt6stringE" title="cvc5::Solver::getOption"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">Solver::getOption()</span></code></a> or
<a class="reference internal" href="solver.html#_CPPv4NK4cvc56Solver13getOptionInfoERKNSt6stringE" title="cvc5::Solver::getOptionInfo"><code class="xref cpp cpp-func docutils literal notranslate"><span class="pre">Solver::getOptionInfo()</span></code></a>
functions. This includes, e.g., the input and output streams that can be
configured via <a class="reference internal" href="../../../options.html#lbl-option-err"><span class="std std-ref">err</span></a>, <a class="reference internal" href="../../../options.html#lbl-option-in"><span class="std std-ref">in</span></a> and
<a class="reference internal" href="../../../options.html#lbl-option-out"><span class="std std-ref">out</span></a>. This class does not store the options itself,
but only acts as a wrapper to the solver object. It can thus no longer be
used after the solver object has been destroyed.</p>
<div class="breathe-sectiondef docutils container">
<p class="breathe-sectiondef-title rubric" id="breathe-section-title-public-functions">Public Functions</p>
<dl class="cpp function">
<dt class="sig sig-object cpp" id="_CPPv4NK4cvc513DriverOptions2inEv">
<span id="_CPPv3NK4cvc513DriverOptions2inEv"></span><span id="_CPPv2NK4cvc513DriverOptions2inEv"></span><span id="cvc5::DriverOptions::inC"></span><span class="target" id="classcvc5_1_1DriverOptions_1a36587f8bea97c94fbabbda3c8e112305"></span><span class="n"><span class="pre">std</span></span><span class="p"><span class="pre">::</span></span><span class="n"><span class="pre">istream</span></span><span class="w"> </span><span class="p"><span class="pre">&amp;</span></span><span class="sig-name descname"><span class="n"><span class="pre">in</span></span></span><span class="sig-paren">(</span><span class="sig-paren">)</span><span class="w"> </span><span class="k"><span class="pre">const</span></span><a class="headerlink" href="#_CPPv4NK4cvc513DriverOptions2inEv" title="Permalink to this definition"></a><br /></dt>
<dd><p>Access the solver’s input stream </p>
</dd></dl>

<dl class="cpp function">
<dt class="sig sig-object cpp" id="_CPPv4NK4cvc513DriverOptions3errEv">
<span id="_CPPv3NK4cvc513DriverOptions3errEv"></span><span id="_CPPv2NK4cvc513DriverOptions3errEv"></span><span id="cvc5::DriverOptions::errC"></span><span class="target" id="classcvc5_1_1DriverOptions_1ae8a2813f1ac2c3ea6ba6b1c43b2ce31a"></span><span class="n"><span class="pre">std</span></span><span class="p"><span class="pre">::</span></span><span class="n"><span class="pre">ostream</span></span><span class="w"> </span><span class="p"><span class="pre">&amp;</span></span><span class="sig-name descname"><span class="n"><span class="pre">err</span></span></span><span class="sig-paren">(</span><span class="sig-paren">)</span><span class="w"> </span><span class="k"><span class="pre">const</span></span><a class="headerlink" href="#_CPPv4NK4cvc513DriverOptions3errEv" title="Permalink to this definition"></a><br /></dt>
<dd><p>Access the solver’s error output stream </p>
</dd></dl>

<dl class="cpp function">
<dt class="sig sig-object cpp" id="_CPPv4NK4cvc513DriverOptions3outEv">
<span id="_CPPv3NK4cvc513DriverOptions3outEv"></span><span id="_CPPv2NK4cvc513DriverOptions3outEv"></span><span id="cvc5::DriverOptions::outC"></span><span class="target" id="classcvc5_1_1DriverOptions_1a7981df80a91bb3c842f9e6cda6aab655"></span><span class="n"><span class="pre">std</span></span><span class="p"><span class="pre">::</span></span><span class="n"><span class="pre">ostream</span></span><span class="w"> </span><span class="p"><span class="pre">&amp;</span></span><span class="sig-name descname"><span class="n"><span class="pre">out</span></span></span><span class="sig-paren">(</span><span class="sig-paren">)</span><span class="w"> </span><span class="k"><span class="pre">const</span></span><a class="headerlink" href="#_CPPv4NK4cvc513DriverOptions3outEv" title="Permalink to this definition"></a><br /></dt>
<dd><p>Access the solver’s output stream </p>
</dd></dl>

</div>
</dd></dl>

</section>


</div>
</div>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="datatypeselector.html" class="btn btn-neutral float-left" title="DatatypeSelector" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="grammar.html" class="btn btn-neutral float-right" title="Grammar" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>

<hr/>

<div role="contentinfo">
<p>&#169; Copyright 2025, the authors of cvc5.</p>
</div>

Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.


</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>

</body>
</html>

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

1,096 changes: 1,096 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/cpp/classes/sort.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

1,648 changes: 1,648 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/cpp/classes/term.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

284 changes: 284 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/cpp/cpp.html

Large diffs are not rendered by default.

7,366 changes: 7,366 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/cpp/enums/kind.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Large diffs are not rendered by default.

1,118 changes: 1,118 additions & 0 deletions docs-pr11501-0654581a137cf89d3e781f89219c209913ad2d2b/api/cpp/quickstart.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
<!DOCTYPE HTML>
<!-- NewPage -->
<html lang="en">
<head>
<!-- Generated by javadoc -->
<title>All Classes</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery/jquery-ui.min.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery-ui.overrides.css" title="Style">
<script type="text/javascript" src="script.js"></script>
<script type="text/javascript" src="jquery/jszip/dist/jszip.min.js"></script>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils.min.js"></script>
<!--[if IE]>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils-ie.min.js"></script>
<![endif]-->
<script type="text/javascript" src="jquery/jquery-3.7.1.min.js"></script>
<script type="text/javascript" src="jquery/jquery-ui.min.js"></script>
</head>
<body>
<main role="main">
<h1 class="bar">All&nbsp;Classes</h1>
<div class="indexContainer">
<ul>
<li><a href="io/github/cvc5/AbstractPlugin.html" title="class in io.github.cvc5">AbstractPlugin</a></li>
<li><a href="io/github/cvc5/modes/BlockModelsMode.html" title="enum in io.github.cvc5.modes">BlockModelsMode</a></li>
<li><a href="io/github/cvc5/Command.html" title="class in io.github.cvc5">Command</a></li>
<li><a href="io/github/cvc5/Context.html" title="class in io.github.cvc5">Context</a></li>
<li><a href="io/github/cvc5/CVC5ApiException.html" title="class in io.github.cvc5">CVC5ApiException</a></li>
<li><a href="io/github/cvc5/CVC5ApiOptionException.html" title="class in io.github.cvc5">CVC5ApiOptionException</a></li>
<li><a href="io/github/cvc5/CVC5ApiRecoverableException.html" title="class in io.github.cvc5">CVC5ApiRecoverableException</a></li>
<li><a href="io/github/cvc5/CVC5ParserException.html" title="class in io.github.cvc5">CVC5ParserException</a></li>
<li><a href="io/github/cvc5/Datatype.html" title="class in io.github.cvc5">Datatype</a></li>
<li><a href="io/github/cvc5/DatatypeConstructor.html" title="class in io.github.cvc5">DatatypeConstructor</a></li>
<li><a href="io/github/cvc5/DatatypeConstructorDecl.html" title="class in io.github.cvc5">DatatypeConstructorDecl</a></li>
<li><a href="io/github/cvc5/DatatypeDecl.html" title="class in io.github.cvc5">DatatypeDecl</a></li>
<li><a href="io/github/cvc5/DatatypeSelector.html" title="class in io.github.cvc5">DatatypeSelector</a></li>
<li><a href="io/github/cvc5/modes/FindSynthTarget.html" title="enum in io.github.cvc5.modes">FindSynthTarget</a></li>
<li><a href="io/github/cvc5/Grammar.html" title="class in io.github.cvc5">Grammar</a></li>
<li><a href="io/github/cvc5/modes/InputLanguage.html" title="enum in io.github.cvc5.modes">InputLanguage</a></li>
<li><a href="io/github/cvc5/InputParser.html" title="class in io.github.cvc5">InputParser</a></li>
<li><a href="io/github/cvc5/IOracle.html" title="interface in io.github.cvc5"><span class="interfaceName">IOracle</span></a></li>
<li><a href="io/github/cvc5/Kind.html" title="enum in io.github.cvc5">Kind</a></li>
<li><a href="io/github/cvc5/modes/LearnedLitType.html" title="enum in io.github.cvc5.modes">LearnedLitType</a></li>
<li><a href="io/github/cvc5/Op.html" title="class in io.github.cvc5">Op</a></li>
<li><a href="io/github/cvc5/OptionInfo.html" title="class in io.github.cvc5">OptionInfo</a></li>
<li><a href="io/github/cvc5/Pair.html" title="class in io.github.cvc5">Pair</a></li>
<li><a href="io/github/cvc5/Proof.html" title="class in io.github.cvc5">Proof</a></li>
<li><a href="io/github/cvc5/modes/ProofComponent.html" title="enum in io.github.cvc5.modes">ProofComponent</a></li>
<li><a href="io/github/cvc5/modes/ProofFormat.html" title="enum in io.github.cvc5.modes">ProofFormat</a></li>
<li><a href="io/github/cvc5/ProofRewriteRule.html" title="enum in io.github.cvc5">ProofRewriteRule</a></li>
<li><a href="io/github/cvc5/ProofRule.html" title="enum in io.github.cvc5">ProofRule</a></li>
<li><a href="io/github/cvc5/Result.html" title="class in io.github.cvc5">Result</a></li>
<li><a href="io/github/cvc5/RoundingMode.html" title="enum in io.github.cvc5">RoundingMode</a></li>
<li><a href="io/github/cvc5/SkolemId.html" title="enum in io.github.cvc5">SkolemId</a></li>
<li><a href="io/github/cvc5/Solver.html" title="class in io.github.cvc5">Solver</a></li>
<li><a href="io/github/cvc5/Sort.html" title="class in io.github.cvc5">Sort</a></li>
<li><a href="io/github/cvc5/SortKind.html" title="enum in io.github.cvc5">SortKind</a></li>
<li><a href="io/github/cvc5/Stat.html" title="class in io.github.cvc5">Stat</a></li>
<li><a href="io/github/cvc5/Statistics.html" title="class in io.github.cvc5">Statistics</a></li>
<li><a href="io/github/cvc5/SymbolManager.html" title="class in io.github.cvc5">SymbolManager</a></li>
<li><a href="io/github/cvc5/SynthResult.html" title="class in io.github.cvc5">SynthResult</a></li>
<li><a href="io/github/cvc5/Term.html" title="class in io.github.cvc5">Term</a></li>
<li><a href="io/github/cvc5/TermManager.html" title="class in io.github.cvc5">TermManager</a></li>
<li><a href="io/github/cvc5/Triplet.html" title="class in io.github.cvc5">Triplet</a></li>
<li><a href="io/github/cvc5/UnknownExplanation.html" title="enum in io.github.cvc5">UnknownExplanation</a></li>
<li><a href="io/github/cvc5/Utils.html" title="class in io.github.cvc5">Utils</a></li>
</ul>
</div>
</main>
</body>
</html>
Original file line number Diff line number Diff line change
@@ -0,0 +1,170 @@
<!DOCTYPE HTML>
<!-- NewPage -->
<html lang="en">
<head>
<!-- Generated by javadoc -->
<title>All Packages</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery/jquery-ui.min.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery-ui.overrides.css" title="Style">
<script type="text/javascript" src="script.js"></script>
<script type="text/javascript" src="jquery/jszip/dist/jszip.min.js"></script>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils.min.js"></script>
<!--[if IE]>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils-ie.min.js"></script>
<![endif]-->
<script type="text/javascript" src="jquery/jquery-3.7.1.min.js"></script>
<script type="text/javascript" src="jquery/jquery-ui.min.js"></script>
</head>
<body>
<script type="text/javascript"><!--
try {
if (location.href.indexOf('is-external=true') == -1) {
parent.document.title="All Packages";
}
}
catch(err) {
}
//-->
var pathtoroot = "./";
var useModuleDirectories = true;
loadScripts(document, 'script');</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<header role="banner">
<nav role="navigation">
<div class="fixedNav">
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a id="navbar.top">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.top" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.top.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li><a href="help-doc.html">Help</a></li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_top">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<ul class="navListSearch">
<li><label for="search">SEARCH:</label>
<input type="text" id="search" value="search" disabled="disabled">
<input type="reset" id="reset" value="reset" disabled="disabled">
</li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_top");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.top">
<!-- -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
</div>
<div class="navPadding">&nbsp;</div>
<script type="text/javascript"><!--
$('.navPadding').css('padding-top', $('.fixedNav').css("height"));
//-->
</script>
</nav>
</header>
<main role="main">
<div class="header">
<h1 title="All&amp;nbsp;Packages" class="title">All&nbsp;Packages</h1>
</div>
<div class="allPackagesContainer">
<ul class="blockList">
<li class="blockList">
<table class="packagesSummary">
<caption><span>Package Summary</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Package</th>
<th class="colLast" scope="col">Description</th>
</tr>
<tbody>
<tr class="altColor">
<th class="colFirst" scope="row"><a href="io/github/cvc5/package-summary.html">io.github.cvc5</a></th>
<td class="colLast">&nbsp;</td>
</tr>
<tr class="rowColor">
<th class="colFirst" scope="row"><a href="io/github/cvc5/modes/package-summary.html">io.github.cvc5.modes</a></th>
<td class="colLast">&nbsp;</td>
</tr>
</tbody>
</table>
</li>
</ul>
</div>
</main>
<footer role="contentinfo">
<nav role="navigation">
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a id="navbar.bottom">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.bottom" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.bottom.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li><a href="help-doc.html">Help</a></li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_bottom");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.bottom">
<!-- -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</nav>
</footer>
</body>
</html>
Original file line number Diff line number Diff line change
@@ -0,0 +1,181 @@
<!DOCTYPE HTML>
<!-- NewPage -->
<html lang="en">
<head>
<!-- Generated by javadoc -->
<title>Constant Field Values</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery/jquery-ui.min.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery-ui.overrides.css" title="Style">
<script type="text/javascript" src="script.js"></script>
<script type="text/javascript" src="jquery/jszip/dist/jszip.min.js"></script>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils.min.js"></script>
<!--[if IE]>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils-ie.min.js"></script>
<![endif]-->
<script type="text/javascript" src="jquery/jquery-3.7.1.min.js"></script>
<script type="text/javascript" src="jquery/jquery-ui.min.js"></script>
</head>
<body>
<script type="text/javascript"><!--
try {
if (location.href.indexOf('is-external=true') == -1) {
parent.document.title="Constant Field Values";
}
}
catch(err) {
}
//-->
var pathtoroot = "./";
var useModuleDirectories = true;
loadScripts(document, 'script');</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<header role="banner">
<nav role="navigation">
<div class="fixedNav">
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a id="navbar.top">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.top" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.top.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li><a href="help-doc.html">Help</a></li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_top">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<ul class="navListSearch">
<li><label for="search">SEARCH:</label>
<input type="text" id="search" value="search" disabled="disabled">
<input type="reset" id="reset" value="reset" disabled="disabled">
</li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_top");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.top">
<!-- -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
</div>
<div class="navPadding">&nbsp;</div>
<script type="text/javascript"><!--
$('.navPadding').css('padding-top', $('.fixedNav').css("height"));
//-->
</script>
</nav>
</header>
<main role="main">
<div class="header">
<h1 title="Constant Field Values" class="title">Constant Field Values</h1>
<section>
<h2 title="Contents">Contents</h2>
<ul>
<li><a href="#io.github">io.github.*</a></li>
</ul>
</section>
</div>
<div class="constantValuesContainer"><a id="io.github">
<!-- -->
</a>
<section>
<h2 title="io.github">io.github.*</h2>
<ul class="blockList">
<li class="blockList">
<table class="constantsSummary">
<caption><span>io.github.cvc5.<a href="io/github/cvc5/Utils.html" title="class in io.github.cvc5">Utils</a></span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colSecond" scope="col">Constant Field</th>
<th class="colLast" scope="col">Value</th>
</tr>
<tbody>
<tr class="altColor">
<td class="colFirst"><a id="io.github.cvc5.Utils.LIBPATH_IN_JAR">
<!-- -->
</a><code>public&nbsp;static&nbsp;final&nbsp;java.lang.String</code></td>
<th class="colSecond" scope="row"><code><a href="io/github/cvc5/Utils.html#LIBPATH_IN_JAR">LIBPATH_IN_JAR</a></code></th>
<td class="colLast"><code>"/cvc5-libs"</code></td>
</tr>
</tbody>
</table>
</li>
</ul>
</section>
</div>
</main>
<footer role="contentinfo">
<nav role="navigation">
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a id="navbar.bottom">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.bottom" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.bottom.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li><a href="help-doc.html">Help</a></li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_bottom");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.bottom">
<!-- -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</nav>
</footer>
</body>
</html>

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
io.github.cvc5
io.github.cvc5.modes
Original file line number Diff line number Diff line change
@@ -0,0 +1,274 @@
<!DOCTYPE HTML>
<!-- NewPage -->
<html lang="en">
<head>
<!-- Generated by javadoc -->
<title>API Help</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<link rel="stylesheet" type="text/css" href="stylesheet.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery/jquery-ui.min.css" title="Style">
<link rel="stylesheet" type="text/css" href="jquery-ui.overrides.css" title="Style">
<script type="text/javascript" src="script.js"></script>
<script type="text/javascript" src="jquery/jszip/dist/jszip.min.js"></script>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils.min.js"></script>
<!--[if IE]>
<script type="text/javascript" src="jquery/jszip-utils/dist/jszip-utils-ie.min.js"></script>
<![endif]-->
<script type="text/javascript" src="jquery/jquery-3.7.1.min.js"></script>
<script type="text/javascript" src="jquery/jquery-ui.min.js"></script>
</head>
<body>
<script type="text/javascript"><!--
try {
if (location.href.indexOf('is-external=true') == -1) {
parent.document.title="API Help";
}
}
catch(err) {
}
//-->
var pathtoroot = "./";
var useModuleDirectories = true;
loadScripts(document, 'script');</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<header role="banner">
<nav role="navigation">
<div class="fixedNav">
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a id="navbar.top">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.top" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.top.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li class="navBarCell1Rev">Help</li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_top">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<ul class="navListSearch">
<li><label for="search">SEARCH:</label>
<input type="text" id="search" value="search" disabled="disabled">
<input type="reset" id="reset" value="reset" disabled="disabled">
</li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_top");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.top">
<!-- -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
</div>
<div class="navPadding">&nbsp;</div>
<script type="text/javascript"><!--
$('.navPadding').css('padding-top', $('.fixedNav').css("height"));
//-->
</script>
</nav>
</header>
<main role="main">
<div class="header">
<h1 class="title">How This API Document Is Organized</h1>
<div class="subTitle">This API (Application Programming Interface) document has pages corresponding to the items in the navigation bar, described as follows.</div>
</div>
<div class="contentContainer">
<ul class="blockList">
<li class="blockList">
<section>
<h2>Overview</h2>
<p>The <a href="index.html">Overview</a> page is the front page of this API document and provides a list of all packages with a summary for each. This page can also contain an overall description of the set of packages.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Package</h2>
<p>Each package has a page that contains a list of its classes and interfaces, with a summary for each. These pages may contain six categories:</p>
<ul>
<li>Interfaces</li>
<li>Classes</li>
<li>Enums</li>
<li>Exceptions</li>
<li>Errors</li>
<li>Annotation Types</li>
</ul>
</section>
</li>
<li class="blockList">
<section>
<h2>Class or Interface</h2>
<p>Each class, interface, nested class and nested interface has its own separate page. Each of these pages has three sections consisting of a class/interface description, summary tables, and detailed member descriptions:</p>
<ul>
<li>Class Inheritance Diagram</li>
<li>Direct Subclasses</li>
<li>All Known Subinterfaces</li>
<li>All Known Implementing Classes</li>
<li>Class or Interface Declaration</li>
<li>Class or Interface Description</li>
</ul>
<br>
<ul>
<li>Nested Class Summary</li>
<li>Field Summary</li>
<li>Property Summary</li>
<li>Constructor Summary</li>
<li>Method Summary</li>
</ul>
<br>
<ul>
<li>Field Detail</li>
<li>Property Detail</li>
<li>Constructor Detail</li>
<li>Method Detail</li>
</ul>
<p>Each summary entry contains the first sentence from the detailed description for that item. The summary entries are alphabetical, while the detailed descriptions are in the order they appear in the source code. This preserves the logical groupings established by the programmer.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Annotation Type</h2>
<p>Each annotation type has its own separate page with the following sections:</p>
<ul>
<li>Annotation Type Declaration</li>
<li>Annotation Type Description</li>
<li>Required Element Summary</li>
<li>Optional Element Summary</li>
<li>Element Detail</li>
</ul>
</section>
</li>
<li class="blockList">
<section>
<h2>Enum</h2>
<p>Each enum has its own separate page with the following sections:</p>
<ul>
<li>Enum Declaration</li>
<li>Enum Description</li>
<li>Enum Constant Summary</li>
<li>Enum Constant Detail</li>
</ul>
</section>
</li>
<li class="blockList">
<section>
<h2>Tree (Class Hierarchy)</h2>
<p>There is a <a href="overview-tree.html">Class Hierarchy</a> page for all packages, plus a hierarchy for each package. Each hierarchy page contains a list of classes and a list of interfaces. Classes are organized by inheritance structure starting with <code>java.lang.Object</code>. Interfaces do not inherit from <code>java.lang.Object</code>.</p>
<ul>
<li>When viewing the Overview page, clicking on "Tree" displays the hierarchy for all packages.</li>
<li>When viewing a particular package, class or interface page, clicking on "Tree" displays the hierarchy for only that package.</li>
</ul>
</section>
</li>
<li class="blockList">
<section>
<h2>Deprecated API</h2>
<p>The <a href="deprecated-list.html">Deprecated API</a> page lists all of the API that have been deprecated. A deprecated API is not recommended for use, generally due to improvements, and a replacement API is usually given. Deprecated APIs may be removed in future implementations.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Index</h2>
<p>The <a href="index-all.html">Index</a> contains an alphabetic index of all classes, interfaces, constructors, methods, and fields, as well as lists of all packages and all classes.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>All&nbsp;Classes</h2>
<p>The <a href="allclasses.html">All Classes</a> link shows all classes and interfaces except non-static nested types.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Serialized Form</h2>
<p>Each serializable or externalizable class has a description of its serialization fields and methods. This information is of interest to re-implementors, not to developers using the API. While there is no link in the navigation bar, you can get to this information by going to any serialized class and clicking "Serialized Form" in the "See also" section of the class description.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Constant Field Values</h2>
<p>The <a href="constant-values.html">Constant Field Values</a> page lists the static final fields and their values.</p>
</section>
</li>
<li class="blockList">
<section>
<h2>Search</h2>
<p>You can search for definitions of modules, packages, types, fields, methods and other terms defined in the API, using some or all of the name. "Camel-case" abbreviations are supported: for example, "InpStr" will find "InputStream" and "InputStreamReader".</p>
</section>
</li>
</ul>
<hr>
<span class="emphasizedPhrase">This help file applies to API documentation generated by the standard doclet.</span></div>
</main>
<footer role="contentinfo">
<nav role="navigation">
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a id="navbar.bottom">
<!-- -->
</a>
<div class="skipNav"><a href="#skip.navbar.bottom" title="Skip navigation links">Skip navigation links</a></div>
<a id="navbar.bottom.firstrow">
<!-- -->
</a>
<ul class="navList" title="Navigation">
<li><a href="index.html">Overview</a></li>
<li>Package</li>
<li>Class</li>
<li><a href="overview-tree.html">Tree</a></li>
<li><a href="deprecated-list.html">Deprecated</a></li>
<li><a href="index-all.html">Index</a></li>
<li class="navBarCell1Rev">Help</li>
</ul>
<div class="aboutLanguage"> <script> window.MathJax = { 'loader': { 'load': ['[tex]/ams','[tex]/bussproofs'], }, 'tex': { 'packages': { '[+]': ['ams','bussproofs'], }, 'macros': { 'xor': '\\mathbin{xor}', 'ite': ['#1~\\mathbin{?}~#2~\\mathbin{:}~#3',3], 'inferrule': ['\\begin{prooftree}\\AxiomC{$#1$}\\UnaryInfC{$#2$}\\end{prooftree}',2], 'inferruleSC': ['\\begin{prooftree}\\AxiomC{$#1$}\\RightLabel{~#3}\\UnaryInfC{$#2$}\\end{prooftree}',3], } } } </script> <script type='text/javascript' id='MathJax-script' async src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'> </script> </div>
</div>
<div class="subNav">
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="allclasses.html">All&nbsp;Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
allClassesLink = document.getElementById("allclasses_navbar_bottom");
if(window==top) {
allClassesLink.style.display = "block";
}
else {
allClassesLink.style.display = "none";
}
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
</div>
<a id="skip.navbar.bottom">
<!-- -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</nav>
</footer>
</body>
</html>
Loading

0 comments on commit 405bf31

Please sign in to comment.