simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-22 01:06:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

deploy: be46f40312

Browse source
This commit is contained in:
c-cube 2021-07-04 01:47:36 +00:00
parent 86ac475398
commit 8167a40579
72 changed files with 69 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
dev/sidekick-base/Sidekick_base/Base_types/Cstor/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base.Base_types.Cstor)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Base_types.Cstor</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../ID/index.html#type-t">ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base.Base_types.Cstor)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Base_types.Cstor</code></h1><p>Datatype constructors.</p><p>A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../ID/index.html#type-t">ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Base_types/Data/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base.Base_types.Data)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Data</nav><h1>Module <code>Base_types.Data</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base.Base_types.Data)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Data</nav><h1>Module <code>Base_types.Data</code></h1><p>Datatypes</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/Base_types/Select/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base.Base_types.Select)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Select</nav><h1>Module <code>Base_types.Select</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base.Base_types.Select)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Select</nav><h1>Module <code>Base_types.Select</code></h1><p>Datatype selectors.</p><p>A selector is a kind of function that allows to obtain an argument of a given constructor.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../ID/index.html#type-t">ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Base_types/Statement/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base.Base_types.Statement)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Base_types.Statement</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../ID/index.html#type-t">ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../ID/index.html#type-t">ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base.Base_types.Statement)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Base_types.Statement</code></h1><p>Statements.</p><p>A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../ID/index.html#type-t">ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../ID/index.html#type-t">ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a statement</p></dd></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Base_types/Term/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/Base_types/Ty/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/Base_types/Value/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/Base_types/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/ID/B/index.html
View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>B (sidekick-base.Sidekick_base.ID.B)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">ID</a> &#x00BB; B</nav><h1>Module <code>ID.B</code></h1></header><dl><dt class="spec value" id="val-rat"><a href="#val-rat" class="anchor"></a><code><span class="keyword">val</span> rat : <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-int"><a href="#val-int" class="anchor"></a><code><span class="keyword">val</span> int : <a href="../index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/ID/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/Model/Fun_interpretation/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base.Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Model.Fun_interpretation</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> list</span> * <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> list</span> * <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base.Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base</a> &#x00BB; <a href="../index.html">Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Model.Fun_interpretation</code></h1><p>Model for function symbols.</p><p>Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:</p><p><code>lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault</code></p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> list</span> * <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a> list</span> * <a href="../../Base_types/Value/index.html#type-t">Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Model/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Model (sidekick-base.Sidekick_base.Model)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base</a> &#x00BB; Model</nav><h1>Module <code>Sidekick_base.Model</code></h1><h2 id="model"><a href="#model" class="anchor"></a>Model</h2></header><div class="spec module" id="module-Val_map"><a href="#module-Val_map" class="anchor"></a><code><span class="keyword">module</span> <a href="Val_map/index.html">Val_map</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Fun_interpretation"><a href="#module-Fun_interpretation" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun_interpretation/index.html">Fun_interpretation</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.values" class="anchored"><td class="def field"><a href="#type-t.values" class="anchor"></a><code>values : <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <a href="../../Sidekick_base__Base_types/Term/index.html#module-Map">Sidekick_base__.Base_types.Term.Map</a>.t</span>;</code></td></tr><tr id="type-t.funs" class="anchored"><td class="def field"><a href="#type-t.funs" class="anchor"></a><code>funs : <span><a href="Fun_interpretation/index.html#type-t">Fun_interpretation.t</a> <a href="../../Sidekick_base__Base_types/Fun/index.html#module-Map">Sidekick_base__.Base_types.Fun.Map</a>.t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> option</span></code></dt><dt class="spec value" id="val-merge"><a href="#val-merge" class="anchor"></a><code><span class="keyword">val</span> merge : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> option</span></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Model (sidekick-base.Sidekick_base.Model)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base</a> &#x00BB; Model</nav><h1>Module <code>Sidekick_base.Model</code></h1><p>Models</p><p>A model is a solution to the satisfiability question, created by the SMT solver when it proves the formula to be <b>satisfiable</b>.</p><p>A model gives a value to each term of the original formula(s), in such a way that the formula(s) is true when the term is replaced by its value.</p></header><div class="spec module" id="module-Val_map"><a href="#module-Val_map" class="anchor"></a><code><span class="keyword">module</span> <a href="Val_map/index.html">Val_map</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><dl><dt class="spec module" id="module-Fun_interpretation"><a href="#module-Fun_interpretation" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun_interpretation/index.html">Fun_interpretation</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Model for function symbols.</p></dd></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.values" class="anchored"><td class="def field"><a href="#type-t.values" class="anchor"></a><code>values : <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <a href="../../Sidekick_base__Base_types/Term/index.html#module-Map">Sidekick_base__.Base_types.Term.Map</a>.t</span>;</code></td></tr><tr id="type-t.funs" class="anchored"><td class="def field"><a href="#type-t.funs" class="anchor"></a><code>funs : <span><a href="Fun_interpretation/index.html#type-t">Fun_interpretation.t</a> <a href="../../Sidekick_base__Base_types/Fun/index.html#module-Map">Sidekick_base__.Base_types.Fun.Map</a>.t</span>;</code></td></tr></table><code>}</code></dt><dd><p>Model</p></dd></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dd><p>Empty model</p></dd></dl><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> option</span></code></dt><dt class="spec value" id="val-merge"><a href="#val-merge" class="anchor"></a><code><span class="keyword">val</span> merge : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Base_types/Term/index.html#type-t">Base_types.Term.t</a> <span>&#45;&gt;</span> <span><a href="../Base_types/Value/index.html#type-t">Base_types.Value.t</a> option</span></code></dt><dd><p><code>eval m t</code> tries to evaluate term <code>t</code> in the model. If it succeeds, the value is returned, otherwise <code>None</code> is.</p></dd></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base/Proof/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Base_types/Cstor/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base__.Base_types.Cstor)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Base_types.Cstor</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base__.Base_types.Cstor)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Base_types.Cstor</code></h1><p>Datatype constructors.</p><p>A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/Base_types/Data/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base__.Base_types.Data)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Data</nav><h1>Module <code>Base_types.Data</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base__.Base_types.Data)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Data</nav><h1>Module <code>Base_types.Data</code></h1><p>Datatypes</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Base_types/Select/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base__.Base_types.Select)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Select</nav><h1>Module <code>Base_types.Select</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base__.Base_types.Select)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Select</nav><h1>Module <code>Base_types.Select</code></h1><p>Datatype selectors.</p><p>A selector is a kind of function that allows to obtain an argument of a given constructor.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/Base_types/Statement/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base__.Base_types.Statement)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Base_types.Statement</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base__.Base_types.Statement)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Base_types.Statement</code></h1><p>Statements.</p><p>A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a statement</p></dd></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Base_types/Ty/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Base_types/Value/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Base_types/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/ID/B/index.html
View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>B (sidekick-base.Sidekick_base__.ID.B)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">ID</a> &#x00BB; B</nav><h1>Module <code>ID.B</code></h1></header><dl><dt class="spec value" id="val-rat"><a href="#val-rat" class="anchor"></a><code><span class="keyword">val</span> rat : <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-int"><a href="#val-int" class="anchor"></a><code><span class="keyword">val</span> int : <a href="../index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/ID/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Model/Fun_interpretation/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base__.Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Model.Fun_interpretation</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base__.Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> &#x00BB; <a href="../../index.html">Sidekick_base__</a> &#x00BB; <a href="../index.html">Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Model.Fun_interpretation</code></h1><p>Model for function symbols.</p><p>Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:</p><p><code>lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault</code></p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__/Model/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__/Proof/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Base_types/Cstor/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base__Base_types.Cstor)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Sidekick_base__Base_types.Cstor</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base__Base_types.Cstor)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Cstor</nav><h1>Module <code>Sidekick_base__Base_types.Cstor</code></h1><p>Datatype constructors.</p><p>A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-cstor">cstor</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.cstor_id" class="anchored"><td class="def field"><a href="#type-t.cstor_id" class="anchor"></a><code>cstor_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_is_a" class="anchored"><td class="def field"><a href="#type-t.cstor_is_a" class="anchor"></a><code>cstor_is_a : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.cstor_arity" class="anchored"><td class="def field"><a href="#type-t.cstor_arity" class="anchor"></a><code><span class="keyword">mutable</span> cstor_arity : int;</code></td></tr><tr id="type-t.cstor_args" class="anchored"><td class="def field"><a href="#type-t.cstor_args" class="anchor"></a><code>cstor_args : <span><span><a href="../index.html#type-select">select</a> list</span> lazy_t</span>;</code></td></tr><tr id="type-t.cstor_ty_as_data" class="anchored"><td class="def field"><a href="#type-t.cstor_ty_as_data" class="anchor"></a><code>cstor_ty_as_data : <a href="../index.html#type-data">data</a>;</code></td></tr><tr id="type-t.cstor_ty" class="anchored"><td class="def field"><a href="#type-t.cstor_ty" class="anchor"></a><code>cstor_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-id"><a href="#val-id" class="anchor"></a><code><span class="keyword">val</span> id : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a></code></dt><dt class="spec value" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span class="keyword">val</span> ty_args : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-ty">ty</a> Iter.t</span></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> <a href="../index.html#type-cstor">cstor</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Base_types/Data/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base__Base_types.Data)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Data</nav><h1>Module <code>Sidekick_base__Base_types.Data</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Data (sidekick-base.Sidekick_base__Base_types.Data)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Data</nav><h1>Module <code>Sidekick_base__Base_types.Data</code></h1><p>Datatypes</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-data">data</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.data_id" class="anchored"><td class="def field"><a href="#type-t.data_id" class="anchor"></a><code>data_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.data_cstors" class="anchored"><td class="def field"><a href="#type-t.data_cstors" class="anchor"></a><code>data_cstors : <span><span><a href="../index.html#type-cstor">cstor</a> <a href="../../Sidekick_base__ID/index.html#module-Map">Sidekick_base__.ID.Map</a>.t</span> lazy_t</span>;</code></td></tr><tr id="type-t.data_as_ty" class="anchored"><td class="def field"><a href="#type-t.data_as_ty" class="anchor"></a><code>data_as_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : CCFormat.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Base_types/Select/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base__Base_types.Select)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Select</nav><h1>Module <code>Sidekick_base__Base_types.Select</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base__Base_types.Select)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Select</nav><h1>Module <code>Sidekick_base__Base_types.Select</code></h1><p>Datatype selectors.</p><p>A selector is a kind of function that allows to obtain an argument of a given constructor.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-select">select</a></code><code> = </code><code>{</code><table class="record"><tr id="type-t.select_id" class="anchored"><td class="def field"><a href="#type-t.select_id" class="anchor"></a><code>select_id : <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a>;</code></td></tr><tr id="type-t.select_cstor" class="anchored"><td class="def field"><a href="#type-t.select_cstor" class="anchor"></a><code>select_cstor : <a href="../index.html#type-cstor">cstor</a>;</code></td></tr><tr id="type-t.select_ty" class="anchored"><td class="def field"><a href="#type-t.select_ty" class="anchor"></a><code>select_ty : <span><a href="../index.html#type-ty">ty</a> lazy_t</span>;</code></td></tr><tr id="type-t.select_i" class="anchored"><td class="def field"><a href="#type-t.select_i" class="anchor"></a><code>select_i : int;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty">ty</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Base_types/Statement/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base__Base_types.Statement)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Sidekick_base__Base_types.Statement</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Statement (sidekick-base.Sidekick_base__Base_types.Statement)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Base_types</a> &#x00BB; Statement</nav><h1>Module <code>Sidekick_base__Base_types.Statement</code></h1><p>Statements.</p><p>A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-statement">statement</a></code><code> = </code><table class="variant"><tr id="type-t.Stmt_set_logic" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_logic" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_logic</span> <span class="keyword">of</span> string</code></td></tr><tr id="type-t.Stmt_set_option" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_option" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_option</span> <span class="keyword">of</span> <span>string list</span></code></td></tr><tr id="type-t.Stmt_set_info" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_set_info" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_set_info</span> <span class="keyword">of</span> string * string</code></td></tr><tr id="type-t.Stmt_data" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_data" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_data</span> <span class="keyword">of</span> <span><a href="../index.html#type-data">data</a> list</span></code></td></tr><tr id="type-t.Stmt_ty_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_ty_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_ty_decl</span> <span class="keyword">of</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * int</code></td></tr><tr id="type-t.Stmt_decl" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_decl" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_decl</span> <span class="keyword">of</span> <a href="../../Sidekick_base/ID/index.html#type-t">Sidekick_base.ID.t</a> * <span><a href="../index.html#type-ty">ty</a> list</span> * <a href="../index.html#type-ty">ty</a></code></td></tr><tr id="type-t.Stmt_define" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_define" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_define</span> <span class="keyword">of</span> <span><a href="../index.html#type-definition">definition</a> list</span></code></td></tr><tr id="type-t.Stmt_assert" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert</span> <span class="keyword">of</span> <a href="../index.html#type-term">term</a></code></td></tr><tr id="type-t.Stmt_assert_clause" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_assert_clause" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_assert_clause</span> <span class="keyword">of</span> <span><a href="../index.html#type-term">term</a> list</span></code></td></tr><tr id="type-t.Stmt_check_sat" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_check_sat" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_check_sat</span> <span class="keyword">of</span> <span><span>(bool * <a href="../index.html#type-term">term</a>)</span> list</span></code></td></tr><tr id="type-t.Stmt_exit" class="anchored"><td class="def constructor"><a href="#type-t.Stmt_exit" class="anchor"></a><code>| </code><code><span class="constructor">Stmt_exit</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../index.html#module-Fmt">Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Pretty print a statement</p></dd></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Base_types/Term/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Base_types/Ty/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Base_types/Value/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Base_types/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__ID/B/index.html
View file

