<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Consistency (libabsolute.Libabsolute.Consistency)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script><link rel="stylesheet" href="../../../odoc.support/katex.min.css"/><script src="../../../odoc.support/katex.min.js"></script><script>
//<![CDATA[

          document.addEventListener("DOMContentLoaded", function () {
            var elements = Array.from(document.getElementsByClassName("odoc-katex-math"));
            for (var i = 0; i < elements.length; i++) {
              var el = elements[i];
              var content = el.textContent;
              var new_el = document.createElement("span");
              new_el.setAttribute("class", "odoc-katex-math-rendered");
              var display = el.classList.contains("display");
              katex.render(content, new_el, { throwOnError: false, displayMode: display });
              el.replaceWith(new_el);
            }
          });
        
//]]>
</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> â€“ <a href="../../index.html">libabsolute</a> &#x00BB; <a href="../index.html">Libabsolute</a> &#x00BB; Consistency</nav><header class="odoc-preamble"><h1>Module <code><span>Libabsolute.Consistency</span></code></h1><p>This module provides types and operations for handling consistencies. A consitency is a property obtained after a filtering operation f(s,p): given an abstract value s, and a predicate p, it computes a set <code class="odoc-katex-math">s' \subseteq s</code> such that : <code class="odoc-katex-math">\forall x \in s, p(x) \implies x \in s'</code></p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> <span>'a t</span></span><span> = </span></code><ol><li id="type-t.Sat" class="def variant constructor anchored"><a href="#type-t.Sat" class="anchor"></a><code><span>| </span><span><span class="constructor">Sat</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>when <code class="odoc-katex-math">s' = s</code></p><span class="comment-delim">*)</span></div></li><li id="type-t.Unsat" class="def variant constructor anchored"><a href="#type-t.Unsat" class="anchor"></a><code><span>| </span><span><span class="constructor">Unsat</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>when <code class="odoc-katex-math">s' = \emptyset</code></p><span class="comment-delim">*)</span></div></li><li id="type-t.Filtered" class="def variant constructor anchored"><a href="#type-t.Filtered" class="anchor"></a><code><span>| </span><span><span class="constructor">Filtered</span> <span class="keyword">of</span> <span class="type-var">'a</span> * bool</span></code><div class="def-doc"><span class="comment-delim">(*</span><p><code class="odoc-katex-math">filtered (s',b) : \forall x \in s', b \implies p(x)</code></p><span class="comment-delim">*)</span></div></li><li id="type-t.Pruned" class="def variant constructor anchored"><a href="#type-t.Pruned" class="anchor"></a><code><span>| </span><span><span class="constructor">Pruned</span> <span class="keyword">of</span> </span><span>{</span></code><ol><li id="type-t.sure" class="def record field anchored"><a href="#type-t.sure" class="anchor"></a><code><span>sure : <span><span class="type-var">'a</span> list</span>;</span></code></li><li id="type-t.unsure" class="def record field anchored"><a href="#type-t.unsure" class="anchor"></a><code><span>unsure : <span><span class="type-var">'a</span> list</span>;</span></code></li></ol><code><span>}</span></code></li></ol></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-feasible"><a href="#type-feasible" class="anchor"></a><code><span><span class="keyword">type</span> feasible</span><span> = </span></code><ol><li id="type-feasible.Unfeasible" class="def variant constructor anchored"><a href="#type-feasible.Unfeasible" class="anchor"></a><code><span>| </span><span><span class="constructor">Unfeasible</span></span></code></li><li id="type-feasible.Maybe" class="def variant constructor anchored"><a href="#type-feasible.Maybe" class="anchor"></a><code><span>| </span><span><span class="constructor">Maybe</span></span></code></li><li id="type-feasible.Witness" class="def variant constructor anchored"><a href="#type-feasible.Witness" class="anchor"></a><code><span>| </span><span><span class="constructor">Witness</span> <span class="keyword">of</span> <a href="../Csp/index.html#type-instance">Csp.instance</a></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-print"><a href="#val-print" class="anchor"></a><code><span><span class="keyword">val</span> print : <span><span class="xref-unresolved">Stdlib</span>.Format.formatter <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'a</span> <a href="#type-t">t</a></span> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-map"><a href="#val-map" class="anchor"></a><code><span><span class="keyword">val</span> map : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'b</span>)</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'c</span> <a href="#type-t">t</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'d</span> <a href="#type-t">t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-bind"><a href="#val-bind" class="anchor"></a><code><span><span class="keyword">val</span> bind : <span><span>(<span><span class="type-var">'a</span> <span class="arrow">&#45;&gt;</span></span> <span>bool <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-t">t</a></span>)</span> <span class="arrow">&#45;&gt;</span></span> <span><span><span class="type-var">'c</span> <a href="#type-t">t</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'b</span> <a href="#type-t">t</a></span></span></code></div></div></div></body></html>
