Regenerated documentation. Removed slides, they were too outdated.

lukstafi · Feb 18, 2015 · 5996a1e · 5996a1e
1 parent c2bdb6a
commit 5996a1e
Show file tree

Hide file tree

Showing 18 changed files with 295 additions and 1,892 deletions.
diff --git a/doc/code/Abduction.html b/doc/code/Abduction.html
@@ -78,6 +78,19 @@ <h1>Module <a href="type_Abduction.html">Abduction</a></h1>
 </div>
 
 <pre><span id="VALno_num_abduction"><span class="keyword">val</span> no_num_abduction</span> : <code class="type">bool Pervasives.ref</code></pre><div class="info ">
+<code class="code">guess_eqs_nonvar=true</code> means the only guess equations <code class="code">x=y</code> tried
+    are for <code class="code">x=s</code>, <code class="code">y=t</code> in either the premise or conclusion of
+    abduction problem where neither <code class="code">s</code> nor <code class="code">t</code> are variables.
+    Default <code class="code">true</code>.<br>
+</div>
+
+<pre><span id="VALguess_eqs_nonvar"><span class="keyword">val</span> guess_eqs_nonvar</span> : <code class="type">bool Pervasives.ref</code></pre><div class="info ">
+<code class="code">prefer_guess=true</code> tries to guess equality-between-parameters
+    before considering other candidate abduction answer atoms.
+    Default <code class="code">false</code>.<br>
+</div>
+
+<pre><span id="VALprefer_guess"><span class="keyword">val</span> prefer_guess</span> : <code class="type">bool Pervasives.ref</code></pre><div class="info ">
 <code class="code">neg_before_abd=false</code> moves numerical negation elimination till
     after numerical abduction, with possibly better determination of
     negative facts, but worse availability of the negative
@@ -92,9 +105,9 @@ <h1>Module <a href="type_Abduction.html">Abduction</a></h1>
 <pre><span id="VALnum_neg_since"><span class="keyword">val</span> num_neg_since</span> : <code class="type">int Pervasives.ref</code></pre>
 <pre><span id="VALabd_fail_flag"><span class="keyword">val</span> abd_fail_flag</span> : <code class="type">bool Pervasives.ref</code></pre>
 <pre><span id="VALabd_timeout_flag"><span class="keyword">val</span> abd_timeout_flag</span> : <code class="type">bool Pervasives.ref</code></pre>
