/usr/share/doc/libapron-ocaml-dev/html/Abstract1.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link rel="previous" href="Tcons1.html">
<link rel="next" href="Parser.html">
<link rel="Up" href="index.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Introduction" rel="Chapter" href="Introduction.html">
<link title="Scalar" rel="Chapter" href="Scalar.html">
<link title="Interval" rel="Chapter" href="Interval.html">
<link title="Coeff" rel="Chapter" href="Coeff.html">
<link title="Dim" rel="Chapter" href="Dim.html">
<link title="Linexpr0" rel="Chapter" href="Linexpr0.html">
<link title="Lincons0" rel="Chapter" href="Lincons0.html">
<link title="Generator0" rel="Chapter" href="Generator0.html">
<link title="Texpr0" rel="Chapter" href="Texpr0.html">
<link title="Tcons0" rel="Chapter" href="Tcons0.html">
<link title="Manager" rel="Chapter" href="Manager.html">
<link title="Abstract0" rel="Chapter" href="Abstract0.html">
<link title="Var" rel="Chapter" href="Var.html">
<link title="Environment" rel="Chapter" href="Environment.html">
<link title="Linexpr1" rel="Chapter" href="Linexpr1.html">
<link title="Lincons1" rel="Chapter" href="Lincons1.html">
<link title="Generator1" rel="Chapter" href="Generator1.html">
<link title="Texpr1" rel="Chapter" href="Texpr1.html">
<link title="Tcons1" rel="Chapter" href="Tcons1.html">
<link title="Abstract1" rel="Chapter" href="Abstract1.html">
<link title="Parser" rel="Chapter" href="Parser.html">
<link title="Box" rel="Chapter" href="Box.html">
<link title="Oct" rel="Chapter" href="Oct.html">
<link title="Polka" rel="Chapter" href="Polka.html">
<link title="Ppl" rel="Chapter" href="Ppl.html">
<link title="PolkaGrid" rel="Chapter" href="PolkaGrid.html">
<link title="Mpz" rel="Chapter" href="Mpz.html">
<link title="Mpq" rel="Chapter" href="Mpq.html">
<link title="Gmp_random" rel="Chapter" href="Gmp_random.html">
<link title="Mpf" rel="Chapter" href="Mpf.html">
<link title="Mpfr" rel="Chapter" href="Mpfr.html">
<link title="Mpzf" rel="Chapter" href="Mpzf.html">
<link title="Mpqf" rel="Chapter" href="Mpqf.html">
<link title="Mpfrf" rel="Chapter" href="Mpfrf.html"><link title="General management" rel="Section" href="#2_Generalmanagement">
<link title="Constructor, accessors, tests and property extraction" rel="Section" href="#2_Constructoraccessorstestsandpropertyextraction">
<link title="Operations" rel="Section" href="#2_Operations">
<link title="Additional operations" rel="Section" href="#2_Additionaloperations">
<link title="Memory" rel="Subsection" href="#3_Memory">
<link title="Control of internal representation" rel="Subsection" href="#3_Controlofinternalrepresentation">
<link title="Printing" rel="Subsection" href="#3_Printing">
<link title="Serialization" rel="Subsection" href="#3_Serialization">
<link title="Basic constructors" rel="Subsection" href="#3_Basicconstructors">
<link title="Accessors" rel="Subsection" href="#3_Accessors">
<link title="Tests" rel="Subsection" href="#3_Tests">
<link title="Extraction of properties" rel="Subsection" href="#3_Extractionofproperties">
<link title="Meet and Join" rel="Subsection" href="#3_MeetandJoin">
<link title="Assignement and Substitutions" rel="Subsection" href="#3_AssignementandSubstitutions">
<link title="Projections" rel="Subsection" href="#3_Projections">
<link title="Change and permutation of dimensions" rel="Subsection" href="#3_Changeandpermutationofdimensions">
<link title="Expansion and folding of dimensions" rel="Subsection" href="#3_Expansionandfoldingofdimensions">
<link title="Widening" rel="Subsection" href="#3_Widening">
<link title="Closure operation" rel="Subsection" href="#3_Closureoperation">
<title>Abstract1</title>
</head>
<body>
<div class="navbar"><a class="pre" href="Tcons1.html" title="Tcons1">Previous</a>
&nbsp;<a class="up" href="index.html" title="Index">Up</a>
&nbsp;<a class="post" href="Parser.html" title="Parser">Next</a>
</div>
<h1>Module <a href="type_Abstract1.html">Abstract1</a></h1>

