This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.
<!DOCTYPE html>
<htmlxmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseCItv (infer.Pulselib__PulseCItv)</title><linkrel="stylesheet"href="../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.1"/><metaname="viewport"content="width=device-width,initial-scale=1.0"/><scriptsrc="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><divclass="content"><header><nav><ahref="../index.html">Up</a>–<ahref="../index.html">infer</a>» Pulselib__PulseCItv</nav><h1>Module <code>Pulselib__PulseCItv</code></h1></header><divclass="spec module"id="module-F"><ahref="#module-F"class="anchor"></a><code><spanclass="keyword">module</span> F = Stdlib.Format</code></div><aside><p>Concrete interval domain (CItv)</p></aside><dl><dtclass="spec type"id="type-t"><ahref="#type-t"class="anchor"></a><code><spanclass="keyword">type</span> t</code></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare"><ahref="#val-compare"class="anchor"></a><code><spanclass="keyword">val</span> compare : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> int</code></dt><dtclass="spec value"id="val-equal"><ahref="#val-equal"class="anchor"></a><code><spanclass="keyword">val</span> equal : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> bool</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-equal_to"><ahref="#val-equal_to"class="anchor"></a><code><spanclass="keyword">val</span> equal_to : <ahref="../IR/IntLit/index.html#type-t">IR.IntLit.t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-is_equal_to_zero"><ahref="#val-is_equal_to_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_equal_to_zero : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-is_not_equal_to_zero"><ahref="#val-is_not_equal_to_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_not_equal_to_zero : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>whether this is literally <code>≠0</code></p></dd></dl><dl><dtclass="spec value"id="val-pp"><ahref="#val-pp"class="anchor"></a><code><spanclass="keyword">val</span> pp : <ahref="index.html#module-F">F</a>.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt></dl><dl><dtclass="spec type"id="type-abduction_result"><ahref="#type-abduction_result"class="anchor"></a><code><spanclass="keyword">type</span> abduction_result</code><code> = </code><tableclass="variant"><trid="type-abduction_result.Unsatisfiable"class="anchored"><tdclass="def constructor"><ahref="#type-abduction_result.Unsatisfiable"class="anchor"></a><code>| </code><code><spanclass="constructor">Unsatisfiable</span></code></td><tdclass="doc"><p>the assertion is never true given the parameters</p></td></tr><trid="type-abduction_result.Satisfiable"class="anchored"><tdclass="def constructor"><ahref="#type-abduction_result.Satisfiable"class="anchor"></a><code>| </code><code><spanclass="constructor">Satisfiable</span><spanclass="keyword">of</span><span><ahref="index.html#type-t">t</a> option</span> * <span><ahref="index.html#type-t">t</a> option</span></code></td><tdclass="doc"><p>the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals</p></td></tr></table></dt></dl><dl><dtclass="spec value"id="val-abduce_binop_is_true"><ahref="#val-abduce_binop_is_true"class="anchor"></a><code><spanclass="keyword">val</span> abduce_binop_is_true : <span>negated:bool</span><span>-></span><ahref="../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><span><ahref="index.html#type-t">t</a> option</span><span>-></span><span><ahref="index.html#type-t">t</a> option</span><span>-></span><ahref="index.html#type-abduction_result">abduction_result</a></code></dt><dd><p>given <code>arith_lhs_opt bop arith_rhs_opt</code> and if not <code>negated</code>, return either</p><ul><li><code>Unsatisfiable</code> iff lhs bop rhs = ∅</li></ul><ul><li><code>Satisfiable (abduced_lhs_opt,abduced_rhs_opt)</code> iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is <code>None</code>, same for rhs) <code>abduced_lhs_opt=Some alhs</code> if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)</li></ul><p>If <code>negated</code> then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.</p></dd></dl><dl><dtclass="spec value"id="val-binop"><ahref="#val-binop"class="anchor"></a><code><spanclass="keyword">val</span> binop : <ahref="../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span><ahref="index.html#type-t">t</a> option</span></code></dt><dtclass="spec value"id="val-unop"><ahref="#val-unop"class="anchor"></a><code><spanclass="keyword">val</span> unop : <ahref="../IR/Unop/index.html#type-t">IR.Unop.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span><ahref="index.html#type-t">t</a> option</span></code></dt><dtclass="spec value"id="val-zero_inf"><ahref="#val-zero_inf"class="anchor"></a><code><spanclass="keyword">val</span> zero_inf : <ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-ge_to"><ahref="#val-ge_to"class="anchor"></a><code><spanclass="keyword">val</span> ge_to : <ahref="../IR/IntLit/index.html#type-t">IR.IntLit.t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt></dl></div></body></html>