-<pre><span id="VALabd_simple"><span class="keyword">val</span> abd_simple</span> : <code class="type">Defs.quant_ops -><br>       ?without_quant:unit -><br>       bvs:Defs.VarSet.t -><br>       pms:Defs.VarSet.t -><br>       dissociate:bool -><br>       validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> unit) -><br>       discard:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       int -><br>       Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -><br>       <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsubst">Terms.subst</a> -><br>       (Defs.VarSet.t * (Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>)) option</code></pre>
-<pre><span id="VALabd_typ"><span class="keyword">val</span> abd_typ</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       ?dissociate:bool -><br>       validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> unit) -><br>       discard:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       (<a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       Defs.VarSet.t * <a href="Terms.html#TYPEsubst">Terms.subst</a> * Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> *<br>       (<a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a>) list</code></pre>
-<pre><span id="TYPEdiscarded"><span class="keyword">type</span> <code class="type"></code>discarded</span> = <code class="type">((Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list, NumDefs.formula list, unit)<br>       <a href="Terms.html#TYPEsep_sorts">Terms.sep_sorts</a></code> </pre>
+<pre><span id="VALabd_simple"><span class="keyword">val</span> abd_simple</span> : <code class="type">Defs.quant_ops -><br>       ?without_quant:unit -><br>       obvs:Defs.VarSet.t -><br>       bvs:Defs.VarSet.t -><br>       dissociate:bool -><br>       validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> unit) -><br>       neg_validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> int) -><br>       discard:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       int -><br>       Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -><br>       <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsubst">Terms.subst</a> -><br>       (Defs.VarSet.t * (Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>)) option</code></pre>
+<pre><span id="VALabd_typ"><span class="keyword">val</span> abd_typ</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       ?dissociate:bool -><br>       validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> unit) -><br>       neg_validate:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> -> int) -><br>       discard:(Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       (<a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list -><br>       Defs.VarSet.t * <a href="Terms.html#TYPEsubst">Terms.subst</a> * Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a> *<br>       (<a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> * <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a>) list</code></pre>
+<pre><span id="TYPEdiscarded"><span class="keyword">type</span> <code class="type"></code>discarded</span> = <code class="type">((Defs.var_name list * <a href="Terms.html#TYPEsubst">Terms.subst</a>) list, NumDefs.formula list,<br>        OrderDefs.formula list, unit)<br>       <a href="Terms.html#TYPEsep_sorts">Terms.sep_sorts</a></code> </pre>
 <div class="info ">
 Raises <code class="code">Contradiction</code> if constraints are contradictory and
     <code class="code">NoAnswer</code> when no answer can be found. Returns candidate
@@ -103,5 +116,5 @@ <h1>Module <a href="type_Abduction.html">Abduction</a></h1>
 </div>
 
 
-<pre><span id="VALabd"><span class="keyword">val</span> abd</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       ?iter_no:int -><br>       discard:<a href="Abduction.html#TYPEdiscarded">discarded</a> -><br>       (bool * <a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -><br>       (<a href="Terms.html#TYPEformula">Terms.formula</a> * Defs.loc) list -><br>       Defs.VarSet.t * <a href="Terms.html#TYPEsubst">Terms.subst</a> * (Defs.var_name list * <a href="Terms.html#TYPEformula">Terms.formula</a>)</code></pre>
+<pre><span id="VALabd"><span class="keyword">val</span> abd</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       xbvs:(int * Defs.VarSet.t) list -><br>       ?orig_ren:(Defs.var_name, Defs.var_name) Hashtbl.t -><br>       ?b_of_v:(Defs.var_name -> Defs.var_name) -><br>       upward_of:(Defs.var_name -> Defs.var_name -> bool) -><br>       nonparam_vars:Defs.VarSet.t -><br>       ?iter_no:int -><br>       discard:<a href="Abduction.html#TYPEdiscarded">discarded</a> -><br>       (bool * (int * (Defs.var_name * Defs.var_name) list) list * <a href="Terms.html#TYPEformula">Terms.formula</a> *<br>        <a href="Terms.html#TYPEformula">Terms.formula</a>)<br>       list -><br>       (<a href="Terms.html#TYPEformula">Terms.formula</a> * Defs.loc) list -><br>       Defs.VarSet.t * <a href="Terms.html#TYPEsubst">Terms.subst</a> * (Defs.var_name list * <a href="Terms.html#TYPEformula">Terms.formula</a>)</code></pre>
 <pre><span id="VALabd_mockup_num"><span class="keyword">val</span> abd_mockup_num</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       (<a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -><br>       (NumDefs.formula * NumDefs.formula) list option</code></pre></body></html>
diff --git a/doc/code/DisjElim.html b/doc/code/DisjElim.html
@@ -37,14 +37,13 @@ <h1>Module <a href="type_DisjElim.html">DisjElim</a></h1>
 
 <pre><span id="VALmore_existential"><span class="keyword">val</span> more_existential</span> : <code class="type">bool Pervasives.ref</code></pre><div class="info ">
 Allow more general argument types by inferring more existential
-    result type. Default value <code class="code">false</code>.<br>
+    result type. Default value <code class="code">false</code>.
+<p>
+If <code class="code">drop_csts=true</code>, drop assignments of existential variables to
+    constants during initial steps of main algorithm, as long as the
+    variables are constrained in other atoms of the answer. Default
+    <code class="code">true</code>.<br>
 </div>
 
-<pre><span id="VALdisjelim"><span class="keyword">val</span> disjelim</span> : <code class="type">Defs.quant_ops -><br>       bvs:Defs.VarSet.t -><br>       preserve:Defs.VarSet.t -><br>       do_num:bool -><br>       initstep:bool -><br>       <a href="Terms.html#TYPEformula">Terms.formula</a> list -> <a href="Terms.html#TYPEsubst">Terms.subst</a> * (Defs.var_name list * <a href="Terms.html#TYPEatom">Terms.atom</a> list)</code></pre>
-<pre><span id="VALinitstep_heur"><span class="keyword">val</span> initstep_heur</span> : <code class="type">Defs.quant_ops -><br>       validate:(<a href="Terms.html#TYPEformula">Terms.formula</a> -> unit) -> <a href="Terms.html#TYPEanswer">Terms.answer</a> -> <a href="Terms.html#TYPEanswer">Terms.answer</a></code></pre><div class="info ">
-Filter out "suspicious" and invalid atoms of a formula. <code class="code">validate</code>
-    should raise <code class="code">Contradiction</code> when a result is
-    incorrect. Currently: first removes min/max atoms comparing a
-    variable to a constant, then performs a greedy search for valid atoms.<br>
-</div>
-</body></html>
+<pre><span id="VALdrop_csts"><span class="keyword">val</span> drop_csts</span> : <code class="type">bool Pervasives.ref</code></pre>
+<pre><span id="VALdisjelim"><span class="keyword">val</span> disjelim</span> : <code class="type">Defs.quant_ops -><br>       ?target:Defs.var_name -><br>       bvs:Defs.VarSet.t -><br>       param_bvs:Defs.VarSet.t -><br>       up_of_anchor:(Defs.var_name -> bool) -><br>       do_num:bool -><br>       guess:bool -><br>       initstep:bool -><br>       residuum:<a href="Terms.html#TYPEformula">Terms.formula</a> -><br>       (<a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -><br>       bool * <a href="Terms.html#TYPEformula">Terms.formula</a> * (Defs.var_name list * <a href="Terms.html#TYPEformula">Terms.formula</a>) *<br>       <a href="Terms.html#TYPEformula">Terms.formula</a> list</code></pre></body></html>
diff --git a/doc/code/Infer.html b/doc/code/Infer.html
@@ -67,7 +67,7 @@ <h1>Module <a href="type_Infer.html">Infer</a></h1>
 <td align="left" valign="top" >
 <code><span class="keyword">|</span></code></td>
 <td align="left" valign="top" >
-<code><span id="TYPEELTcnstrnt.Or"><span class="constructor">Or</span></span> <span class="keyword">of</span> <code class="type">(<a href="Infer.html#TYPEcnstrnt">cnstrnt</a> * (unit -> unit)) list</code></code></td>
+<code><span id="TYPEELTcnstrnt.Or"><span class="constructor">Or</span></span> <span class="keyword">of</span> <code class="type">Defs.var_name<br>        * (Defs.VarSet.t * <a href="Infer.html#TYPEcnstrnt">cnstrnt</a> * <a href="Terms.html#TYPEformula">Terms.formula</a> * (unit -> unit)) list<br>        * <a href="Infer.html#TYPEcnstrnt">cnstrnt</a></code></code></td>
 
 </tr>
 <tr>
@@ -129,15 +129,26 @@ <h2 id="2_Normalization">Normalization</h2><br>
 </div>
 
 <pre><span id="VALnormalize"><span class="keyword">val</span> normalize</span> : <code class="type">Defs.quant_ops -> <a href="Infer.html#TYPEcnstrnt">cnstrnt</a> -> (int, int) Hashtbl.t * <a href="Infer.html#TYPEbranch">branch</a> list</code></pre>
-<pre><span id="VALsimplify"><span class="keyword">val</span> simplify</span> : <code class="type">Defs.VarSet.t -> Defs.quant_ops -> <a href="Infer.html#TYPEbranch">branch</a> list -> <a href="Infer.html#TYPEbranch">branch</a> list</code></pre><br>
+<pre><span id="VALphantom_enumeration"><span class="keyword">val</span> phantom_enumeration</span> : <code class="type">(<a href="Terms.html#TYPEcns_name">Terms.cns_name</a>, <a href="Terms.html#TYPEcns_name">Terms.cns_name</a> list) Hashtbl.t</code></pre><div class="info ">
+Contains information about phantom enumerations,
+    i.e. alternatives to a datatype parameter's nullary concrete type
+    excluded by an <code class="code">assert false</code> pattern-matching branch.
+    If the value for an is an empty list, the entry is not a phantom
+    enumeration.<br>
+</div>
+
+<pre><span id="VALsimplify"><span class="keyword">val</span> simplify</span> : <code class="type">Defs.VarSet.t -> Defs.quant_ops -> <a href="Infer.html#TYPEbranch">branch</a> list -> <a href="Infer.html#TYPEbranch">branch</a> list</code></pre><div class="info ">
+Eliminate shared conclusions. Solve <code class="code">RetType</code> constraints.<br>
+</div>
+<br>
 <h2 id="2_Postprocessingandprinting">Postprocessing and printing</h2><br>
 
-<pre><span id="VALseparate_subst"><span class="keyword">val</span> separate_subst</span> : <code class="type">?avoid:Defs.VarSet.t -><br>       ?keep_uni:bool -><br>       Defs.quant_ops -> <a href="Terms.html#TYPEformula">Terms.formula</a> -> <a href="Terms.html#TYPEsubst">Terms.subst</a> * <a href="Terms.html#TYPEformula">Terms.formula</a></code></pre>
-<pre><span id="VALseparate_sep_subst"><span class="keyword">val</span> separate_sep_subst</span> : <code class="type">?avoid:Defs.VarSet.t -><br>       ?keep_uni:bool -><br>       Defs.quant_ops -> <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> -> <a href="Terms.html#TYPEsubst">Terms.subst</a> * <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a></code></pre>
+<pre><span id="VALseparate_subst"><span class="keyword">val</span> separate_subst</span> : <code class="type">?avoid:Defs.VarSet.t -><br>       ?keep:Defs.VarSet.t -><br>       ?bvs:Defs.VarSet.t -><br>       ?keep_uni:bool -><br>       apply:bool -> Defs.quant_ops -> <a href="Terms.html#TYPEformula">Terms.formula</a> -> <a href="Terms.html#TYPEsubst">Terms.subst</a> * <a href="Terms.html#TYPEformula">Terms.formula</a></code></pre>
+<pre><span id="VALseparate_sep_subst"><span class="keyword">val</span> separate_sep_subst</span> : <code class="type">?avoid:Defs.VarSet.t -><br>       ?keep:Defs.VarSet.t -><br>       ?bvs:Defs.VarSet.t -><br>       ?keep_uni:bool -><br>       apply:bool -><br>       Defs.quant_ops -> <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a> -> <a href="Terms.html#TYPEsubst">Terms.subst</a> * <a href="Terms.html#TYPEsep_formula">Terms.sep_formula</a></code></pre>
 <pre><span id="VALpr_cnstrnt"><span class="keyword">val</span> pr_cnstrnt</span> : <code class="type">Format.formatter -> <a href="Infer.html#TYPEcnstrnt">cnstrnt</a> -> unit</code></pre>
 <pre><span id="VALpr_brs"><span class="keyword">val</span> pr_brs</span> : <code class="type">Format.formatter -> <a href="Infer.html#TYPEbranch">branch</a> list -> unit</code></pre>
 <pre><span id="VALpr_rbrs"><span class="keyword">val</span> pr_rbrs</span> : <code class="type">Format.formatter -> (<a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -> unit</code></pre>
 <pre><span id="VALpr_rbrs3"><span class="keyword">val</span> pr_rbrs3</span> : <code class="type">Format.formatter -> (bool * <a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -> unit</code></pre>
-<pre><span id="VALpr_rbrs4"><span class="keyword">val</span> pr_rbrs4</span> : <code class="type">Format.formatter -> (bool * 'a * <a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -> unit</code></pre>
-<pre><span id="VALpr_rbrs5"><span class="keyword">val</span> pr_rbrs5</span> : <code class="type">Format.formatter -><br>       (bool * 'a * 'b * <a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -> unit</code></pre>
+<pre><span id="VALpr_rbrs4"><span class="keyword">val</span> pr_rbrs4</span> : <code class="type">Format.formatter -><br>       (bool * 'a list * <a href="Terms.html#TYPEformula">Terms.formula</a> * <a href="Terms.html#TYPEformula">Terms.formula</a>) list -> unit</code></pre>
+<pre><span id="VALpr_rbrs5"><span class="keyword">val</span> pr_rbrs5</span> : <code class="type">Format.formatter -><br>       (bool * (int * <a href="Terms.html#TYPEtyp">Terms.typ</a>) list *<br>        (int * <a href="Terms.html#TYPEtyp">Terms.typ</a> * <a href="Terms.html#TYPEtyp">Terms.typ</a> * <a href="Terms.html#TYPElc">Terms.lc</a>) list * <a href="Terms.html#TYPEatom">Terms.atom</a> list *<br>        <a href="Terms.html#TYPEatom">Terms.atom</a> list)<br>       list -> unit</code></pre>
 <pre><span id="VALreset_state"><span class="keyword">val</span> reset_state</span> : <code class="type">unit -> unit</code></pre></body></html>
diff --git a/doc/code/Invariants.html b/doc/code/Invariants.html
@@ -37,6 +37,18 @@ <h1>Module <a href="type_Invariants.html">Invariants</a></h1>
 <pre><span id="VALtimeout_count"><span class="keyword">val</span> timeout_count</span> : <code class="type">int Pervasives.ref</code></pre>
 <pre><span id="VALtimeout_flag"><span class="keyword">val</span> timeout_flag</span> : <code class="type">bool Pervasives.ref</code></pre>
 <pre><span id="VALunfinished_postcond_flag"><span class="keyword">val</span> unfinished_postcond_flag</span> : <code class="type">bool Pervasives.ref</code></pre>
+<pre><span id="VALuse_prior_discards"><span class="keyword">val</span> use_prior_discards</span> : <code class="type">bool Pervasives.ref</code></pre><div class="info ">
+Breakdown of steps through the main iteration to achieve
+    convergence, counting from 0. The iteration:
+<p>
+
+    * <code class="code">disj_step.(0)</code> is 
+    * <code class="code">disj_step.(1)</code> is 
+    * <code class="code">disj_step.(2)</code> is 
+    * <code class="code">disj_step.(3)</code> is when convergence of postconditions is enforced.<br>
+</div>
+
+<pre><span id="VALdisj_step"><span class="keyword">val</span> disj_step</span> : <code class="type">int array</code></pre>
 <pre><span id="TYPEchi_subst"><span class="keyword">type</span> <code class="type"></code>chi_subst</span> = <code class="type">(int * (Defs.var_name list * <a href="Terms.html#TYPEformula">Terms.formula</a>)) list</code> </pre>