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

deploy: 8a4747d5d1

Browse source
This commit is contained in:
c-cube 2021-06-10 17:14:24 +00:00
parent a85730b8ee
commit 9bc52f493b
1067 changed files with 1405 additions and 682 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
dev/highlight.pack.js
View file

File diff suppressed because one or more lines are too long

1
dev/index.html
View file

@ -12,6 +12,7 @@
<h2>OCaml package documentation</h2>
<ol>
<li><a href="sidekick/index.html">sidekick</a> <span class="version">dev</span></li>
<li><a href="sidekick-arith/index.html">sidekick-arith</a> <span class="version">dev</span></li>
<li><a href="sidekick-bin/index.html">sidekick-bin</a> <span class="version">dev</span></li>
</ol>
</div>

2
dev/odoc.css
View file

@ -1,7 +1,7 @@
@charset "UTF-8";
/* Copyright (c) 2016 The odoc contributors. All rights reserved.
Distributed under the ISC license, see terms at the end of the file.
odoc 1.4.0 */
odoc 1.5.2 */
/* Fonts */
@import url('https://fonts.googleapis.com/css?family=Fira+Mono:400,500');

0
dev/sidekick-bin/Sidekick_smtlib__Ast/.dune-keep → dev/sidekick-arith/Sidekick_arith_lra/.dune-keep
View file

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/Comb/Infix/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Infix (sidekick-arith.Sidekick_arith_lra.Linear_expr.Make.Comb.Infix)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Linear_expr</a> &#x00BB; <a href="../../index.html">Make</a> &#x00BB; <a href="../index.html">Comb</a> &#x00BB; Infix</nav><h1>Module <code>Comb.Infix</code></h1><p>Infix operations on combinations</p><p>This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.</p></header><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Addition between combinations.</p></dd></dl><dl><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Substraction between combinations.</p></dd></dl><dl><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="../../C/index.html#type-t">C.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Multiplication by a constant.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/Comb/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/Constr/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/Expr/Infix/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Infix (sidekick-arith.Sidekick_arith_lra.Linear_expr.Make.Expr.Infix)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Linear_expr</a> &#x00BB; <a href="../../index.html">Make</a> &#x00BB; <a href="../index.html">Expr</a> &#x00BB; Infix</nav><h1>Module <code>Expr.Infix</code></h1><p>Infix operations on expressions</p><p>This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.</p></header><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Addition between expressions.</p></dd></dl><dl><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Substraction between expressions.</p></dd></dl><dl><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="../../C/index.html#type-t">C.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Multiplication by a constant.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/Expr/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/argument-1-C/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-C (sidekick-arith.Sidekick_arith_lra.Linear_expr.Make.1-C)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Linear_expr</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; 1-C</nav><h1>Parameter <code>Make.1-C</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Comparison on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for coefficients.</p></dd></dl><dl><dt class="spec value" id="val-zero"><a href="#val-zero" class="anchor"></a><code><span class="keyword">val</span> zero : <a href="index.html#type-t">t</a></code></dt><dd><p>The zero coefficient.</p></dd></dl><dl><dt class="spec value" id="val-one"><a href="#val-one" class="anchor"></a><code><span class="keyword">val</span> one : <a href="index.html#type-t">t</a></code></dt><dd><p>The one coefficient (to rule them all, :p).</p></dd></dl><dl><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Unary negation</p></dd></dl><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Standard operations on coefficients.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/argument-2-Var/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-Var (sidekick-arith.Sidekick_arith_lra.Linear_expr.Make.2-Var)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Linear_expr</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; 2-Var</nav><h1>Parameter <code>Make.2-Var</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/Make/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick-arith.Sidekick_arith_lra.Linear_expr.Make)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Linear_expr</a> &#x00BB; Make</nav><h1>Module <code>Linear_expr.Make</code></h1><nav class="toc"><ul><li><a href="#linear-expressions.">Linear expressions.</a></li></ul></nav></header><h3 class="heading">Parameters</h3><ul><li><code><a href="argument-1-C/index.html">C</a> : <a href="../index.html#module-type-COEFF">COEFF</a></code></li><li><code><a href="argument-2-Var/index.html">Var</a> : <a href="../index.html#module-type-VAR">VAR</a></code></li></ul><h3 class="heading">Signature</h3><dl><dt class="spec module" id="module-C"><a href="#module-C" class="anchor"></a><code><span class="keyword">module</span> C = <a href="index.html#argument-1-C">C</a></code></dt><dd><p>Coeficients used. Can be integers as well as rationals.</p></dd></dl><dl><dt class="spec module" id="module-Var"><a href="#module-Var" class="anchor"></a><code><span class="keyword">module</span> Var = <a href="index.html#argument-2-Var">Var</a></code></dt><dd><p>Variables used in expressions.</p></dd></dl><dl><dt class="spec type" id="type-var"><a href="#type-var" class="anchor"></a><code><span class="keyword">type</span> var</code><code> = <a href="Var/index.html#type-t">Var.t</a></code></dt><dd><p>The type of variables appearing in expressions.</p></dd></dl><dl><dt class="spec module" id="module-Var_map"><a href="#module-Var_map" class="anchor"></a><code><span class="keyword">module</span> Var_map = CCMap.Make(<a href="index.html#argument-2-Var">Var</a>)</code></dt><dd><p>Maps from variables, used for expressions as well as substitutions.</p></dd></dl><dl><dt class="spec type" id="type-subst"><a href="#type-subst" class="anchor"></a><code><span class="keyword">type</span> subst</code><code> = <span><a href="C/index.html#type-t">C.t</a> <a href="index.html#module-Var_map">Var_map</a>.t</span></code></dt><dd><p>Type for substitutions.</p></dd></dl><dl><dt class="spec module" id="module-Comb"><a href="#module-Comb" class="anchor"></a><code><span class="keyword">module</span> <a href="Comb/index.html">Comb</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Combinations.</p></dd></dl><section><header><h3 id="linear-expressions."><a href="#linear-expressions." class="anchor"></a>Linear expressions.</h3></header><dl><dt class="spec module" id="module-Expr"><a href="#module-Expr" class="anchor"></a><code><span class="keyword">module</span> <a href="Expr/index.html">Expr</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Linear expressions represent linear arithmetic expressions as a linear combination and a constant.</p></dd></dl><dl><dt class="spec module" id="module-Constr"><a href="#module-Constr" class="anchor"></a><code><span class="keyword">module</span> <a href="Constr/index.html">Constr</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd></dd></dl></section></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Linear_expr (sidekick-arith.Sidekick_arith_lra.Linear_expr)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; Linear_expr</nav><h1>Module <code>Sidekick_arith_lra.Linear_expr</code></h1><p>Arithmetic expressions</p></header><div class="spec module-type" id="module-type-COEFF"><a href="#module-type-COEFF" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-COEFF/index.html">COEFF</a> = <a href="../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-COEFF">Sidekick_arith_lra__.Linear_expr_intf.COEFF</a></code></div><div class="spec module-type" id="module-type-VAR"><a href="#module-type-VAR" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-VAR/index.html">VAR</a> = <a href="../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-VAR">Sidekick_arith_lra__.Linear_expr_intf.VAR</a></code></div><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-S/index.html">S</a> = <a href="../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-S">Sidekick_arith_lra__.Linear_expr_intf.S</a></code></div><dl><dt class="spec type" id="type-bool_op"><a href="#type-bool_op" class="anchor"></a><code><span class="keyword">type</span> <span class="keyword">nonrec</span> bool_op</code><code> = <a href="../../Sidekick_arith_lra__/Linear_expr_intf/index.html#type-bool_op">Sidekick_arith_lra__.Linear_expr_intf.bool_op</a></code><code> = </code><table class="variant"><tr id="type-bool_op.Leq" class="anchored"><td class="def constructor"><a href="#type-bool_op.Leq" class="anchor"></a><code>| </code><code><span class="constructor">Leq</span></code></td></tr><tr id="type-bool_op.Geq" class="anchored"><td class="def constructor"><a href="#type-bool_op.Geq" class="anchor"></a><code>| </code><code><span class="constructor">Geq</span></code></td></tr><tr id="type-bool_op.Lt" class="anchored"><td class="def constructor"><a href="#type-bool_op.Lt" class="anchor"></a><code>| </code><code><span class="constructor">Lt</span></code></td></tr><tr id="type-bool_op.Gt" class="anchored"><td class="def constructor"><a href="#type-bool_op.Gt" class="anchor"></a><code>| </code><code><span class="constructor">Gt</span></code></td></tr><tr id="type-bool_op.Eq" class="anchored"><td class="def constructor"><a href="#type-bool_op.Eq" class="anchor"></a><code>| </code><code><span class="constructor">Eq</span></code></td></tr><tr id="type-bool_op.Neq" class="anchored"><td class="def constructor"><a href="#type-bool_op.Neq" class="anchor"></a><code>| </code><code><span class="constructor">Neq</span></code></td></tr></table></dt></dl><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><code><span class="keyword">module</span> <a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-C/index.html">C</a> : <a href="index.html#module-type-COEFF">COEFF</a>) <span>&#45;&gt;</span> <span class="keyword">functor</span> (<a href="Make/argument-2-Var/index.html">Var</a> : <a href="index.html#module-type-VAR">VAR</a>) <span>&#45;&gt;</span> <a href="index.html#module-type-S">S</a> <span class="keyword">with</span> <span class="keyword">module</span> <a href="Make/C/index.html">C</a> = <a href="Make/index.html#argument-1-C">C</a> <span class="keyword">and</span> <span class="keyword">module</span> <a href="Make/Var/index.html">Var</a> = <a href="Make/index.html#argument-2-Var">Var</a> <span class="keyword">and</span> <span class="keyword">module</span> <a href="Make/Var_map/index.html">Var_map</a> = CCMap.Make(<a href="Make/index.html#argument-2-Var">Var</a>)</code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-COEFF/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>COEFF (sidekick-arith.Sidekick_arith_lra.Linear_expr.COEFF)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Linear_expr</a> &#x00BB; COEFF</nav><h1>Module type <code>Linear_expr.COEFF</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Comparison on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for coefficients.</p></dd></dl><dl><dt class="spec value" id="val-zero"><a href="#val-zero" class="anchor"></a><code><span class="keyword">val</span> zero : <a href="index.html#type-t">t</a></code></dt><dd><p>The zero coefficient.</p></dd></dl><dl><dt class="spec value" id="val-one"><a href="#val-one" class="anchor"></a><code><span class="keyword">val</span> one : <a href="index.html#type-t">t</a></code></dt><dd><p>The one coefficient (to rule them all, :p).</p></dd></dl><dl><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Unary negation</p></dd></dl><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Standard operations on coefficients.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/C/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>C (sidekick-arith.Sidekick_arith_lra.Linear_expr.S.C)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Linear_expr</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; C</nav><h1>Module <code>S.C</code></h1><p>Coeficients used. Can be integers as well as rationals.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Equality on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Comparison on coefficients.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for coefficients.</p></dd></dl><dl><dt class="spec value" id="val-zero"><a href="#val-zero" class="anchor"></a><code><span class="keyword">val</span> zero : <a href="index.html#type-t">t</a></code></dt><dd><p>The zero coefficient.</p></dd></dl><dl><dt class="spec value" id="val-one"><a href="#val-one" class="anchor"></a><code><span class="keyword">val</span> one : <a href="index.html#type-t">t</a></code></dt><dd><p>The one coefficient (to rule them all, :p).</p></dd></dl><dl><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Unary negation</p></dd></dl><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Standard operations on coefficients.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Comb/Infix/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Infix (sidekick-arith.Sidekick_arith_lra.Linear_expr.S.Comb.Infix)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Linear_expr</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">Comb</a> &#x00BB; Infix</nav><h1>Module <code>Comb.Infix</code></h1><p>Infix operations on combinations</p><p>This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.</p></header><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Addition between combinations.</p></dd></dl><dl><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Substraction between combinations.</p></dd></dl><dl><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="../../C/index.html#type-t">C.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Multiplication by a constant.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Comb/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Constr/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Expr/Infix/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Infix (sidekick-arith.Sidekick_arith_lra.Linear_expr.S.Expr.Infix)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Linear_expr</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">Expr</a> &#x00BB; Infix</nav><h1>Module <code>Expr.Infix</code></h1><p>Infix operations on expressions</p><p>This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.</p></header><dl><dt class="spec value" id="val-(+)"><a href="#val-(+)" class="anchor"></a><code><span class="keyword">val</span> (+) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Addition between expressions.</p></dd></dl><dl><dt class="spec value" id="val-(-)"><a href="#val-(-)" class="anchor"></a><code><span class="keyword">val</span> (-) : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Substraction between expressions.</p></dd></dl><dl><dt class="spec value" id="val-(*)"><a href="#val-(*)" class="anchor"></a><code><span class="keyword">val</span> (*) : <a href="../../C/index.html#type-t">C.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Multiplication by a constant.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Expr/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/Var/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Var (sidekick-arith.Sidekick_arith_lra.Linear_expr.S.Var)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Linear_expr</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Var</nav><h1>Module <code>S.Var</code></h1><p>Variables used in expressions.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-S/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick-arith.Sidekick_arith_lra.Linear_expr.S)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Linear_expr</a> &#x00BB; S</nav><h1>Module type <code>Linear_expr.S</code></h1><nav class="toc"><ul><li><a href="#linear-expressions.">Linear expressions.</a></li></ul></nav></header><dl><dt class="spec module" id="module-C"><a href="#module-C" class="anchor"></a><code><span class="keyword">module</span> <a href="C/index.html">C</a> : <a href="../../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-COEFF">Sidekick_arith_lra__.Linear_expr_intf.COEFF</a></code></dt><dd><p>Coeficients used. Can be integers as well as rationals.</p></dd></dl><dl><dt class="spec module" id="module-Var"><a href="#module-Var" class="anchor"></a><code><span class="keyword">module</span> <a href="Var/index.html">Var</a> : <a href="../../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-VAR">Sidekick_arith_lra__.Linear_expr_intf.VAR</a></code></dt><dd><p>Variables used in expressions.</p></dd></dl><dl><dt class="spec type" id="type-var"><a href="#type-var" class="anchor"></a><code><span class="keyword">type</span> var</code><code> = <a href="Var/index.html#type-t">Var.t</a></code></dt><dd><p>The type of variables appearing in expressions.</p></dd></dl><dl><dt class="spec module" id="module-Var_map"><a href="#module-Var_map" class="anchor"></a><code><span class="keyword">module</span> Var_map : CCMap.S <span class="keyword">with</span> <span class="keyword">type</span> <a href="index.html#module-Var_map">Var_map</a>.key = <a href="index.html#type-var">var</a></code></dt><dd><p>Maps from variables, used for expressions as well as substitutions.</p></dd></dl><dl><dt class="spec type" id="type-subst"><a href="#type-subst" class="anchor"></a><code><span class="keyword">type</span> subst</code><code> = <span><a href="C/index.html#type-t">C.t</a> <a href="index.html#module-Var_map">Var_map</a>.t</span></code></dt><dd><p>Type for substitutions.</p></dd></dl><dl><dt class="spec module" id="module-Comb"><a href="#module-Comb" class="anchor"></a><code><span class="keyword">module</span> <a href="Comb/index.html">Comb</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Combinations.</p></dd></dl><section><header><h3 id="linear-expressions."><a href="#linear-expressions." class="anchor"></a>Linear expressions.</h3></header><dl><dt class="spec module" id="module-Expr"><a href="#module-Expr" class="anchor"></a><code><span class="keyword">module</span> <a href="Expr/index.html">Expr</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Linear expressions represent linear arithmetic expressions as a linear combination and a constant.</p></dd></dl><dl><dt class="spec module" id="module-Constr"><a href="#module-Constr" class="anchor"></a><code><span class="keyword">module</span> <a href="Constr/index.html">Constr</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd></dd></dl></section></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Linear_expr/module-type-VAR/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>VAR (sidekick-arith.Sidekick_arith_lra.Linear_expr.VAR)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Linear_expr</a> &#x00BB; VAR</nav><h1>Module type <code>Linear_expr.VAR</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/Gensym/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Gensym (sidekick-arith.Sidekick_arith_lra.Make.1-A.Gensym)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Make</a> &#x00BB; <a href="../index.html">1-A</a> &#x00BB; Gensym</nav><h1>Module <code>1-A.Gensym</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-create"><a href="#val-create" class="anchor"></a><code><span class="keyword">val</span> create : <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a></code></dt><dt class="spec value" id="val-copy"><a href="#val-copy" class="anchor"></a><code><span class="keyword">val</span> copy : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fresh_term"><a href="#val-fresh_term" class="anchor"></a><code><span class="keyword">val</span> fresh_term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>pre:string</span> <span>&#45;&gt;</span> <a href="../S/T/Ty/index.html#type-t">S.T.Ty.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Make a fresh term of the given type</p></dd></dl></div></body></html>

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

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Atom)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Make</a> &#x00BB; <a href="../../index.html">1-A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Atom</nav><h1>Module <code>S.Atom</code></h1><h4 id="boolean-atoms"><a href="#boolean-atoms" class="anchor"></a>Boolean Atoms</h4></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-formula"><a href="#val-formula" class="anchor"></a><code><span class="keyword">val</span> formula : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

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

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Lit (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Lit)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Make</a> &#x00BB; <a href="../../index.html">1-A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Lit</nav><h1>Module <code>S.Lit</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="T/Term/index.html#type-t">T.Term.t</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

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

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Model (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Model)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Make</a> &#x00BB; <a href="../../index.html">1-A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Model</nav><h1>Module <code>S.Model</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

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

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

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

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

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/CC/Actions/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Actions (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Solver_internal.CC.Actions)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">Make</a> &#x00BB; <a href="../../../../index.html">1-A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Actions</nav><h1>Module <code>CC.Actions</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><div class="spec module" id="module-P"><a href="#module-P" class="anchor"></a><code><span class="keyword">module</span> P = <a href="../index.html#module-P">P</a></code></div><div class="spec module" id="module-Lit"><a href="#module-Lit" class="anchor"></a><code><span class="keyword">module</span> Lit = <a href="../index.html#module-Lit">Lit</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../../index.html#type-actions">actions</a></code></dt></dl><dl><dt class="spec value" id="val-raise_conflict"><a href="#val-raise_conflict" class="anchor"></a><code><span class="keyword">val</span> raise_conflict : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-propagate"><a href="#val-propagate" class="anchor"></a><code><span class="keyword">val</span> propagate : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="Lit/index.html#type-t">Lit.t</a> <span>&#45;&gt;</span> <span>reason:<span>(unit <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span>)</span></span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/CC/Expl/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Solver_internal.CC.Expl)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">Make</a> &#x00BB; <a href="../../../../index.html">1-A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Expl</nav><h1>Module <code>CC.Expl</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span class="keyword">val</span> mk_merge : <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span class="keyword">val</span> mk_merge_t : <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span class="keyword">val</span> mk_lit : <a href="../index.html#type-lit">lit</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span class="keyword">val</span> mk_list : <span><a href="index.html#type-t">t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span class="keyword">val</span> mk_theory : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/CC/N/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>N (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Solver_internal.CC.N)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">Make</a> &#x00BB; <a href="../../../../index.html">1-A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; N</nav><h1>Module <code>CC.N</code></h1><p>An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the &quot;representative&quot;.</p><p>All information pertaining to the whole equivalence class is stored in this representative's node.</p><p>When two classes become equal (are &quot;merged&quot;), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.</p><p>We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-is_root"><a href="#val-is_root" class="anchor"></a><code><span class="keyword">val</span> is_root : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Is the node a root (ie the representative of its class)?</p></dd></dl><dl><dt class="spec value" id="val-iter_class"><a href="#val-iter_class" class="anchor"></a><code><span class="keyword">val</span> iter_class : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the congruence class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec value" id="val-iter_parents"><a href="#val-iter_parents" class="anchor"></a><code><span class="keyword">val</span> iter_parents : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the parents of the class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec type" id="type-bitfield"><a href="#type-bitfield" class="anchor"></a><code><span class="keyword">type</span> bitfield</code></dt><dd><p>A field in the bitfield of this node. This should only be allocated when a theory is initialized.</p><p>All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.</p></dd></dl><dl><dt class="spec value" id="val-get_field"><a href="#val-get_field" class="anchor"></a><code><span class="keyword">val</span> get_field : <a href="index.html#type-bitfield">bitfield</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/CC/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/Simplify/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simplify (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.Solver_internal.Simplify)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">Make</a> &#x00BB; <a href="../../../index.html">1-A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">Solver_internal</a> &#x00BB; Simplify</nav><h1>Module <code>Solver_internal.Simplify</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term_state">term_state</a></code></dt><dt class="spec value" id="val-ty_st"><a href="#val-ty_st" class="anchor"></a><code><span class="keyword">val</span> ty_st : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty_state">ty_state</a></code></dt><dt class="spec value" id="val-clear"><a href="#val-clear" class="anchor"></a><code><span class="keyword">val</span> clear : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Reset internal cache, etc.</p></dd></dl><dl><dt class="spec type" id="type-hook"><a href="#type-hook" class="anchor"></a><code><span class="keyword">type</span> hook</code><code> = <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dd><p>Given a term, try to simplify it. Return <code>None</code> if it didn't change.</p></dd></dl><dl><dt class="spec value" id="val-normalize"><a href="#val-normalize" class="anchor"></a><code><span class="keyword">val</span> normalize : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Normalize a term using all the hooks.</p></dd></dl></div></body></html>

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

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/T/Fun/index.html Normal file
View file

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

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/T/Term/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Term (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.T.Term)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">Make</a> &#x00BB; <a href="../../../index.html">1-A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Term</nav><h1>Module <code>T.Term</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Ty/index.html#type-t">Ty.t</a></code></dt><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-as_bool"><a href="#val-as_bool" class="anchor"></a><code><span class="keyword">val</span> as_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>bool option</span></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> * bool</code></dt><dt class="spec value" id="val-map_shallow"><a href="#val-map_shallow" class="anchor"></a><code><span class="keyword">val</span> map_shallow : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Map function on immediate subterms</p></dd></dl><dl><dt class="spec value" id="val-iter_dag"><a href="#val-iter_dag" class="anchor"></a><code><span class="keyword">val</span> iter_dag : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span> <span>&#45;&gt;</span> unit</code></dt></dl><div class="spec module" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><code><span class="keyword">module</span> Tbl : CCHashtbl.S <span class="keyword">with</span> <span class="keyword">type</span> <a href="index.html#module-Tbl">Tbl</a>.key = <a href="index.html#type-t">t</a></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/T/Ty/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ty (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.T.Ty)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">Make</a> &#x00BB; <a href="../../../index.html">1-A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Ty</nav><h1>Module <code>T.Ty</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-is_bool"><a href="#val-is_bool" class="anchor"></a><code><span class="keyword">val</span> is_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

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

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>T (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.T)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Make</a> &#x00BB; <a href="../../index.html">1-A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; T</nav><h1>Module <code>S.T</code></h1></header><div class="spec module" id="module-Fun"><a href="#module-Fun" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun/index.html">Fun</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Ty"><a href="#module-Ty" class="anchor"></a><code><span class="keyword">module</span> <a href="Ty/index.html">Ty</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span class="keyword">module</span> <a href="Term/index.html">Term</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

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

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

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

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/S/module-type-THEORY/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>THEORY (sidekick-arith.Sidekick_arith_lra.Make.1-A.S.THEORY)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">Make</a> &#x00BB; <a href="../../index.html">1-A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; THEORY</nav><h1>Module type <code>S.THEORY</code></h1><h4 id="a-theory"><a href="#a-theory" class="anchor"></a>A theory</h4><p>Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.</p><p>Typically a theory should be a functor taking an argument containing a <code>SOLVER_INTERNAL</code> or even a full <code>SOLVER</code>, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type <a href="../../../../../../sidekick/Sidekick_core/module-type-SOLVER/index.html#type-theory"><code>Sidekick_core.SOLVER.theory</code></a>) can be added to the solver.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>The theory's state</p></dd></dl><dl><dt class="spec value" id="val-name"><a href="#val-name" class="anchor"></a><code><span class="keyword">val</span> name : string</code></dt><dd><p>Name of the theory</p></dd></dl><dl><dt class="spec value" id="val-create_and_setup"><a href="#val-create_and_setup" class="anchor"></a><code><span class="keyword">val</span> create_and_setup : <a href="../Solver_internal/index.html#type-t">Solver_internal.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Instantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.</p></dd></dl><dl><dt class="spec value" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span class="keyword">val</span> push_level : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Push backtracking level</p></dd></dl><dl><dt class="spec value" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span class="keyword">val</span> pop_levels : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int <span>&#45;&gt;</span> unit</code></dt><dd><p>Pop backtracking levels, restoring the theory to its former state</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/argument-1-A/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-A (sidekick-arith.Sidekick_arith_lra.Make.1-A)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; 1-A</nav><h1>Parameter <code>Make.1-A</code></h1></header><div class="spec module" id="module-S"><a href="#module-S" class="anchor"></a><code><span class="keyword">module</span> <a href="S/index.html">S</a> : <a href="../../../../sidekick/Sidekick_core/index.html#module-type-SOLVER">Sidekick_core.SOLVER</a></code></div><dl><dt class="spec type" id="type-term"><a href="#type-term" class="anchor"></a><code><span class="keyword">type</span> term</code><code> = <a href="S/T/Term/index.html#type-t">S.T.Term.t</a></code></dt><dt class="spec type" id="type-ty"><a href="#type-ty" class="anchor"></a><code><span class="keyword">type</span> ty</code><code> = <a href="S/T/Ty/index.html#type-t">S.T.Ty.t</a></code></dt></dl><dl><dt class="spec value" id="val-view_as_lra"><a href="#val-view_as_lra" class="anchor"></a><code><span class="keyword">val</span> view_as_lra : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../../index.html#type-lra_view">lra_view</a></span></code></dt><dd><p>Project the term into the theory view</p></dd></dl><dl><dt class="spec value" id="val-mk_bool"><a href="#val-mk_bool" class="anchor"></a><code><span class="keyword">val</span> mk_bool : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dt class="spec value" id="val-mk_lra"><a href="#val-mk_lra" class="anchor"></a><code><span class="keyword">val</span> mk_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../../index.html#type-lra_view">lra_view</a></span> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>Make a term from the given theory view</p></dd></dl><dl><dt class="spec value" id="val-ty_lra"><a href="#val-ty_lra" class="anchor"></a><code><span class="keyword">val</span> ty_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-ty">ty</a></code></dt><dt class="spec value" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><code><span class="keyword">val</span> mk_eq : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>syntactic equality</p></dd></dl><dl><dt class="spec value" id="val-has_ty_real"><a href="#val-has_ty_real" class="anchor"></a><code><span class="keyword">val</span> has_ty_real : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Does this term have the type <code>Real</code></p></dd></dl><div class="spec module" id="module-Gensym"><a href="#module-Gensym" class="anchor"></a><code><span class="keyword">module</span> <a href="Gensym/index.html">Gensym</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Make/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (sidekick-arith.Sidekick_arith_lra.Make)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; Make</nav><h1>Module <code>Sidekick_arith_lra.Make</code></h1></header><h3 class="heading">Parameters</h3><ul><li><code><a href="argument-1-A/index.html">A</a> : <a href="../index.html#module-type-ARG">ARG</a></code></li></ul><h3 class="heading">Signature</h3><div class="spec module" id="module-A"><a href="#module-A" class="anchor"></a><code><span class="keyword">module</span> A = <a href="index.html#argument-1-A">A</a></code></div><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-create"><a href="#val-create" class="anchor"></a><code><span class="keyword">val</span> create : <span>?&#8288;stat:<a href="../../../sidekick/Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a></span> <span>&#45;&gt;</span> <a href="A/S/T/Term/index.html#type-state">A.S.T.Term.state</a> <span>&#45;&gt;</span> <a href="A/S/T/Ty/index.html#type-state">A.S.T.Ty.state</a> <span>&#45;&gt;</span> <a href="index.html#type-state">state</a></code></dt><dt class="spec value" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span class="keyword">val</span> theory : <a href="A/S/index.html#type-theory">A.S.theory</a></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Predicate/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Predicate (sidekick-arith.Sidekick_arith_lra.Predicate)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; Predicate</nav><h1>Module <code>Sidekick_arith_lra.Predicate</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><table class="variant"><tr id="type-t.Leq" class="anchored"><td class="def constructor"><a href="#type-t.Leq" class="anchor"></a><code>| </code><code><span class="constructor">Leq</span></code></td></tr><tr id="type-t.Geq" class="anchored"><td class="def constructor"><a href="#type-t.Geq" class="anchor"></a><code>| </code><code><span class="constructor">Geq</span></code></td></tr><tr id="type-t.Lt" class="anchored"><td class="def constructor"><a href="#type-t.Lt" class="anchor"></a><code>| </code><code><span class="constructor">Lt</span></code></td></tr><tr id="type-t.Gt" class="anchored"><td class="def constructor"><a href="#type-t.Gt" class="anchor"></a><code>| </code><code><span class="constructor">Gt</span></code></td></tr><tr id="type-t.Eq" class="anchored"><td class="def constructor"><a href="#type-t.Eq" class="anchor"></a><code>| </code><code><span class="constructor">Eq</span></code></td></tr><tr id="type-t.Neq" class="anchored"><td class="def constructor"><a href="#type-t.Neq" class="anchor"></a><code>| </code><code><span class="constructor">Neq</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-neg_sign"><a href="#val-neg_sign" class="anchor"></a><code><span class="keyword">val</span> neg_sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Make/Constraint/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Constraint (sidekick-arith.Sidekick_arith_lra.Simplex2.Make.Constraint)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; Constraint</nav><h1>Module <code>Make.Constraint</code></h1></header><dl><dt class="spec type" id="type-op"><a href="#type-op" class="anchor"></a><code><span class="keyword">type</span> op</code><code> = <a href="../../Op/index.html#type-t">Op.t</a></code></dt><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.op" class="anchored"><td class="def field"><a href="#type-t.op" class="anchor"></a><code>op : <a href="index.html#type-op">op</a>;</code></td></tr><tr id="type-t.lhs" class="anchored"><td class="def field"><a href="#type-t.lhs" class="anchor"></a><code>lhs : <a href="../V/index.html#type-t">V.t</a>;</code></td></tr><tr id="type-t.rhs" class="anchored"><td class="def field"><a href="#type-t.rhs" class="anchor"></a><code>rhs : <a href="../index.html#type-num">num</a>;</code></td></tr></table><code>}</code></dt><dd><p>A constraint is the comparison of a variable to a constant.</p></dd></dl><dl><dt class="spec value" id="val-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="index.html#type-op">op</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-lt"><a href="#val-lt" class="anchor"></a><code><span class="keyword">val</span> lt : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-geq"><a href="#val-geq" class="anchor"></a><code><span class="keyword">val</span> geq : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-gt"><a href="#val-gt" class="anchor"></a><code><span class="keyword">val</span> gt : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Make/Subst/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Subst (sidekick-arith.Sidekick_arith_lra.Simplex2.Make.Subst)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; Subst</nav><h1>Module <code>Make.Subst</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <span><a href="../index.html#type-num">num</a> <a href="../index.html#module-V_map">V_map</a>.t</span></code></dt></dl><dl><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> Q.t</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Make/Unsat_cert/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Unsat_cert (sidekick-arith.Sidekick_arith_lra.Simplex2.Make.Unsat_cert)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; Unsat_cert</nav><h1>Module <code>Make.Unsat_cert</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-unsat_cert">unsat_cert</a></code></dt></dl><dl><dt class="spec value" id="val-lits"><a href="#val-lits" class="anchor"></a><code><span class="keyword">val</span> lits : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../V/index.html#type-lit">V.lit</a> list</span></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Make/argument-1-Var/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-Var (sidekick-arith.Sidekick_arith_lra.Simplex2.Make.1-Var)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; 1-Var</nav><h1>Parameter <code>Make.1-Var</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Make/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/Op/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Op (sidekick-arith.Sidekick_arith_lra.Simplex2.Op)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Simplex2</a> &#x00BB; Op</nav><h1>Module <code>Simplex2.Op</code></h1><h3 id="basic-operator"><a href="#basic-operator" class="anchor"></a>Basic operator</h3></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><table class="variant"><tr id="type-t.Leq" class="anchored"><td class="def constructor"><a href="#type-t.Leq" class="anchor"></a><code>| </code><code><span class="constructor">Leq</span></code></td></tr><tr id="type-t.Lt" class="anchored"><td class="def constructor"><a href="#type-t.Lt" class="anchor"></a><code>| </code><code><span class="constructor">Lt</span></code></td></tr><tr id="type-t.Geq" class="anchored"><td class="def constructor"><a href="#type-t.Geq" class="anchor"></a><code>| </code><code><span class="constructor">Geq</span></code></td></tr><tr id="type-t.Gt" class="anchored"><td class="def constructor"><a href="#type-t.Gt" class="anchor"></a><code>| </code><code><span class="constructor">Gt</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-neg_sign"><a href="#val-neg_sign" class="anchor"></a><code><span class="keyword">val</span> neg_sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-not_"><a href="#val-not_" class="anchor"></a><code><span class="keyword">val</span> not_ : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.t <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simplex2 (sidekick-arith.Sidekick_arith_lra.Simplex2)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; Simplex2</nav><h1>Module <code>Sidekick_arith_lra.Simplex2</code></h1><h2 id="fast-simplex-for-cdcl(t)"><a href="#fast-simplex-for-cdcl(t)" class="anchor"></a>Fast Simplex for CDCL(T)</h2><p>We follow the paper &quot;Integrating Simplex with DPLL(T )&quot; from de Moura and Dutertre.</p></header><div class="spec module-type" id="module-type-VAR"><a href="#module-type-VAR" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-VAR/index.html">VAR</a> = <a href="../../Sidekick_arith_lra__/Linear_expr_intf/index.html#module-type-VAR">Sidekick_arith_lra__.Linear_expr_intf.VAR</a></code></div><dl><dt class="spec module" id="module-Op"><a href="#module-Op" class="anchor"></a><code><span class="keyword">module</span> <a href="Op/index.html">Op</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd></dd></dl><div class="spec module-type" id="module-type-S"><a href="#module-type-S" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-S/index.html">S</a> = <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Make"><a href="#module-Make" class="anchor"></a><code><span class="keyword">module</span> <a href="Make/index.html">Make</a> : <span class="keyword">functor</span> (<a href="Make/argument-1-Var/index.html">Var</a> : <a href="index.html#module-type-VAR">VAR</a>) <span>&#45;&gt;</span> <a href="index.html#module-type-S">S</a> <span class="keyword">with</span> <span class="keyword">module</span> <a href="Make/V/index.html">V</a> = <a href="Make/index.html#argument-1-Var">Var</a></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-S/Constraint/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Constraint (sidekick-arith.Sidekick_arith_lra.Simplex2.S.Constraint)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Constraint</nav><h1>Module <code>S.Constraint</code></h1></header><dl><dt class="spec type" id="type-op"><a href="#type-op" class="anchor"></a><code><span class="keyword">type</span> op</code><code> = <a href="../../Op/index.html#type-t">Op.t</a></code></dt><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.op" class="anchored"><td class="def field"><a href="#type-t.op" class="anchor"></a><code>op : <a href="index.html#type-op">op</a>;</code></td></tr><tr id="type-t.lhs" class="anchored"><td class="def field"><a href="#type-t.lhs" class="anchor"></a><code>lhs : <a href="../V/index.html#type-t">V.t</a>;</code></td></tr><tr id="type-t.rhs" class="anchored"><td class="def field"><a href="#type-t.rhs" class="anchor"></a><code>rhs : <a href="../index.html#type-num">num</a>;</code></td></tr></table><code>}</code></dt><dd><p>A constraint is the comparison of a variable to a constant.</p></dd></dl><dl><dt class="spec value" id="val-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="index.html#type-op">op</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-lt"><a href="#val-lt" class="anchor"></a><code><span class="keyword">val</span> lt : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-geq"><a href="#val-geq" class="anchor"></a><code><span class="keyword">val</span> geq : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-gt"><a href="#val-gt" class="anchor"></a><code><span class="keyword">val</span> gt : <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-num">num</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-S/Subst/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Subst (sidekick-arith.Sidekick_arith_lra.Simplex2.S.Subst)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Subst</nav><h1>Module <code>S.Subst</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <span><a href="../index.html#type-num">num</a> <a href="../index.html#module-V_map">V_map</a>.t</span></code></dt></dl><dl><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../V/index.html#type-t">V.t</a> <span>&#45;&gt;</span> Q.t</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-S/Unsat_cert/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Unsat_cert (sidekick-arith.Sidekick_arith_lra.Simplex2.S.Unsat_cert)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Unsat_cert</nav><h1>Module <code>S.Unsat_cert</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../index.html#type-unsat_cert">unsat_cert</a></code></dt></dl><dl><dt class="spec value" id="val-lits"><a href="#val-lits" class="anchor"></a><code><span class="keyword">val</span> lits : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../V/index.html#type-lit">V.lit</a> list</span></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-S/V/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>V (sidekick-arith.Sidekick_arith_lra.Simplex2.S.V)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">Simplex2</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; V</nav><h1>Module <code>S.V</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-S/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/Simplex2/module-type-VAR/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>VAR (sidekick-arith.Sidekick_arith_lra.Simplex2.VAR)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">Simplex2</a> &#x00BB; VAR</nav><h1>Module type <code>Simplex2.VAR</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Variable type.</p></dd></dl><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dd><p>Standard comparison function on variables.</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dd><p>Printer for variables.</p></dd></dl><dl><dt class="spec type" id="type-lit"><a href="#type-lit" class="anchor"></a><code><span class="keyword">type</span> lit</code></dt></dl><dl><dt class="spec value" id="val-pp_lit"><a href="#val-pp_lit" class="anchor"></a><code><span class="keyword">val</span> pp_lit : <span><a href="index.html#type-lit">lit</a> <a href="../../../../sidekick/Sidekick_util/index.html#module-Fmt">Sidekick_util.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-not_lit"><a href="#val-not_lit" class="anchor"></a><code><span class="keyword">val</span> not_lit : <a href="index.html#type-lit">lit</a> <span>&#45;&gt;</span> <span><a href="index.html#type-lit">lit</a> option</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/Gensym/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Gensym (sidekick-arith.Sidekick_arith_lra.ARG.Gensym)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">ARG</a> &#x00BB; Gensym</nav><h1>Module <code>ARG.Gensym</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-create"><a href="#val-create" class="anchor"></a><code><span class="keyword">val</span> create : <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a></code></dt><dt class="spec value" id="val-copy"><a href="#val-copy" class="anchor"></a><code><span class="keyword">val</span> copy : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fresh_term"><a href="#val-fresh_term" class="anchor"></a><code><span class="keyword">val</span> fresh_term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>pre:string</span> <span>&#45;&gt;</span> <a href="../S/T/Ty/index.html#type-t">S.T.Ty.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Make a fresh term of the given type</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Atom/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick-arith.Sidekick_arith_lra.ARG.S.Atom)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">ARG</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Atom</nav><h1>Module <code>S.Atom</code></h1><h4 id="boolean-atoms"><a href="#boolean-atoms" class="anchor"></a>Boolean Atoms</h4></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-formula"><a href="#val-formula" class="anchor"></a><code><span class="keyword">val</span> formula : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Lit/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Lit (sidekick-arith.Sidekick_arith_lra.ARG.S.Lit)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">ARG</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Lit</nav><h1>Module <code>S.Lit</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="T/Term/index.html#type-t">T.Term.t</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Model/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Model (sidekick-arith.Sidekick_arith_lra.ARG.S.Model)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">ARG</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Model</nav><h1>Module <code>S.Model</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

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

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Proof/index.html Normal file
View file

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/CC/Actions/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Actions (sidekick-arith.Sidekick_arith_lra.ARG.S.Solver_internal.CC.Actions)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">ARG</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Actions</nav><h1>Module <code>CC.Actions</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><div class="spec module" id="module-P"><a href="#module-P" class="anchor"></a><code><span class="keyword">module</span> P = <a href="../index.html#module-P">P</a></code></div><div class="spec module" id="module-Lit"><a href="#module-Lit" class="anchor"></a><code><span class="keyword">module</span> Lit = <a href="../index.html#module-Lit">Lit</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../../index.html#type-actions">actions</a></code></dt></dl><dl><dt class="spec value" id="val-raise_conflict"><a href="#val-raise_conflict" class="anchor"></a><code><span class="keyword">val</span> raise_conflict : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-propagate"><a href="#val-propagate" class="anchor"></a><code><span class="keyword">val</span> propagate : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="Lit/index.html#type-t">Lit.t</a> <span>&#45;&gt;</span> <span>reason:<span>(unit <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span>)</span></span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/CC/Expl/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick-arith.Sidekick_arith_lra.ARG.S.Solver_internal.CC.Expl)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">ARG</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Expl</nav><h1>Module <code>CC.Expl</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span class="keyword">val</span> mk_merge : <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span class="keyword">val</span> mk_merge_t : <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span class="keyword">val</span> mk_lit : <a href="../index.html#type-lit">lit</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span class="keyword">val</span> mk_list : <span><a href="index.html#type-t">t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span class="keyword">val</span> mk_theory : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/CC/N/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>N (sidekick-arith.Sidekick_arith_lra.ARG.S.Solver_internal.CC.N)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">ARG</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; N</nav><h1>Module <code>CC.N</code></h1><p>An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the &quot;representative&quot;.</p><p>All information pertaining to the whole equivalence class is stored in this representative's node.</p><p>When two classes become equal (are &quot;merged&quot;), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.</p><p>We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-is_root"><a href="#val-is_root" class="anchor"></a><code><span class="keyword">val</span> is_root : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Is the node a root (ie the representative of its class)?</p></dd></dl><dl><dt class="spec value" id="val-iter_class"><a href="#val-iter_class" class="anchor"></a><code><span class="keyword">val</span> iter_class : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the congruence class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec value" id="val-iter_parents"><a href="#val-iter_parents" class="anchor"></a><code><span class="keyword">val</span> iter_parents : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the parents of the class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec type" id="type-bitfield"><a href="#type-bitfield" class="anchor"></a><code><span class="keyword">type</span> bitfield</code></dt><dd><p>A field in the bitfield of this node. This should only be allocated when a theory is initialized.</p><p>All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.</p></dd></dl><dl><dt class="spec value" id="val-get_field"><a href="#val-get_field" class="anchor"></a><code><span class="keyword">val</span> get_field : <a href="index.html#type-bitfield">bitfield</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/CC/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/Simplify/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simplify (sidekick-arith.Sidekick_arith_lra.ARG.S.Solver_internal.Simplify)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">ARG</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">Solver_internal</a> &#x00BB; Simplify</nav><h1>Module <code>Solver_internal.Simplify</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term_state">term_state</a></code></dt><dt class="spec value" id="val-ty_st"><a href="#val-ty_st" class="anchor"></a><code><span class="keyword">val</span> ty_st : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty_state">ty_state</a></code></dt><dt class="spec value" id="val-clear"><a href="#val-clear" class="anchor"></a><code><span class="keyword">val</span> clear : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Reset internal cache, etc.</p></dd></dl><dl><dt class="spec type" id="type-hook"><a href="#type-hook" class="anchor"></a><code><span class="keyword">type</span> hook</code><code> = <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dd><p>Given a term, try to simplify it. Return <code>None</code> if it didn't change.</p></dd></dl><dl><dt class="spec value" id="val-normalize"><a href="#val-normalize" class="anchor"></a><code><span class="keyword">val</span> normalize : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Normalize a term using all the hooks.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/T/Fun/index.html Normal file
View file

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/T/Term/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Term (sidekick-arith.Sidekick_arith_lra.ARG.S.T.Term)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">ARG</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Term</nav><h1>Module <code>T.Term</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Ty/index.html#type-t">Ty.t</a></code></dt><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-as_bool"><a href="#val-as_bool" class="anchor"></a><code><span class="keyword">val</span> as_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>bool option</span></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> * bool</code></dt><dt class="spec value" id="val-map_shallow"><a href="#val-map_shallow" class="anchor"></a><code><span class="keyword">val</span> map_shallow : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Map function on immediate subterms</p></dd></dl><dl><dt class="spec value" id="val-iter_dag"><a href="#val-iter_dag" class="anchor"></a><code><span class="keyword">val</span> iter_dag : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span> <span>&#45;&gt;</span> unit</code></dt></dl><div class="spec module" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><code><span class="keyword">module</span> Tbl : CCHashtbl.S <span class="keyword">with</span> <span class="keyword">type</span> <a href="index.html#module-Tbl">Tbl</a>.key = <a href="index.html#type-t">t</a></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/T/Ty/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ty (sidekick-arith.Sidekick_arith_lra.ARG.S.T.Ty)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">ARG</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Ty</nav><h1>Module <code>T.Ty</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-is_bool"><a href="#val-is_bool" class="anchor"></a><code><span class="keyword">val</span> is_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/T/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>T (sidekick-arith.Sidekick_arith_lra.ARG.S.T)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">ARG</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; T</nav><h1>Module <code>S.T</code></h1></header><div class="spec module" id="module-Fun"><a href="#module-Fun" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun/index.html">Fun</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Ty"><a href="#module-Ty" class="anchor"></a><code><span class="keyword">module</span> <a href="Ty/index.html">Ty</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span class="keyword">module</span> <a href="Term/index.html">Term</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/Unknown/index.html Normal file
View file

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

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

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/S/module-type-THEORY/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>THEORY (sidekick-arith.Sidekick_arith_lra.ARG.S.THEORY)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">ARG</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; THEORY</nav><h1>Module type <code>S.THEORY</code></h1><h4 id="a-theory"><a href="#a-theory" class="anchor"></a>A theory</h4><p>Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.</p><p>Typically a theory should be a functor taking an argument containing a <code>SOLVER_INTERNAL</code> or even a full <code>SOLVER</code>, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type <a href="../../../../../sidekick/Sidekick_core/module-type-SOLVER/index.html#type-theory"><code>Sidekick_core.SOLVER.theory</code></a>) can be added to the solver.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>The theory's state</p></dd></dl><dl><dt class="spec value" id="val-name"><a href="#val-name" class="anchor"></a><code><span class="keyword">val</span> name : string</code></dt><dd><p>Name of the theory</p></dd></dl><dl><dt class="spec value" id="val-create_and_setup"><a href="#val-create_and_setup" class="anchor"></a><code><span class="keyword">val</span> create_and_setup : <a href="../Solver_internal/index.html#type-t">Solver_internal.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Instantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.</p></dd></dl><dl><dt class="spec value" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span class="keyword">val</span> push_level : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Push backtracking level</p></dd></dl><dl><dt class="spec value" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span class="keyword">val</span> pop_levels : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int <span>&#45;&gt;</span> unit</code></dt><dd><p>Pop backtracking levels, restoring the theory to its former state</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-ARG/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ARG (sidekick-arith.Sidekick_arith_lra.ARG)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; ARG</nav><h1>Module type <code>Sidekick_arith_lra.ARG</code></h1></header><div class="spec module" id="module-S"><a href="#module-S" class="anchor"></a><code><span class="keyword">module</span> <a href="S/index.html">S</a> : <a href="../../../sidekick/Sidekick_core/index.html#module-type-SOLVER">Sidekick_core.SOLVER</a></code></div><dl><dt class="spec type" id="type-term"><a href="#type-term" class="anchor"></a><code><span class="keyword">type</span> term</code><code> = <a href="S/T/Term/index.html#type-t">S.T.Term.t</a></code></dt><dt class="spec type" id="type-ty"><a href="#type-ty" class="anchor"></a><code><span class="keyword">type</span> ty</code><code> = <a href="S/T/Ty/index.html#type-t">S.T.Ty.t</a></code></dt></dl><dl><dt class="spec value" id="val-view_as_lra"><a href="#val-view_as_lra" class="anchor"></a><code><span class="keyword">val</span> view_as_lra : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../index.html#type-lra_view">lra_view</a></span></code></dt><dd><p>Project the term into the theory view</p></dd></dl><dl><dt class="spec value" id="val-mk_bool"><a href="#val-mk_bool" class="anchor"></a><code><span class="keyword">val</span> mk_bool : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dt class="spec value" id="val-mk_lra"><a href="#val-mk_lra" class="anchor"></a><code><span class="keyword">val</span> mk_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../index.html#type-lra_view">lra_view</a></span> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>Make a term from the given theory view</p></dd></dl><dl><dt class="spec value" id="val-ty_lra"><a href="#val-ty_lra" class="anchor"></a><code><span class="keyword">val</span> ty_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-ty">ty</a></code></dt><dt class="spec value" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><code><span class="keyword">val</span> mk_eq : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>syntactic equality</p></dd></dl><dl><dt class="spec value" id="val-has_ty_real"><a href="#val-has_ty_real" class="anchor"></a><code><span class="keyword">val</span> has_ty_real : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Does this term have the type <code>Real</code></p></dd></dl><div class="spec module" id="module-Gensym"><a href="#module-Gensym" class="anchor"></a><code><span class="keyword">module</span> <a href="Gensym/index.html">Gensym</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/Gensym/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Gensym (sidekick-arith.Sidekick_arith_lra.S.A.Gensym)</title><link rel="stylesheet" href="../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">A</a> &#x00BB; Gensym</nav><h1>Module <code>A.Gensym</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-create"><a href="#val-create" class="anchor"></a><code><span class="keyword">val</span> create : <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../S/T/Term/index.html#type-state">S.T.Term.state</a></code></dt><dt class="spec value" id="val-copy"><a href="#val-copy" class="anchor"></a><code><span class="keyword">val</span> copy : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fresh_term"><a href="#val-fresh_term" class="anchor"></a><code><span class="keyword">val</span> fresh_term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>pre:string</span> <span>&#45;&gt;</span> <a href="../S/T/Ty/index.html#type-t">S.T.Ty.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Make a fresh term of the given type</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Atom/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Atom (sidekick-arith.Sidekick_arith_lra.S.A.S.Atom)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Atom</nav><h1>Module <code>S.Atom</code></h1><h4 id="boolean-atoms"><a href="#boolean-atoms" class="anchor"></a>Boolean Atoms</h4></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> CCFormat.printer</span></code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-formula"><a href="#val-formula" class="anchor"></a><code><span class="keyword">val</span> formula : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-lit">lit</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Lit/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Lit (sidekick-arith.Sidekick_arith_lra.S.A.S.Lit)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Lit</nav><h1>Module <code>S.Lit</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="T/Term/index.html#type-t">T.Term.t</a></code></dt><dt class="spec value" id="val-sign"><a href="#val-sign" class="anchor"></a><code><span class="keyword">val</span> sign : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Model/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Model (sidekick-arith.Sidekick_arith_lra.S.A.S.Model)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; Model</nav><h1>Module <code>S.Model</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-find"><a href="#val-find" class="anchor"></a><code><span class="keyword">val</span> find : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl></div></body></html>

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

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Proof/index.html Normal file
View file

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/CC/Actions/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Actions (sidekick-arith.Sidekick_arith_lra.S.A.S.Solver_internal.CC.Actions)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">S</a> &#x00BB; <a href="../../../../index.html">A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Actions</nav><h1>Module <code>CC.Actions</code></h1></header><div class="spec module" id="module-T"><a href="#module-T" class="anchor"></a><code><span class="keyword">module</span> T = <a href="../index.html#module-T">T</a></code></div><div class="spec module" id="module-P"><a href="#module-P" class="anchor"></a><code><span class="keyword">module</span> P = <a href="../index.html#module-P">P</a></code></div><div class="spec module" id="module-Lit"><a href="#module-Lit" class="anchor"></a><code><span class="keyword">module</span> Lit = <a href="../index.html#module-Lit">Lit</a></code></div><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../../index.html#type-actions">actions</a></code></dt></dl><dl><dt class="spec value" id="val-raise_conflict"><a href="#val-raise_conflict" class="anchor"></a><code><span class="keyword">val</span> raise_conflict : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-propagate"><a href="#val-propagate" class="anchor"></a><code><span class="keyword">val</span> propagate : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="Lit/index.html#type-t">Lit.t</a> <span>&#45;&gt;</span> <span>reason:<span>(unit <span>&#45;&gt;</span> <span><a href="Lit/index.html#type-t">Lit.t</a> list</span>)</span></span> <span>&#45;&gt;</span> <a href="P/index.html#type-t">P.t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/CC/Expl/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick-arith.Sidekick_arith_lra.S.A.S.Solver_internal.CC.Expl)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">S</a> &#x00BB; <a href="../../../../index.html">A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; Expl</nav><h1>Module <code>CC.Expl</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span class="keyword">val</span> mk_merge : <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="../N/index.html#type-t">N.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span class="keyword">val</span> mk_merge_t : <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span class="keyword">val</span> mk_lit : <a href="../index.html#type-lit">lit</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span class="keyword">val</span> mk_list : <span><a href="index.html#type-t">t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span class="keyword">val</span> mk_theory : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/CC/N/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>N (sidekick-arith.Sidekick_arith_lra.S.A.S.Solver_internal.CC.N)</title><link rel="stylesheet" href="../../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../../index.html">S</a> &#x00BB; <a href="../../../../index.html">A</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">Solver_internal</a> &#x00BB; <a href="../index.html">CC</a> &#x00BB; N</nav><h1>Module <code>CC.N</code></h1><p>An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the &quot;representative&quot;.</p><p>All information pertaining to the whole equivalence class is stored in this representative's node.</p><p>When two classes become equal (are &quot;merged&quot;), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.</p><p>We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-term"><a href="#val-term" class="anchor"></a><code><span class="keyword">val</span> term : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt><dt class="spec value" id="val-is_root"><a href="#val-is_root" class="anchor"></a><code><span class="keyword">val</span> is_root : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Is the node a root (ie the representative of its class)?</p></dd></dl><dl><dt class="spec value" id="val-iter_class"><a href="#val-iter_class" class="anchor"></a><code><span class="keyword">val</span> iter_class : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the congruence class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec value" id="val-iter_parents"><a href="#val-iter_parents" class="anchor"></a><code><span class="keyword">val</span> iter_parents : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> Iter.t</span></code></dt><dd><p>Traverse the parents of the class. Precondition: <code>is_root n</code> (see <a href="../index.html#val-find"><code>find</code></a> below)</p></dd></dl><dl><dt class="spec type" id="type-bitfield"><a href="#type-bitfield" class="anchor"></a><code><span class="keyword">type</span> bitfield</code></dt><dd><p>A field in the bitfield of this node. This should only be allocated when a theory is initialized.</p><p>All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.</p></dd></dl><dl><dt class="spec value" id="val-get_field"><a href="#val-get_field" class="anchor"></a><code><span class="keyword">val</span> get_field : <a href="index.html#type-bitfield">bitfield</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/CC/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/Simplify/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Simplify (sidekick-arith.Sidekick_arith_lra.S.A.S.Solver_internal.Simplify)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">S</a> &#x00BB; <a href="../../../index.html">A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">Solver_internal</a> &#x00BB; Simplify</nav><h1>Module <code>Solver_internal.Simplify</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-tst"><a href="#val-tst" class="anchor"></a><code><span class="keyword">val</span> tst : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term_state">term_state</a></code></dt><dt class="spec value" id="val-ty_st"><a href="#val-ty_st" class="anchor"></a><code><span class="keyword">val</span> ty_st : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-ty_state">ty_state</a></code></dt><dt class="spec value" id="val-clear"><a href="#val-clear" class="anchor"></a><code><span class="keyword">val</span> clear : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Reset internal cache, etc.</p></dd></dl><dl><dt class="spec type" id="type-hook"><a href="#type-hook" class="anchor"></a><code><span class="keyword">type</span> hook</code><code> = <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-term">term</a> option</span></code></dt><dd><p>Given a term, try to simplify it. Return <code>None</code> if it didn't change.</p></dd></dl><dl><dt class="spec value" id="val-normalize"><a href="#val-normalize" class="anchor"></a><code><span class="keyword">val</span> normalize : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="../index.html#type-term">term</a></code></dt><dd><p>Normalize a term using all the hooks.</p></dd></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/index.html Normal file
View file

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/T/Fun/index.html Normal file
View file

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

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/T/Term/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Term (sidekick-arith.Sidekick_arith_lra.S.A.S.T.Term)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">S</a> &#x00BB; <a href="../../../index.html">A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Term</nav><h1>Module <code>T.Term</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span class="keyword">val</span> ty : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../Ty/index.html#type-t">Ty.t</a></code></dt><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-as_bool"><a href="#val-as_bool" class="anchor"></a><code><span class="keyword">val</span> as_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>bool option</span></code></dt><dt class="spec value" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span class="keyword">val</span> abs : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> * bool</code></dt><dt class="spec value" id="val-map_shallow"><a href="#val-map_shallow" class="anchor"></a><code><span class="keyword">val</span> map_shallow : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a>)</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Map function on immediate subterms</p></dd></dl><dl><dt class="spec value" id="val-iter_dag"><a href="#val-iter_dag" class="anchor"></a><code><span class="keyword">val</span> iter_dag : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>(<a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span> <span>&#45;&gt;</span> unit</code></dt></dl><div class="spec module" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><code><span class="keyword">module</span> Tbl : CCHashtbl.S <span class="keyword">with</span> <span class="keyword">type</span> <a href="index.html#module-Tbl">Tbl</a>.key = <a href="index.html#type-t">t</a></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/T/Ty/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ty (sidekick-arith.Sidekick_arith_lra.S.A.S.T.Ty)</title><link rel="stylesheet" href="../../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../../index.html">S</a> &#x00BB; <a href="../../../index.html">A</a> &#x00BB; <a href="../../index.html">S</a> &#x00BB; <a href="../index.html">T</a> &#x00BB; Ty</nav><h1>Module <code>T.Ty</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span class="keyword">val</span> hash : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <span><a href="index.html#type-t">t</a> <a href="../../../../../../../sidekick/Sidekick_core/index.html#module-Fmt">Sidekick_core.Fmt</a>.printer</span></code></dt></dl><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span class="keyword">val</span> bool : <a href="index.html#type-state">state</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-is_bool"><a href="#val-is_bool" class="anchor"></a><code><span class="keyword">val</span> is_bool : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/T/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>T (sidekick-arith.Sidekick_arith_lra.S.A.S.T)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; T</nav><h1>Module <code>S.T</code></h1></header><div class="spec module" id="module-Fun"><a href="#module-Fun" class="anchor"></a><code><span class="keyword">module</span> <a href="Fun/index.html">Fun</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Ty"><a href="#module-Ty" class="anchor"></a><code><span class="keyword">module</span> <a href="Ty/index.html">Ty</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="spec module" id="module-Term"><a href="#module-Term" class="anchor"></a><code><span class="keyword">module</span> <a href="Term/index.html">Term</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/Unknown/index.html Normal file
View file

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

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

