mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-21 16:56:41 -05:00
deploy: 619da6fbcb
This commit is contained in:
c-cube
parent
97dab9ef8c
commit
66a155a155
320 changed files with 296 additions and 296 deletions
|
|
@ -2,7 +2,7 @@
|
|||
<html xmlns="http://www.w3.org/1999/xhtml">
|
||||
<head>
|
||||
<title>index</title>
|
||||
<link rel="stylesheet" href="./_odoc_support/odoc.css"/>
|
||||
<link rel="stylesheet" href="./odoc.support/odoc.css"/>
|
||||
<meta charset="utf-8"/>
|
||||
<meta name="viewport" content="width=device-width,initial-scale=1.0"/>
|
||||
</head>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Key (sidekick-base.Sidekick_base.Config.Key)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Config</a> » Key</nav><header class="odoc-preamble"><h1>Module <code><span>Config.Key</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span>unit <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Compare two keys that have compatible types</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Key (sidekick-base.Sidekick_base.Config.Key)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Config</a> » Key</nav><header class="odoc-preamble"><h1>Module <code><span>Config.Key</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span>unit <span class="arrow">-></span></span> <span><span class="type-var">'a</span> <a href="#type-t">t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Compare two keys that have compatible types</p></div></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base.Data_ty.Cstor)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Data_ty</a> » Cstor</nav><header class="odoc-preamble"><h1>Module <code><span>Data_ty.Cstor</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../index.html#type-cstor">cstor</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span><span class="keyword">val</span> ty_args : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../../Types_/index.html#type-ty">Types_.ty</a> list</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-select_idx"><a href="#val-select_idx" class="anchor"></a><code><span><span class="keyword">val</span> select_idx : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="../index.html#type-select">select</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Cstor (sidekick-base.Sidekick_base.Data_ty.Cstor)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Data_ty</a> » Cstor</nav><header class="odoc-preamble"><h1>Module <code><span>Data_ty.Cstor</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../index.html#type-cstor">cstor</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ty_args"><a href="#val-ty_args" class="anchor"></a><code><span><span class="keyword">val</span> ty_args : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../../Types_/index.html#type-ty">Types_.ty</a> list</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-select_idx"><a href="#val-select_idx" class="anchor"></a><code><span><span class="keyword">val</span> select_idx : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="../index.html#type-select">select</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base.Data_ty.Select)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Data_ty</a> » Select</nav><header class="odoc-preamble"><h1>Module <code><span>Data_ty.Select</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../index.html#type-select">select</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Select (sidekick-base.Sidekick_base.Data_ty.Select)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">Data_ty</a> » Select</nav><header class="odoc-preamble"><h1>Module <code><span>Data_ty.Select</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../index.html#type-select">select</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Op (sidekick-base.Sidekick_base.LRA_term.Op)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">LRA_term</a> » Op</nav><header class="odoc-preamble"><h1>Module <code><span>LRA_term.Op</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../../sidekick/Sidekick_th_lra/index.html#type-op">Sidekick_th_lra.op</a></span><span> = </span></code><ol><li id="type-t.Plus" class="def variant constructor anchored"><a href="#type-t.Plus" class="anchor"></a><code><span>| </span><span><span class="constructor">Plus</span></span></code></li><li id="type-t.Minus" class="def variant constructor anchored"><a href="#type-t.Minus" class="anchor"></a><code><span>| </span><span><span class="constructor">Minus</span></span></code></li></ol></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Op (sidekick-base.Sidekick_base.LRA_term.Op)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-base</a> » <a href="../../index.html">Sidekick_base</a> » <a href="../index.html">LRA_term</a> » Op</nav><header class="odoc-preamble"><h1>Module <code><span>LRA_term.Op</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../../sidekick/Sidekick_th_lra/index.html#type-op">Sidekick_th_lra.op</a></span><span> = </span></code><ol><li id="type-t.Plus" class="def variant constructor anchored"><a href="#type-t.Plus" class="anchor"></a><code><span>| </span><span><span class="constructor">Plus</span></span></code></li><li id="type-t.Minus" class="def variant constructor anchored"><a href="#type-t.Minus" class="anchor"></a><code><span>| </span><span><span class="constructor">Minus</span></span></code></li></ol></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html">Sidekick_sigs.EQ_HASH_PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ_HASH_PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../sidekick/Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../sidekick/Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></details></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Solver (sidekick-base.Sidekick_base.Solver)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Solver</span></code></h1></header><div class="odoc-content"><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_smt_solver/Solver/index.html">Sidekick_smt_solver.Solver</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> Check_res</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Check_res/index.html">Sidekick_smt_solver.Solver.Check_res</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> Unknown</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Unknown/index.html">Sidekick_smt_solver.Solver.Unknown</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/Solver/index.html#type-t">Sidekick_smt_solver.Solver.t</a></span></code></div><div class="spec-doc"><p>The solver's state.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-registry"><a href="#val-registry" class="anchor"></a><code><span><span class="keyword">val</span> registry : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_smt_solver/Registry/index.html#type-t">Sidekick_smt_solver.Registry.t</a></span></code></div><div class="spec-doc"><p>A solver contains a registry so that theories can share data</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-theory"><a href="#type-theory" class="anchor"></a><code><span><span class="keyword">type</span> theory</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/Theory/index.html#type-t">Sidekick_smt_solver.Theory.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span><span class="keyword">val</span> mk_theory :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Solver (sidekick-base.Sidekick_base.Solver)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Solver</span></code></h1></header><div class="odoc-content"><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_smt_solver/Solver/index.html">Sidekick_smt_solver.Solver</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> Check_res</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Check_res/index.html">Sidekick_smt_solver.Solver.Check_res</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> Unknown</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Unknown/index.html">Sidekick_smt_solver.Solver.Unknown</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/Solver/index.html#type-t">Sidekick_smt_solver.Solver.t</a></span></code></div><div class="spec-doc"><p>The solver's state.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-registry"><a href="#val-registry" class="anchor"></a><code><span><span class="keyword">val</span> registry : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_smt_solver/Registry/index.html#type-t">Sidekick_smt_solver.Registry.t</a></span></code></div><div class="spec-doc"><p>A solver contains a registry so that theories can share data</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-theory"><a href="#type-theory" class="anchor"></a><code><span><span class="keyword">type</span> theory</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/Theory/index.html#type-t">Sidekick_smt_solver.Theory.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span><span class="keyword">val</span> mk_theory :
|
||||
<span>name:string <span class="arrow">-></span></span>
|
||||
<span>create_and_setup:
|
||||
<span>(<span>id:<a href="../../../sidekick/Sidekick_smt_solver/Theory_id/index.html#type-t">Sidekick_smt_solver.Theory_id.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_bool (sidekick-base.Sidekick_base.Th_bool)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_bool</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_bool</span></code></h1><p>Reducing boolean formulas to clauses</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-k_config"><a href="#val-k_config" class="anchor"></a><code><span><span class="keyword">val</span> k_config : <span><span>[ `Dyn <span>| `Static</span> ]</span> <a href="../Config/Key/index.html#type-t">Config.Key.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory_static"><a href="#val-theory_static" class="anchor"></a><code><span><span class="keyword">val</span> theory_static : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory_dyn"><a href="#val-theory_dyn" class="anchor"></a><code><span><span class="keyword">val</span> theory_dyn : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <span><a href="../Config/index.html#type-t">Config.t</a> <span class="arrow">-></span></span> <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_bool (sidekick-base.Sidekick_base.Th_bool)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_bool</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_bool</span></code></h1><p>Reducing boolean formulas to clauses</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-k_config"><a href="#val-k_config" class="anchor"></a><code><span><span class="keyword">val</span> k_config : <span><span>[ `Dyn <span>| `Static</span> ]</span> <a href="../Config/Key/index.html#type-t">Config.Key.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory_static"><a href="#val-theory_static" class="anchor"></a><code><span><span class="keyword">val</span> theory_static : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory_dyn"><a href="#val-theory_dyn" class="anchor"></a><code><span><span class="keyword">val</span> theory_dyn : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <span><a href="../Config/index.html#type-t">Config.t</a> <span class="arrow">-></span></span> <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_data (sidekick-base.Sidekick_base.Th_data)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_data</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_data</span></code></h1><p>Theory of datatypes</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-arg"><a href="#val-arg" class="anchor"></a><code><span><span class="keyword">val</span> arg : <span>(<span class="keyword">module</span> <a href="../../../sidekick/Sidekick_th_data/module-type-ARG/index.html">Sidekick_th_data.ARG</a>)</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../../../sidekick/Sidekick_smt_solver/index.html#type-theory">Sidekick_th_data.SMT.theory</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_data (sidekick-base.Sidekick_base.Th_data)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_data</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_data</span></code></h1><p>Theory of datatypes</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-arg"><a href="#val-arg" class="anchor"></a><code><span><span class="keyword">val</span> arg : <span>(<span class="keyword">module</span> <a href="../../../sidekick/Sidekick_th_data/module-type-ARG/index.html">Sidekick_th_data.ARG</a>)</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../../../sidekick/Sidekick_smt_solver/index.html#type-theory">Sidekick_th_data.SMT.theory</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_lra (sidekick-base.Sidekick_base.Th_lra)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_lra</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_lra</span></code></h1><p>Theory of Linear Rational Arithmetic</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-T"><a href="#module-T" class="anchor"></a><code><span><span class="keyword">module</span> T</span><span> = <a href="../../../sidekick/Sidekick_core/Term/index.html">Sidekick_core.Term</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Q"><a href="#module-Q" class="anchor"></a><code><span><span class="keyword">module</span> Q</span><span> = <a href="../../../sidekick/Sidekick_zarith/Rational/index.html">Sidekick_zarith.Rational</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><code><span><span class="keyword">val</span> mk_eq : <span><a href="../../../sidekick/Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span> <span><a href="../Form/index.html#type-term">Form.term</a> <span class="arrow">-></span></span> <span><a href="../Form/index.html#type-term">Form.term</a> <span class="arrow">-></span></span> <a href="../Form/index.html#type-term">Form.term</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_bool"><a href="#val-mk_bool" class="anchor"></a><code><span><span class="keyword">val</span> mk_bool : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_lra (sidekick-base.Sidekick_base.Th_lra)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_lra</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_lra</span></code></h1><p>Theory of Linear Rational Arithmetic</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-T"><a href="#module-T" class="anchor"></a><code><span><span class="keyword">module</span> T</span><span> = <a href="../../../sidekick/Sidekick_core/Term/index.html">Sidekick_core.Term</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Q"><a href="#module-Q" class="anchor"></a><code><span><span class="keyword">module</span> Q</span><span> = <a href="../../../sidekick/Sidekick_zarith/Rational/index.html">Sidekick_zarith.Rational</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><code><span><span class="keyword">val</span> mk_eq : <span><a href="../../../sidekick/Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span> <span><a href="../Form/index.html#type-term">Form.term</a> <span class="arrow">-></span></span> <span><a href="../Form/index.html#type-term">Form.term</a> <span class="arrow">-></span></span> <a href="../Form/index.html#type-term">Form.term</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_bool"><a href="#val-mk_bool" class="anchor"></a><code><span><span class="keyword">val</span> mk_bool : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_ty_unin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_ty_unin</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Th_ty_unin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Th_ty_unin</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-theory">Solver.theory</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ty (sidekick-base.Sidekick_base.Ty)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Ty</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Ty</span></code></h1></header><div class="odoc-content"><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core/Term/index.html">Sidekick_core.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html">Sidekick_core_logic.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec type anchored" id="type-var"><a href="#type-var" class="anchor"></a><code><span><span class="keyword">type</span> var</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Var/index.html#type-t">Sidekick_core_logic.Var.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-bvar"><a href="#type-bvar" class="anchor"></a><code><span><span class="keyword">type</span> bvar</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Bvar/index.html#type-t">Sidekick_core_logic.Bvar.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-store"><a href="#type-store" class="anchor"></a><code><span><span class="keyword">type</span> store</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a></span></code></div><div class="spec-doc"><p>The store for terms.</p><p>The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-view"><a href="#type-view" class="anchor"></a><code><span><span class="keyword">type</span> view</span><span> = </span></code><ol><li id="type-view.E_type" class="def variant constructor anchored"><a href="#type-view.E_type" class="anchor"></a><code><span>| </span><span><span class="constructor">E_type</span> <span class="keyword">of</span> int</span></code></li><li id="type-view.E_var" class="def variant constructor anchored"><a href="#type-view.E_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_var</span> <span class="keyword">of</span> <a href="#type-var">var</a></span></code></li><li id="type-view.E_bound_var" class="def variant constructor anchored"><a href="#type-view.E_bound_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_bound_var</span> <span class="keyword">of</span> <a href="#type-bvar">bvar</a></span></code></li></ol></div><div class="spec-doc"><p>View.</p><p>A view is the shape of the root node of a term.</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ_ORD_HASH/index.html">Sidekick_sigs.EQ_ORD_HASH</a>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ty (sidekick-base.Sidekick_base.Ty)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Ty</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Ty</span></code></h1></header><div class="odoc-content"><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core/Term/index.html">Sidekick_core.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html">Sidekick_core_logic.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec type anchored" id="type-var"><a href="#type-var" class="anchor"></a><code><span><span class="keyword">type</span> var</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Var/index.html#type-t">Sidekick_core_logic.Var.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-bvar"><a href="#type-bvar" class="anchor"></a><code><span><span class="keyword">type</span> bvar</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Bvar/index.html#type-t">Sidekick_core_logic.Bvar.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-store"><a href="#type-store" class="anchor"></a><code><span><span class="keyword">type</span> store</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a></span></code></div><div class="spec-doc"><p>The store for terms.</p><p>The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-view"><a href="#type-view" class="anchor"></a><code><span><span class="keyword">type</span> view</span><span> = </span></code><ol><li id="type-view.E_type" class="def variant constructor anchored"><a href="#type-view.E_type" class="anchor"></a><code><span>| </span><span><span class="constructor">E_type</span> <span class="keyword">of</span> int</span></code></li><li id="type-view.E_var" class="def variant constructor anchored"><a href="#type-view.E_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_var</span> <span class="keyword">of</span> <a href="#type-var">var</a></span></code></li><li id="type-view.E_bound_var" class="def variant constructor anchored"><a href="#type-view.E_bound_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_bound_var</span> <span class="keyword">of</span> <a href="#type-bvar">bvar</a></span></code></li></ol></div><div class="spec-doc"><p>View.</p><p>A view is the shape of the root node of a term.</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ_ORD_HASH/index.html">Sidekick_sigs.EQ_ORD_HASH</a>
|
||||
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ_ORD_HASH/index.html#type-t">t</a> := <span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span></span></span></code></summary><div class="odoc-include shadowed-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span></span></span></code></summary></details></div><div class="odoc-include shadowed-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-ORD/index.html">Sidekick_sigs.ORD</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-ORD/index.html#type-t">t</a> := <span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span></span></span></code></summary></details></div><div class="odoc-include shadowed-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span></span></span></code></summary></details></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_debug"><a href="#val-pp_debug" class="anchor"></a><code><span><span class="keyword">val</span> pp_debug : <span><span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_debug_with_ids"><a href="#val-pp_debug_with_ids" class="anchor"></a><code><span><span class="keyword">val</span> pp_debug_with_ids :
|
||||
<span><span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><h3 id="containers"><a href="#containers" class="anchor"></a>Containers</h3><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_SET_MAP_TBL/index.html">Sidekick_sigs.WITH_SET_MAP_TBL</a>
|
||||
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_SET_MAP_TBL/index.html#type-t">t</a> := <span class="xref-unresolved">Sidekick_core_logic__.Types_.term</span></span></span></code></summary><div class="odoc-spec"><div class="spec module anchored" id="module-Set"><a href="#module-Set" class="anchor"></a><code><span><span class="keyword">module</span> Set</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Set/index.html">Sidekick_core.Term.Set</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Map"><a href="#module-Map" class="anchor"></a><code><span><span class="keyword">module</span> Map</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Map/index.html">Sidekick_core.Term.Map</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><code><span><span class="keyword">module</span> Tbl</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Tbl/index.html">Sidekick_core.Term.Tbl</a></span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html">Sidekick_sigs.WITH_WEAK</a>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Check_cc (sidekick-base.Sidekick_smtlib.Check_cc)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Check_cc</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Check_cc</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-cdcl_theory">Solver.cdcl_theory</a></span></code></div><div class="spec-doc"><p>theory that check validity of EUF conflicts, on the fly</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Check_cc (sidekick-base.Sidekick_smtlib.Check_cc)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Check_cc</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Check_cc</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span><span class="keyword">val</span> theory : <a href="../Solver/index.html#type-cdcl_theory">Solver.cdcl_theory</a></span></code></div><div class="spec-doc"><p>theory that check validity of EUF conflicts, on the fly</p></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Driver (sidekick-base.Sidekick_smtlib.Driver)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Driver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Driver</span></code></h1><p>Driver.</p><p>The driver is responsible for processing statements from a SMTLIB file, and interacting with the solver based on the statement (asserting formulas, calling "solve", etc.)</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> Asolver</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/index.html">Sidekick_abstract_solver.Asolver</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_dyn"><a href="#val-th_bool_dyn" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_dyn : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_static"><a href="#val-th_bool_static" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_static : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool"><a href="#val-th_bool" class="anchor"></a><code><span><span class="keyword">val</span> th_bool : <span><a href="../../Sidekick_base/Config/index.html#type-t">Sidekick_base.Config.t</a> <span class="arrow">-></span></span> <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_data"><a href="#val-th_data" class="anchor"></a><code><span><span class="keyword">val</span> th_data : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_lra"><a href="#val-th_lra" class="anchor"></a><code><span><span class="keyword">val</span> th_lra : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_ty_unin"><a href="#val-th_ty_unin" class="anchor"></a><code><span><span class="keyword">val</span> th_ty_unin : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_error"><a href="#type-or_error" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a or_error</span></span><span> = <span><span>(<span class="type-var">'a</span>, string)</span> <span class="xref-unresolved">CCResult</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>The SMTLIB driver</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Driver (sidekick-base.Sidekick_smtlib.Driver)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Driver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Driver</span></code></h1><p>Driver.</p><p>The driver is responsible for processing statements from a SMTLIB file, and interacting with the solver based on the statement (asserting formulas, calling "solve", etc.)</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> Asolver</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/index.html">Sidekick_abstract_solver.Asolver</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_dyn"><a href="#val-th_bool_dyn" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_dyn : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool_static"><a href="#val-th_bool_static" class="anchor"></a><code><span><span class="keyword">val</span> th_bool_static : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_bool"><a href="#val-th_bool" class="anchor"></a><code><span><span class="keyword">val</span> th_bool : <span><a href="../../Sidekick_base/Config/index.html#type-t">Sidekick_base.Config.t</a> <span class="arrow">-></span></span> <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_data"><a href="#val-th_data" class="anchor"></a><code><span><span class="keyword">val</span> th_data : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_lra"><a href="#val-th_lra" class="anchor"></a><code><span><span class="keyword">val</span> th_lra : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-th_ty_unin"><a href="#val-th_ty_unin" class="anchor"></a><code><span><span class="keyword">val</span> th_ty_unin : <a href="../../Sidekick_base/Solver/index.html#type-theory">Sidekick_base.Solver.theory</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_error"><a href="#type-or_error" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a or_error</span></span><span> = <span><span>(<span class="type-var">'a</span>, string)</span> <span class="xref-unresolved">CCResult</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>The SMTLIB driver</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<span>?pp_cnf:bool <span class="arrow">-></span></span>
|
||||
<span>?proof_file:string <span class="arrow">-></span></span>
|
||||
<span>?pp_model:bool <span class="arrow">-></span></span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Solver (sidekick-base.Sidekick_smtlib.Solver)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Solver</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> Asolver</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/index.html">Sidekick_abstract_solver.Asolver</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Smt_solver"><a href="#module-Smt_solver" class="anchor"></a><code><span><span class="keyword">module</span> Smt_solver</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/index.html">Sidekick_smt_solver</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html">Asolver.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-cdcl_theory"><a href="#type-cdcl_theory" class="anchor"></a><code><span><span class="keyword">type</span> cdcl_theory</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/index.html#type-theory">Smt_solver.theory</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Solver (sidekick-base.Sidekick_smtlib.Solver)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-base</a> » <a href="../index.html">Sidekick_smtlib</a> » Solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib.Solver</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> Asolver</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/index.html">Sidekick_abstract_solver.Asolver</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Smt_solver"><a href="#module-Smt_solver" class="anchor"></a><code><span><span class="keyword">module</span> Smt_solver</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/index.html">Sidekick_smt_solver</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../../../sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html">Asolver.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-cdcl_theory"><a href="#type-cdcl_theory" class="anchor"></a><code><span><span class="keyword">type</span> cdcl_theory</span><span> = <a href="../../../sidekick/Sidekick_smt_solver/index.html#type-theory">Smt_solver.theory</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_smtlib (sidekick-base.Sidekick_smtlib)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick-base</a> » Sidekick_smtlib</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib</span></code></h1><p>SMTLib-2.6 Driver</p></header><div class="odoc-content"><p>This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.</p><div class="odoc-spec"><div class="spec type anchored" id="type-or_error"><a href="#type-or_error" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a or_error</span></span><span> = <span><span>(<span class="type-var">'a</span>, string)</span> <span class="xref-unresolved">CCResult</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span><span class="keyword">module</span> Term</span><span> = <a href="../Sidekick_base/Term/index.html">Sidekick_base.Term</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Stmt"><a href="#module-Stmt" class="anchor"></a><code><span><span class="keyword">module</span> Stmt</span><span> = <a href="../Sidekick_base/Statement/index.html">Sidekick_base.Statement</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Driver"><a href="#module-Driver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Driver/index.html">Driver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Driver.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Solver"><a href="#module-Solver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Solver/index.html">Solver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_cc"><a href="#module-Check_cc" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Check_cc/index.html">Check_cc</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Model"><a href="#module-Model" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Model/index.html">Model</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Models</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse"><a href="#val-parse" class="anchor"></a><code><span><span class="keyword">val</span> parse : <span><a href="../Sidekick_base/Term/index.html#type-store">Term.store</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <span><span><a href="../Sidekick_base/Statement/index.html#type-t">Stmt.t</a> list</span> <a href="#type-or_error">or_error</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_stdin"><a href="#val-parse_stdin" class="anchor"></a><code><span><span class="keyword">val</span> parse_stdin : <span><a href="../Sidekick_base/Term/index.html#type-store">Term.store</a> <span class="arrow">-></span></span> <span><span><a href="../Sidekick_base/Statement/index.html#type-t">Stmt.t</a> list</span> <a href="#type-or_error">or_error</a></span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_smtlib (sidekick-base.Sidekick_smtlib)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick-base</a> » Sidekick_smtlib</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_smtlib</span></code></h1><p>SMTLib-2.6 Driver</p></header><div class="odoc-content"><p>This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.</p><div class="odoc-spec"><div class="spec type anchored" id="type-or_error"><a href="#type-or_error" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a or_error</span></span><span> = <span><span>(<span class="type-var">'a</span>, string)</span> <span class="xref-unresolved">CCResult</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span><span class="keyword">module</span> Term</span><span> = <a href="../Sidekick_base/Term/index.html">Sidekick_base.Term</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Stmt"><a href="#module-Stmt" class="anchor"></a><code><span><span class="keyword">module</span> Stmt</span><span> = <a href="../Sidekick_base/Statement/index.html">Sidekick_base.Statement</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Driver"><a href="#module-Driver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Driver/index.html">Driver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Driver.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Solver"><a href="#module-Solver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Solver/index.html">Solver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_cc"><a href="#module-Check_cc" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Check_cc/index.html">Check_cc</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Model"><a href="#module-Model" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Model/index.html">Model</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Models</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse"><a href="#val-parse" class="anchor"></a><code><span><span class="keyword">val</span> parse : <span><a href="../Sidekick_base/Term/index.html#type-store">Term.store</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <span><span><a href="../Sidekick_base/Statement/index.html#type-t">Stmt.t</a> list</span> <a href="#type-or_error">or_error</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_stdin"><a href="#val-parse_stdin" class="anchor"></a><code><span><span class="keyword">val</span> parse_stdin : <span><a href="../Sidekick_base/Term/index.html#type-store">Term.store</a> <span class="arrow">-></span></span> <span><span><a href="../Sidekick_base/Statement/index.html#type-t">Stmt.t</a> list</span> <a href="#type-or_error">or_error</a></span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>index (sidekick-base.index)</title><link rel="stylesheet" href="../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – sidekick-base</nav><header class="odoc-preamble"><h1 id="sidekick-base-index"><a href="#sidekick-base-index" class="anchor"></a>sidekick-base index</h1></header><nav class="odoc-toc"><ul><li><a href="#library-sidekick-base">Library sidekick-base</a></li><li><a href="#library-sidekick-base.smtlib">Library sidekick-base.smtlib</a></li></ul></nav><div class="odoc-content"><h2 id="library-sidekick-base"><a href="#library-sidekick-base" class="anchor"></a>Library sidekick-base</h2><p>The entry point of this library is the module: <a href="Sidekick_base/index.html"><code>Sidekick_base</code></a>.</p><h2 id="library-sidekick-base.smtlib"><a href="#library-sidekick-base.smtlib" class="anchor"></a>Library sidekick-base.smtlib</h2><p>The entry point of this library is the module: <a href="Sidekick_smtlib/index.html"><code>Sidekick_smtlib</code></a>.</p></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>index (sidekick-base.index)</title><link rel="stylesheet" href="../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – sidekick-base</nav><header class="odoc-preamble"><h1 id="sidekick-base-index"><a href="#sidekick-base-index" class="anchor"></a>sidekick-base index</h1></header><nav class="odoc-toc"><ul><li><a href="#library-sidekick-base">Library sidekick-base</a></li><li><a href="#library-sidekick-base.smtlib">Library sidekick-base.smtlib</a></li></ul></nav><div class="odoc-content"><h2 id="library-sidekick-base"><a href="#library-sidekick-base" class="anchor"></a>Library sidekick-base</h2><p>The entry point of this library is the module: <a href="Sidekick_base/index.html"><code>Sidekick_base</code></a>.</p><h2 id="library-sidekick-base.smtlib"><a href="#library-sidekick-base.smtlib" class="anchor"></a>Library sidekick-base.smtlib</h2><p>The entry point of this library is the module: <a href="Sidekick_smtlib/index.html"><code>Sidekick_smtlib</code></a>.</p></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dimacs_lexer (sidekick-bin.Sidekick_bin_lib.Dimacs_lexer)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Dimacs_lexer</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Dimacs_lexer</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-token"><a href="#type-token" class="anchor"></a><code><span><span class="keyword">type</span> token</span><span> = </span></code><ol><li id="type-token.EOF" class="def variant constructor anchored"><a href="#type-token.EOF" class="anchor"></a><code><span>| </span><span><span class="constructor">EOF</span></span></code></li><li id="type-token.P" class="def variant constructor anchored"><a href="#type-token.P" class="anchor"></a><code><span>| </span><span><span class="constructor">P</span></span></code></li><li id="type-token.CNF" class="def variant constructor anchored"><a href="#type-token.CNF" class="anchor"></a><code><span>| </span><span><span class="constructor">CNF</span></span></code></li><li id="type-token.ZERO" class="def variant constructor anchored"><a href="#type-token.ZERO" class="anchor"></a><code><span>| </span><span><span class="constructor">ZERO</span></span></code></li><li id="type-token.LIT" class="def variant constructor anchored"><a href="#type-token.LIT" class="anchor"></a><code><span>| </span><span><span class="constructor">LIT</span> <span class="keyword">of</span> int</span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_tables"><a href="#val-__ocaml_lex_tables" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_tables : <span class="xref-unresolved">Stdlib</span>.Lexing.lex_tables</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-token"><a href="#val-token" class="anchor"></a><code><span><span class="keyword">val</span> token : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_token_rec"><a href="#val-__ocaml_lex_token_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_token_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-comment"><a href="#val-comment" class="anchor"></a><code><span><span class="keyword">val</span> comment : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_comment_rec"><a href="#val-__ocaml_lex_comment_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_comment_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dimacs_lexer (sidekick-bin.Sidekick_bin_lib.Dimacs_lexer)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Dimacs_lexer</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Dimacs_lexer</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-token"><a href="#type-token" class="anchor"></a><code><span><span class="keyword">type</span> token</span><span> = </span></code><ol><li id="type-token.EOF" class="def variant constructor anchored"><a href="#type-token.EOF" class="anchor"></a><code><span>| </span><span><span class="constructor">EOF</span></span></code></li><li id="type-token.P" class="def variant constructor anchored"><a href="#type-token.P" class="anchor"></a><code><span>| </span><span><span class="constructor">P</span></span></code></li><li id="type-token.CNF" class="def variant constructor anchored"><a href="#type-token.CNF" class="anchor"></a><code><span>| </span><span><span class="constructor">CNF</span></span></code></li><li id="type-token.ZERO" class="def variant constructor anchored"><a href="#type-token.ZERO" class="anchor"></a><code><span>| </span><span><span class="constructor">ZERO</span></span></code></li><li id="type-token.LIT" class="def variant constructor anchored"><a href="#type-token.LIT" class="anchor"></a><code><span>| </span><span><span class="constructor">LIT</span> <span class="keyword">of</span> int</span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_tables"><a href="#val-__ocaml_lex_tables" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_tables : <span class="xref-unresolved">Stdlib</span>.Lexing.lex_tables</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-token"><a href="#val-token" class="anchor"></a><code><span><span class="keyword">val</span> token : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_token_rec"><a href="#val-__ocaml_lex_token_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_token_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-comment"><a href="#val-comment" class="anchor"></a><code><span><span class="keyword">val</span> comment : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_comment_rec"><a href="#val-__ocaml_lex_comment_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_comment_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dimacs_parser (sidekick-bin.Sidekick_bin_lib.Dimacs_parser)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Dimacs_parser</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Dimacs_parser</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#dimacs-parser">DIMACS parser</a></li></ul></nav><div class="odoc-content"><h2 id="dimacs-parser"><a href="#dimacs-parser" class="anchor"></a>DIMACS parser</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><span class="xref-unresolved">Stdlib</span>.in_channel <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_header"><a href="#val-parse_header" class="anchor"></a><code><span><span class="keyword">val</span> parse_header : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int * int</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-next_clause"><a href="#val-next_clause" class="anchor"></a><code><span><span class="keyword">val</span> next_clause : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>int list</span> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter"><a href="#val-iter" class="anchor"></a><code><span><span class="keyword">val</span> iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>int list</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Dimacs_parser (sidekick-bin.Sidekick_bin_lib.Dimacs_parser)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Dimacs_parser</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Dimacs_parser</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#dimacs-parser">DIMACS parser</a></li></ul></nav><div class="odoc-content"><h2 id="dimacs-parser"><a href="#dimacs-parser" class="anchor"></a>DIMACS parser</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><span class="xref-unresolved">Stdlib</span>.in_channel <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_header"><a href="#val-parse_header" class="anchor"></a><code><span><span class="keyword">val</span> parse_header : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int * int</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-next_clause"><a href="#val-next_clause" class="anchor"></a><code><span><span class="keyword">val</span> next_clause : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>int list</span> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter"><a href="#val-iter" class="anchor"></a><code><span><span class="keyword">val</span> iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>int list</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Drup_lexer (sidekick-bin.Sidekick_bin_lib.Drup_lexer)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Drup_lexer</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Drup_lexer</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-token"><a href="#type-token" class="anchor"></a><code><span><span class="keyword">type</span> token</span><span> = </span></code><ol><li id="type-token.EOF" class="def variant constructor anchored"><a href="#type-token.EOF" class="anchor"></a><code><span>| </span><span><span class="constructor">EOF</span></span></code></li><li id="type-token.ZERO" class="def variant constructor anchored"><a href="#type-token.ZERO" class="anchor"></a><code><span>| </span><span><span class="constructor">ZERO</span></span></code></li><li id="type-token.LIT" class="def variant constructor anchored"><a href="#type-token.LIT" class="anchor"></a><code><span>| </span><span><span class="constructor">LIT</span> <span class="keyword">of</span> int</span></code></li><li id="type-token.D" class="def variant constructor anchored"><a href="#type-token.D" class="anchor"></a><code><span>| </span><span><span class="constructor">D</span></span></code></li><li id="type-token.R" class="def variant constructor anchored"><a href="#type-token.R" class="anchor"></a><code><span>| </span><span><span class="constructor">R</span></span></code></li><li id="type-token.I" class="def variant constructor anchored"><a href="#type-token.I" class="anchor"></a><code><span>| </span><span><span class="constructor">I</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_tables"><a href="#val-__ocaml_lex_tables" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_tables : <span class="xref-unresolved">Stdlib</span>.Lexing.lex_tables</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-token"><a href="#val-token" class="anchor"></a><code><span><span class="keyword">val</span> token : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_token_rec"><a href="#val-__ocaml_lex_token_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_token_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-comment"><a href="#val-comment" class="anchor"></a><code><span><span class="keyword">val</span> comment : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_comment_rec"><a href="#val-__ocaml_lex_comment_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_comment_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Drup_lexer (sidekick-bin.Sidekick_bin_lib.Drup_lexer)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Drup_lexer</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Drup_lexer</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-token"><a href="#type-token" class="anchor"></a><code><span><span class="keyword">type</span> token</span><span> = </span></code><ol><li id="type-token.EOF" class="def variant constructor anchored"><a href="#type-token.EOF" class="anchor"></a><code><span>| </span><span><span class="constructor">EOF</span></span></code></li><li id="type-token.ZERO" class="def variant constructor anchored"><a href="#type-token.ZERO" class="anchor"></a><code><span>| </span><span><span class="constructor">ZERO</span></span></code></li><li id="type-token.LIT" class="def variant constructor anchored"><a href="#type-token.LIT" class="anchor"></a><code><span>| </span><span><span class="constructor">LIT</span> <span class="keyword">of</span> int</span></code></li><li id="type-token.D" class="def variant constructor anchored"><a href="#type-token.D" class="anchor"></a><code><span>| </span><span><span class="constructor">D</span></span></code></li><li id="type-token.R" class="def variant constructor anchored"><a href="#type-token.R" class="anchor"></a><code><span>| </span><span><span class="constructor">R</span></span></code></li><li id="type-token.I" class="def variant constructor anchored"><a href="#type-token.I" class="anchor"></a><code><span>| </span><span><span class="constructor">I</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_tables"><a href="#val-__ocaml_lex_tables" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_tables : <span class="xref-unresolved">Stdlib</span>.Lexing.lex_tables</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-token"><a href="#val-token" class="anchor"></a><code><span><span class="keyword">val</span> token : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_token_rec"><a href="#val-__ocaml_lex_token_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_token_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-comment"><a href="#val-comment" class="anchor"></a><code><span><span class="keyword">val</span> comment : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-__ocaml_lex_comment_rec"><a href="#val-__ocaml_lex_comment_rec" class="anchor"></a><code><span><span class="keyword">val</span> __ocaml_lex_comment_rec : <span><span class="xref-unresolved">Stdlib</span>.Lexing.lexbuf <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-token">token</a></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Drup_parser (sidekick-bin.Sidekick_bin_lib.Drup_parser)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Drup_parser</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Drup_parser</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#drup-parser">DRUP parser</a></li></ul></nav><div class="odoc-content"><h2 id="drup-parser"><a href="#drup-parser" class="anchor"></a>DRUP parser</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-event"><a href="#type-event" class="anchor"></a><code><span><span class="keyword">type</span> event</span><span> = </span></code><ol><li id="type-event.Input" class="def variant constructor anchored"><a href="#type-event.Input" class="anchor"></a><code><span>| </span><span><span class="constructor">Input</span> <span class="keyword">of</span> <span>int list</span></span></code></li><li id="type-event.Add" class="def variant constructor anchored"><a href="#type-event.Add" class="anchor"></a><code><span>| </span><span><span class="constructor">Add</span> <span class="keyword">of</span> <span>int list</span></span></code></li><li id="type-event.Delete" class="def variant constructor anchored"><a href="#type-event.Delete" class="anchor"></a><code><span>| </span><span><span class="constructor">Delete</span> <span class="keyword">of</span> <span>int list</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_chan"><a href="#val-create_chan" class="anchor"></a><code><span><span class="keyword">val</span> create_chan : <span><span class="xref-unresolved">Stdlib</span>.in_channel <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_string"><a href="#val-create_string" class="anchor"></a><code><span><span class="keyword">val</span> create_string : <span>string <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-next"><a href="#val-next" class="anchor"></a><code><span><span class="keyword">val</span> next : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-event">event</a> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter"><a href="#val-iter" class="anchor"></a><code><span><span class="keyword">val</span> iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-event">event</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Drup_parser (sidekick-bin.Sidekick_bin_lib.Drup_parser)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-bin</a> » <a href="../index.html">Sidekick_bin_lib</a> » Drup_parser</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib.Drup_parser</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#drup-parser">DRUP parser</a></li></ul></nav><div class="odoc-content"><h2 id="drup-parser"><a href="#drup-parser" class="anchor"></a>DRUP parser</h2><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-event"><a href="#type-event" class="anchor"></a><code><span><span class="keyword">type</span> event</span><span> = </span></code><ol><li id="type-event.Input" class="def variant constructor anchored"><a href="#type-event.Input" class="anchor"></a><code><span>| </span><span><span class="constructor">Input</span> <span class="keyword">of</span> <span>int list</span></span></code></li><li id="type-event.Add" class="def variant constructor anchored"><a href="#type-event.Add" class="anchor"></a><code><span>| </span><span><span class="constructor">Add</span> <span class="keyword">of</span> <span>int list</span></span></code></li><li id="type-event.Delete" class="def variant constructor anchored"><a href="#type-event.Delete" class="anchor"></a><code><span>| </span><span><span class="constructor">Delete</span> <span class="keyword">of</span> <span>int list</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_chan"><a href="#val-create_chan" class="anchor"></a><code><span><span class="keyword">val</span> create_chan : <span><span class="xref-unresolved">Stdlib</span>.in_channel <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_string"><a href="#val-create_string" class="anchor"></a><code><span><span class="keyword">val</span> create_string : <span>string <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-next"><a href="#val-next" class="anchor"></a><code><span><span class="keyword">val</span> next : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-event">event</a> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter"><a href="#val-iter" class="anchor"></a><code><span><span class="keyword">val</span> iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-event">event</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_bin_lib (sidekick-bin.Sidekick_bin_lib)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick-bin</a> » Sidekick_bin_lib</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib</span></code></h1><p>Library for the Sidekick executables</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Dimacs_lexer"><a href="#module-Dimacs_lexer" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Dimacs_lexer/index.html">Dimacs_lexer</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Dimacs_parser"><a href="#module-Dimacs_parser" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Dimacs_parser/index.html">Dimacs_parser</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Drup_lexer"><a href="#module-Drup_lexer" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Drup_lexer/index.html">Drup_lexer</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Drup_parser"><a href="#module-Drup_parser" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Drup_parser/index.html">Drup_parser</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_bin_lib (sidekick-bin.Sidekick_bin_lib)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick-bin</a> » Sidekick_bin_lib</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bin_lib</span></code></h1><p>Library for the Sidekick executables</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Dimacs_lexer"><a href="#module-Dimacs_lexer" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Dimacs_lexer/index.html">Dimacs_lexer</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Dimacs_parser"><a href="#module-Dimacs_parser" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Dimacs_parser/index.html">Dimacs_parser</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Drup_lexer"><a href="#module-Drup_lexer" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Drup_lexer/index.html">Drup_lexer</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Drup_parser"><a href="#module-Drup_parser" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Drup_parser/index.html">Drup_parser</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>index (sidekick-bin.index)</title><link rel="stylesheet" href="../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – sidekick-bin</nav><header class="odoc-preamble"><h1 id="sidekick-bin-index"><a href="#sidekick-bin-index" class="anchor"></a>sidekick-bin index</h1></header><nav class="odoc-toc"><ul><li><a href="#library-sidekick-bin.lib">Library sidekick-bin.lib</a></li></ul></nav><div class="odoc-content"><h2 id="library-sidekick-bin.lib"><a href="#library-sidekick-bin.lib" class="anchor"></a>Library sidekick-bin.lib</h2><p>The entry point of this library is the module: <a href="Sidekick_bin_lib/index.html"><code>Sidekick_bin_lib</code></a>.</p></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>index (sidekick-bin.index)</title><link rel="stylesheet" href="../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – sidekick-bin</nav><header class="odoc-preamble"><h1 id="sidekick-bin-index"><a href="#sidekick-bin-index" class="anchor"></a>sidekick-bin index</h1></header><nav class="odoc-toc"><ul><li><a href="#library-sidekick-bin.lib">Library sidekick-bin.lib</a></li></ul></nav><div class="odoc-content"><h2 id="library-sidekick-bin.lib"><a href="#library-sidekick-bin.lib" class="anchor"></a>Library sidekick-bin.lib</h2><p>The entry point of this library is the module: <a href="Sidekick_bin_lib/index.html"><code>Sidekick_bin_lib</code></a>.</p></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>t (sidekick.Sidekick_abstract_solver.Asolver.t)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_abstract_solver</a> » <a href="../index.html">Asolver</a> » t</nav><header class="odoc-preamble"><h1>Class type <code><span>Asolver.t</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec method anchored" id="method-assert_term"><a href="#method-assert_term" class="anchor"></a><code><span><span class="keyword">method</span> assert_term : <span><a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.</p><p>This uses <code>Proof_sat</code>.sat_input_clause to justify the assertion.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause"><a href="#method-assert_clause" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause : <span><span><a href="../../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> array</span> <span class="arrow">-></span></span> <span><a href="../../../Sidekick_proof__/Pterm/index.html#type-delayed">Proof.Pterm.delayed</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>add_clause solver cs</code> adds a boolean clause to the solver. Subsequent calls to <code>solve</code> will need to satisfy this clause.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause_l"><a href="#method-assert_clause_l" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause_l : <span><span><a href="../../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> <span class="arrow">-></span></span>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>t (sidekick.Sidekick_abstract_solver.Asolver.t)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_abstract_solver</a> » <a href="../index.html">Asolver</a> » t</nav><header class="odoc-preamble"><h1>Class type <code><span>Asolver.t</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec method anchored" id="method-assert_term"><a href="#method-assert_term" class="anchor"></a><code><span><span class="keyword">method</span> assert_term : <span><a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.</p><p>This uses <code>Proof_sat</code>.sat_input_clause to justify the assertion.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause"><a href="#method-assert_clause" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause : <span><span><a href="../../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> array</span> <span class="arrow">-></span></span> <span><a href="../../../Sidekick_proof__/Pterm/index.html#type-delayed">Proof.Pterm.delayed</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>add_clause solver cs</code> adds a boolean clause to the solver. Subsequent calls to <code>solve</code> will need to satisfy this clause.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause_l"><a href="#method-assert_clause_l" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause_l : <span><span><a href="../../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../../Sidekick_proof__/Pterm/index.html#type-delayed">Proof.Pterm.delayed</a> <span class="arrow">-></span></span>
|
||||
unit</span></code></div><div class="spec-doc"><p>Add a clause to the solver, given as a list.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-add_ty"><a href="#method-add_ty" class="anchor"></a><code><span><span class="keyword">method</span> add_ty : <span>ty:<a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Add a new sort/atomic type.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-lit_of_term"><a href="#method-lit_of_term" class="anchor"></a><code><span><span class="keyword">method</span> lit_of_term : <span>?sign:bool <span class="arrow">-></span></span> <span><a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="../../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a></span></code></div><div class="spec-doc"><p>Convert a term into a simplified literal.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-tst"><a href="#method-tst" class="anchor"></a><code><span><span class="keyword">method</span> tst : <a href="../../../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a></span></code></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-solve"><a href="#method-solve" class="anchor"></a><code><span><span class="keyword">method</span> solve : <span>?on_exit:<span><span>(<span>unit <span class="arrow">-></span></span> unit)</span> list</span> <span class="arrow">-></span></span>
|
||||
<span>?on_progress:<span>(<span>unit <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Asolver (sidekick.Sidekick_abstract_solver.Asolver)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » Asolver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver.Asolver</span></code></h1><p>Abstract interface for a solver</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> Unknown</span><span> = <a href="../Unknown/index.html">Unknown</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> Check_res</span><span> = <a href="../Check_res/index.html">Check_res</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Proof"><a href="#module-Proof" class="anchor"></a><code><span><span class="keyword">module</span> Proof</span><span> = <a href="../../Sidekick_proof/index.html">Sidekick_proof</a></span></code></div></div><div class="odoc-spec"><div class="spec class-type anchored" id="class-type-t"><a href="#class-type-t" class="anchor"></a><code><span><span class="keyword">class</span> <span class="keyword">type</span> </span><span><a href="class-type-t/index.html">t</a></span><span> = <span class="keyword">object</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span><span class="keyword">val</span> tst : <span><a href="class-type-t/index.html">t</a> <span class="arrow">-></span></span> <a href="../../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assert_term"><a href="#val-assert_term" class="anchor"></a><code><span><span class="keyword">val</span> assert_term : <span><a href="class-type-t/index.html">t</a> <span class="arrow">-></span></span> <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assert_clause"><a href="#val-assert_clause" class="anchor"></a><code><span><span class="keyword">val</span> assert_clause :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Asolver (sidekick.Sidekick_abstract_solver.Asolver)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » Asolver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver.Asolver</span></code></h1><p>Abstract interface for a solver</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> Unknown</span><span> = <a href="../Unknown/index.html">Unknown</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> Check_res</span><span> = <a href="../Check_res/index.html">Check_res</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Proof"><a href="#module-Proof" class="anchor"></a><code><span><span class="keyword">module</span> Proof</span><span> = <a href="../../Sidekick_proof/index.html">Sidekick_proof</a></span></code></div></div><div class="odoc-spec"><div class="spec class-type anchored" id="class-type-t"><a href="#class-type-t" class="anchor"></a><code><span><span class="keyword">class</span> <span class="keyword">type</span> </span><span><a href="class-type-t/index.html">t</a></span><span> = <span class="keyword">object</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span><span class="keyword">val</span> tst : <span><a href="class-type-t/index.html">t</a> <span class="arrow">-></span></span> <a href="../../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assert_term"><a href="#val-assert_term" class="anchor"></a><code><span><span class="keyword">val</span> assert_term : <span><a href="class-type-t/index.html">t</a> <span class="arrow">-></span></span> <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-assert_clause"><a href="#val-assert_clause" class="anchor"></a><code><span><span class="keyword">val</span> assert_clause :
|
||||
<span><a href="class-type-t/index.html">t</a> <span class="arrow">-></span></span>
|
||||
<span><span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> array</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../Sidekick_proof/Pterm/index.html#type-delayed">Proof.Pterm.delayed</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Unknown (sidekick.Sidekick_abstract_solver.Unknown)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » Unknown</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver.Unknown</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.U_timeout" class="def variant constructor anchored"><a href="#type-t.U_timeout" class="anchor"></a><code><span>| </span><span><span class="constructor">U_timeout</span></span></code></li><li id="type-t.U_max_depth" class="def variant constructor anchored"><a href="#type-t.U_max_depth" class="anchor"></a><code><span>| </span><span><span class="constructor">U_max_depth</span></span></code></li><li id="type-t.U_incomplete" class="def variant constructor anchored"><a href="#type-t.U_incomplete" class="anchor"></a><code><span>| </span><span><span class="constructor">U_incomplete</span></span></code></li><li id="type-t.U_asked_to_stop" class="def variant constructor anchored"><a href="#type-t.U_asked_to_stop" class="anchor"></a><code><span>| </span><span><span class="constructor">U_asked_to_stop</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <span class="xref-unresolved">Sidekick_core</span>.Fmt.printer</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Unknown (sidekick.Sidekick_abstract_solver.Unknown)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » Unknown</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver.Unknown</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.U_timeout" class="def variant constructor anchored"><a href="#type-t.U_timeout" class="anchor"></a><code><span>| </span><span><span class="constructor">U_timeout</span></span></code></li><li id="type-t.U_max_depth" class="def variant constructor anchored"><a href="#type-t.U_max_depth" class="anchor"></a><code><span>| </span><span><span class="constructor">U_max_depth</span></span></code></li><li id="type-t.U_incomplete" class="def variant constructor anchored"><a href="#type-t.U_incomplete" class="anchor"></a><code><span>| </span><span><span class="constructor">U_incomplete</span></span></code></li><li id="type-t.U_asked_to_stop" class="def variant constructor anchored"><a href="#type-t.U_asked_to_stop" class="anchor"></a><code><span>| </span><span><span class="constructor">U_asked_to_stop</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <span class="xref-unresolved">Sidekick_core</span>.Fmt.printer</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>t (sidekick.Sidekick_abstract_solver.t)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » t</nav><header class="odoc-preamble"><h1>Class type <code><span>Sidekick_abstract_solver.t</span></code></h1><p>Main abstract solver type</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec method anchored" id="method-assert_term"><a href="#method-assert_term" class="anchor"></a><code><span><span class="keyword">method</span> assert_term : <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.</p><p>This uses <code>Proof_sat</code>.sat_input_clause to justify the assertion.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause"><a href="#method-assert_clause" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause : <span><span><a href="../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> array</span> <span class="arrow">-></span></span>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>t (sidekick.Sidekick_abstract_solver.t)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_abstract_solver</a> » t</nav><header class="odoc-preamble"><h1>Class type <code><span>Sidekick_abstract_solver.t</span></code></h1><p>Main abstract solver type</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec method anchored" id="method-assert_term"><a href="#method-assert_term" class="anchor"></a><code><span><span class="keyword">method</span> assert_term : <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.</p><p>This uses <code>Proof_sat</code>.sat_input_clause to justify the assertion.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause"><a href="#method-assert_clause" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause : <span><span><a href="../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> array</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../Sidekick_proof__/Pterm/index.html#type-delayed">Asolver.Proof.Pterm.delayed</a> <span class="arrow">-></span></span>
|
||||
unit</span></code></div><div class="spec-doc"><p><code>add_clause solver cs</code> adds a boolean clause to the solver. Subsequent calls to <code>solve</code> will need to satisfy this clause.</p></div></div><div class="odoc-spec"><div class="spec method anchored" id="method-assert_clause_l"><a href="#method-assert_clause_l" class="anchor"></a><code><span><span class="keyword">method</span> assert_clause_l : <span><span><a href="../../Sidekick_core__/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../Sidekick_proof__/Pterm/index.html#type-delayed">Asolver.Proof.Pterm.delayed</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_abstract_solver (sidekick.Sidekick_abstract_solver)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_abstract_solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver</span></code></h1><p>Abstract interface for a solver</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Unknown/index.html">Unknown</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Check_res/index.html">Check_res</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Result of solving for the current set of clauses</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Asolver/index.html">Asolver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Abstract interface for a solver</p></div></div><div class="odoc-spec"><div class="spec class-type anchored" id="class-type-t"><a href="#class-type-t" class="anchor"></a><code><span><span class="keyword">class</span> <span class="keyword">type</span> </span><span><a href="class-type-t/index.html">t</a></span><span> = <a href="../Sidekick_abstract_solver__/Asolver/class-type-t/index.html">Asolver.t</a></span></code></div><div class="spec-doc"><p>Main abstract solver type</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_abstract_solver (sidekick.Sidekick_abstract_solver)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_abstract_solver</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_abstract_solver</span></code></h1><p>Abstract interface for a solver</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Unknown"><a href="#module-Unknown" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Unknown/index.html">Unknown</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Check_res"><a href="#module-Check_res" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Check_res/index.html">Check_res</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Result of solving for the current set of clauses</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Asolver"><a href="#module-Asolver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Asolver/index.html">Asolver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Abstract interface for a solver</p></div></div><div class="odoc-spec"><div class="spec class-type anchored" id="class-type-t"><a href="#class-type-t" class="anchor"></a><code><span><span class="keyword">class</span> <span class="keyword">type</span> </span><span><a href="class-type-t/index.html">t</a></span><span> = <a href="../Sidekick_abstract_solver__/Asolver/class-type-t/index.html">Asolver.t</a></span></code></div><div class="spec-doc"><p>Main abstract solver type</p></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_arith (sidekick.Sidekick_arith)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_arith</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_arith</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-NUM"><a href="#module-type-NUM" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-NUM/index.html">NUM</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-INT"><a href="#module-type-INT" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-INT/index.html">INT</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-RATIONAL"><a href="#module-type-RATIONAL" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-RATIONAL/index.html">RATIONAL</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-INT_FULL"><a href="#module-type-INT_FULL" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-INT_FULL/index.html">INT_FULL</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_arith (sidekick.Sidekick_arith)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_arith</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_arith</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-NUM"><a href="#module-type-NUM" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-NUM/index.html">NUM</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-INT"><a href="#module-type-INT" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-INT/index.html">INT</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-RATIONAL"><a href="#module-type-RATIONAL" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-RATIONAL/index.html">RATIONAL</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-INT_FULL"><a href="#module-type-INT_FULL" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-INT_FULL/index.html">INT_FULL</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Decode (sidekick.Sidekick_bencode.Decode)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_bencode</a> » Decode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode.Decode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-of_string"><a href="#val-of_string" class="anchor"></a><code><span><span class="keyword">val</span> of_string : <span>?idx:int <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <span><span>(int * <a href="../index.html#type-t">t</a>)</span> option</span></span></code></div><div class="spec-doc"><p>Decode string, and also return how many bytes were consumed.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">idx</span> <p>initial index (default 0)</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_string_exn"><a href="#val-of_string_exn" class="anchor"></a><code><span><span class="keyword">val</span> of_string_exn : <span>?idx:int <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> int * <a href="../index.html#type-t">t</a></span></code></div><div class="spec-doc"><p>Parse string.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <span class="value">Error.Error</span> <p>if the string is not valid bencode.</p></li></ul></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Decode (sidekick.Sidekick_bencode.Decode)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_bencode</a> » Decode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode.Decode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-of_string"><a href="#val-of_string" class="anchor"></a><code><span><span class="keyword">val</span> of_string : <span>?idx:int <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <span><span>(int * <a href="../index.html#type-t">t</a>)</span> option</span></span></code></div><div class="spec-doc"><p>Decode string, and also return how many bytes were consumed.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">idx</span> <p>initial index (default 0)</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_string_exn"><a href="#val-of_string_exn" class="anchor"></a><code><span><span class="keyword">val</span> of_string_exn : <span>?idx:int <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> int * <a href="../index.html#type-t">t</a></span></code></div><div class="spec-doc"><p>Parse string.</p><ul class="at-tags"><li class="raises"><span class="at-tag">raises</span> <span class="value">Error.Error</span> <p>if the string is not valid bencode.</p></li></ul></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Encode (sidekick.Sidekick_bencode.Encode)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_bencode</a> » Encode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode.Encode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-to_buffer"><a href="#val-to_buffer" class="anchor"></a><code><span><span class="keyword">val</span> to_buffer : <span><span class="xref-unresolved">Stdlib</span>.Buffer.t <span class="arrow">-></span></span> <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span><span class="keyword">val</span> to_string : <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> string</span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Encode (sidekick.Sidekick_bencode.Encode)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_bencode</a> » Encode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode.Encode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-to_buffer"><a href="#val-to_buffer" class="anchor"></a><code><span><span class="keyword">val</span> to_buffer : <span><span class="xref-unresolved">Stdlib</span>.Buffer.t <span class="arrow">-></span></span> <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span><span class="keyword">val</span> to_string : <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> string</span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_bencode (sidekick.Sidekick_bencode)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_bencode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../Sidekick_util/Ser_value/index.html#type-t">Sidekick_util.Ser_value.t</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Encode"><a href="#module-Encode" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Encode/index.html">Encode</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Decode"><a href="#module-Decode" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Decode/index.html">Decode</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_bencode (sidekick.Sidekick_bencode)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_bencode</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_bencode</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <a href="../Sidekick_util/Ser_value/index.html#type-t">Sidekick_util.Ser_value.t</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Encode"><a href="#module-Encode" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Encode/index.html">Encode</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Decode"><a href="#module-Decode" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Decode/index.html">Decode</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Handler_action (sidekick.Sidekick_cc.CC.Handler_action)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Handler_action</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Handler_action</span></code></h1><p>Handler Actions</p><p>Actions that can be scheduled by event handlers.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.Act_merge" class="def variant constructor anchored"><a href="#type-t.Act_merge" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_merge</span> <span class="keyword">of</span> <a href="../../E_node/index.html#type-t">E_node.t</a> * <a href="../../E_node/index.html#type-t">E_node.t</a> * <a href="../../Expl/index.html#type-t">Expl.t</a></span></code></li><li id="type-t.Act_propagate" class="def variant constructor anchored"><a href="#type-t.Act_propagate" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_propagate</span> <span class="keyword">of</span> <a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> * <a href="../index.html#type-propagation_reason">propagation_reason</a></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-conflict"><a href="#type-conflict" class="anchor"></a><code><span><span class="keyword">type</span> conflict</span><span> = </span></code><ol><li id="type-conflict.Conflict" class="def variant constructor anchored"><a href="#type-conflict.Conflict" class="anchor"></a><code><span>| </span><span><span class="constructor">Conflict</span> <span class="keyword">of</span> <a href="../../Expl/index.html#type-t">Expl.t</a></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_conflict"><a href="#type-or_conflict" class="anchor"></a><code><span><span class="keyword">type</span> or_conflict</span><span> = <span><span>(<span><a href="#type-t">t</a> list</span>, <a href="#type-conflict">conflict</a>)</span> <span class="xref-unresolved">Stdlib</span>.result</span></span></code></div><div class="spec-doc"><p>Actions or conflict scheduled by an event handler.</p><ul><li><code>Ok acts</code> is a list of merges and propagations</li><li><code>Error confl</code> is a conflict to resolve.</li></ul></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Handler_action (sidekick.Sidekick_cc.CC.Handler_action)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Handler_action</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Handler_action</span></code></h1><p>Handler Actions</p><p>Actions that can be scheduled by event handlers.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.Act_merge" class="def variant constructor anchored"><a href="#type-t.Act_merge" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_merge</span> <span class="keyword">of</span> <a href="../../E_node/index.html#type-t">E_node.t</a> * <a href="../../E_node/index.html#type-t">E_node.t</a> * <a href="../../Expl/index.html#type-t">Expl.t</a></span></code></li><li id="type-t.Act_propagate" class="def variant constructor anchored"><a href="#type-t.Act_propagate" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_propagate</span> <span class="keyword">of</span> <a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> * <a href="../index.html#type-propagation_reason">propagation_reason</a></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-conflict"><a href="#type-conflict" class="anchor"></a><code><span><span class="keyword">type</span> conflict</span><span> = </span></code><ol><li id="type-conflict.Conflict" class="def variant constructor anchored"><a href="#type-conflict.Conflict" class="anchor"></a><code><span>| </span><span><span class="constructor">Conflict</span> <span class="keyword">of</span> <a href="../../Expl/index.html#type-t">Expl.t</a></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_conflict"><a href="#type-or_conflict" class="anchor"></a><code><span><span class="keyword">type</span> or_conflict</span><span> = <span><span>(<span><a href="#type-t">t</a> list</span>, <a href="#type-conflict">conflict</a>)</span> <span class="xref-unresolved">Stdlib</span>.result</span></span></code></div><div class="spec-doc"><p>Actions or conflict scheduled by an event handler.</p><ul><li><code>Ok acts</code> is a list of merges and propagations</li><li><code>Error confl</code> is a conflict to resolve.</li></ul></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>_ (sidekick.Sidekick_cc.CC.Make._)</title><link rel="stylesheet" href="../../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">CC</a> » <a href="../index.html">Make</a> » _</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make._</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-view_as_cc"><a href="#val-view_as_cc" class="anchor"></a><code><span><span class="keyword">val</span> view_as_cc : <a href="../../index.html#type-view_as_cc">view_as_cc</a></span></code></div><div class="spec-doc"><p>View the Term.t through the lens of the congruence closure</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>_ (sidekick.Sidekick_cc.CC.Make._)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">CC</a> » <a href="../index.html">Make</a> » _</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make._</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-view_as_cc"><a href="#val-view_as_cc" class="anchor"></a><code><span><span class="keyword">val</span> view_as_cc : <a href="../../index.html#type-view_as_cc">view_as_cc</a></span></code></div><div class="spec-doc"><p>View the Term.t through the lens of the congruence closure</p></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_cc.CC.Make)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Make</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Make</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#parameters">Parameters</a></li><li><a href="#signature">Signature</a></li></ul></nav><div class="odoc-content"><h2 id="parameters"><a href="#parameters" class="anchor"></a>Parameters</h2><div class="odoc-spec"><div class="spec parameter anchored" id="argument-1-_"><a href="#argument-1-_" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="argument-1-_/index.html">_</a></span><span> : <a href="../module-type-ARG/index.html">ARG</a></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick.Sidekick_cc.CC.Make)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Make</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Make</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#parameters">Parameters</a></li><li><a href="#signature">Signature</a></li></ul></nav><div class="odoc-content"><h2 id="parameters"><a href="#parameters" class="anchor"></a>Parameters</h2><div class="odoc-spec"><div class="spec parameter anchored" id="argument-1-_"><a href="#argument-1-_" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="argument-1-_/index.html">_</a></span><span> : <a href="../module-type-ARG/index.html">ARG</a></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<span>?stat:<a href="../../../Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a> <span class="arrow">-></span></span>
|
||||
<span>?size:<span>[ `Small <span>| `Big</span> ]</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Result_action (sidekick.Sidekick_cc.CC.Result_action)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Result_action</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Result_action</span></code></h1><p>Result Actions.</p><p>Actions returned by the congruence closure after calling <a href="../index.html#val-check"><code>check</code></a>.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.Act_propagate" class="def variant constructor anchored"><a href="#type-t.Act_propagate" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_propagate</span> <span class="keyword">of</span> </span><span>{</span></code><ol><li id="type-t.lit" class="def record field anchored"><a href="#type-t.lit" class="anchor"></a><code><span>lit : <a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a>;</span></code></li><li id="type-t.reason" class="def record field anchored"><a href="#type-t.reason" class="anchor"></a><code><span>reason : <a href="../index.html#type-propagation_reason">propagation_reason</a>;</span></code></li></ol><code><span>}</span></code><div class="def-doc"><span class="comment-delim">(*</span><p><code>propagate (Lit.t, reason)</code> declares that <code>reason() => Lit.t</code> is a tautology.</p><ul><li><code>reason()</code> should return a list of literals that are currently true, as well as a proof.</li><li><code>Lit.t</code> should be a literal of interest (see <code>S</code>.set_as_lit).</li></ul><p>This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.</p><span class="comment-delim">*)</span></div></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-conflict"><a href="#type-conflict" class="anchor"></a><code><span><span class="keyword">type</span> conflict</span><span> = </span></code><ol><li id="type-conflict.Conflict" class="def variant constructor anchored"><a href="#type-conflict.Conflict" class="anchor"></a><code><span>| </span><span><span class="constructor">Conflict</span> <span class="keyword">of</span> <span><a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> * <a href="../../../Sidekick_proof/Step/index.html#type-id">Sidekick_proof.Step.id</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p><code>raise_conflict (c,pr)</code> declares that <code>c</code> is a tautology of the theory of congruence.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">pr</span> <p>the proof of <code>c</code> being a tautology</p></li></ul><span class="comment-delim">*)</span></div></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_conflict"><a href="#type-or_conflict" class="anchor"></a><code><span><span class="keyword">type</span> or_conflict</span><span> = <span><span>(<span><a href="#type-t">t</a> list</span>, <a href="#type-conflict">conflict</a>)</span> <span class="xref-unresolved">Stdlib</span>.result</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Result_action (sidekick.Sidekick_cc.CC.Result_action)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » Result_action</nav><header class="odoc-preamble"><h1>Module <code><span>CC.Result_action</span></code></h1><p>Result Actions.</p><p>Actions returned by the congruence closure after calling <a href="../index.html#val-check"><code>check</code></a>.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span></code><ol><li id="type-t.Act_propagate" class="def variant constructor anchored"><a href="#type-t.Act_propagate" class="anchor"></a><code><span>| </span><span><span class="constructor">Act_propagate</span> <span class="keyword">of</span> </span><span>{</span></code><ol><li id="type-t.lit" class="def record field anchored"><a href="#type-t.lit" class="anchor"></a><code><span>lit : <a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a>;</span></code></li><li id="type-t.reason" class="def record field anchored"><a href="#type-t.reason" class="anchor"></a><code><span>reason : <a href="../index.html#type-propagation_reason">propagation_reason</a>;</span></code></li></ol><code><span>}</span></code><div class="def-doc"><span class="comment-delim">(*</span><p><code>propagate (Lit.t, reason)</code> declares that <code>reason() => Lit.t</code> is a tautology.</p><ul><li><code>reason()</code> should return a list of literals that are currently true, as well as a proof.</li><li><code>Lit.t</code> should be a literal of interest (see <code>S</code>.set_as_lit).</li></ul><p>This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.</p><span class="comment-delim">*)</span></div></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-conflict"><a href="#type-conflict" class="anchor"></a><code><span><span class="keyword">type</span> conflict</span><span> = </span></code><ol><li id="type-conflict.Conflict" class="def variant constructor anchored"><a href="#type-conflict.Conflict" class="anchor"></a><code><span>| </span><span><span class="constructor">Conflict</span> <span class="keyword">of</span> <span><a href="../../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span> * <a href="../../../Sidekick_proof/Step/index.html#type-id">Sidekick_proof.Step.id</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p><code>raise_conflict (c,pr)</code> declares that <code>c</code> is a tautology of the theory of congruence.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">pr</span> <p>the proof of <code>c</code> being a tautology</p></li></ul><span class="comment-delim">*)</span></div></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-or_conflict"><a href="#type-or_conflict" class="anchor"></a><code><span><span class="keyword">type</span> or_conflict</span><span> = <span><span>(<span><a href="#type-t">t</a> list</span>, <a href="#type-conflict">conflict</a>)</span> <span class="xref-unresolved">Stdlib</span>.result</span></span></code></div></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ARG (sidekick.Sidekick_cc.CC.ARG)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » ARG</nav><header class="odoc-preamble"><h1>Module type <code><span>CC.ARG</span></code></h1><p>Arguments to a congruence closure's implementation</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-view_as_cc"><a href="#val-view_as_cc" class="anchor"></a><code><span><span class="keyword">val</span> view_as_cc : <a href="../index.html#type-view_as_cc">view_as_cc</a></span></code></div><div class="spec-doc"><p>View the Term.t through the lens of the congruence closure</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ARG (sidekick.Sidekick_cc.CC.ARG)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » ARG</nav><header class="odoc-preamble"><h1>Module type <code><span>CC.ARG</span></code></h1><p>Arguments to a congruence closure's implementation</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-view_as_cc"><a href="#val-view_as_cc" class="anchor"></a><code><span><span class="keyword">val</span> view_as_cc : <a href="../index.html#type-view_as_cc">view_as_cc</a></span></code></div><div class="spec-doc"><p>View the Term.t through the lens of the congruence closure</p></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>BUILD (sidekick.Sidekick_cc.CC.BUILD)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » BUILD</nav><header class="odoc-preamble"><h1>Module type <code><span>CC.BUILD</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>BUILD (sidekick.Sidekick_cc.CC.BUILD)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">CC</a> » BUILD</nav><header class="odoc-preamble"><h1>Module type <code><span>CC.BUILD</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create :
|
||||
<span>?stat:<a href="../../../Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a> <span class="arrow">-></span></span>
|
||||
<span>?size:<span>[ `Small <span>| `Big</span> ]</span> <span class="arrow">-></span></span>
|
||||
<span><a href="../../../Sidekick_core/Term/index.html#type-store">Sidekick_core.Term.store</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Internal_ (sidekick.Sidekick_cc.E_node.Internal_)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">E_node</a> » Internal_</nav><header class="odoc-preamble"><h1>Module <code><span>E_node.Internal_</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-iter_class_"><a href="#val-iter_class_" class="anchor"></a><code><span><span class="keyword">val</span> iter_class_ : <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../index.html#type-t">t</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-make"><a href="#val-make" class="anchor"></a><code><span><span class="keyword">val</span> make : <span><a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="../index.html#type-t">t</a></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Internal_ (sidekick.Sidekick_cc.E_node.Internal_)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">E_node</a> » Internal_</nav><header class="odoc-preamble"><h1>Module <code><span>E_node.Internal_</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-iter_class_"><a href="#val-iter_class_" class="anchor"></a><code><span><span class="keyword">val</span> iter_class_ : <span><a href="../index.html#type-t">t</a> <span class="arrow">-></span></span> <span><a href="../index.html#type-t">t</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-make"><a href="#val-make" class="anchor"></a><code><span><span class="keyword">val</span> make : <span><a href="../../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="../index.html#type-t">t</a></span></code></div></div></div></body></html>
|
||||
File diff suppressed because one or more lines are too long
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick.Sidekick_cc.Expl)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Expl</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Expl</span></code></h1><p>Explanations</p><p>Explanations are specialized proofs, created by the congruence closure when asked to justify why two terms are equal.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the nodes were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge_t : <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the terms were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span><span class="keyword">val</span> mk_lit : <span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: we merged <code>t</code> and <code>u</code> because of literal <code>t=u</code>, or we merged <code>t</code> and <code>true</code> because of literal <code>t</code>, or <code>t</code> and <code>false</code> because of literal <code>¬t</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span><span class="keyword">val</span> mk_list : <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Conjunction of explanations</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_congruence"><a href="#val-mk_congruence" class="anchor"></a><code><span><span class="keyword">val</span> mk_congruence : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span><span class="keyword">val</span> mk_theory :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick.Sidekick_cc.Expl)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Expl</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Expl</span></code></h1><p>Explanations</p><p>Explanations are specialized proofs, created by the congruence closure when asked to justify why two terms are equal.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the nodes were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge_t : <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the terms were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span><span class="keyword">val</span> mk_lit : <span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: we merged <code>t</code> and <code>u</code> because of literal <code>t=u</code>, or we merged <code>t</code> and <code>true</code> because of literal <code>t</code>, or <code>t</code> and <code>false</code> because of literal <code>¬t</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span><span class="keyword">val</span> mk_list : <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Conjunction of explanations</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_congruence"><a href="#val-mk_congruence" class="anchor"></a><code><span><span class="keyword">val</span> mk_congruence : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span><span class="keyword">val</span> mk_theory :
|
||||
<span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||||
<span><span><span>(<a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> * <a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> * <span><a href="#type-t">t</a> list</span>)</span> list</span> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.Plugin.Make.M)</title><link rel="stylesheet" href="../../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">Make</a> » M</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.Plugin.Make.M)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">Make</a> » M</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="#type-state">state</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.Make.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">Make</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>Make.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../argument-1-M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../argument-1-M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../../CC/index.html#type-repr">CC.repr</a> * <a href="../argument-1-M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.Make.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">Make</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>Make.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../argument-1-M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../argument-1-M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../../CC/index.html#type-repr">CC.repr</a> * <a href="../argument-1-M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Plugin (sidekick.Sidekick_cc.Plugin)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Plugin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Plugin</span></code></h1><p>Congruence Closure Plugin</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-EXTENDED_PLUGIN_BUILDER"><a href="#module-type-EXTENDED_PLUGIN_BUILDER" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-EXTENDED_PLUGIN_BUILDER/index.html">EXTENDED_PLUGIN_BUILDER</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Make"><a href="#module-Make" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Make/index.html">Make</a></span><span> (<a href="Make/argument-1-M/index.html">M</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span>) : <a href="module-type-EXTENDED_PLUGIN_BUILDER/index.html">EXTENDED_PLUGIN_BUILDER</a> <span class="keyword">with</span> <span><span class="keyword">module</span> <a href="module-type-EXTENDED_PLUGIN_BUILDER/M/index.html">M</a> = <a href="Make/argument-1-M/index.html">M</a></span></span></code></div><div class="spec-doc"><p>Create a plugin builder from the given per-class monoid</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Plugin (sidekick.Sidekick_cc.Plugin)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Plugin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Plugin</span></code></h1><p>Congruence Closure Plugin</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-EXTENDED_PLUGIN_BUILDER"><a href="#module-type-EXTENDED_PLUGIN_BUILDER" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-EXTENDED_PLUGIN_BUILDER/index.html">EXTENDED_PLUGIN_BUILDER</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Make"><a href="#module-Make" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Make/index.html">Make</a></span><span> (<a href="Make/argument-1-M/index.html">M</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span>) : <a href="module-type-EXTENDED_PLUGIN_BUILDER/index.html">EXTENDED_PLUGIN_BUILDER</a> <span class="keyword">with</span> <span><span class="keyword">module</span> <a href="module-type-EXTENDED_PLUGIN_BUILDER/M/index.html">M</a> = <a href="Make/argument-1-M/index.html">M</a></span></span></code></div><div class="spec-doc"><p>Create a plugin builder from the given per-class monoid</p></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.M)</title><link rel="stylesheet" href="../../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">EXTENDED_PLUGIN_BUILDER</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>EXTENDED_PLUGIN_BUILDER.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.M)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">EXTENDED_PLUGIN_BUILDER</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>EXTENDED_PLUGIN_BUILDER.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<span><a href="../../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="#type-state">state</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">EXTENDED_PLUGIN_BUILDER</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../../CC/index.html#type-repr">CC.repr</a> * <a href="../M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick</a> » <a href="../../../index.html">Sidekick_cc</a> » <a href="../../index.html">Plugin</a> » <a href="../index.html">EXTENDED_PLUGIN_BUILDER</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../../CC/index.html#type-repr">CC.repr</a> * <a href="../M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Resolved_expl (sidekick.Sidekick_cc.Resolved_expl)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Resolved_expl</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Resolved_expl</span></code></h1><p>Resolved explanations.</p><p>The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to <b>resolve</b> them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.</p><p>However, we can also have merged classes because they have the same value in the current model.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span><span>{</span></code><ol><li id="type-t.lits" class="def record field anchored"><a href="#type-t.lits" class="anchor"></a><code><span>lits : <span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span>;</span></code></li><li id="type-t.pr" class="def record field anchored"><a href="#type-t.pr" class="anchor"></a><code><span>pr : <a href="../../Sidekick_proof/Pterm/index.html#type-delayed">Sidekick_proof.Pterm.delayed</a>;</span></code></li></ol><code><span>}</span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Resolved_expl (sidekick.Sidekick_cc.Resolved_expl)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Resolved_expl</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Resolved_expl</span></code></h1><p>Resolved explanations.</p><p>The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to <b>resolve</b> them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.</p><p>However, we can also have merged classes because they have the same value in the current model.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span><span>{</span></code><ol><li id="type-t.lits" class="def record field anchored"><a href="#type-t.lits" class="anchor"></a><code><span>lits : <span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> list</span>;</span></code></li><li id="type-t.pr" class="def record field anchored"><a href="#type-t.pr" class="anchor"></a><code><span>pr : <a href="../../Sidekick_proof/Pterm/index.html#type-delayed">Sidekick_proof.Pterm.delayed</a>;</span></code></li></ol><code><span>}</span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Signature (sidekick.Sidekick_cc.Signature)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Signature</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Signature</span></code></h1><p>A signature is a shallow term shape where immediate subterms are representative</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> =
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Signature (sidekick.Sidekick_cc.Signature)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Signature</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Signature</span></code></h1><p>A signature is a shallow term shape where immediate subterms are representative</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> =
|
||||
<span><span>(<a href="../../Sidekick_core_logic/Const/index.html#type-t">Sidekick_core.Const.t</a>,
|
||||
<span class="xref-unresolved">Sidekick_cc__.Types_.e_node</span>,
|
||||
<span><span class="xref-unresolved">Sidekick_cc__.Types_.e_node</span> list</span>)</span>
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN.M)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">DYN_MONOID_PLUGIN</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>DYN_MONOID_PLUGIN.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN.M)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">DYN_MONOID_PLUGIN</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>DYN_MONOID_PLUGIN.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="#type-state">state</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_MONOID_PLUGIN (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » DYN_MONOID_PLUGIN</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.DYN_MONOID_PLUGIN</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> <a href="M/index.html">M</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../CC/index.html#type-repr">CC.repr</a> * <a href="M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_MONOID_PLUGIN (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » DYN_MONOID_PLUGIN</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.DYN_MONOID_PLUGIN</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> <a href="M/index.html">M</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../CC/index.html#type-repr">CC.repr</a> * <a href="M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>MONOID_PLUGIN_ARG (sidekick.Sidekick_cc.MONOID_PLUGIN_ARG)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » MONOID_PLUGIN_ARG</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.MONOID_PLUGIN_ARG</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>MONOID_PLUGIN_ARG (sidekick.Sidekick_cc.MONOID_PLUGIN_ARG)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » MONOID_PLUGIN_ARG</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.MONOID_PLUGIN_ARG</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<span><a href="../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="#type-state">state</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.M)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">MONOID_PLUGIN_BUILDER</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>MONOID_PLUGIN_BUILDER.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.M)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">MONOID_PLUGIN_BUILDER</a> » M</nav><header class="odoc-preamble"><h1>Module <code><span>MONOID_PLUGIN_BUILDER.M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Some type with a monoid structure</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-state"><a href="#type-state" class="anchor"></a><code><span><span class="keyword">type</span> state</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-state">state</a></span></code></div><div class="spec-doc"><p>Initialize state from the congruence closure</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-name"><a href="#val-name" class="anchor"></a><code><span><span class="keyword">val</span> name : string</span></code></div><div class="spec-doc"><p>name of the monoid structure (short)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-of_term"><a href="#val-of_term" class="anchor"></a><code><span><span class="keyword">val</span> of_term :
|
||||
<span><a href="../../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span>
|
||||
<span><a href="#type-state">state</a> <span class="arrow">-></span></span>
|
||||
<span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span>
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>MONOID_PLUGIN_BUILDER (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER)</title><link rel="stylesheet" href="../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » MONOID_PLUGIN_BUILDER</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.MONOID_PLUGIN_BUILDER</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> <a href="M/index.html">M</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-DYN_PL_FOR_M"><a href="#module-type-DYN_PL_FOR_M" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-DYN_PL_FOR_M/index.html">DYN_PL_FOR_M</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <span>(<span class="keyword">module</span> <a href="module-type-DYN_PL_FOR_M/index.html">DYN_PL_FOR_M</a>)</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_and_setup"><a href="#val-create_and_setup" class="anchor"></a><code><span><span class="keyword">val</span> create_and_setup : <span>?size:int <span class="arrow">-></span></span> <span><a href="../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Create a new monoid state</p></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>MONOID_PLUGIN_BUILDER (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » MONOID_PLUGIN_BUILDER</nav><header class="odoc-preamble"><h1>Module type <code><span>Sidekick_cc.MONOID_PLUGIN_BUILDER</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> <a href="M/index.html">M</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module-type anchored" id="module-type-DYN_PL_FOR_M"><a href="#module-type-DYN_PL_FOR_M" class="anchor"></a><code><span><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-DYN_PL_FOR_M/index.html">DYN_PL_FOR_M</a></span><span> = <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = <span>(<span class="keyword">module</span> <a href="module-type-DYN_PL_FOR_M/index.html">DYN_PL_FOR_M</a>)</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-create_and_setup"><a href="#val-create_and_setup" class="anchor"></a><code><span><span class="keyword">val</span> create_and_setup : <span>?size:int <span class="arrow">-></span></span> <span><a href="../CC/index.html#type-t">CC.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Create a new monoid state</p></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">MONOID_PLUGIN_BUILDER</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../CC/index.html#type-repr">CC.repr</a> * <a href="../M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_PL_FOR_M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M)</title><link rel="stylesheet" href="../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> » <a href="../../index.html">Sidekick_cc</a> » <a href="../index.html">MONOID_PLUGIN_BUILDER</a> » DYN_PL_FOR_M</nav><header class="odoc-preamble"><h1>Module type <code><span>MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-M"><a href="#module-M" class="anchor"></a><code><span><span class="keyword">module</span> M</span><span> = <a href="../M/index.html">M</a></span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../Sidekick_sigs/module-type-DYN_BACKTRACKABLE/index.html">Sidekick_sigs.DYN_BACKTRACKABLE</a></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-n_levels"><a href="#val-n_levels" class="anchor"></a><code><span><span class="keyword">val</span> n_levels : <span>unit <span class="arrow">-></span></span> int</span></code></div><div class="spec-doc"><p>Number of levels</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span><span class="keyword">val</span> push_level : <span>unit <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p>Push a backtracking point</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span><span class="keyword">val</span> pop_levels : <span>int <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>pop_levels n</code> removes <code>n</code> levels</p></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span>unit <span class="xref-unresolved">Sidekick_cc__</span>.Types_.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span><span class="keyword">val</span> mem : <span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the CC E_node.t have a monoid value?</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-get"><a href="#val-get" class="anchor"></a><code><span><span class="keyword">val</span> get : <span><a href="../../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../M/index.html#type-t">M.t</a> option</span></span></code></div><div class="spec-doc"><p>Get monoid value for this CC E_node.t, if any</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_all"><a href="#val-iter_all" class="anchor"></a><code><span><span class="keyword">val</span> iter_all : <span><span>(<a href="../../CC/index.html#type-repr">CC.repr</a> * <a href="../M/index.html#type-t">M.t</a>)</span> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div></div></body></html>
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_cc_plugin (sidekick.Sidekick_cc_plugin)</title><link rel="stylesheet" href="../../_odoc_support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../_odoc_support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_cc_plugin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc_plugin</span></code></h1></header><div class="odoc-content"></div></body></html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Sidekick_cc_plugin (sidekick.Sidekick_cc_plugin)</title><link rel="stylesheet" href="../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../index.html">sidekick</a> » Sidekick_cc_plugin</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc_plugin</span></code></h1></header><div class="odoc-content"></div></body></html>
|
||||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Reference in a new issue