@ -1,2 +0,0 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>B (sidekick-base.Sidekick_base__ID.B)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__ID</a> &#x00BB; B</nav><h1>Module <code>Sidekick_base__ID.B</code></h1></header><dl><dt class="spec value" id="val-rat"><a href="#val-rat" class="anchor"></a><code><span class="keyword">val</span> rat : <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-int"><a href="#val-int" class="anchor"></a><code><span class="keyword">val</span> int : <a href="../index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__ID/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-base/Sidekick_base__Model/Fun_interpretation/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base__Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Sidekick_base__Model.Fun_interpretation</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Fun_interpretation (sidekick-base.Sidekick_base__Model.Fun_interpretation)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> &#x00BB; <a href="../index.html">Sidekick_base__Model</a> &#x00BB; Fun_interpretation</nav><h1>Module <code>Sidekick_base__Model.Fun_interpretation</code></h1><p>Model for function symbols.</p><p>Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:</p><p><code>lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault</code></p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.cases" class="anchored"><td class="def field"><a href="#type-t.cases" class="anchor"></a><code>cases : <span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Val_map/index.html#type-t">Val_map.t</a></span>;</code></td></tr><tr id="type-t.default" class="anchored"><td class="def field"><a href="#type-t.default" class="anchor"></a><code>default : <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-default"><a href="#val-default" class="anchor"></a><code><span class="keyword">val</span> default : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></code></dt><dt class="spec value" id="val-cases_list"><a href="#val-cases_list" class="anchor"></a><code><span class="keyword">val</span> cases_list : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span></code></dt><dt class="spec value" id="val-make"><a href="#val-make" class="anchor"></a><code><span class="keyword">val</span> make : <span>default:<a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a></span> <span>&#45;&gt;</span> <span><span>(<span><a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> list</span> * <a href="../../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a>)</span> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Model/index.html
View file

