<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 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="Fcl_genesis" rel="Chapter" href="Fcl_genesis.html"> <link title="Fcl_debug" rel="Chapter" href="Fcl_debug.html"> <link title="Fcl_misc" rel="Chapter" href="Fcl_misc.html"> <link title="Fcl_float" rel="Chapter" href="Fcl_float.html"> <link title="Fcl_stak" rel="Chapter" href="Fcl_stak.html"> <link title="Fcl_domain" rel="Chapter" href="Fcl_domain.html"> <link title="Fcl_setDomain" rel="Chapter" href="Fcl_setDomain.html"> <link title="Fcl_data" rel="Chapter" href="Fcl_data.html"> <link title="Fcl_cstr" rel="Chapter" href="Fcl_cstr.html"> <link title="Fcl_var" rel="Chapter" href="Fcl_var.html"> <link title="Fcl_reify" rel="Chapter" href="Fcl_reify.html"> <link title="Fcl_invariant" rel="Chapter" href="Fcl_invariant.html"> <link title="Fcl_boolean" rel="Chapter" href="Fcl_boolean.html"> <link title="Fcl_alldiff" rel="Chapter" href="Fcl_alldiff.html"> <link title="Fcl_linear" rel="Chapter" href="Fcl_linear.html"> <link title="Fcl_nonlinear" rel="Chapter" href="Fcl_nonlinear.html"> <link title="Fcl_expr" rel="Chapter" href="Fcl_expr.html"> <link title="Fcl_arith" rel="Chapter" href="Fcl_arith.html"> <link title="Fcl_interval" rel="Chapter" href="Fcl_interval.html"> <link title="Fcl_gcc" rel="Chapter" href="Fcl_gcc.html"> <link title="Fcl_fdArray" rel="Chapter" href="Fcl_fdArray.html"> <link title="Fcl_conjunto" rel="Chapter" href="Fcl_conjunto.html"> <link title="Fcl_sorting" rel="Chapter" href="Fcl_sorting.html"> <link title="Fcl_goals" rel="Chapter" href="Fcl_goals.html"> <link title="Fcl_opti" rel="Chapter" href="Fcl_opti.html"> <link title="Facile" rel="Chapter" href="Facile.html"><title>Facile</title> </head> <body> <code class="code"><span class="keyword">sig</span><br> <span class="keyword">module</span> <span class="constructor">Domain</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> elt = int<br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> empty : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> create : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> unsafe_create : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> interval :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> int : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> boolean : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> is_empty : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> size : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> min : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> max : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> min_max : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt * <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> iter : (<span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> interval_iter :<br> (<span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> member : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> values : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt list<br> <span class="keyword">val</span> fprint_elt : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> sprint : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> included : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> add : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove_up : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove_low :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove_low_up :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove_closed_inter :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> intersection :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> union : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> difference : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> diff : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> remove_min : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> minus : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> plus : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> times : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t<br> <span class="keyword">val</span> smallest_geq :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> greatest_leq :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> largest_hole_around :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt * <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> choose :<br> (<span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> compare : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> compare_elt :<br> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.elt<br> <span class="keyword">val</span> disjoint : <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">SetDomain</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">module</span> <span class="constructor">S</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> empty : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> is_empty : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> mem : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> add : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> singleton : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> remove : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> union :<br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> inter :<br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> diff :<br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> compare : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> subset : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> iter : (int <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> cardinal : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> elements : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int list<br> <span class="keyword">val</span> min_elt : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> max_elt : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> choose : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> remove_up : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">val</span> remove_low :<br> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">type</span> elt = <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> min : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt<br> <span class="keyword">val</span> max : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt<br> <span class="keyword">val</span> min_max :<br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt * <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt<br> <span class="keyword">val</span> mem : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> interval :<br> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t<br> <span class="keyword">val</span> fprint_elt : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> included : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> iter : (<span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br> <span class="keyword">val</span> values : <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt list<br> <span class="keyword">val</span> elt_of_list : int list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Stak</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> level<br> <span class="keyword">val</span> older : <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> size : unit <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> depth : unit <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> level : unit <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level<br> <span class="keyword">val</span> levels : unit <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level list<br> <span class="keyword">val</span> nb_choice_points : unit <span class="keywordsign">-></span> int<br> <span class="keyword">exception</span> <span class="constructor">Level_not_found</span> <span class="keyword">of</span> <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level<br> <span class="keyword">val</span> cut : <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.level <span class="keywordsign">-></span> unit<br> <span class="keyword">exception</span> <span class="constructor">Fail</span> <span class="keyword">of</span> string<br> <span class="keyword">val</span> fail : string <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br> <span class="keyword">val</span> trail : (unit <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> unit<br> <span class="keyword">type</span> <span class="keywordsign">'</span>a ref<br> <span class="keyword">val</span> ref : <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.ref<br> <span class="keyword">val</span> set : <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.ref <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> get : <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Stak</span>.ref <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Data</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">module</span> <span class="constructor">Array</span> : <span class="keyword">sig</span> <span class="keyword">val</span> set : <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Hashtbl</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) t<br> <span class="keyword">val</span> create : int <span class="keywordsign">-></span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t<br> <span class="keyword">val</span> get : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Hashtbl</span>.t<br> <span class="keyword">val</span> add : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> find : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b<br> <span class="keyword">val</span> mem : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> remove : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> replace : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> iter :<br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fold :<br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>c <span class="keywordsign">-></span> <span class="keywordsign">'</span>c) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Data</span>.<span class="constructor">Hashtbl</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>c <span class="keywordsign">-></span> <span class="keywordsign">'</span>c<br> <span class="keyword">end</span><br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Cstr</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">exception</span> <span class="constructor">DontKnow</span><br> <span class="keyword">type</span> priority<br> <span class="keyword">val</span> immediate : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.priority<br> <span class="keyword">val</span> normal : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.priority<br> <span class="keyword">val</span> later : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.priority<br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> id : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> priority : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.priority<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> is_solved : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> create :<br> ?name:string <span class="keywordsign">-></span><br> ?nb_wakings:int <span class="keywordsign">-></span><br> ?fprint:(<span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span><br> ?priority:<span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.priority <span class="keywordsign">-></span><br> ?init:(unit <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span><br> ?check:(unit <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span><br> ?not:(unit <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t) <span class="keywordsign">-></span><br> (int <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span> (<span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> post : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> init : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> one : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> zero : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> active_store : unit <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t list<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Var</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">module</span> <span class="keyword">type</span> <span class="constructor">ATTR</span> =<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> domain<br> <span class="keyword">type</span> elt<br> <span class="keyword">type</span> event<br> <span class="keyword">val</span> dom : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.domain<br> <span class="keyword">val</span> on_refine : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.event<br> <span class="keyword">val</span> on_subst : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.event<br> <span class="keyword">val</span> on_min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.event<br> <span class="keyword">val</span> on_max : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.event<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.elt<br> <span class="keyword">val</span> max : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.elt<br> <span class="keyword">val</span> member : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> constraints_number : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> size : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">ATTR</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Attr</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> domain = <span class="constructor">Domain</span>.t<br> <span class="keyword">type</span> elt = int<br> <span class="keyword">type</span> event<br> <span class="keyword">val</span> dom : t <span class="keywordsign">-></span> domain<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> constraints_number : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">SetAttr</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> domain = <span class="constructor">SetDomain</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">type</span> event<br> <span class="keyword">val</span> dom : t <span class="keywordsign">-></span> domain<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> constraints_number : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">end</span><br> <span class="keyword">type</span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) concrete = <span class="constructor">Unk</span> <span class="keyword">of</span> <span class="keywordsign">'</span>a <span class="keywordsign">|</span> <span class="constructor">Val</span> <span class="keyword">of</span> <span class="keywordsign">'</span>b<br> <span class="keyword">module</span> <span class="keyword">type</span> <span class="constructor">BASICFD</span> =<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> attr<br> <span class="keyword">type</span> domain<br> <span class="keyword">type</span> elt<br> <span class="keyword">type</span> event<br> <span class="keyword">val</span> create :<br> ?name:string <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.domain <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t<br> <span class="keyword">val</span> interval :<br> ?name:string <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t<br> <span class="keyword">val</span> array :<br> ?name:string <span class="keywordsign">-></span><br> int <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t array<br> <span class="keyword">val</span> elt : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t<br> <span class="keyword">val</span> is_var : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> is_bound : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> value :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span><br> (<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.attr, <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt)<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.concrete<br> <span class="keyword">val</span> min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt<br> <span class="keyword">val</span> max : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt<br> <span class="keyword">val</span> min_max :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt * <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt<br> <span class="keyword">val</span> elt_value : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt<br> <span class="keyword">val</span> int_value : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt<br> <span class="keyword">val</span> size : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> member : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> compare : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint_array :<br> <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t array <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.domain <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_up :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low_up :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> on_refine : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.event<br> <span class="keyword">val</span> on_subst : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.event<br> <span class="keyword">val</span> on_min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.event<br> <span class="keyword">val</span> on_max : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.event<br> <span class="keyword">val</span> delay :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.event list <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> int : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t<br> <span class="keyword">val</span> subst : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify_cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">BASICFD</span>.elt <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="keyword">type</span> <span class="constructor">FD</span> =<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> attr<br> <span class="keyword">type</span> domain<br> <span class="keyword">type</span> elt<br> <span class="keyword">type</span> event<br> <span class="keyword">val</span> create : ?name:string <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> interval : ?name:string <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> array : ?name:string <span class="keywordsign">-></span> int <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t array<br> <span class="keyword">val</span> elt : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> is_var : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> is_bound : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> value : t <span class="keywordsign">-></span> (attr, elt) concrete<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> min_max : t <span class="keywordsign">-></span> elt * elt<br> <span class="keyword">val</span> elt_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> int_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint_array : out_channel <span class="keywordsign">-></span> t array <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine : t <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> delay : event list <span class="keywordsign">-></span> t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> int : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> subst : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify_cstr : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> remove : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> values : t <span class="keywordsign">-></span> elt list<br> <span class="keyword">val</span> iter : (elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Fd</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> attr = <span class="constructor">Attr</span>.t<br> <span class="keyword">type</span> domain = <span class="constructor">Domain</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">Domain</span>.elt<br> <span class="keyword">type</span> event = <span class="constructor">Attr</span>.event<br> <span class="keyword">val</span> create : ?name:string <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> interval : ?name:string <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> array : ?name:string <span class="keywordsign">-></span> int <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t array<br> <span class="keyword">val</span> elt : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> is_var : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> is_bound : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> value : t <span class="keywordsign">-></span> (attr, elt) concrete<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> min_max : t <span class="keywordsign">-></span> elt * elt<br> <span class="keyword">val</span> elt_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> int_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint_array : out_channel <span class="keywordsign">-></span> t array <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine : t <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> delay : event list <span class="keywordsign">-></span> t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> int : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> subst : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify_cstr : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> remove : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> values : t <span class="keywordsign">-></span> elt list<br> <span class="keyword">val</span> iter : (elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">SetFd</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">type</span> attr = <span class="constructor">SetAttr</span>.t<br> <span class="keyword">type</span> domain = <span class="constructor">SetDomain</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">SetDomain</span>.<span class="constructor">S</span>.t<br> <span class="keyword">type</span> event = <span class="constructor">SetAttr</span>.event<br> <span class="keyword">val</span> create : ?name:string <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> interval : ?name:string <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> array : ?name:string <span class="keywordsign">-></span> int <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t array<br> <span class="keyword">val</span> elt : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> is_var : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> is_bound : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> value : t <span class="keywordsign">-></span> (attr, elt) concrete<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> min_max : t <span class="keywordsign">-></span> elt * elt<br> <span class="keyword">val</span> elt_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> int_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint_array : out_channel <span class="keywordsign">-></span> t array <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine : t <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> delay : event list <span class="keywordsign">-></span> t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> int : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> subst : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify_cstr : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">val</span> delay :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Attr</span>.event list <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Reify</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> boolean :<br> ?delay_on_negation:bool <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> cstr :<br> ?delay_on_negation:bool <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( ||~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( &&~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <=>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> xor : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> not : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( =>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Alldiff</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> algo = <span class="constructor">Lazy</span> <span class="keywordsign">|</span> <span class="constructor">Bin_matching</span> <span class="keyword">of</span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.event<br> <span class="keyword">val</span> cstr :<br> ?algo:<span class="constructor">Facile</span>.<span class="constructor">Alldiff</span>.algo <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Goals</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> name : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> atomic : ?name:string <span class="keywordsign">-></span> (unit <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> create :<br> ?name:string <span class="keywordsign">-></span> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> create_rec :<br> ?name:string <span class="keywordsign">-></span> (<span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> fail : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> success : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> ( &&~ ) : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> ( ||~ ) : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> once : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> solve : ?control:(int <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> lds : ?step:int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> unify : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> indomain : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> instantiate :<br> (<span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span> int) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> dichotomic : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> forto : int <span class="keywordsign">-></span> int <span class="keywordsign">-></span> (int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> fordownto : int <span class="keywordsign">-></span> int <span class="keywordsign">-></span> (int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">module</span> <span class="constructor">Array</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> foralli :<br> ?select:(<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> forall :<br> ?select:(<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> existsi :<br> ?select:(<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> exists :<br> ?select:(<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> choose_index :<br> (<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Attr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Attr</span>.t <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> not_instantiated_fd : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> labeling : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">GlArray</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> iter_h :<br> (<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> iter_hi :<br> (<span class="keywordsign">'</span>a array <span class="keywordsign">-></span> int) <span class="keywordsign">-></span><br> (int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> iter : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> iteri :<br> (int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> iter2 :<br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span><br> <span class="keywordsign">'</span>a array <span class="keywordsign">-></span> <span class="keywordsign">'</span>b array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> labeling : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> choose_index :<br> (<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Attr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Attr</span>.t <span class="keywordsign">-></span> bool) <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> not_instantiated_fd : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> int<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">List</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> forall :<br> ?select:(<span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="keywordsign">'</span>a * <span class="keywordsign">'</span>a list) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> exists :<br> ?select:(<span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="keywordsign">'</span>a * <span class="keywordsign">'</span>a list) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> member : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> labeling : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">GlList</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> iter : (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> labeling : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> member : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> iter_h :<br> (<span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="keywordsign">'</span>a * <span class="keywordsign">'</span>a list) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">type</span> bb_mode = <span class="constructor">Restart</span> <span class="keywordsign">|</span> <span class="constructor">Continue</span><br> <span class="keyword">val</span> minimize :<br> ?step:int <span class="keywordsign">-></span><br> ?mode:<span class="constructor">Facile</span>.<span class="constructor">Goals</span>.bb_mode <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> (int <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> sigma :<br> ?domain:<span class="constructor">Facile</span>.<span class="constructor">Domain</span>.t <span class="keywordsign">-></span><br> (<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t) <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">module</span> <span class="constructor">Conjunto</span> :<br> <span class="keyword">sig</span> <span class="keyword">val</span> indomain : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keyword">end</span><br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Sorting</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> sort : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array<br> <span class="keyword">val</span> sortp :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array * <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array<br> <span class="keyword">val</span> cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span><br> ?p:<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array option <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Boolean</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> cstr : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> sum : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Expr</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Expr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> eval : <span class="constructor">Facile</span>.<span class="constructor">Expr</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> min_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Expr</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> max_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Expr</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> min_max_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Expr</span>.t <span class="keywordsign">-></span> int * int<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Arith</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t<br> <span class="keyword">val</span> i2e : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> fd2e : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( +~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( *~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( -~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( /~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( **~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( %~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> abs : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> sum : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> sum_fd : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> scalprod : int array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> scalprod_fd : int array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> prod : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> prod_fd : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> fprint : <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> eval : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> min_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> max_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> min_max_of_expr : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int * int<br> <span class="keyword">val</span> ( <=~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( >~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( =~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <>~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( >=~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> e2fd : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> ( <=~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( <~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( >~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( =~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( <>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( >=~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> shift : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> get_boolsum_threshold : unit <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> set_boolsum_threshold : int <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Invariant</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) t<br> <span class="keyword">type</span> setable<br> <span class="keyword">type</span> unsetable<br> <span class="keyword">type</span> <span class="keywordsign">'</span>a setable_t = (<span class="keywordsign">'</span>a, <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.setable) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t<br> <span class="keyword">type</span> <span class="keywordsign">'</span>a unsetable_t =<br> (<span class="keywordsign">'</span>a, <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t<br> <span class="keyword">val</span> create : ?name:string <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.setable_t<br> <span class="keyword">val</span> constant : ?name:string <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> set : <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.setable_t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> get : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a<br> <span class="keyword">val</span> id : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> fprint :<br> <span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span><br> ?printer:(<span class="constructor">Pervasives</span>.out_channel <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unary :<br> ?name:string <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>c) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> binary :<br> ?name:string <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>c) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>d) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>b, <span class="keywordsign">'</span>e) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>c <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> ternary :<br> ?name:string <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>b <span class="keywordsign">-></span> <span class="keywordsign">'</span>c <span class="keywordsign">-></span> <span class="keywordsign">'</span>d) <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>e) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>b, <span class="keywordsign">'</span>f) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>c, <span class="keywordsign">'</span>g) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>d <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> sum :<br> (int, <span class="keywordsign">'</span>a) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t array <span class="keywordsign">-></span><br> int <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> prod :<br> (int, <span class="keywordsign">'</span>a) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t array <span class="keywordsign">-></span><br> int <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">module</span> <span class="constructor">Array</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> get :<br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t array <span class="keywordsign">-></span><br> (int, <span class="keywordsign">'</span>c) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> argmin :<br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t array <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>c) <span class="keywordsign">-></span> int <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> min :<br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.t array <span class="keywordsign">-></span><br> (<span class="keywordsign">'</span>a <span class="keywordsign">-></span> <span class="keywordsign">'</span>c) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="keyword">type</span> <span class="constructor">FD</span> =<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> fd<br> <span class="keyword">type</span> elt<br> <span class="keyword">val</span> min :<br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.elt <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> max :<br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.elt <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> size :<br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span> int <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> is_var :<br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span> bool <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">val</span> unary :<br> ?name:string <span class="keywordsign">-></span><br> (<span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.<span class="constructor">FD</span>.fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a <span class="constructor">Facile</span>.<span class="constructor">Invariant</span>.unsetable_t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Fd</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> fd = <span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">Var</span>.<span class="constructor">Fd</span>.elt<br> <span class="keyword">val</span> min : fd <span class="keywordsign">-></span> elt unsetable_t<br> <span class="keyword">val</span> max : fd <span class="keywordsign">-></span> elt unsetable_t<br> <span class="keyword">val</span> size : fd <span class="keywordsign">-></span> int unsetable_t<br> <span class="keyword">val</span> is_var : fd <span class="keywordsign">-></span> bool unsetable_t<br> <span class="keyword">val</span> unary : ?name:string <span class="keywordsign">-></span> (fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a unsetable_t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">SetFd</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> fd = <span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">Var</span>.<span class="constructor">SetFd</span>.elt<br> <span class="keyword">val</span> min : fd <span class="keywordsign">-></span> elt unsetable_t<br> <span class="keyword">val</span> max : fd <span class="keywordsign">-></span> elt unsetable_t<br> <span class="keyword">val</span> size : fd <span class="keywordsign">-></span> int unsetable_t<br> <span class="keyword">val</span> is_var : fd <span class="keywordsign">-></span> bool unsetable_t<br> <span class="keyword">val</span> unary : ?name:string <span class="keywordsign">-></span> (fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> fd <span class="keywordsign">-></span> <span class="keywordsign">'</span>a unsetable_t<br> <span class="keyword">end</span><br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Interval</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> is_member : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">FdArray</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> min_cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> max : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> max_cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> get : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> get_cstr :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Gcc</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> level = <span class="constructor">Basic</span> <span class="keywordsign">|</span> <span class="constructor">Medium</span> <span class="keywordsign">|</span> <span class="constructor">High</span><br> <span class="keyword">val</span> cstr :<br> ?level:<span class="constructor">Facile</span>.<span class="constructor">Gcc</span>.level <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t array <span class="keywordsign">-></span><br> (<span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t * int) array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Opti</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> mode = <span class="constructor">Restart</span> <span class="keywordsign">|</span> <span class="constructor">Continue</span><br> <span class="keyword">val</span> minimize :<br> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span><br> ?control:(int <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span><br> ?step:int <span class="keywordsign">-></span> ?mode:<span class="constructor">Facile</span>.<span class="constructor">Opti</span>.mode <span class="keywordsign">-></span> (int <span class="keywordsign">-></span> <span class="keywordsign">'</span>a) <span class="keywordsign">-></span> <span class="keywordsign">'</span>a option<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Conjunto</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> subset : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> cardinal : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> smallest : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> union :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t<br> <span class="keyword">val</span> inter :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t<br> <span class="keyword">val</span> all_disjoint : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t array <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> disjoint :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> inside : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> outside : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> inf_min : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> order : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> order_with_card :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span><br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> member :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">SetDomain</span>.elt list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> mem : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> sum_weight :<br> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t <span class="keywordsign">-></span> (int * int) list <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">val</span> atmost1 : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">SetFd</span>.t array <span class="keywordsign">-></span> int <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">module</span> <span class="constructor">Easy</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">val</span> i2e : int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> fd2e : <span class="constructor">Facile</span>.<span class="constructor">Var</span>.<span class="constructor">Fd</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( +~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( *~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( -~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( /~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( **~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> int <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( %~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( <=~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( >~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( =~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <>~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( >=~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <=~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( <~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( >~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( =~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( <>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( >=~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Arith</span>.t<br> <span class="keyword">val</span> ( &&~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( ||~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( =>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( <=>~~ ) : <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> ( &&~ ) : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">val</span> ( ||~ ) : <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t <span class="keywordsign">-></span> <span class="constructor">Facile</span>.<span class="constructor">Goals</span>.t<br> <span class="keyword">module</span> <span class="constructor">Fd</span> :<br> <span class="keyword">sig</span><br> <span class="keyword">type</span> t = <span class="constructor">Var</span>.<span class="constructor">Fd</span>.t<br> <span class="keyword">type</span> attr = <span class="constructor">Var</span>.<span class="constructor">Attr</span>.t<br> <span class="keyword">type</span> domain = <span class="constructor">Domain</span>.t<br> <span class="keyword">type</span> elt = <span class="constructor">Domain</span>.elt<br> <span class="keyword">type</span> event = <span class="constructor">Var</span>.<span class="constructor">Attr</span>.event<br> <span class="keyword">val</span> create : ?name:string <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> interval : ?name:string <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> array : ?name:string <span class="keywordsign">-></span> int <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> t array<br> <span class="keyword">val</span> elt : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> is_var : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> is_bound : t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> value : t <span class="keywordsign">-></span> (attr, elt) <span class="constructor">Var</span>.concrete<br> <span class="keyword">val</span> min : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> max : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> min_max : t <span class="keywordsign">-></span> elt * elt<br> <span class="keyword">val</span> elt_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> int_value : t <span class="keywordsign">-></span> elt<br> <span class="keyword">val</span> size : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> member : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> id : t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> name : t <span class="keywordsign">-></span> string<br> <span class="keyword">val</span> compare : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> int<br> <span class="keyword">val</span> equal : t <span class="keywordsign">-></span> t <span class="keywordsign">-></span> bool<br> <span class="keyword">val</span> fprint : out_channel <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> fprint_array : out_channel <span class="keywordsign">-></span> t array <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine : t <span class="keywordsign">-></span> domain <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> refine_low_up : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> on_refine : event<br> <span class="keyword">val</span> on_subst : event<br> <span class="keyword">val</span> on_min : event<br> <span class="keyword">val</span> on_max : event<br> <span class="keyword">val</span> delay : event list <span class="keywordsign">-></span> t <span class="keywordsign">-></span> ?waking_id:int <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> int : elt <span class="keywordsign">-></span> t<br> <span class="keyword">val</span> subst : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> unify_cstr : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> <span class="constructor">Cstr</span>.t<br> <span class="keyword">val</span> remove : t <span class="keywordsign">-></span> elt <span class="keywordsign">-></span> unit<br> <span class="keyword">val</span> values : t <span class="keywordsign">-></span> elt list<br> <span class="keyword">val</span> iter : (elt <span class="keywordsign">-></span> unit) <span class="keywordsign">-></span> t <span class="keywordsign">-></span> unit<br> <span class="keyword">end</span><br> <span class="keyword">type</span> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) concrete' =<br> (<span class="keywordsign">'</span>a, <span class="keywordsign">'</span>b) <span class="constructor">Facile</span>.<span class="constructor">Var</span>.concrete =<br> <span class="constructor">Unk</span> <span class="keyword">of</span> <span class="keywordsign">'</span>a<br> <span class="keywordsign">|</span> <span class="constructor">Val</span> <span class="keyword">of</span> <span class="keywordsign">'</span>b<br> <span class="keyword">type</span> concrete_fd =<br> (<span class="constructor">Facile</span>.<span class="constructor">Easy</span>.<span class="constructor">Fd</span>.attr, <span class="constructor">Facile</span>.<span class="constructor">Easy</span>.<span class="constructor">Fd</span>.elt) <span class="constructor">Facile</span>.<span class="constructor">Easy</span>.concrete'<br> <span class="keyword">end</span><br> <span class="keyword">end</span></code></body></html>