Special-case numerical abduction heuristic settings for definitions w…

…ith positive assertions, i.e. `assert num` and `assert type`. Update of tests and documentation.

doc/invargent-manual.tm

@@ -819,6 +819,10 @@
     abduction. This makes it faster but less likely to find the correct
     solution.
 
+    <item*|<verbatim|-convergence_step>>The iteration at which to start
+    truncating postconditions by only keeping atoms present in the previous
+    iteration, to force convergence (default 8).
+
     <item*|<verbatim|-early_postcond_abd>>Include postconditions from
     recursive calls in abduction from the start. We do not derive
     requirements put on postconditions by recursive calls on first iteration.
@@ -853,6 +857,10 @@
     will pick an answer <math|a+1>, which in the following step will force an
     answer <math|a+2>, then <math|a+3>, etc.
 
+    <item*|<verbatim|-reward_constrn>>How much to reward introducing a
+    constraint on so-far unconstrained varialbe, or penalize if negative
+    (default 2).
+
     <item*|<verbatim|-complexity_penalty>>How much to penalize an abduction
     candidate inequality for complexity of its coefficients; the coefficient
     of either the linear or power scaling of the coefficients (default 2.5).
@@ -879,6 +887,12 @@
     constant 1. This corresponds to an upper bound of an index into a
     zero-indexed array/matrix/etc.
 
+    <item*|<verbatim|-same_with_assertions>>Do not treat definitions with
+    positive assertions (<verbatim|assert num>, <verbatim|assert type>)
+    specially. The special treatment is currently equivalent to passing
+    <verbatim|-<no-break>reward_constrn -1> and
+    <verbatim|-prefer_bound_to_local>.
+
     <item*|<verbatim|-concl_abd_penalty>>Penalize abductive guess when the
     supporting argument comes from the partial answer, instead of from the
     current premise (default 4). Guesses involving the partial answer are
@@ -1004,8 +1018,8 @@
     <verbatim|.ml> file.
   </description>
 
-  Let us have a look at test-suite examples that need a non-default parameter
-  setting.
+  Let us have a look at tests from the <verbatim|examples> direcotory that
+  need a non-default parameter setting.
 
   <\code>
     $ ./invargent -inform examples/non_pointwise_leq.gadt
@@ -1017,7 +1031,7 @@
     \;
 
     Perhaps increase the -iterations_timeout parameter or try the
-    -more_existential option.
+    -more_existential option or -prefer_guess option.
 
     $ ./invargent -inform -prefer_guess examples/non_pointwise_leq.gadt
 
@@ -1037,47 +1051,52 @@
   <verbatim|non_pointwise_zip1_modified.gadt>. On the other hand,
   <verbatim|non_pointwise_zip1.gadt> is inferred with default settings.
 
+  The response from the system does not always include an option which would
+  make the inference succeed.
+
   <\code>
-    $ ./invargent -inform examples/liquid_heapsort_heapify_simpler.gadt
+    $ ./invargent -inform examples/liquid_simplex_step_3a.gadt
+
+    File "examples/liquid_simplex_step_3a.gadt", line 7, characters 49-1651:
 
-    val heapify :
+    No answer in type: Answers do not converge
 
-    \ \ <math|\<forall\>>k, n, a[0 <math|\<leqslant\>> n <math|\<wedge\>> n +
-    1 <math|\<leqslant\>> k].
+    \;
 
-    \ \ Num k <math|\<rightarrow\>> Array (a, k) <math|\<rightarrow\>> Num n
-    <math|\<rightarrow\>> ()
+    Perhaps do not pass the -no_dead_code flag.
 
-    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.gadti
+    Perhaps increase the -iterations_timeout parameter or try one of the
+    options: -<no-break>more_existential, -prefer_guess,
+    -prefer_bound_to_local.
 
-    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.ml
+    Perhaps some definition is used with requirements on
 
-    InvarGenT: Command "ocamlc -w -25 -c examples/liquid_heapsort_heapify_simpler.ml"
-    exited with code 0
+    its inferred postcondition not warranted by the definition.
 
