<html> <head> <link rel="stylesheet" href="style.css" type="text/css"> <link rel="Start" href="index.html"> <link rel="previous" href="Conjunto.html"> <link rel="next" href="FdArray.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"><link title="Access" rel="Section" href="#2_Access"> <link title="Creation" rel="Section" href="#2_Creation"> <link title="Operators and Built-in Goals" rel="Section" href="#2_OperatorsandBuiltinGoals"> <link title="Operations on Array of Variables" rel="Section" href="#2_OperationsonArrayofVariables"> <link title="Operations on List of Variables" rel="Section" href="#2_OperationsonListofVariables"> <link title="Optimization" rel="Section" href="#2_Optimization"> <link title="Search Strategy" rel="Section" href="#2_SearchStrategy"> <link title="Solving" rel="Section" href="#2_Solving"> <link title="Instantiation of Finite Domain Variables" rel="Subsection" href="#3_InstantiationofFiniteDomainVariables"> <link title="Instantiation of Set Variables" rel="Subsection" href="#3_InstantiationofSetVariables"> <title>Goals</title> </head> <body> <div class="navbar"><a href="Conjunto.html">Previous</a> <a href="index.html">Up</a> <a href="FdArray.html">Next</a> </div> <center><h1>Module <a href="type_Goals.html">Goals</a></h1></center> <br> <pre><span class="keyword">module</span> Goals: <code class="code">sig</code> <a href="Goals.html">..</a> <code class="code">end</code></pre><a name="1_BuildingandSolvingGoals"></a> <h1>Building and Solving Goals</h1><br> <hr width="100%"> <br> This module provides functions and operators to build goals that will control the search, i.e. mainly choose and instantiate variables.<br> <br> <a name="2_Access"></a> <h2>Access</h2><br> <pre><span class="keyword">type</span> <a name="TYPEt"></a><code class="type"></code>t </pre> <div class="info"> The type of goals.<br> </div> <pre><span class="keyword">val</span> <a name="VALname"></a>name : <code class="type"><a href="Goals.html#TYPEt">t</a> -> string</code></pre><div class="info"> <code class="code">name g</code> returns the name of the goal <code class="code">g</code>.<br> </div> <pre><span class="keyword">val</span> <a name="VALfprint"></a>fprint : <code class="type">Pervasives.out_channel -> <a href="Goals.html#TYPEt">t</a> -> unit</code></pre><div class="info"> <code class="code">fprint chan g</code> prints the name of goal <code class="code">g</code> on channel <code class="code">chan</code>.<br> </div> <br> <a name="2_Creation"></a> <h2>Creation</h2><br> <pre><span class="keyword">val</span> <a name="VALfail"></a>fail : <code class="type"><a href="Goals.html#TYPEt">t</a></code></pre><pre><span class="keyword">val</span> <a name="VALsuccess"></a>success : <code class="type"><a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> Failure (resp. success). Neutral element for the disjunction (resp. conjunction) over goals. Could be implemented as <code class="code">create (fun () -> Stak.fail "fail")</code> (resp. <code class="code">create (fun () -> ())</code>).<br> </div> <pre><span class="keyword">val</span> <a name="VALatomic"></a>atomic : <code class="type">?name:string -> (unit -> unit) -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">atomic ~name:"atomic" f</code> returns a goal calling function <code class="code">f</code>. <code class="code">f</code> must take <code class="code">()</code> as argument and return <code class="code">()</code>. <code class="code">name</code> default value is <code class="code">"atomic"</code>.<br> </div> <pre><span class="keyword">val</span> <a name="VALcreate"></a>create : <code class="type">?name:string -> ('a -> <a href="Goals.html#TYPEt">t</a>) -> 'a -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">create ~name:"create" f a</code> returns a goal calling <code class="code">f a</code>. <code class="code">f</code> should return a goal (success to stop). <code class="code">name</code> default value is <code class="code">"create"</code>.<br> </div> <pre><span class="keyword">val</span> <a name="VALcreate_rec"></a>create_rec : <code class="type">?name:string -> (<a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a>) -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">create_rec ~name:"create_rec" f</code> returns a goal calling <code class="code">f</code>. <code class="code">f</code> takes the goal itself as argument and should return a goal (success to stop). Useful to write recursive goals. <code class="code">name</code> default value is <code class="code">"create_rec"</code>.<br> </div> <br> <a name="2_OperatorsandBuiltinGoals"></a> <h2>Operators and Built-in Goals</h2><br> <pre><span class="keyword">val</span> <a name="VAL(&&~)"></a>(&&~) : <code class="type"><a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a></code></pre><pre><span class="keyword">val</span> <a name="VAL(||~)"></a>(||~) : <code class="type"><a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> Conjunction and disjunction over goals. Note that these two operators do have the <b>same priority</b>. Goals expressions must therefore be carefully parenthesized to produce the expected result.<br> </div> <pre><span class="keyword">val</span> <a name="VALforto"></a>forto : <code class="type">int -> int -> (int -> <a href="Goals.html#TYPEt">t</a>) -> <a href="Goals.html#TYPEt">t</a></code></pre><pre><span class="keyword">val</span> <a name="VALfordownto"></a>fordownto : <code class="type">int -> int -> (int -> <a href="Goals.html#TYPEt">t</a>) -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">forto min max g</code> (resp. <code class="code">fordownto min max g</code>) returns the conjunctive iteration of goal <code class="code">g</code> on increasing (resp. decreasing) integers from <code class="code">min</code> (resp. <code class="code">max</code>) to <code class="code">max</code> (resp. <code class="code">min</code>).<br> </div> <pre><span class="keyword">val</span> <a name="VALonce"></a>once : <code class="type"><a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">once g</code> cuts choice points left on goal <code class="code">g</code>.<br> </div> <pre><span class="keyword">val</span> <a name="VALsigma"></a>sigma : <code class="type">?domain:<a href="Domain.html#TYPEt">Domain.t</a> -> (Var.Fd.t -> <a href="Goals.html#TYPEt">t</a>) -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">sigma ~domain:Domain.int fgoal</code> creates the goal <code class="code">(fgoal v)</code> where <code class="code">v</code> is a new variable of domain <code class="code">domain</code>. Default domain is the largest one. It can be considered as an existential quantification, hence the concrete notation <code class="code">sigma</code> of this function (because existential quantification can be seen as a generalized disjunction).<br> </div> <br> <a name="3_InstantiationofFiniteDomainVariables"></a> <h3>Instantiation of Finite Domain Variables</h3><br> <pre><span class="keyword">val</span> <a name="VALunify"></a>unify : <code class="type">Var.Fd.t -> int -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">unify var x</code> instantiates variable <code class="code">var</code> to <code class="code">x</code>.<br> </div> <pre><span class="keyword">val</span> <a name="VALindomain"></a>indomain : <code class="type">Var.Fd.t -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> Non-deterministic instantiation of a variable, by labeling its domain (in increasing order).<br> </div> <pre><span class="keyword">val</span> <a name="VALinstantiate"></a>instantiate : <code class="type">(<a href="Domain.html#TYPEt">Domain.t</a> -> int) -> Var.Fd.t -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">instantiate choose var</code> Non-deterministic instantiation of a variable, by labeling its domain using the value returned by the <code class="code">choose</code> function.<br> </div> <pre><span class="keyword">val</span> <a name="VALdichotomic"></a>dichotomic : <code class="type">Var.Fd.t -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> Non-deterministic instantiation of a variable, by dichotomic recursive exploration of its domain.<br> </div> <br> <a name="3_InstantiationofSetVariables"></a> <h3>Instantiation of Set Variables</h3><br> <pre><span class="keyword">module</span> <a href="Goals.Conjunto.html">Conjunto</a>: <code class="code">sig</code> <a href="Goals.Conjunto.html">..</a> <code class="code">end</code></pre><br> <a name="2_OperationsonArrayofVariables"></a> <h2>Operations on Array of Variables</h2><br> <pre><span class="keyword">module</span> <a href="Goals.Array.html">Array</a>: <code class="code">sig</code> <a href="Goals.Array.html">..</a> <code class="code">end</code></pre><br> <a name="2_OperationsonListofVariables"></a> <h2>Operations on List of Variables</h2><br> <pre><span class="keyword">module</span> <a href="Goals.List.html">List</a>: <code class="code">sig</code> <a href="Goals.List.html">..</a> <code class="code">end</code></pre><br> <a name="2_Optimization"></a> <h2>Optimization</h2><br> <br><code><span class="keyword">type</span> <a name="TYPEbb_mode"></a><code class="type"></code>bb_mode = </code><table class="typetable"> <tr> <td align="left" valign="top" > <code><span class="keyword">|</span></code></td> <td align="left" valign="top" > <code><span class="constructor">Restart</span></code></td> </tr> <tr> <td align="left" valign="top" > <code><span class="keyword">|</span></code></td> <td align="left" valign="top" > <code><span class="constructor">Continue</span></code></td> <td class="typefieldcomment" align="left" valign="top" ><code>(*</code></td><td class="typefieldcomment" align="left" valign="top" ><code>Branch and bound mode.</code></td><td class="typefieldcomment" align="left" valign="bottom" ><code>*)</code></td> </tr></table> <pre><span class="keyword">val</span> <a name="VALminimize"></a>minimize : <code class="type">?step:int -><br> ?mode:<a href="Goals.html#TYPEbb_mode">bb_mode</a> -> <a href="Goals.html#TYPEt">t</a> -> Var.Fd.t -> (int -> unit) -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">minimize ~step:1 ~mode:Continue goal cost solution</code> runs a Branch and Bound algorithm on <code class="code">goal</code> for bound <code class="code">cost</code>, with an improvement of at least <code class="code">step</code> between each solution found. With <code class="code">mode</code> equal to <code class="code">Restart</code>, the search restarts from the beginning for every step whereas with mode <code class="code">Continue</code> (default) the search simply carries on with an update of the cost constraint. <code class="code">solution</code> is called with the instantiation value of <code class="code">cost</code> (which must be instantiated by <code class="code">goal</code>) as argument each time a solution is found; this function can therefore be used to store (e.g. in a reference) the current solution. Default <code class="code">step</code> is 1. <code class="code">minimize</code> <b>always fails</b>.<br> </div> <br> <a name="2_SearchStrategy"></a> <h2>Search Strategy</h2><br> <pre><span class="keyword">val</span> <a name="VALlds"></a>lds : <code class="type">?step:int -> <a href="Goals.html#TYPEt">t</a> -> <a href="Goals.html#TYPEt">t</a></code></pre><div class="info"> <code class="code">lds ~step:1 g</code> returns a goal which will iteratively search <code class="code">g</code> with increasing limited discrepancy (see ) by increment <code class="code">step</code>. <code class="code">step</code> default value is 1.<br> </div> <br> <a name="2_Solving"></a> <h2>Solving</h2><br> <pre><span class="keyword">val</span> <a name="VALsolve"></a>solve : <code class="type">?control:(int -> unit) -> <a href="Goals.html#TYPEt">t</a> -> bool</code></pre><div class="info"> <code class="code">solve ~control:(fun _ -> ()) g</code> solves the goal <code class="code">g</code> and returns a success (<code class="code">true</code>) or a failure (<code class="code">false</code>). The execution can be precisely controlled with the <code class="code">control</code> argument whose single argument is the number of bactracks since the beginning of the search. This function is called after every local failure: <p> <ul> <li>it can raise <code class="code">Stak.Fail</code> to force a failure of the search in the current branch (i.e. backtrack);</li> </ul> <ul> <li>it can raise any other user exception to stop the search process;</li> </ul> <ul> <li>it must return <code class="code">unit</code> to continue the search; this is the default behavior.</li> </ul> <br> </div> </body></html>