<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Make (libabsolute.Libabsolute__.Domains.D2.Make)</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; <a href="../../../index.html">Libabsolute__</a> &#x00BB; <a href="../../index.html">Domains</a> &#x00BB; <a href="../index.html">D2</a> &#x00BB; Make</nav><h1>Module <code>D2.Make</code></h1></header><h3 class="heading">Parameters</h3><ul><li><code><a href="argument-1-A/index.html">A</a> : <a href="../../../../Libabsolute/Signature/index.html#module-type-Domain">Libabsolute.Signature.Domain</a></code></li><li><code><a href="argument-2-B/index.html">B</a> : <a href="../../../../Libabsolute/Signature/index.html#module-type-Domain">Libabsolute.Signature.Domain</a></code></li></ul><h3 class="heading">Signature</h3><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../../Libabsolute/Signature/index.html#module-type-Numeric">Libabsolute.Signature.Numeric</a></code></span></summary><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 type of (non-bottom) abstract elements</p></dd></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><dd><p>returns an empty element</p></dd></dl><section><header><h2 id="variables-management"><a href="#variables-management" class="anchor"></a>Variables management</h2></header><dl><dt class="spec value" id="val-add_var"><a href="#val-add_var" class="anchor"></a><code><span class="keyword">val</span> add_var : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Csp/index.html#type-decl">Libabsolute.Csp.decl</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>adds an unconstrained variable to the environnement</p></dd></dl><dl><dt class="spec value" id="val-rm_var"><a href="#val-rm_var" class="anchor"></a><code><span class="keyword">val</span> rm_var : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>removes a variable from the environnement</p></dd></dl><dl><dt class="spec value" id="val-vars"><a href="#val-vars" class="anchor"></a><code><span class="keyword">val</span> vars : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span>(<a href="../../../../Libabsolute/Csp/index.html#type-typ">Libabsolute.Csp.typ</a> * string)</span> list</span></code></dt><dd><p>returns the variables annoted by their type</p></dd></dl></section><section><header><h2 id="measure"><a href="#measure" class="anchor"></a>Measure</h2></header><dl><dt class="spec value" id="val-volume"><a href="#val-volume" class="anchor"></a><code><span class="keyword">val</span> volume : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> float</code></dt><dd><p>computes the volume of an abstract element</p></dd></dl></section><section><header><h2 id="set-theoretic-operations"><a href="#set-theoretic-operations" class="anchor"></a>Set-theoretic operations</h2></header><dl><dt class="spec value" id="val-join"><a href="#val-join" class="anchor"></a><code><span class="keyword">val</span> join : <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> * bool</code></dt><dd><p>Joins two abstract elements. The boolean flag indicates if the join was exact. It is always sound to return false</p></dd></dl><dl><dt class="spec value" id="val-join_list"><a href="#val-join_list" class="anchor"></a><code><span class="keyword">val</span> join_list : <span><a href="index.html#type-t">t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> * bool</code></dt><dd><p>Joins a list of <code>n</code> abstract elements. May be faster than joining pairwise. The boolean flag indicates if the join was exact. It is always sound to return false</p></dd></dl><dl><dt class="spec value" id="val-meet"><a href="#val-meet" class="anchor"></a><code><span class="keyword">val</span> meet : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> option</span></code></dt><dd><p>meet two abstract elements</p></dd></dl><dl><dt class="spec value" id="val-diff"><a href="#val-diff" class="anchor"></a><code><span class="keyword">val</span> diff : <span><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> <span><a href="index.html#type-t">t</a> list</span>)</span> option</span></code></dt><dd><p>substracts the second abstract element from the first (difference operator) if an exact operator can not be defined (None), the solver doesn't use the pruning features. precondition: the two abstract elements must be defined onto the same set of variables.</p></dd></dl><dl><dt class="spec value" id="val-split"><a href="#val-split" class="anchor"></a><code><span class="keyword">val</span> split : float <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> list</span></code></dt><dd><p>splits an abstract element</p></dd></dl><section><header><h3 id="constraint-conversion"><a href="#constraint-conversion" class="anchor"></a>constraint conversion</h3></header><dl><dt class="spec type" id="type-internal_constr"><a href="#type-internal_constr" class="anchor"></a><code><span class="keyword">type</span> internal_constr</code></dt><dd><p>domain's internal representation of a comparison</p></dd></dl><dl><dt class="spec value" id="val-internalize"><a href="#val-internalize" class="anchor"></a><code><span class="keyword">val</span> internalize : <span>?&#8288;elem:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Constraint/index.html#type-comparison">Libabsolute.Constraint.comparison</a> <span>&#45;&gt;</span> <a href="index.html#type-internal_constr">internal_constr</a></code></dt><dd><p>may use a current abstract element to simplify the constaint</p></dd></dl><dl><dt class="spec value" id="val-externalize"><a href="#val-externalize" class="anchor"></a><code><span class="keyword">val</span> externalize : <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Constraint/index.html#type-comparison">Libabsolute.Constraint.comparison</a></code></dt></dl></section></section><section><header><h2 id="constraint-management"><a href="#constraint-management" class="anchor"></a>Constraint management</h2></header><dl><dt class="spec value" id="val-filter"><a href="#val-filter" class="anchor"></a><code><span class="keyword">val</span> filter : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> <a href="../../../../Libabsolute/Consistency/index.html#type-t">Libabsolute.Consistency.t</a></span></code></dt><dd><p>filters an abstract element with respect to an arithmetic constraint, may raise bot found.</p></dd></dl><dl><dt class="spec value" id="val-is_representable"><a href="#val-is_representable" class="anchor"></a><code><span class="keyword">val</span> is_representable : <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Kleene/index.html#type-t">Libabsolute.Kleene.t</a></code></dt><dd><p>checks if a constraint is suited for this abstract domain</p></dd></dl><dl><dt class="spec value" id="val-forward_eval"><a href="#val-forward_eval" class="anchor"></a><code><span class="keyword">val</span> forward_eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> * <a href="../../../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a></code></dt><dd><p>computes the range of value of a given expression within an abstract element</p></dd></dl><dl><dt class="spec value" id="val-to_constraint"><a href="#val-to_constraint" class="anchor"></a><code><span class="keyword">val</span> to_constraint : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Constraint/index.html#type-t">Libabsolute.Constraint.t</a></code></dt><dd><p>transforms an abstract element into constraints</p></dd></dl><dl><dt class="spec value" id="val-spawn"><a href="#val-spawn" class="anchor"></a><code><span class="keyword">val</span> spawn : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Csp/index.html#type-instance">Libabsolute.Csp.instance</a></code></dt><dd><p>Random concretization function. useful to do tests, and to reuse the results. values are generated uniformly when possible</p></dd></dl><dl><dt class="spec value" id="val-is_abstraction"><a href="#val-is_abstraction" class="anchor"></a><code><span class="keyword">val</span> is_abstraction : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Csp/index.html#type-instance">Libabsolute.Csp.instance</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>check if an abstract element is an abstraction of an instance</p></dd></dl><dl><dt class="spec value" id="val-print"><a href="#val-print" class="anchor"></a><code><span class="keyword">val</span> print : Stdlib.Format.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>printing</p></dd></dl><dl><dt class="spec value" id="val-render"><a href="#val-render" class="anchor"></a><code><span class="keyword">val</span> render : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> Picasso.Drawable.t</code></dt><dd><p>transforms an abstract element into a Picasso.Drawable.t for drawing</p></dd></dl></section></details></div></div></div><dl><dt class="spec type" id="type-internal_constr"><a href="#type-internal_constr" class="anchor"></a><code><span class="keyword">type</span> internal_constr</code></dt><dd><p>domain's internal representation of a constraint</p></dd></dl><dl><dt class="spec value" id="val-internalize"><a href="#val-internalize" class="anchor"></a><code><span class="keyword">val</span> internalize : <span>?&#8288;elem:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Constraint/index.html#type-t">Libabsolute.Constraint.t</a> <span>&#45;&gt;</span> <a href="index.html#type-internal_constr">internal_constr</a></code></dt><dd><p>constraint conversion</p></dd></dl><dl><dt class="spec value" id="val-externalize"><a href="#val-externalize" class="anchor"></a><code><span class="keyword">val</span> externalize : <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Constraint/index.html#type-t">Libabsolute.Constraint.t</a></code></dt><dt class="spec value" id="val-filter"><a href="#val-filter" class="anchor"></a><code><span class="keyword">val</span> filter : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <span><span>(<a href="index.html#type-t">t</a> * <a href="index.html#type-internal_constr">internal_constr</a>)</span> <a href="../../../../Libabsolute/Consistency/index.html#type-t">Libabsolute.Consistency.t</a></span></code></dt><dd><p>redefinition of filter and is_representable using boolean expression</p></dd></dl><dl><dt class="spec value" id="val-is_representable"><a href="#val-is_representable" class="anchor"></a><code><span class="keyword">val</span> is_representable : <a href="index.html#type-internal_constr">internal_constr</a> <span>&#45;&gt;</span> <a href="../../../../Libabsolute/Kleene/index.html#type-t">Libabsolute.Kleene.t</a></code></dt></dl></div></body></html>