-    $ ./invargent -inform -prefer_bound_to_local \\
-    examples/liquid_heapsort_heapify_simpler.gadt
+    $ ./invargent -inform -prefer_bound_to_local -only_off_by_1 \\
 
-    val heapify :
+    examples/liquid_simplex_step_3a.gadt
 
-    \ \ <math|\<forall\>>i, k, n, a[0 <math|\<leqslant\>> n <math|\<wedge\>>
-    n + 1 <math|\<leqslant\>> i <math|\<wedge\>> i <math|\<leqslant\>> k].
+    val main_step3_test : <math|\<forall\>>k, n[1 <math|\<leqslant\>> n
+    <math|\<wedge\>> 3 <math|\<leqslant\>> k]. Matrix (n, k)
+    <math|\<rightarrow\>> Float
 
-    \ \ Num i <math|\<rightarrow\>> Array (a, k) <math|\<rightarrow\>> Num n
-    <math|\<rightarrow\>> ()
+    InvarGenT: Generated file examples/liquid_simplex_step_3a.gadti
 
-    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.gadti
+    InvarGenT: Generated file examples/liquid_simplex_step_3a.ml
 
-    InvarGenT: Generated file examples/liquid_heapsort_heapify_simpler.ml
+    File "examples/liquid_simplex_step_3a.ml", line 43, characters 8-9:
 
-    InvarGenT: Command "ocamlc -w -25 -c examples/liquid_heapsort_heapify_simpler.ml"
+    Warning 26: unused variable m.
+
+    InvarGenT: Command "ocamlc -w -25 -c examples/liquid_simplex_step_3a.ml"
     exited with code 0
   </code>
 
-  Above, the type inferred with default parameter setting is insufficiently
-  general. Other examples that need the <verbatim|-prefer_bound_to_local>
-  option: <verbatim|liquid_simplex_step_3a.gadt>,
-  <verbatim|liquid_simplex_step_6a_2.gadt>.
+  The other examples that need the <verbatim|-prefer_bound_to_local> option,
+  but not the <verbatim|-<no-break>only_off_by_1> option:
+  <verbatim|liquid_simplex_step_6a_2.gadt>,
+  <verbatim|liquid_tower_harder.gadt>.
 
   <\code>
     $ ./invargent -inform examples/pointwise_zip2_harder.gadt
@@ -1322,14 +1341,8 @@
   n + 1].Num n> instead of <verbatim|<math|\<exists\>>k[k <math|\<leqslant\>>
   n <math|\<wedge\>> 0 <math|\<leqslant\>> k + 1].Num k>. The inference of
   the intended type succeeds after we introduce an appropriate assertion,
-  e.g. <verbatim|assert num -1 \<= hi>.
-
-  The example <verbatim|liquid_tower_harder.gadt> creates too complex an
-  abduction problem at a late iteration of the type inference problem.
-  Paradoxically, the example is harder than <verbatim|liquid_tower.gadt>,
-  despite the latter performing a joint inference of all the functions. The
-  <verbatim|liquid_tower.gadt> example leads to more parameter sharing and
-  thus easier abduction problems.
+  e.g. <verbatim|assert num -1 \<= hi>. Alternatively, we could include a use
+  case for <verbatim|bsearch> where the full postcondition is required.
 
   Examples <verbatim|liquid_simplex_step_3.gadt>,
   <verbatim|liquid_simplex_step_4.gadt> and
@@ -1357,14 +1370,16 @@
   intended postcondition.
 
   The example <verbatim|liquid_gauss_harder.gadt> poses too big a challenge
-  for InvarGenT. To get the example <verbatim|liquid_gauss.gadt> that passes
-  inference, we needed to modify it in two ways. One was streamlining one of
-  the nested definitions, to not introduce another, unnecessary level of
-  nesting. The other was to relax the constraint on the processed portion of
-  the matrix, coming from the restriction on the matrix size intended in the
-  original source of the <verbatim|liquid_gauss_harder.gadt> example. In
+  for InvarGenT. To get it pass the inference, we streamline one of the
+  nested definitions, to not introduce another, unnecessary level of nesting.
+  This gives the example <verbatim|liquid_gauss2.gadt>, which needs to be run
+  with the option <verbatim|-prefer_bound_to_local>. Additionally, we can
+  relax the constraint on the processed portion of the matrix, coming from
+  the restriction on the matrix size intended in the original source of the
+  <verbatim|liquid_gauss_harder.gadt> example. In
   <verbatim|liquid_gauss.gadt>, the whole matrix is processed and the