File diff suppressed because one or more lines are too long

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/A/S/module-type-THEORY/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>THEORY (sidekick-arith.Sidekick_arith_lra.S.A.S.THEORY)</title><link rel="stylesheet" href="../../../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../../../index.html">S</a> &#x00BB; <a href="../../index.html">A</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; THEORY</nav><h1>Module type <code>S.THEORY</code></h1><h4 id="a-theory"><a href="#a-theory" class="anchor"></a>A theory</h4><p>Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.</p><p>Typically a theory should be a functor taking an argument containing a <code>SOLVER_INTERNAL</code> or even a full <code>SOLVER</code>, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type <a href="../../../../../../sidekick/Sidekick_core/module-type-SOLVER/index.html#type-theory"><code>Sidekick_core.SOLVER.theory</code></a>) can be added to the solver.</p></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>The theory's state</p></dd></dl><dl><dt class="spec value" id="val-name"><a href="#val-name" class="anchor"></a><code><span class="keyword">val</span> name : string</code></dt><dd><p>Name of the theory</p></dd></dl><dl><dt class="spec value" id="val-create_and_setup"><a href="#val-create_and_setup" class="anchor"></a><code><span class="keyword">val</span> create_and_setup : <a href="../Solver_internal/index.html#type-t">Solver_internal.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Instantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.</p></dd></dl><dl><dt class="spec value" id="val-push_level"><a href="#val-push_level" class="anchor"></a><code><span class="keyword">val</span> push_level : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Push backtracking level</p></dd></dl><dl><dt class="spec value" id="val-pop_levels"><a href="#val-pop_levels" class="anchor"></a><code><span class="keyword">val</span> pop_levels : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int <span>&#45;&gt;</span> unit</code></dt><dd><p>Pop backtracking levels, restoring the theory to its former state</p></dd></dl></div></body></html>

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

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>A (sidekick-arith.Sidekick_arith_lra.S.A)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick-arith</a> &#x00BB; <a href="../../index.html">Sidekick_arith_lra</a> &#x00BB; <a href="../index.html">S</a> &#x00BB; A</nav><h1>Module <code>S.A</code></h1></header><div class="spec module" id="module-S"><a href="#module-S" class="anchor"></a><code><span class="keyword">module</span> <a href="S/index.html">S</a> : <a href="../../../../sidekick/Sidekick_core/index.html#module-type-SOLVER">Sidekick_core.SOLVER</a></code></div><dl><dt class="spec type" id="type-term"><a href="#type-term" class="anchor"></a><code><span class="keyword">type</span> term</code><code> = <a href="S/T/Term/index.html#type-t">S.T.Term.t</a></code></dt><dt class="spec type" id="type-ty"><a href="#type-ty" class="anchor"></a><code><span class="keyword">type</span> ty</code><code> = <a href="S/T/Ty/index.html#type-t">S.T.Ty.t</a></code></dt></dl><dl><dt class="spec value" id="val-view_as_lra"><a href="#val-view_as_lra" class="anchor"></a><code><span class="keyword">val</span> view_as_lra : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../../index.html#type-lra_view">lra_view</a></span></code></dt><dd><p>Project the term into the theory view</p></dd></dl><dl><dt class="spec value" id="val-mk_bool"><a href="#val-mk_bool" class="anchor"></a><code><span class="keyword">val</span> mk_bool : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dt class="spec value" id="val-mk_lra"><a href="#val-mk_lra" class="anchor"></a><code><span class="keyword">val</span> mk_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <span><a href="index.html#type-term">term</a> <a href="../../index.html#type-lra_view">lra_view</a></span> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>Make a term from the given theory view</p></dd></dl><dl><dt class="spec value" id="val-ty_lra"><a href="#val-ty_lra" class="anchor"></a><code><span class="keyword">val</span> ty_lra : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-ty">ty</a></code></dt><dt class="spec value" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><code><span class="keyword">val</span> mk_eq : <a href="S/T/Term/index.html#type-state">S.T.Term.state</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> <a href="index.html#type-term">term</a></code></dt><dd><p>syntactic equality</p></dd></dl><dl><dt class="spec value" id="val-has_ty_real"><a href="#val-has_ty_real" class="anchor"></a><code><span class="keyword">val</span> has_ty_real : <a href="index.html#type-term">term</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Does this term have the type <code>Real</code></p></dd></dl><div class="spec module" id="module-Gensym"><a href="#module-Gensym" class="anchor"></a><code><span class="keyword">module</span> <a href="Gensym/index.html">Gensym</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></div></body></html>

