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