-  inferred type is most general.
+  inferred type is most general, under the default settings -- no need to
+  pass any options to InvarGenT.
 </body>
 
 <\initial>

examples/avl_tree.gadti.target

@@ -50,9 +50,9 @@ val remove_min_binding :
 
 val merge :
    ∀k, n, a[n ≤ k + 2 ∧ k ≤ n + 2].
-   (Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ i ≤ n + k ∧ k ≤ i ∧
+   (Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ k ≤ i ∧ i ≤ n + k ∧
      i≤max (k + 1, n + 1)].Avl (a, i)
 
 val remove :
    ∀n, a.
-   a → Avl (a, n) → ∃k[k ≤ n ∧ n ≤ k + 1 ∧ 0 ≤ k].Avl (a, k)
+   a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ 0 ≤ k ∧ k ≤ n].Avl (a, k)

examples/liquid_gauss2.gadt

@@ -0,0 +1,112 @@
+external type Matrix : num * num =
+  "(float, Bigarray.float64_elt, Bigarray.c_layout) Bigarray.Array2.t"
+external let matrix_make :
+  ∀n, k [0≤n ∧ 0≤k]. Num n → Num k → Matrix (n, k) =
+  "fun a b -> Bigarray.Array2.create Bigarray.float64 Bigarray.c_layout a b"
+external let matrix_get :
+  ∀n, k, i, j [0≤i ∧ i+1≤n ∧ 0≤j ∧ j+1≤k].
+   Matrix (n, k) → Num i → Num j → Float = "Bigarray.Array2.get"
+external let matrix_set :
+  ∀n, k, i, j [0≤i ∧ i+1≤n ∧ 0≤j ∧ j+1≤k].
+   Matrix (n, k) → Num i → Num j → Float → () = "Bigarray.Array2.set"
+external let matrix_dim1 :
+  ∀n, k [0≤n ∧ 0≤k]. Matrix (n, k) → Num n = "Bigarray.Array2.dim1"
+external let matrix_dim2 :
+  ∀n, k [0≤n ∧ 0≤k]. Matrix (n, k) → Num k = "Bigarray.Array2.dim2"
+
+datatype Array : type * num
+external let array_make :
+  ∀n, a [0≤n]. Num n → a → Array (a, n) = "fun a b -> Array.make a b"
+external let array_get :
+  ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a = "fun a b -> Array.get a b"
+external let array_set :
+  ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a → () =
+  "fun a b c -> Array.set a b c"
+external let array_length :
+  ∀n, a [0≤n]. Array (a, n) → Num n = "fun a -> Array.length a"
+
+external let n2f : ∀n. Num n → Float = "float_of_int"
+external let equal : ∀a. a → a → Bool = "fun x y -> x = y"
+external let leq : ∀a. a → a → Bool = "fun x y -> x <= y"
+external let less : ∀a. a → a → Bool = "fun x y -> x < y"
+
+external let minus : Float → Float → Float = "(-.)"
+external let plus : Float → Float → Float = "(+.)"
+external let mult : Float → Float → Float = "( *. )"
+external let div : Float → Float → Float = "( /. )"
+external let fabs : Float → Float = "abs_float"
+external let fl0 : Float = "0.0"
+external let fl1 : Float = "1.0"
+
+let getRow data i =
+  let stride = matrix_dim2 data in
+  let rowData = array_make stride fl0 in
+  let rec extract j =
+    if j + 1 <= stride then (
+      array_set rowData j (matrix_get data i j);
+      (* lukstafi: the call below missing in the original source? *)
+      extract (j + 1))
+    else () in
+  extract 0;
+  rowData
+
+let putRow data i row =
+  let stride = array_length row in
+  let rec put j =
+    if j + 1 <= stride then (
+      matrix_set data i j (array_get row j);
+      (* lukstafi: the call below missing in the original source? *)
+      put (j + 1))
+    else () in
+  put 0
+
+let rowSwap data i j =
+  let temp = getRow data i in
+  putRow data i (getRow data j);
+  putRow data j temp
+
+let norm r n i =
+  let x = array_get r i in
+  array_set r i fl1;
+  let rec loop k =
+    if k + 1 <= n then (
+      array_set r k (div (array_get r k) x);
+      loop (k+1))
+    else () in
+  loop (i+1)
+
+let rowElim r s n i =
+  let x = array_get s i in
+  array_set s i fl0;
+  let rec loop k =
+    if k + 1 <= n then (
+      array_set s k (minus (array_get s k) (mult x (array_get r k)));
+      loop (k+1))
+    else () in
+  loop (i+1)
+
+let gauss data =
+  let n = matrix_dim1 data in
+
+  let rec rowMax i j x mx =
+    eif j + 1 <= n then
+      let y = fabs (matrix_get data j i) in
+      eif (less x y) then rowMax i (j+1) y j
+      else rowMax i (j+1) x mx
+    else mx in
+
+  let rec loop1 i =
+    if i + 1 <= n then
+      let x = fabs (matrix_get data i i) in
+      let mx = rowMax i (i+1) x i in
+      norm (getRow data mx) (n+1) i;
+      rowSwap data i mx;
+      let rec loop2 j =
+        if j + 1 <= n then (
+          rowElim (getRow data i) (getRow data j) (n+1) i;
+          loop2 (j+1))
+        else () in
+      loop2 (i+1);
+      loop1 (i+1)
+    else () in
+  loop1 0