@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_base__Model (sidekick-base.Sidekick_base__Model)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../index.html">sidekick-base</a> &#x00BB; Sidekick_base__Model</nav><h1>Module <code>Sidekick_base__Model</code></h1><h2 id="model"><a href="#model" class="anchor"></a>Model</h2></header><div class="spec module" id="module-Val_map"><a href="#module-Val_map" class="anchor"></a><code><span class="keyword">module</span> <a href="Val_map/index.html">Val_map</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Fun_interpretation"><a href="#module-Fun_interpretation" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun_interpretation/index.html">Fun_interpretation</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.values" class="anchored"><td class="def field"><a href="#type-t.values" class="anchor"></a><code>values : <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Sidekick_base__Base_types/Term/index.html#module-Map">Sidekick_base__.Base_types.Term.Map</a>.t</span>;</code></td></tr><tr id="type-t.funs" class="anchored"><td class="def field"><a href="#type-t.funs" class="anchor"></a><code>funs : <span><a href="Fun_interpretation/index.html#type-t">Fun_interpretation.t</a> <a href="../Sidekick_base__Base_types/Fun/index.html#module-Map">Sidekick_base__.Base_types.Fun.Map</a>.t</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> option</span></code></dt><dt class="spec value" id="val-merge"><a href="#val-merge" class="anchor"></a><code><span class="keyword">val</span> merge : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> option</span></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_base__Model (sidekick-base.Sidekick_base__Model)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../index.html">sidekick-base</a> &#x00BB; Sidekick_base__Model</nav><h1>Module <code>Sidekick_base__Model</code></h1><p>Models</p><p>A model is a solution to the satisfiability question, created by the SMT solver when it proves the formula to be <b>satisfiable</b>.</p><p>A model gives a value to each term of the original formula(s), in such a way that the formula(s) is true when the term is replaced by its value.</p></header><div class="spec module" id="module-Val_map"><a href="#module-Val_map" class="anchor"></a><code><span class="keyword">module</span> <a href="Val_map/index.html">Val_map</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><dl><dt class="spec module" id="module-Fun_interpretation"><a href="#module-Fun_interpretation" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun_interpretation/index.html">Fun_interpretation</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Model for function symbols.</p></dd></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.values" class="anchored"><td class="def field"><a href="#type-t.values" class="anchor"></a><code>values : <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <a href="../Sidekick_base__Base_types/Term/index.html#module-Map">Sidekick_base__.Base_types.Term.Map</a>.t</span>;</code></td></tr><tr id="type-t.funs" class="anchored"><td class="def field"><a href="#type-t.funs" class="anchor"></a><code>funs : <span><a href="Fun_interpretation/index.html#type-t">Fun_interpretation.t</a> <a href="../Sidekick_base__Base_types/Fun/index.html#module-Map">Sidekick_base__.Base_types.Fun.Map</a>.t</span>;</code></td></tr></table><code>}</code></dt><dd><p>Model</p></dd></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dd><p>Empty model</p></dd></dl><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> option</span></code></dt><dt class="spec value" id="val-merge"><a href="#val-merge" class="anchor"></a><code><span class="keyword">val</span> merge : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Sidekick_base/Base_types/Term/index.html#type-t">Sidekick_base.Base_types.Term.t</a> <span>&#45;&gt;</span> <span><a href="../Sidekick_base/Base_types/Value/index.html#type-t">Sidekick_base.Base_types.Value.t</a> option</span></code></dt><dd><p><code>eval m t</code> tries to evaluate term <code>t</code> in the model. If it succeeds, the value is returned, otherwise <code>None</code> is.</p></dd></dl></div></body></html>

2
dev/sidekick-base/Sidekick_base__Proof/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-bin/Sidekick_smtlib__Process/Solver/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_cc/Make/argument-1-A/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_cc/module-type-S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-CC_ARG/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-CC_S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-PROOF/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_msat_solver/Make/argument-1-A/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_msat_solver/module-type-ARG/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_msat_solver/module-type-S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html
View file

File diff suppressed because one or more lines are too long