Abudction heuristic changes. Check for definiton-site counterparts of…

… use-site variables. Another special-case heuristic setting.

doc/invargent-manual.tm

@@ -875,12 +875,17 @@
     <item*|<strong|<verbatim|-abd_pow_scaling>>>Scale the complexity cost of
     coefficients according to the given power.
 
-    <item*|<verbatim|-prefer_source_bound>>Prefer a zero-indexed
+    <item*|<verbatim|-prefer_bound_to_local>>Prefer a zero-indexed
     array/matrix/etc. bound coming from outer scope, to inequality between
     two local parameters. In numerical abduction heuristic, such bounds are
     usually doubly penalized: for having a constant, and non-locality of
     parameters.
 
+    <item*|<verbatim|-prefer_bound_to_outer>>Prefer a zero-indexed
+    array/matrix/etc. bound coming from outer scope, to inequality between
+    two outer scope parameters. Outer-scope constraints sometimes lead to an
+    answer not general enough.
+
     <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

examples/liquid_gauss_simpler.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
+
+external getRow :
+   ∀n, k, i[0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ n].
+   Matrix (n, k) → Num i → Array (Float, k)
+
+external putRow :
+   ∀n, k, i, j[0 ≤ j ∧ 0 ≤ i ∧ i + 1 ≤ n ∧ j ≤ k].
+   Matrix (n, k) → Num i → Array (Float, j) → ()
+
+external rowSwap :
+   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
+   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+
+external norm :
+   ∀i, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i].
+   Array (Float, i) → Num k → Num n → ()
+
+external 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[0 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()

src/Abduction.ml

@@ -800,7 +800,7 @@ type discarded =
   (TermAbd.answer list, NumDefs.formula list,
    OrderDefs.formula list, unit) sep_sorts
 
-let abd q ~bvs ~xbvs ~upward_of ~nonparam_vars
+let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars
     ?(iter_no=2) ~discard brs neg_brs =
   let dissociate = iter_no <= 0 in
   (* Do not change the order and no. of branches afterwards. *)
@@ -1001,7 +1001,7 @@ let abd q ~bvs ~xbvs ~upward_of ~nonparam_vars
     else
       try
         (* [tvs] includes alien variables! *)
-        NumS.abd q ~bvs ~xbvs ~upward_of ~nonparam_vars
+        NumS.abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars
           ~discard:discard.at_num ~iter_no
           (* [true] means non-recursive *)
           ((true, [], [], neg_num_res)::brs_num)

src/Abduction.mli

@@ -82,6 +82,8 @@ val abd :
   Defs.quant_ops ->
   bvs:Defs.VarSet.t ->
   xbvs:(int * Defs.VarSet.t) list ->
+  ?orig_ren:((Defs.var_name, Defs.var_name) Hashtbl.t) ->
+  ?b_of_v:(Defs.var_name -> Defs.var_name) ->
   upward_of:(Defs.var_name -> Defs.var_name -> bool) ->
   nonparam_vars:Defs.VarSet.t ->
   ?iter_no:int ->

src/InvarGenT.ml

@@ -135,9 +135,12 @@ let main () =
      the given height after coefficient 1 (default 2.0)";
     "-abd_pow_scaling", Arg.Float set_pow_scaling,
     "Scale the complexity cost of coefficients according to the given power";
-    "-prefer_source_bound", Arg.Set NumS.prefer_source_bound,
+    "-prefer_bound_to_local", Arg.Set NumS.prefer_bound_to_local,
     "Prefer a zero-indexed array/matrix/etc. bound coming from outer \
      scope, to inequality between two local parameters";
+    "-prefer_bound_to_outer", Arg.Set NumS.prefer_bound_to_outer,
+    "Prefer a zero-indexed array/matrix/etc. bound coming from outer \
+     scope, to inequality between two outer scope parameters";
     "-concl_abd_penalty", Arg.Set_int NumS.concl_abd_penalty,
     "Penalize abductive guess when the supporting argument comes from \
      the partial answer, instead of from the current premise (default 4)";

src/InvarGenTTest.ml

@@ -18,7 +18,8 @@ let input_file file =
   Buffer.contents buf
 
 let test_case ?(test_annot=false) ?richer_answers ?more_general_num
-    ?prefer_guess ?prefer_source_bound ?abd_rotations ?num_abd_timeout
+    ?prefer_guess ?prefer_bound_to_local ?prefer_bound_to_outer
+    ?abd_rotations ?num_abd_timeout
     ?num_abd_fail_timeout ?nodeadcode file () =
   if !debug then Printexc.record_backtrace true;
   let ntime = Sys.time () in
@@ -45,11 +46,16 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
   (match prefer_guess with
    | None -> ()
    | Some prefer_guess -> Abduction.prefer_guess := prefer_guess);
-  let old_prefer_source_bound = !NumS.prefer_source_bound in
-  (match prefer_source_bound with
+  let old_prefer_bound_to_local = !NumS.prefer_bound_to_local in
+  (match prefer_bound_to_local with
    | None -> ()
-   | Some prefer_source_bound ->
-     NumS.prefer_source_bound := prefer_source_bound);
+   | Some prefer_bound_to_local ->
+     NumS.prefer_bound_to_local := prefer_bound_to_local);
+  let old_prefer_bound_to_outer = !NumS.prefer_bound_to_outer in
+  (match prefer_bound_to_outer with
+   | None -> ()
+   | Some prefer_bound_to_outer ->
+     NumS.prefer_bound_to_outer := prefer_bound_to_outer);
   let old_abd_rotations = !NumS.abd_rotations in
   (match abd_rotations with
    | None -> ()
@@ -92,7 +98,8 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
      Abduction.richer_answers := old_richer_answers;
      NumS.more_general := old_more_general_num;
      Abduction.prefer_guess := old_prefer_guess;
-     NumS.prefer_source_bound := old_prefer_source_bound;
+     NumS.prefer_bound_to_local := old_prefer_bound_to_local;
+     NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
      NumS.abd_rotations := old_abd_rotations;
      NumS.abd_timeout_count := old_num_abd_timeout;
      NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -102,7 +109,8 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
      Abduction.richer_answers := old_richer_answers;
      NumS.more_general := old_more_general_num;
      Abduction.prefer_guess := old_prefer_guess;
-     NumS.prefer_source_bound := old_prefer_source_bound;
+     NumS.prefer_bound_to_local := old_prefer_bound_to_local;
+     NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
      NumS.abd_rotations := old_abd_rotations;
      NumS.abd_timeout_count := old_num_abd_timeout;
      NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -111,7 +119,8 @@ let test_case ?(test_annot=false) ?richer_answers ?more_general_num
   Abduction.richer_answers := old_richer_answers;
   NumS.more_general := old_more_general_num;
   Abduction.prefer_guess := old_prefer_guess;
-  NumS.prefer_source_bound := old_prefer_source_bound;
+  NumS.prefer_bound_to_local := old_prefer_bound_to_local;
+  NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
   NumS.abd_rotations := old_abd_rotations;
   NumS.abd_timeout_count := old_num_abd_timeout;
   NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -508,7 +517,7 @@ let tests = "InvarGenT" >::: [
       "liquid_heapsort-heapify-simpler" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_source_bound:true
+           test_case ~prefer_bound_to_local:true
              "liquid_heapsort_heapify_simpler" ());
       "liquid_heapsort-heapify-simpler2" >::
         (fun () ->
@@ -555,7 +564,7 @@ let tests = "InvarGenT" >::: [
            skip_if !debug "debug";
            (* Type in target is slightly less general than most general type:
               ∀k, n[1 ≤ n ∧ 3 ≤ k]. Matrix (n, k) → Float *)
-           test_case ~prefer_source_bound:true "liquid_simplex_step_3a" ());
+           test_case ~prefer_bound_to_local:true "liquid_simplex_step_3a" ());
       "liquid_simplex_step_4" >::
         (fun () ->
            todo "FIXME"; (* "too hard for current InvarGenT"; ? *)
@@ -580,7 +589,7 @@ let tests = "InvarGenT" >::: [
       "liquid_simplex_step_6a_2" >::
         (fun () ->
            skip_if !debug "debug";
-           test_case ~prefer_source_bound:true
+           test_case ~prefer_bound_to_local:true
              "liquid_simplex_step_6a_2" ());
       "liquid_simplex_step_6_3" >::
         (fun () ->
@@ -627,9 +636,8 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_gauss_rowMax_2" ());
       "liquid_gauss_simpler" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
-           test_case "liquid_gauss_simpler" ());
+           test_case ~prefer_bound_to_outer:true "liquid_gauss_simpler" ());
       "liquid_gauss" >::
         (fun () ->
            todo "FIXME";