<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>