<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<link rel="Start" href="index.html">
<link rel="previous" href="Data.html">
<link rel="next" href="Var.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="Index of module types" rel=Appendix href="index_module_types.html">
<link title="Domain" rel="Chapter" href="Domain.html">
<link title="SetDomain" rel="Chapter" href="SetDomain.html">
<link title="Stak" rel="Chapter" href="Stak.html">
<link title="Data" rel="Chapter" href="Data.html">
<link title="Cstr" rel="Chapter" href="Cstr.html">
<link title="Var" rel="Chapter" href="Var.html">
<link title="Invariant" rel="Chapter" href="Invariant.html">
<link title="Reify" rel="Chapter" href="Reify.html">
<link title="Arith" rel="Chapter" href="Arith.html">
<link title="Conjunto" rel="Chapter" href="Conjunto.html">
<link title="Goals" rel="Chapter" href="Goals.html">
<link title="FdArray" rel="Chapter" href="FdArray.html">
<link title="Gcc" rel="Chapter" href="Gcc.html">
<link title="Alldiff" rel="Chapter" href="Alldiff.html">
<link title="Sorting" rel="Chapter" href="Sorting.html">
<link title="Interval" rel="Chapter" href="Interval.html"><title>Cstr</title>
</head>
<body>
<div class="navbar"><a href="Data.html">Previous</a>
<a href="index.html">Up</a>
<a href="Var.html">Next</a>
</div>
<center><h1>Module <a href="type_Cstr.html">Cstr</a></h1></center>
<br>
<pre><span class="keyword">module</span> Cstr: <code class="code">sig</code> <a href="Cstr.html">..</a> <code class="code">end</code></pre>Posting Constraints and Building New Ones<br>
<hr width="100%">
<br>
<br>
<br>
This module defines the type <code class="code">t</code> of constraints and functions to create
and post constraints: mainly a <code class="code">create</code> function which allows to build new
constraints from scratch (this function is not needed when using
standard FaCiLe predefined constraints) and the mostly useful <code class="code">post</code>
function which must be called to actually add a constraint to the
constraint store.<br>
<br>
<br>
<pre><span class="keyword">exception</span> <a name="EXCEPTIONDontKnow"></a>DontKnow</pre>
<div class="info">
Exception raised by the <code class="code">check</code> function of a reified constraint when it
is not known whether the constraint is satisfied or violated.<br>
</div>
<pre><span class="keyword">type</span> <a name="TYPEpriority"></a><code class="type"></code>priority </pre>
<div class="info">
Type of waking priority.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALimmediate"></a>immediate : <code class="type"><a href="Cstr.html#TYPEpriority">priority</a></code></pre><pre><span class="keyword">val</span> <a name="VALnormal"></a>normal : <code class="type"><a href="Cstr.html#TYPEpriority">priority</a></code></pre><pre><span class="keyword">val</span> <a name="VALlater"></a>later : <code class="type"><a href="Cstr.html#TYPEpriority">priority</a></code></pre><div class="info">
Available priorities:<ul>
<li>immediate: as soon as possible, for quick updates;</li>
<li>normal: standard priority;</li>
<li>later: for time consuming constraints (e.g. <code class="code">Gcc.cstr</code>, <code class="code">Alldiff.cstr</code>...).</li>
</ul>
<br>
</div>
<pre><span class="keyword">type</span> <a name="TYPEt"></a><code class="type"></code>t </pre>
<div class="info">
The type of constraints.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALcreate"></a>create : <code class="type">?name:string -><br> ?nb_wakings:int -><br> ?fprint:(Pervasives.out_channel -> unit) -><br> ?priority:<a href="Cstr.html#TYPEpriority">priority</a> -><br> ?init:(unit -> unit) -><br> ?check:(unit -> bool) -><br> ?not:(unit -> <a href="Cstr.html#TYPEt">t</a>) -> (int -> bool) -> (<a href="Cstr.html#TYPEt">t</a> -> unit) -> <a href="Cstr.html#TYPEt">t</a></code></pre><div class="info">
<code class="code">create ?name ?nb_wakings ?fprint ?priority ?init ?check ?not update delay</code>
builds a new constraint:<ul>
<li> <code class="code">name</code> is a describing string for the constraint. Default value
is <code class="code">"anonymous"</code>.</li>
<li> <code class="code">nb_wakings</code> is the number of calls to <code class="code">Var.delay</code> with distinct
"<code class="code">waking_id</code>" arguments within the
constraint own <code class="code">delay</code> function (see below). Default value is <code class="code">1</code>.
Beware that if <code class="code">nb_wakings</code> is greater than 1 and the optional <code class="code">init</code>
argument is not provided, <code class="code">init</code> default behaviour is to do nothing
(i.e. the <code class="code">update</code> function will not be called).</li>
<li> <code class="code">fprint</code> should print the constraint on an output channel taken as
its only argument. Default value is to print the <code class="code">name</code> string.</li>
<li> <code class="code">priority</code> is either <code class="code">immediate</code>, <code class="code">normal</code> or <code class="code">later</code>. Time costly
constraints should be waken after quick ones. Default value is <code class="code">normal</code>.</li>
<li> <code class="code">init</code> is useful to perform initialization of auxiliary data
structures needed and maintained by the <code class="code">update</code> function.
<code class="code">init ()</code> is called as soon as the constraint is posted. Default
value is to call <code class="code">(update 0)</code> if <code class="code">nb_wakings</code> is equal to 1 to
perform an initial propagation; if <code class="code">nb_wakings</code> is greater than 1,
default value is <code class="code">fun () -> ()</code>, i.e. it does nothing. Hence, an
<code class="code">init</code> argument must be provided if this is not the desired
behaviour.</li>
<li> <code class="code">check</code> must be specified if the constraint is to be reifiable
(as well as the <code class="code">not</code> function). When the constraint is reified,
<code class="code">check ()</code> is called to verify whether the constraint is satisfied
or violated, i.e. the constraint itself or its negation is entailed
by the constraint store. It should return <code class="code">true</code> if the constraint
is satisfied, <code class="code">false</code> if it is violated and raise <code class="code">DontKnow</code> when
it is not known. <code class="code">check</code> <b>must not</b> change the domains of the
variables involved in the constraint.
Default: <code class="code">Failure</code> exception is raised.</li>
<li> <code class="code">not</code> must be specified if the constraint is reifiable (as well
as <code class="code">check</code>). <code class="code">not ()</code> should return a constraint which is the
negation of the constraint being defined. When the constraint is
reified, it is called to post the negation of the constraint whenever
<code class="code">check ()</code> return <code class="code">false</code>, i.e. the negation is entailed by the
constraint store. Default: <code class="code">Failure</code> exception is raised.</li>
<li> <code class="code">update</code> is a mandatory argument which propagates the constraint,
i.e. filters domains and checks consistency. This function takes an
integer as its unique parameter, according to the optional
<code class="code">waking_id</code> argument given to the <code class="code">Var.delay</code> calls featured in the
constraint own <code class="code">delay</code> function (see below). When a waking event
occurs, this function is called with the corresponding integer
"<code class="code">waking_id</code>", and must return <code class="code">true</code> when the constraint is
(partially) satisfied <em>for this event</em>, <code class="code">false</code> if further
propagations have to be performed, and raise <code class="code">Stak.Fail</code>
whenever an inconsistency is detected. The whole
constraint is solved when <code class="code">update 0</code>, ..., <code class="code">update (nb_wakings-1)</code>
have all returned <code class="code">true</code>. E.g. a global constraint on an array
of variables can be aware of which variable has triggered the
awakening by providing the integer index of the variable as its
"<code class="code">waking_id</code>" to the <code class="code">Var.delay</code> function. <code class="code">update</code> is called with
<code class="code">0</code> by default when the <code class="code">nb_wakings</code> argument has been omitted; in
this case, the constraint is solved as soon as <code class="code">update</code> returns <code class="code">true</code>.</li>
<li> <code class="code">delay</code> schedules the awakening of the constraint <code class="code">ct</code> (which is
taken as its unique argument), i.e. the execution of its <code class="code">update</code>
function. If <code class="code">update id</code> should be called (because it may propagates)
when one of the events contained in the events
list <code class="code">es</code> occurred
on variable <code class="code">v</code>, then <code class="code">Var.delay es v ~waking_id:id ct</code> should be called
within the body of the <code class="code">delay</code> function. Beware that
<b>all the "<code class="code">waking_id</code>s" must be contiguous integers ranging from</b>
<code class="code">0</code> <b>to</b> <code class="code">nb_wakings-1</code>, otherwise the behaviour is unspecified.
<code class="code">delay</code> is a mandatory argument.</li>
</ul>
<br>
</div>
<pre><span class="keyword">val</span> <a name="VALpost"></a>post : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> unit</code></pre><div class="info">
<code class="code">post c</code> posts the constraint <code class="code">c</code> to the constraint store.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALone"></a>one : <code class="type"><a href="Cstr.html#TYPEt">t</a></code></pre><pre><span class="keyword">val</span> <a name="VALzero"></a>zero : <code class="type"><a href="Cstr.html#TYPEt">t</a></code></pre><div class="info">
The constraint which succeeds (resp. fails) immediately.<br>
</div>
<br>
<br>
<pre><span class="keyword">val</span> <a name="VALid"></a>id : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> int</code></pre><div class="info">
<code class="code">id c</code> returns a unique integer identifying the constraint <code class="code">c</code>.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALname"></a>name : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> string</code></pre><div class="info">
<code class="code">name c</code> returns the name of the constraint <code class="code">c</code>.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALpriority"></a>priority : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> <a href="Cstr.html#TYPEpriority">priority</a></code></pre><div class="info">
<code class="code">priority c</code> returns the priority of the constraint <code class="code">c</code>.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALfprint"></a>fprint : <code class="type">Pervasives.out_channel -> <a href="Cstr.html#TYPEt">t</a> -> unit</code></pre><div class="info">
<code class="code">fprint chan c</code> prints the constraint <code class="code">c</code> on channel <code class="code">chan</code>. Calls
the <code class="code">fprint</code> function passed to <code class="code">create</code>.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALis_solved"></a>is_solved : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> bool</code></pre><div class="info">
<code class="code">is_solved c</code> returns <code class="code">true</code> if <code class="code">c</code> is satisfied and <code class="code">false</code> otherwise.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALactive_store"></a>active_store : <code class="type">unit -> <a href="Cstr.html#TYPEt">t</a> list</code></pre><div class="info">
<code class="code">active_store ()</code> returns the list of all active constraints, i.e. whose
<code class="code">update</code> functions have returned <code class="code">false</code>.<br>
</div>
<pre><span class="keyword">val</span> <a name="VALnot"></a>not : <code class="type"><a href="Cstr.html#TYPEt">t</a> -> <a href="Cstr.html#TYPEt">t</a></code></pre><div class="info">
<code class="code">not c</code> returns the negation of <code class="code">c</code>.<br>
</div>
</body></html>