<pre><span class="keyword">module</span> Abstract1: <code class="code"><span class="keyword">sig</span></code> <a href="Abstract1.html">..</a> <code class="code"><span class="keyword">end</span></code></pre><div class="info module top">
APRON Abstract values of level 1<br>
</div>
<hr width="100%">

<pre><code><span id="TYPEt"><span class="keyword">type</span> <code class="type">'a</code> t</span> = {</code></pre><table class="typetable">
<tr>
<td align="left" valign="top" >
<code>&nbsp;&nbsp;</code></td>
<td align="left" valign="top" >
<code><span class="keyword">mutable&nbsp;</span><span id="TYPEELTt.abstract0">abstract0</span>&nbsp;: <code class="type">'a <a href="Abstract0.html#TYPEt">Abstract0.t</a></code>;</code></td>

</tr>
<tr>
<td align="left" valign="top" >
<code>&nbsp;&nbsp;</code></td>
<td align="left" valign="top" >
<code><span class="keyword">mutable&nbsp;</span><span id="TYPEELTt.env">env</span>&nbsp;: <code class="type"><a href="Environment.html#TYPEt">Environment.t</a></code>;</code></td>

</tr></table>
}


<br>
APRON Abstract values of level 1<br>
<br>
The type parameter <code class="code"><span class="keywordsign">'</span>a</code> allows to distinguish abstract values with different underlying abstract domains.<br>

<pre><code><span id="TYPEbox1"><span class="keyword">type</span> <code class="type"></code>box1</span> = {</code></pre><table class="typetable">
<tr>
<td align="left" valign="top" >
<code>&nbsp;&nbsp;</code></td>
<td align="left" valign="top" >
<code><span class="keyword">mutable&nbsp;</span><span id="TYPEELTbox1.interval_array">interval_array</span>&nbsp;: <code class="type"><a href="Interval.html#TYPEt">Interval.t</a> array</code>;</code></td>

</tr>
<tr>
<td align="left" valign="top" >
<code>&nbsp;&nbsp;</code></td>
<td align="left" valign="top" >
<code><span class="keyword">mutable&nbsp;</span><span id="TYPEELTbox1.box1_env">box1_env</span>&nbsp;: <code class="type"><a href="Environment.html#TYPEt">Environment.t</a></code>;</code></td>

</tr></table>
}


<br>
<h2 id="2_Generalmanagement">General management</h2><br>
<br>
<h3 id="3_Memory">Memory</h3><br>

<pre><span id="VALcopy"><span class="keyword">val</span> copy</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Copy a value<br>
</div>

<pre><span id="VALsize"><span class="keyword">val</span> size</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> int</code></pre><div class="info ">
Return the abstract size of a value<br>
</div>
<br>
<h3 id="3_Controlofinternalrepresentation">Control of internal representation</h3><br>

<pre><span id="VALminimize"><span class="keyword">val</span> minimize</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Minimize the size of the representation of the value. This may result in a later recomputation of internal information.<br>
</div>

<pre><span id="VALcanonicalize"><span class="keyword">val</span> canonicalize</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Put the abstract value in canonical form. (not yet clear definition)<br>
</div>

<pre><span id="VALhash"><span class="keyword">val</span> hash</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> int</code></pre>
<pre><span id="VALapproximate"><span class="keyword">val</span> approximate</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> int -> unit</code></pre><div class="info ">
<code class="code">approximate man abs alg</code> perform some transformation on the abstract value, guided by the argument <code class="code">alg</code>. The transformation may lose information.  The argument <code class="code">alg</code> overrides the field algorithm of the structure of type <code class="code"><span class="constructor">Manager</span>.funopt</code> associated to ap_abstract0_approximate (commodity feature).<br>
</div>
<br>
<h3 id="3_Printing">Printing</h3><br>

