<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Libabsolute (libabsolute.Libabsolute)</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; Libabsolute</nav><header class="odoc-preamble"><h1>Module <code><span>Libabsolute</span></code></h1><p>Libabsolute is a constraint solving library based on abstract domains</p></header><nav class="odoc-toc"><ul><li><a href="#core-constraint-language">Core constraint language</a></li><li><a href="#solver-parametrization">Solver parametrization</a></li><li><a href="#arithmetic-modules">Arithmetic modules</a></li><li><a href="#miscellaneous">Miscellaneous</a></li></ul></nav><div class="odoc-content"><h2 id="core-constraint-language"><a href="#core-constraint-language" class="anchor"></a>Core constraint language</h2><div class="odoc-spec"><div class="spec module anchored" id="module-Csp"><a href="#module-Csp" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Csp/index.html">Csp</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines the main types used for the constraint language of AbSolute, along with the type of problems, and instance.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Constraint"><a href="#module-Constraint" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Constraint/index.html">Constraint</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines the constraint language, and some basic operations over it</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Expr"><a href="#module-Expr" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Expr/index.html">Expr</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines the numerical language and some basic operations over it</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Dom"><a href="#module-Dom" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Dom/index.html">Dom</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines the different kinds of definition domains of variables</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Instance"><a href="#module-Instance" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Instance/index.html">Instance</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines the type of points (also called instances), i.e mappings from variables to rational coordinates.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Parser"><a href="#module-Parser" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Parser/index.html">Parser</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines several parsing utilities</p></div></div><h2 id="solver-parametrization"><a href="#solver-parametrization" class="anchor"></a>Solver parametrization</h2><div class="odoc-spec"><div class="spec module anchored" id="module-Signature"><a href="#module-Signature" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Signature/index.html">Signature</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Module signature for Abstract Domains for Constraint Programming (ADCP) they must feature consistency, split and precision operators.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Domains"><a href="#module-Domains" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Domains/index.html">Domains</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module handle the domain environment, already equipped with some basic domains. You can add your own using the <code>register_*</code> functions, and combine them with the already defined ones.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Solver"><a href="#module-Solver" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Solver/index.html">Solver</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Functor parametrized by an abstract domain and defines the three main solving functions</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Iterator"><a href="#module-Iterator" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Iterator/index.html">Iterator</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module converts the constraints into an internal state and handles the order of filtering</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Consistency"><a href="#module-Consistency" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Consistency/index.html">Consistency</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><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></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Result"><a href="#module-Result" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Result/index.html">Result</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines solution of the abstract solver as covers</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Constant"><a href="#module-Constant" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Constant/index.html">Constant</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><h2 id="arithmetic-modules"><a href="#arithmetic-modules" class="anchor"></a>Arithmetic modules</h2><div class="odoc-spec"><div class="spec module anchored" id="module-Ring"><a href="#module-Ring" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Ring/index.html">Ring</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Q"><a href="#module-Q" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Q/index.html">Q</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Rational arithmetic module</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-F"><a href="#module-F" class="anchor"></a><code><span><span class="keyword">module</span> <a href="F/index.html">F</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Float arithmetic module</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-I"><a href="#module-I" class="anchor"></a><code><span><span class="keyword">module</span> <a href="I/index.html">I</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Integer arithmetic module</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Polynom"><a href="#module-Polynom" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Polynom/index.html">Polynom</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>Module for polynomials over an abstract arithmetic rings</p></div></div><h2 id="miscellaneous"><a href="#miscellaneous" class="anchor"></a>Miscellaneous</h2><div class="odoc-spec"><div class="spec module anchored" id="module-Tools"><a href="#module-Tools" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Tools/index.html">Tools</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module defines diverse utilities</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Kleene"><a href="#module-Kleene" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Kleene/index.html">Kleene</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div><div class="spec-doc"><p>This module implements a 3-valued logic</p></div></div></div></body></html>