examples/liquid_gauss2.gadti.target

@@ -0,0 +1,74 @@
+external type Matrix : num * num
+
+external val matrix_make :
+   ∀n, k[0 ≤ n ∧ 0 ≤ k]. Num n → Num k → Matrix (n, k)
+
+external val matrix_get :
+   ∀n, k, i, j[0 ≤ i ∧ i + 1 ≤ n ∧ 0 ≤ j ∧ j + 1 ≤ k].
+   Matrix (n, k) → Num i → Num j → Float
+
+external val matrix_set :
+   ∀n, k, i, j[0 ≤ i ∧ i + 1 ≤ n ∧ 0 ≤ j ∧ j + 1 ≤ k].
+   Matrix (n, k) → Num i → Num j → Float → ()
+
+external val matrix_dim1 :
+   ∀n, k[0 ≤ n ∧ 0 ≤ k]. Matrix (n, k) → Num n
+
+external val matrix_dim2 :
+   ∀n, k[0 ≤ n ∧ 0 ≤ k]. Matrix (n, k) → Num k
+
+datatype Array : type * num
+
+external val array_make : ∀n, a[0 ≤ n]. Num n → a → Array (a, n)
+
+external val array_get :
+   ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a
+
+external val array_set :
+   ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a → ()
+
+external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n
+
+external val n2f : ∀n. Num n → Float
+
+external val equal : ∀a. a → a → Bool
+
+external val leq : ∀a. a → a → Bool
+
+external val less : ∀a. a → a → Bool
+
+external val minus : Float → Float → Float
+
+external val plus : Float → Float → Float
+
+external val mult : Float → Float → Float
+
+external val div : Float → Float → Float
+
+external val fabs : Float → Float
+
+external val fl0 : Float
+
+external val fl1 : Float
+
+val getRow :
+   ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i].
+   Matrix (i, n) → Num k → Array (Float, n)
+
+val putRow :
+   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j].
+   Matrix (i, j) → Num k → Array (Float, n) → ()
+
+val rowSwap :
+   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
+   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+
+val norm :
+   ∀i, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i].
+   Array (Float, i) → Num k → Num n → ()
+
+val rowElim :
+   ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
+   Array (Float, j) → Array (Float, i) → Num k → Num n → ()
+
+val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()