<pre><span id="VALfdump"><span class="keyword">val</span> fdump</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Dump on the <code class="code">stdout</code> C stream the internal representation of an abstract value, for debugging purposes<br>
</div>

<pre><span id="VALprint"><span class="keyword">val</span> print</span> : <code class="type">Format.formatter -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Print as a set of constraints<br>
</div>
<br>
<h3 id="3_Serialization">Serialization</h3><br>
<br>
<h2 id="2_Constructoraccessorstestsandpropertyextraction">Constructor, accessors, tests and property extraction</h2><br>
<br>
<h3 id="3_Basicconstructors">Basic constructors</h3><br>
<br>
All these functions request explicitly an environment in their arguments.<br>

<pre><span id="VALbottom"><span class="keyword">val</span> bottom</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Create a bottom (empty) value defined on the given environment<br>
</div>

<pre><span id="VALtop"><span class="keyword">val</span> top</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Create a top (universe) value defined on the given environment<br>
</div>

<pre><span id="VALof_box"><span class="keyword">val</span> of_box</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       <a href="Environment.html#TYPEt">Environment.t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Interval.html#TYPEt">Interval.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Abstract an hypercube.
<p>

<code class="code">of_box man env tvar tinterval</code> abstracts an hypercube defined by the arrays <code class="code">tvar</code> and <code class="code">tinterval</code>. The result is defined on the environment <code class="code">env</code>, which should contain all the variables in <code class="code">tvar</code> (and defines their type)<br>
</div>
<br>
<h3 id="3_Accessors">Accessors</h3><br>

<pre><span id="VALmanager"><span class="keyword">val</span> manager</span> : <code class="type">'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Manager.html#TYPEt">Manager.t</a></code></pre>
<pre><span id="VALenv"><span class="keyword">val</span> env</span> : <code class="type">'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Environment.html#TYPEt">Environment.t</a></code></pre>
<pre><span id="VALabstract0"><span class="keyword">val</span> abstract0</span> : <code class="type">'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract0.html#TYPEt">Abstract0.t</a></code></pre><div class="info ">
Return resp. the underlying manager, environment and abstract value of level 0<br>
</div>
<br>
<h3 id="3_Tests">Tests</h3><br>

<pre><span id="VALis_bottom"><span class="keyword">val</span> is_bottom</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> bool</code></pre><div class="info ">
Emptiness test<br>
</div>

<pre><span id="VALis_top"><span class="keyword">val</span> is_top</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> bool</code></pre><div class="info ">
Universality test<br>
</div>

<pre><span id="VALis_leq"><span class="keyword">val</span> is_leq</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> bool</code></pre><div class="info ">
Inclusion test. The 2 abstract values should be compatible.<br>
</div>

<pre><span id="VALis_eq"><span class="keyword">val</span> is_eq</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> bool</code></pre><div class="info ">
Equality test. The 2 abstract values should be compatible.<br>
</div>

<pre><span id="VALsat_lincons"><span class="keyword">val</span> sat_lincons</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Lincons1.html#TYPEt">Lincons1.t</a> -> bool</code></pre><div class="info ">
Does the abstract value satisfy the linear constraint ?<br>
</div>

<pre><span id="VALsat_tcons"><span class="keyword">val</span> sat_tcons</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Tcons1.html#TYPEt">Tcons1.t</a> -> bool</code></pre><div class="info ">
Does the abstract value satisfy the tree expression constraint ?<br>
</div>

<pre><span id="VALsat_interval"><span class="keyword">val</span> sat_interval</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Interval.html#TYPEt">Interval.t</a> -> bool</code></pre><div class="info ">
Does the abstract value satisfy the constraint <code class="code">dim <span class="keyword">in</span> interval</code> ?<br>
</div>

