<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Libabsolute__Domains (libabsolute.Libabsolute__Domains)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><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">libabsolute</a> &#x00BB; Libabsolute__Domains</nav><h1>Module <code>Libabsolute__Domains</code></h1><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><nav class="toc"><ul><li><a href="#domain-environment-management">Domain environment management</a></li><li><a href="#predefined-abstract-domains">Predefined Abstract Domains</a><ul><li><a href="#numeric-domains">Numeric domains</a></li><li><a href="#boolean-domains">Boolean domains</a></li><li><a href="#combinators">Combinators</a></li></ul></li></ul></nav></header><dl><dt class="spec module-type" id="module-type-B"><a href="#module-type-B" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-B/index.html">B</a> = <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Type of generic functors that lift a numeric domain to a boolean one</p></dd></dl><dl><dt class="spec module-type" id="module-type-D1"><a href="#module-type-D1" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-D1/index.html">D1</a> = <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Type of domain combinator of arity 1 (e.g powerset)</p></dd></dl><dl><dt class="spec module-type" id="module-type-D2"><a href="#module-type-D2" class="anchor"></a><code><span class="keyword">module</span> <span class="keyword">type</span> <a href="module-type-D2/index.html">D2</a> = <span class="keyword">sig</span> ... <span class="keyword">end</span></code></dt><dd><p>Type of domain combinator of arity 2 (e.g products)</p></dd></dl><section><header><h2 id="domain-environment-management"><a href="#domain-environment-management" class="anchor"></a>Domain environment management</h2></header><dl><dt class="spec value" id="val-get_all"><a href="#val-get_all" class="anchor"></a><code><span class="keyword">val</span> get_all : unit <span>&#45;&gt;</span> <span>string list</span></code></dt><dd><p>collect the list of all registered domain names</p></dd></dl><dl><dt class="spec value" id="val-register_numeric"><a href="#val-register_numeric" class="anchor"></a><code><span class="keyword">val</span> register_numeric : string <span>&#45;&gt;</span> <span>(<span class="keyword">module</span> <a href="../Libabsolute/Signature/module-type-Numeric/index.html">Libabsolute.Signature.Numeric</a>)</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>registers a numeric domain into the list of available abstract domains</p></dd></dl><dl><dt class="spec value" id="val-register_boolean"><a href="#val-register_boolean" class="anchor"></a><code><span class="keyword">val</span> register_boolean : string <span>&#45;&gt;</span> <span>(<span class="keyword">module</span> <a href="module-type-B/index.html">B</a>)</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>registers a boolean domain into the list of available abstract domains</p></dd></dl><dl><dt class="spec value" id="val-register_1"><a href="#val-register_1" class="anchor"></a><code><span class="keyword">val</span> register_1 : string <span>&#45;&gt;</span> <span>(<span class="keyword">module</span> <a href="module-type-D1/index.html">D1</a>)</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>registers a domain combinator into the list of combinators of arity 1</p></dd></dl><dl><dt class="spec value" id="val-register_2"><a href="#val-register_2" class="anchor"></a><code><span class="keyword">val</span> register_2 : string <span>&#45;&gt;</span> <span>(<span class="keyword">module</span> <a href="module-type-D2/index.html">D2</a>)</span> <span>&#45;&gt;</span> unit</code></dt><dd><p>registers a domain combinator into the list of combinators of arity 2</p></dd></dl><dl><dt class="spec value" id="val-parse"><a href="#val-parse" class="anchor"></a><code><span class="keyword">val</span> parse : string <span>&#45;&gt;</span> string <span>&#45;&gt;</span> <span>(<span class="keyword">module</span> <a href="../Libabsolute/Signature/module-type-Domain/index.html">Libabsolute.Signature.Domain</a>)</span></code></dt><dd><p>builds the abstract domain corresponding to the name of the numeric representaion and boolean representation given in parameter. Domain application follows the syntax : <code>&quot;combinator(domain1,domain2)&quot;</code> where <code>combinator</code> has to be registered with the <code>register_2</code> function (or be one of the predefined comibnator), and both <code>domain1</code> and <code>domain2</code> has to be registered. Useful to build a domain from a command line description</p></dd></dl></section><section><header><h2 id="predefined-abstract-domains"><a href="#predefined-abstract-domains" class="anchor"></a>Predefined Abstract Domains</h2></header><section><header><h3 id="numeric-domains"><a href="#numeric-domains" class="anchor"></a>Numeric domains</h3></header><dl><dt class="spec module" id="module-BoxF"><a href="#module-BoxF" class="anchor"></a><code><span class="keyword">module</span> <a href="BoxF/index.html">BoxF</a> : <a href="../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></dt><dd><p>Boxes with floatting point included bounds</p></dd></dl><dl><dt class="spec module" id="module-BoxS"><a href="#module-BoxS" class="anchor"></a><code><span class="keyword">module</span> <a href="BoxS/index.html">BoxS</a> : <a href="../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></dt><dd><p>Boxes with floatting point included or excluded bounds</p></dd></dl><dl><dt class="spec module" id="module-ApronBox"><a href="#module-ApronBox" class="anchor"></a><code><span class="keyword">module</span> <a href="ApronBox/index.html">ApronBox</a> : <a href="../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></dt><dd><p>Apron Boxes</p></dd></dl><dl><dt class="spec module" id="module-Poly"><a href="#module-Poly" class="anchor"></a><code><span class="keyword">module</span> <a href="Poly/index.html">Poly</a> : <a href="../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></dt><dd><p>Apron Polyhedra</p></dd></dl><dl><dt class="spec module" id="module-Oct"><a href="#module-Oct" class="anchor"></a><code><span class="keyword">module</span> <a href="Oct/index.html">Oct</a> : <a href="../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></dt><dd><p>Apron Octagons</p></dd></dl></section><section><header><h3 id="boolean-domains"><a href="#boolean-domains" class="anchor"></a>Boolean domains</h3></header><dl><dt class="spec module" id="module-Boolean"><a href="#module-Boolean" class="anchor"></a><code><span class="keyword">module</span> <a href="Boolean/index.html">Boolean</a> : <a href="index.html#module-type-B">B</a></code></dt><dd><p>Lfts a numerical domain to a boolean one</p></dd></dl><dl><dt class="spec module" id="module-Utree"><a href="#module-Utree" class="anchor"></a><code><span class="keyword">module</span> <a href="Utree/index.html">Utree</a> : <a href="index.html#module-type-B">B</a></code></dt><dd><p>Disjunctive form with fast-precomputation for meets</p></dd></dl></section><section><header><h3 id="combinators"><a href="#combinators" class="anchor"></a>Combinators</h3></header><dl><dt class="spec module" id="module-Product"><a href="#module-Product" class="anchor"></a><code><span class="keyword">module</span> <a href="Product/index.html">Product</a> : <a href="index.html#module-type-D2">D2</a></code></dt><dd><p>Specialized Reduced Product. Corresponds to the option <code>-d product (a,b)</code> of AbSolute. if a constraint can be filtered exactly by the domain <code>b</code>, it is affected to it, otherwise it is affected to <code>b</code>.</p></dd></dl></section></section></div></body></html>