2
dev/sidekick-arith/Sidekick_arith_lra/module-type-S/index.html Normal file
View file

@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>S (sidekick-arith.Sidekick_arith_lra.S)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">sidekick-arith</a> &#x00BB; <a href="../index.html">Sidekick_arith_lra</a> &#x00BB; S</nav><h1>Module type <code>Sidekick_arith_lra.S</code></h1></header><div class="spec module" id="module-A"><a href="#module-A" class="anchor"></a><code><span class="keyword">module</span> <a href="A/index.html">A</a> : <a href="../index.html#module-type-ARG">ARG</a></code></div><dl><dt class="spec type" id="type-state"><a href="#type-state" class="anchor"></a><code><span class="keyword">type</span> state</code></dt></dl><dl><dt class="spec value" id="val-create"><a href="#val-create" class="anchor"></a><code><span class="keyword">val</span> create : <span>?&#8288;stat:<a href="../../../sidekick/Sidekick_util/Stat/index.html#type-t">Sidekick_util.Stat.t</a></span> <span>&#45;&gt;</span> <a href="A/S/T/Term/index.html#type-state">A.S.T.Term.state</a> <span>&#45;&gt;</span> <a href="A/S/T/Ty/index.html#type-state">A.S.T.Ty.state</a> <span>&#45;&gt;</span> <a href="index.html#type-state">state</a></code></dt><dt class="spec value" id="val-theory"><a href="#val-theory" class="anchor"></a><code><span class="keyword">val</span> theory : <a href="A/S/index.html#type-theory">A.S.theory</a></code></dt></dl></div></body></html>

Some files were not shown because too many files have changed in this diff Show more