<pre><span id="VALis_variable_unconstrained"><span class="keyword">val</span> is_variable_unconstrained</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> bool</code></pre><div class="info ">
Is the variable unconstrained in the abstract value ? If yes, this means that the existential quantification of the dimension does not change the value.<br>
</div>
<br>
<h3 id="3_Extractionofproperties">Extraction of properties</h3><br>

<pre><span id="VALbound_variable"><span class="keyword">val</span> bound_variable</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Interval.html#TYPEt">Interval.t</a></code></pre><div class="info ">
Return the interval of variation of the variable in the abstract value.<br>
</div>

<pre><span id="VALbound_linexpr"><span class="keyword">val</span> bound_linexpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> -> <a href="Interval.html#TYPEt">Interval.t</a></code></pre><div class="info ">
Return the interval of variation of the linear expression in the abstract value. 
<p>

Implement a form of linear programming, where the argument linear expression is the one to optimize under the constraints induced by the abstract value.<br>
</div>

<pre><span id="VALbound_texpr"><span class="keyword">val</span> bound_texpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> -> <a href="Interval.html#TYPEt">Interval.t</a></code></pre><div class="info ">
Return the interval of variation of the tree expression in the abstract value.<br>
</div>

<pre><span id="VALto_box"><span class="keyword">val</span> to_box</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Abstract1.html#TYPEbox1">box1</a></code></pre><div class="info ">
Convert the abstract value to an hypercube<br>
</div>

<pre><span id="VALto_lincons_array"><span class="keyword">val</span> to_lincons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Lincons1.html#TYPEearray">Lincons1.earray</a></code></pre><div class="info ">
Convert the abstract value to a conjunction of linear constraints.
<p>
Convert the abstract value to a conjunction of tree expressions constraints.<br>
</div>

<pre><span id="VALto_tcons_array"><span class="keyword">val</span> to_tcons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Tcons1.html#TYPEearray">Tcons1.earray</a></code></pre>
<pre><span id="VALto_generator_array"><span class="keyword">val</span> to_generator_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Generator1.html#TYPEearray">Generator1.earray</a></code></pre><div class="info ">
Convert the abstract value to a set of generators that defines it.<br>
</div>
<br>
<h2 id="2_Operations">Operations</h2><br>
<br>
<h3 id="3_MeetandJoin">Meet and Join</h3><br>

<pre><span id="VALmeet"><span class="keyword">val</span> meet</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Meet of 2 abstract values.<br>
</div>

<pre><span id="VALmeet_array"><span class="keyword">val</span> meet_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Meet of a non empty array of abstract values.<br>
</div>

<pre><span id="VALmeet_lincons_array"><span class="keyword">val</span> meet_lincons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Lincons1.html#TYPEearray">Lincons1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Meet of an abstract value with an array of linear constraints.<br>
</div>

<pre><span id="VALmeet_tcons_array"><span class="keyword">val</span> meet_tcons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Tcons1.html#TYPEearray">Tcons1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Meet of an abstract value with an array of tree expressions constraints.<br>
</div>

<pre><span id="VALjoin"><span class="keyword">val</span> join</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Join of 2 abstract values.<br>
</div>

<pre><span id="VALjoin_array"><span class="keyword">val</span> join_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Join of a non empty array of abstract values.<br>
</div>

<pre><span id="VALadd_ray_array"><span class="keyword">val</span> add_ray_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Generator1.html#TYPEearray">Generator1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Add the array of generators to the abstract value (time elapse operator).
<p>

 The generators should either lines or rays, not vertices.<br>
</div>
<br>
<h5 id="5_Sideeffectversionsofthepreviousfunctions">Side-effect versions of the previous functions</h5><br>

