simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
sidekick/dev/sidekick-base/Sidekick_base/index.html
c-cube 97dab9ef8c deploy: 40a743badb
2023-02-24 02:08:35 +00:00

7 lines
No EOL
10 KiB
HTML
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_base (sidekick-base.Sidekick_base)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick-base</a> &#x00BB; Sidekick_base</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base</span></code></h1><p>Sidekick base</p><p>This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.</p><p>It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.</p><p>In addition, it has a notion of <a href="Statement/index.html#type-t">Statement</a>. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar notion of statements, and a <code>.smt2</code> files contains a list of statements.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Types_"><a href="#module-Types_" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Types_/index.html">Types_</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Term/index.html">Term</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Const"><a href="#module-Const" class="anchor"></a><code><span><span class="keyword">module</span> Const</span><span> = <a href="../../sidekick/Sidekick_core_logic/Const/index.html">Sidekick_core.Const</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Ty"><a href="#module-Ty" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Ty/index.html">Ty</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-ID"><a href="#module-ID" class="anchor"></a><code><span><span class="keyword">module</span> <a href="ID/index.html">ID</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Unique Identifiers</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Form"><a href="#module-Form" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Form/index.html">Form</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Formulas (boolean terms).</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Data_ty"><a href="#module-Data_ty" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Data_ty/index.html">Data_ty</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Cstor"><a href="#module-Cstor" class="anchor"></a><code><span><span class="keyword">module</span> Cstor</span><span> = <a href="Data_ty/Cstor/index.html">Data_ty.Cstor</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Select"><a href="#module-Select" class="anchor"></a><code><span><span class="keyword">module</span> Select</span><span> = <a href="Data_ty/Select/index.html">Data_ty.Select</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Statement"><a href="#module-Statement" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Statement/index.html">Statement</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Statements.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Solver"><a href="#module-Solver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Solver/index.html">Solver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Uconst"><a href="#module-Uconst" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Uconst/index.html">Uconst</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Uninterpreted constants</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Config"><a href="#module-Config" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Config/index.html">Config</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Configuration</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-LRA_term"><a href="#module-LRA_term" class="anchor"></a><code><span><span class="keyword">module</span> <a href="LRA_term/index.html">LRA_term</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Th_data"><a href="#module-Th_data" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Th_data/index.html">Th_data</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Theory of datatypes</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Th_bool"><a href="#module-Th_bool" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Th_bool/index.html">Th_bool</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Reducing boolean formulas to clauses</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Th_lra"><a href="#module-Th_lra" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Th_lra/index.html">Th_lra</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Theory of Linear Rational Arithmetic</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Th_ty_unin"><a href="#module-Th_ty_unin" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Th_ty_unin/index.html">Th_ty_unin</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-k_th_bool_config"><a href="#val-k_th_bool_config" class="anchor"></a><code><span><span class="keyword">val</span> k_th_bool_config : <span><span>[ `Dyn <span>| `Static</span> ]</span> <a href="Config/Key/index.html#type-t">Config.Key.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool"><a href="#val-th_bool" class="anchor"></a><code><span><span class="keyword">val</span> th_bool : <span><a href="Config/index.html#type-t">Config.t</a> <span class="arrow">&#45;&gt;</span></span> <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_dyn"><a href="#val-th_bool_dyn" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_dyn : <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_static"><a href="#val-th_bool_static" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_static : <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_data"><a href="#val-th_data" class="anchor"></a><code><span><span class="keyword">val</span> th_data : <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_lra"><a href="#val-th_lra" class="anchor"></a><code><span><span class="keyword">val</span> th_lra : <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_ty_unin"><a href="#val-th_ty_unin" class="anchor"></a><code><span><span class="keyword">val</span> th_ty_unin : <a href="Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-const_decoders"><a href="#val-const_decoders" class="anchor"></a><code><span><span class="keyword">val</span> const_decoders :
<span><span>(string
* <a href="../../sidekick/Sidekick_core_logic/Const/Ops/index.html#type-t">Sidekick_core.Const.Ops.t</a>
* <span>(<span><span><span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span> <a href="../../sidekick/Sidekick_util/Ser_decode/index.html#type-t">Sidekick_util.Ser_decode.t</a></span> <span class="arrow">&#45;&gt;</span></span>
<span><a href="../../sidekick/Sidekick_core_logic/Const/index.html#type-view">Sidekick_core.Const.view</a> <a href="../../sidekick/Sidekick_util/Ser_decode/index.html#type-t">Sidekick_util.Ser_decode.t</a></span>)</span>)</span>
list</span></span></code></div><div class="spec-doc"><p>All constant decoders</p></div></div></div></body></html>
Reference in a new issue View git blame Copy permalink