<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Constraint (libabsolute.Libabsolute__.Constraint)</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; Constraint</nav><h1>Module <code>Libabsolute__.Constraint</code></h1><nav class="toc"><ul><li><a href="#constructors">Constructors</a><ul><li><a href="#comparisons">Comparisons</a></li><li><a href="#boolean-formulae">Boolean formulae</a></li><li><a href="#utilities">Utilities</a></li></ul></li><li><a href="#operations">Operations</a></li><li><a href="#printing">Printing</a></li></ul></nav></header><aside><p>This module defines the constraint language, and some basic operations over it</p></aside><dl><dt class="spec type" id="type-cmpop"><a href="#type-cmpop" class="anchor"></a><code><span class="keyword">type</span> cmpop</code><code> = </code><table class="variant"><tr id="type-cmpop.EQ" class="anchored"><td class="def constructor"><a href="#type-cmpop.EQ" class="anchor"></a><code>| </code><code><span class="constructor">EQ</span></code></td></tr><tr id="type-cmpop.LEQ" class="anchored"><td class="def constructor"><a href="#type-cmpop.LEQ" class="anchor"></a><code>| </code><code><span class="constructor">LEQ</span></code></td></tr><tr id="type-cmpop.GEQ" class="anchored"><td class="def constructor"><a href="#type-cmpop.GEQ" class="anchor"></a><code>| </code><code><span class="constructor">GEQ</span></code></td></tr><tr id="type-cmpop.NEQ" class="anchored"><td class="def constructor"><a href="#type-cmpop.NEQ" class="anchor"></a><code>| </code><code><span class="constructor">NEQ</span></code></td></tr><tr id="type-cmpop.GT" class="anchored"><td class="def constructor"><a href="#type-cmpop.GT" class="anchor"></a><code>| </code><code><span class="constructor">GT</span></code></td></tr><tr id="type-cmpop.LT" class="anchored"><td class="def constructor"><a href="#type-cmpop.LT" class="anchor"></a><code>| </code><code><span class="constructor">LT</span></code></td></tr></table></dt><dd><p>arithmetic comparison operators</p></dd></dl><dl><dt class="spec type" id="type-comparison"><a href="#type-comparison" class="anchor"></a><code><span class="keyword">type</span> comparison</code><code> = <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> * <a href="index.html#type-cmpop">cmpop</a> * <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a></code></dt><dd><p>boolean comparison : e1 &lt;&gt; e2</p></dd></dl><dl><dt class="spec type" id="type-boolean"><a href="#type-boolean" class="anchor"></a><code><span class="keyword">type</span> <span>'a boolean</span></code><code> = </code><table class="variant"><tr id="type-boolean.Cmp" class="anchored"><td class="def constructor"><a href="#type-boolean.Cmp" class="anchor"></a><code>| </code><code><span class="constructor">Cmp</span> <span class="keyword">of</span> <span class="type-var">'a</span></code></td></tr><tr id="type-boolean.And" class="anchored"><td class="def constructor"><a href="#type-boolean.And" class="anchor"></a><code>| </code><code><span class="constructor">And</span> <span class="keyword">of</span> <span><span class="type-var">'a</span> <a href="index.html#type-boolean">boolean</a></span> * <span><span class="type-var">'a</span> <a href="index.html#type-boolean">boolean</a></span></code></td></tr><tr id="type-boolean.Or" class="anchored"><td class="def constructor"><a href="#type-boolean.Or" class="anchor"></a><code>| </code><code><span class="constructor">Or</span> <span class="keyword">of</span> <span><span class="type-var">'a</span> <a href="index.html#type-boolean">boolean</a></span> * <span><span class="type-var">'a</span> <a href="index.html#type-boolean">boolean</a></span></code></td></tr><tr id="type-boolean.Not" class="anchored"><td class="def constructor"><a href="#type-boolean.Not" class="anchor"></a><code>| </code><code><span class="constructor">Not</span> <span class="keyword">of</span> <span><span class="type-var">'a</span> <a href="index.html#type-boolean">boolean</a></span></code></td></tr></table></dt><dd><p>boolean expressions</p></dd></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <span><a href="index.html#type-comparison">comparison</a> <a href="index.html#type-boolean">boolean</a></span></code></dt><dd><p>type for constraints</p></dd></dl><section><header><h2 id="constructors"><a href="#constructors" class="anchor"></a>Constructors</h2></header><section><header><h3 id="comparisons"><a href="#comparisons" class="anchor"></a>Comparisons</h3></header><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 &lt;= e2</p></dd></dl><dl><dt class="spec value" id="val-lt"><a href="#val-lt" class="anchor"></a><code><span class="keyword">val</span> lt : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 &lt; e2</p></dd></dl><dl><dt class="spec value" id="val-geq"><a href="#val-geq" class="anchor"></a><code><span class="keyword">val</span> geq : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 &gt;= e2</p></dd></dl><dl><dt class="spec value" id="val-gt"><a href="#val-gt" class="anchor"></a><code><span class="keyword">val</span> gt : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 &gt; e2</p></dd></dl><dl><dt class="spec value" id="val-eq"><a href="#val-eq" class="anchor"></a><code><span class="keyword">val</span> eq : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 = e2</p></dd></dl><dl><dt class="spec value" id="val-neq"><a href="#val-neq" class="anchor"></a><code><span class="keyword">val</span> neq : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>e1 &lt;&gt; e2</p></dd></dl></section><section><header><h3 id="boolean-formulae"><a href="#boolean-formulae" class="anchor"></a>Boolean formulae</h3></header><dl><dt class="spec value" id="val-and_"><a href="#val-and_" class="anchor"></a><code><span class="keyword">val</span> and_ : <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></code></dt><dd><p>b1 &amp;&amp; b2</p></dd></dl><dl><dt class="spec value" id="val-or_"><a href="#val-or_" class="anchor"></a><code><span class="keyword">val</span> or_ : <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></code></dt><dd><p>b1 || b2</p></dd></dl><dl><dt class="spec value" id="val-imply"><a href="#val-imply" class="anchor"></a><code><span class="keyword">val</span> imply : <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></code></dt><dd><p>b1 =&gt; b2</p></dd></dl><dl><dt class="spec value" id="val-not_"><a href="#val-not_" class="anchor"></a><code><span class="keyword">val</span> not_ : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>not b</p></dd></dl></section><section><header><h3 id="utilities"><a href="#utilities" class="anchor"></a>Utilities</h3></header><dl><dt class="spec value" id="val-assign"><a href="#val-assign" class="anchor"></a><code><span class="keyword">val</span> assign : string <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>constraint for variable assignment by a constant</p></dd></dl><dl><dt class="spec value" id="val-inside"><a href="#val-inside" class="anchor"></a><code><span class="keyword">val</span> inside : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.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/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>constraint for 'e \in [low;high]'</p></dd></dl><dl><dt class="spec value" id="val-outside"><a href="#val-outside" class="anchor"></a><code><span class="keyword">val</span> outside : <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.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/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>constraint for 'e \notin [low;high]'</p></dd></dl><dl><dt class="spec value" id="val-inside_cst"><a href="#val-inside_cst" class="anchor"></a><code><span class="keyword">val</span> inside_cst : string <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>same as inside but with string and rationals instead of expressions'</p></dd></dl><dl><dt class="spec value" id="val-outside_cst"><a href="#val-outside_cst" class="anchor"></a><code><span class="keyword">val</span> outside_cst : string <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>same as outside but with string and rationals instead of expressions'</p></dd></dl><dl><dt class="spec value" id="val-of_instance"><a href="#val-of_instance" class="anchor"></a><code><span class="keyword">val</span> of_instance : <a href="../../Libabsolute/Instance/index.html#type-t">Libabsolute.Instance.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>conversion of a point <code>p</code> to a conjunctive constraint whose only solution is the point p.</p><dl><dt>raises [Invalid_arg]</dt><dd><p>if the instance is empty</p></dd></dl></dd></dl><dl><dt class="spec value" id="val-convex_hull"><a href="#val-convex_hull" class="anchor"></a><code><span class="keyword">val</span> convex_hull : <span><a href="../../Libabsolute/Instance/index.html#type-t">Libabsolute.Instance.t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Builds the conjuntive constraint defined by the linear system corresponding to the convex hull of the given set of points. The list of instance must not be empty and all the instances should be defined over the same set of keys, otherwise the behaviour in undefined.</p></dd></dl></section></section><section><header><h2 id="operations"><a href="#operations" class="anchor"></a>Operations</h2></header><dl><dt class="spec value" id="val-inv_cmp"><a href="#val-inv_cmp" class="anchor"></a><code><span class="keyword">val</span> inv_cmp : <a href="index.html#type-cmpop">cmpop</a> <span>&#45;&gt;</span> <a href="index.html#type-cmpop">cmpop</a></code></dt><dd><p>cmp operator inversion</p></dd></dl><dl><dt class="spec value" id="val-neg_cmp"><a href="#val-neg_cmp" class="anchor"></a><code><span class="keyword">val</span> neg_cmp : <a href="index.html#type-cmpop">cmpop</a> <span>&#45;&gt;</span> <a href="index.html#type-cmpop">cmpop</a></code></dt><dd><p>comparison operator negation</p></dd></dl><dl><dt class="spec value" id="val-cmp_to_fun"><a href="#val-cmp_to_fun" class="anchor"></a><code><span class="keyword">val</span> cmp_to_fun : <a href="index.html#type-cmpop">cmpop</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>returns the rational function corresponding to the cmp operator</p></dd></dl><dl><dt class="spec value" id="val-nullify_rhs"><a href="#val-nullify_rhs" class="anchor"></a><code><span class="keyword">val</span> nullify_rhs : <a href="index.html#type-comparison">comparison</a> <span>&#45;&gt;</span> <a href="index.html#type-comparison">comparison</a></code></dt><dd><p><code>nullify c</code> computes a comparison equivalent to <code>c</code>, with its right-hand-side being 0</p></dd></dl><dl><dt class="spec value" id="val-neg"><a href="#val-neg" class="anchor"></a><code><span class="keyword">val</span> neg : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>constraint negation</p></dd></dl><dl><dt class="spec value" id="val-remove_not"><a href="#val-remove_not" class="anchor"></a><code><span class="keyword">val</span> remove_not : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>rewrites a constraint into an equivalent constraint without the logical operator 'Not'</p></dd></dl><dl><dt class="spec value" id="val-collect_vars"><a href="#val-collect_vars" class="anchor"></a><code><span class="keyword">val</span> collect_vars : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span>int <a href="../../Libabsolute/Tools/VarMap/index.html#type-t">Libabsolute.Tools.VarMap.t</a></span></code></dt><dd><p>Returns all the variables appearing in a constraint as a map where to each variable is associated the (integer) number of occurences</p></dd></dl><dl><dt class="spec value" id="val-replace"><a href="#val-replace" class="anchor"></a><code><span class="keyword">val</span> replace : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string <span>&#45;&gt;</span> <a href="../../Libabsolute/Expr/index.html#type-t">Libabsolute.Expr.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p><code>replace constr var expr</code> builds a new constraint identical to <code>constr</code> where all the occurences of the variable <code>var</code> are replaced by the expression <code>expr</code></p></dd></dl><dl><dt class="spec value" id="val-fix_var"><a href="#val-fix_var" class="anchor"></a><code><span class="keyword">val</span> fix_var : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string <span>&#45;&gt;</span> <a href="../../Libabsolute/Q/index.html#type-t">Libabsolute.Q.t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p><code>fix_var constr var cst</code> builds a new constraint identical to <code>constr</code> where all the occurences of the variable <code>var</code> are replaced by the constant <code>cst</code></p></dd></dl><dl><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../Libabsolute/Instance/index.html#type-t">Libabsolute.Instance.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Evaluates the constraint a the given point.</p><dl><dt>raises [Invalid_arg]</dt><dd><p>if a division by zero occurs or if an exponentitation by a non integer exposant is made.</p></dd></dl></dd></dl></section><section><header><h2 id="printing"><a href="#printing" class="anchor"></a>Printing</h2></header><dl><dt class="spec value" id="val-pp_cmpop"><a href="#val-pp_cmpop" class="anchor"></a><code><span class="keyword">val</span> pp_cmpop : Stdlib.Format.formatter <span>&#45;&gt;</span> <a href="index.html#type-cmpop">cmpop</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>comparison operator printer</p></dd></dl><dl><dt class="spec value" id="val-pp_comparison"><a href="#val-pp_comparison" class="anchor"></a><code><span class="keyword">val</span> pp_comparison : Stdlib.Format.formatter <span>&#45;&gt;</span> <a href="index.html#type-comparison">comparison</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>comparison printer</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>printer</p></dd></dl><dl><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt><dd><p>Conversion to a string</p></dd></dl></section></div></body></html>