<pre><span id="VALmeet_with"><span class="keyword">val</span> meet_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre>
<pre><span id="VALmeet_lincons_array_with"><span class="keyword">val</span> meet_lincons_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Lincons1.html#TYPEearray">Lincons1.earray</a> -> unit</code></pre>
<pre><span id="VALmeet_tcons_array_with"><span class="keyword">val</span> meet_tcons_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Tcons1.html#TYPEearray">Tcons1.earray</a> -> unit</code></pre>
<pre><span id="VALjoin_with"><span class="keyword">val</span> join_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre>
<pre><span id="VALadd_ray_array_with"><span class="keyword">val</span> add_ray_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Generator1.html#TYPEearray">Generator1.earray</a> -> unit</code></pre><br>
<h3 id="3_AssignementandSubstitutions">Assignement and Substitutions</h3><br>

<pre><span id="VALassign_linexpr_array"><span class="keyword">val</span> assign_linexpr_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Parallel assignement of an array of dimensions by an array of same size of linear expressions<br>
</div>

<pre><span id="VALsubstitute_linexpr_array"><span class="keyword">val</span> substitute_linexpr_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Parallel substitution of an array of dimensions by an array of same size of linear expressions<br>
</div>

<pre><span id="VALassign_texpr_array"><span class="keyword">val</span> assign_texpr_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Parallel assignement of an array of dimensions by an array of same size of tree expressions<br>
</div>

<pre><span id="VALsubstitute_texpr_array"><span class="keyword">val</span> substitute_texpr_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Parallel substitution of an array of dimensions by an array of same size of tree expressions<br>
</div>
<br>
<h5 id="5_Sideeffectversionsofthepreviousfunctions">Side-effect versions of the previous functions</h5><br>

<pre><span id="VALassign_linexpr_array_with"><span class="keyword">val</span> assign_linexpr_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALsubstitute_linexpr_array_with"><span class="keyword">val</span> substitute_linexpr_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALassign_texpr_array_with"><span class="keyword">val</span> assign_texpr_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALsubstitute_texpr_array_with"><span class="keyword">val</span> substitute_texpr_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre><br>
<h3 id="3_Projections">Projections</h3><br>
<br>
These functions implements forgeting (existential quantification) of (array of) variables. Both functional and side-effect versions are provided. The Boolean, if true, adds a projection onto 0-plane.<br>

<pre><span id="VALforget_array"><span class="keyword">val</span> forget_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> bool -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre>
<pre><span id="VALforget_array_with"><span class="keyword">val</span> forget_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> bool -> unit</code></pre><br>
<h3 id="3_Changeandpermutationofdimensions">Change and permutation of dimensions</h3><br>

<pre><span id="VALchange_environment"><span class="keyword">val</span> change_environment</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> bool -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Change the environement of the abstract values.
<p>

Variables that are removed are first existentially quantified, and variables that are introduced are unconstrained. The Boolean, if true, adds a projection onto 0-plane for these ones.<br>
</div>

<pre><span id="VALminimize_environment"><span class="keyword">val</span> minimize_environment</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Remove from the environment of the abstract value and from the abstract value itself variables that are unconstrained in it.<br>
</div>

<pre><span id="VALrename_array"><span class="keyword">val</span> rename_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Var.html#TYPEt">Var.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Parallel renaming of the environment of the abstract value.
<p>

The new variables should not interfere with the variables that are not renamed.<br>
</div>

<pre><span id="VALchange_environment_with"><span class="keyword">val</span> change_environment_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> bool -> unit</code></pre>
<pre><span id="VALminimize_environment_with"><span class="keyword">val</span> minimize_environment_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre>
<pre><span id="VALrename_array_with"><span class="keyword">val</span> rename_array_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> <a href="Var.html#TYPEt">Var.t</a> array -> unit</code></pre><br>
<h3 id="3_Expansionandfoldingofdimensions">Expansion and folding of dimensions</h3><br>
<br>
These functions allows to expand one dimension into several ones having the
same properties with respect to the other dimensions, and to fold several
dimensions into one. Formally,
<p>
<ul>
<li>expand P(x,y,z) z w = P(x,y,z) inter P(x,y,w) if z is expanded in z and w</li>
<li>fold Q(x,y,z,w) z w = exists w:Q(x,y,z,w) union (exist z:Q(x,y,z,w))(z&lt;-w)
if z and w are folded onto z</li>
</ul>
<br>

