<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>N (libabsolute.Libabsolute.Domains.Utree.Make.N)</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></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; <a href="../../../index.html">Domains</a> &#x00BB; <a href="../../index.html">Utree</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; N</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make.N</span></code></h1></header><nav class="odoc-toc"><ul><li><a href="#variables-management">Variables management</a></li><li><a href="#measure">Measure</a></li><li><a href="#set-theoretic-operations">Set-theoretic operations</a><ul><li><a href="#constraint-conversion">constraint conversion</a></li></ul></li><li><a href="#constraint-management">Constraint management</a></li></ul></nav><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> t</span></code></div><div class="spec-doc"><p>the type of (non-bottom) abstract elements</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span><span class="keyword">val</span> empty : <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>returns an empty element</p></div></div><h2 id="variables-management"><a href="#variables-management" class="anchor"></a>Variables management</h2><div class="odoc-spec"><div class="spec value anchored" id="val-add_var"><a href="#val-add_var" class="anchor"></a><code><span><span class="keyword">val</span> add_var : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../../../Csp/index.html#type-decl">Csp.decl</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>adds an unconstrained variable to the environnement</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-rm_var"><a href="#val-rm_var" class="anchor"></a><code><span><span class="keyword">val</span> rm_var : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>removes a variable from the environnement</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-vars"><a href="#val-vars" class="anchor"></a><code><span><span class="keyword">val</span> vars : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="../../../../Csp/index.html#type-typ">Csp.typ</a> * string * <a href="../../../../Dom/index.html#type-t">Dom.t</a>)</span> list</span></span></code></div><div class="spec-doc"><p>returns the variables annoted by their type and their definition domain</p></div></div><h2 id="measure"><a href="#measure" class="anchor"></a>Measure</h2><div class="odoc-spec"><div class="spec value anchored" id="val-volume"><a href="#val-volume" class="anchor"></a><code><span><span class="keyword">val</span> volume : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> float</span></code></div><div class="spec-doc"><p>computes the volume of an abstract element</p></div></div><h2 id="set-theoretic-operations"><a href="#set-theoretic-operations" class="anchor"></a>Set-theoretic operations</h2><div class="odoc-spec"><div class="spec value anchored" id="val-join"><a href="#val-join" class="anchor"></a><code><span><span class="keyword">val</span> join : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a> * bool</span></code></div><div class="spec-doc"><p>Joins two abstract elements. The boolean flag indicates if the join was exact. It is always sound to return false</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-join_list"><a href="#val-join_list" class="anchor"></a><code><span><span class="keyword">val</span> join_list : <span><span><a href="#type-t">t</a> list</span> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a> * bool</span></code></div><div class="spec-doc"><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></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-meet"><a href="#val-meet" class="anchor"></a><code><span><span class="keyword">val</span> meet : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> option</span></span></code></div><div class="spec-doc"><p>meet two abstract elements</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-diff"><a href="#val-diff" class="anchor"></a><code><span><span class="keyword">val</span> diff : <span><span>(<span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> list</span>)</span> option</span></span></code></div><div class="spec-doc"><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></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-split_along"><a href="#val-split_along" class="anchor"></a><code><span><span class="keyword">val</span> split_along : <span><span class="optlabel">?prec</span>:float <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> list</span></span></code></div><div class="spec-doc"><p>splits an abstract element along the specified variable</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-split"><a href="#val-split" class="anchor"></a><code><span><span class="keyword">val</span> split : <span><span class="optlabel">?prec</span>:float <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> list</span></span></code></div><div class="spec-doc"><p>splits an abstract element according to an internal heuristic</p></div></div><h3 id="constraint-conversion"><a href="#constraint-conversion" class="anchor"></a>constraint conversion</h3><div class="odoc-spec"><div class="spec type anchored" id="type-internal_constr"><a href="#type-internal_constr" class="anchor"></a><code><span><span class="keyword">type</span> internal_constr</span></code></div><div class="spec-doc"><p>domain's internal representation of a comparison</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-internalize"><a href="#val-internalize" class="anchor"></a><code><span><span class="keyword">val</span> internalize : <span><span class="optlabel">?elem</span>:<a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../../../Constraint/index.html#type-comparison">Constraint.comparison</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-internal_constr">internal_constr</a></span></code></div><div class="spec-doc"><p>may use a current abstract element to simplify the constaint</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-externalize"><a href="#val-externalize" class="anchor"></a><code><span><span class="keyword">val</span> externalize : <span><a href="#type-internal_constr">internal_constr</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../../../Constraint/index.html#type-comparison">Constraint.comparison</a></span></code></div></div><h2 id="constraint-management"><a href="#constraint-management" class="anchor"></a>Constraint management</h2><div class="odoc-spec"><div class="spec value anchored" id="val-sat"><a href="#val-sat" class="anchor"></a><code><span><span class="keyword">val</span> sat : <span><a href="../../../../Instance/index.html#type-t">Instance.t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-internal_constr">internal_constr</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p>satisfaction test on the internal constraint representation</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-filter"><a href="#val-filter" class="anchor"></a><code><span><span class="keyword">val</span> filter : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-internal_constr">internal_constr</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <a href="../../../../Consistency/index.html#type-t">Consistency.t</a></span></span></code></div><div class="spec-doc"><p>filters an abstract element with respect to an arithmetic constraint, may raise bot found.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-filter_diff"><a href="#val-filter_diff" class="anchor"></a><code><span><span class="keyword">val</span> filter_diff : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-internal_constr">internal_constr</a> <span class="arrow">&#45;&gt;</span></span> <span><span>(<a href="#type-t">t</a> * <a href="../../../../Tools/VarSet/index.html#type-t">Tools.VarSet.t</a>)</span> <a href="../../../../Consistency/index.html#type-t">Consistency.t</a></span></span></code></div><div class="spec-doc"><p>same as filter but also return a set of variables that had their domains effectively reduced</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_representable"><a href="#val-is_representable" class="anchor"></a><code><span><span class="keyword">val</span> is_representable : <span><a href="#type-internal_constr">internal_constr</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../../../Kleene/index.html#type-t">Kleene.t</a></span></code></div><div class="spec-doc"><p>checks if a constraint is suited for this abstract domain</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-forward_eval"><a href="#val-forward_eval" class="anchor"></a><code><span><span class="keyword">val</span> forward_eval : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../../../Expr/index.html#type-t">Expr.t</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../../../Q/index.html#type-t">Q.t</a> * <a href="../../../../Q/index.html#type-t">Q.t</a></span></code></div><div class="spec-doc"><p>computes the range of value of a given expression within an abstract element</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-to_constraint"><a href="#val-to_constraint" class="anchor"></a><code><span><span class="keyword">val</span> to_constraint : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../../../Constraint/index.html#type-t">Constraint.t</a></span></code></div><div class="spec-doc"><p>transforms an abstract element into constraints</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-spawn"><a href="#val-spawn" class="anchor"></a><code><span><span class="keyword">val</span> spawn : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <a href="../../../../Csp/index.html#type-instance">Csp.instance</a></span></code></div><div class="spec-doc"><p>Random concretization function. useful to do tests, and to reuse the results. values are generated uniformly when possible</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_abstraction"><a href="#val-is_abstraction" class="anchor"></a><code><span><span class="keyword">val</span> is_abstraction : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../../../../Csp/index.html#type-instance">Csp.instance</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div><div class="spec-doc"><p>check if an abstract element is an abstraction of an instance</p></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><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p>printing</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-render"><a href="#val-render" class="anchor"></a><code><span><span class="keyword">val</span> render : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span class="xref-unresolved">Picasso</span>.Drawable.t</span></code></div><div class="spec-doc"><p>transforms an abstract element into a Picasso.Drawable.t for drawing</p></div></div></div></body></html>