<pre><span id="VALexpand"><span class="keyword">val</span> expand</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Expansion: <code class="code">expand a var tvar</code> expands the variable <code class="code">var</code> into itself and
	the additional variables in <code class="code">tvar</code>, which are given the same type as <code class="code">var</code>.
<p>

It results in (n+1) unrelated variables having
			same relations with other variables. The additional variables are added to the environment of 
the argument for making the environment of the result, so they should
not belong to the initial environement.<br>
</div>

<pre><span id="VALfold"><span class="keyword">val</span> fold</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Folding: <code class="code">fold a tvar</code> fold the variables in the array <code class="code">tvar</code> of size n&gt;=1
and put the result in the first variable of the array. The other
variables of the array are then removed, both from the environment and the abstract value.<br>
</div>

<pre><span id="VALexpand_with"><span class="keyword">val</span> expand_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> unit</code></pre>
<pre><span id="VALfold_with"><span class="keyword">val</span> fold_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> array -> unit</code></pre><br>
<h3 id="3_Widening">Widening</h3><br>

<pre><span id="VALwidening"><span class="keyword">val</span> widening</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Widening<br>
</div>

<pre><span id="VALwidening_threshold"><span class="keyword">val</span> widening_threshold</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Lincons1.html#TYPEearray">Lincons1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><br>
<h3 id="3_Closureoperation">Closure operation</h3><br>

<pre><span id="VALclosure"><span class="keyword">val</span> closure</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Closure: transform strict constraints into non-strict ones.<br>
</div>

<pre><span id="VALclosure_with"><span class="keyword">val</span> closure_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Side-effect version<br>
</div>
<br>
<h2 id="2_Additionaloperations">Additional operations</h2><br>

<pre><span id="VALof_lincons_array"><span class="keyword">val</span> of_lincons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> <a href="Lincons1.html#TYPEearray">Lincons1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre>
<pre><span id="VALof_tcons_array"><span class="keyword">val</span> of_tcons_array</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> <a href="Environment.html#TYPEt">Environment.t</a> -> <a href="Tcons1.html#TYPEearray">Tcons1.earray</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Abstract a conjunction of constraints<br>
</div>

<pre><span id="VALassign_linexpr"><span class="keyword">val</span> assign_linexpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre>
<pre><span id="VALsubstitute_linexpr"><span class="keyword">val</span> substitute_linexpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre>
<pre><span id="VALassign_texpr"><span class="keyword">val</span> assign_texpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre>
<pre><span id="VALsubstitute_texpr"><span class="keyword">val</span> substitute_texpr</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -><br>       <a href="Var.html#TYPEt">Var.t</a> -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Assignement/Substitution of a single dimension by a single expression<br>
</div>

<pre><span id="VALassign_linexpr_with"><span class="keyword">val</span> assign_linexpr_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALsubstitute_linexpr_with"><span class="keyword">val</span> substitute_linexpr_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Linexpr1.html#TYPEt">Linexpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALassign_texpr_with"><span class="keyword">val</span> assign_texpr_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre>
<pre><span id="VALsubstitute_texpr_with"><span class="keyword">val</span> substitute_texpr_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -><br>       'a <a href="Abstract1.html#TYPEt">t</a> -> <a href="Var.html#TYPEt">Var.t</a> -> <a href="Texpr1.html#TYPEt">Texpr1.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> option -> unit</code></pre><div class="info ">
Side-effect version of the previous functions<br>
</div>

<pre><span id="VALunify"><span class="keyword">val</span> unify</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a></code></pre><div class="info ">
Unification of 2 abstract values on their least common environment<br>
</div>

<pre><span id="VALunify_with"><span class="keyword">val</span> unify_with</span> : <code class="type">'a <a href="Manager.html#TYPEt">Manager.t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> 'a <a href="Abstract1.html#TYPEt">t</a> -> unit</code></pre><div class="info ">
Side-effect version<br>
</div>
</body></html>
libapron-ocaml-dev 0.9.10-6 / usr / share / doc / libapron-ocaml-dev / html / Abstract1.html
