From 9e3c875e077205210ee401e02345b8098a36a5de Mon Sep 17 00:00:00 2001
From: lukstafi <lukstafi@gmail.com>
Date: Thu, 19 Feb 2015 06:24:18 +0100
Subject: [PATCH] New numerical abduction knobs and variants of the tower
 (passing) and Gauss (not yet tuned) examples with assertions.

---
 doc/invargent-manual.tm                     |  24 +++--
 examples/liquid_gauss_asserted.gadt         | 113 ++++++++++++++++++++
 examples/liquid_gauss_harder_asserted.gadt  | 113 ++++++++++++++++++++
 examples/liquid_gauss_simpler_asserted.gadt |  87 +++++++++++++++
 examples/liquid_tower_asserted.gadt         |  75 +++++++++++++
 examples/liquid_tower_asserted.gadti.target |  33 ++++++
 src/InvarGenT.ml                            |  14 ++-
 src/InvarGenTTest.ml                        |  40 ++++++-
 src/NumS.ml                                 |  12 ++-
 src/NumS.mli                                |  16 ++-
 10 files changed, 504 insertions(+), 23 deletions(-)
 create mode 100644 examples/liquid_gauss_asserted.gadt
 create mode 100644 examples/liquid_gauss_harder_asserted.gadt
 create mode 100644 examples/liquid_gauss_simpler_asserted.gadt
 create mode 100644 examples/liquid_tower_asserted.gadt
 create mode 100644 examples/liquid_tower_asserted.gadti.target

diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm
index 0bdc55c..25ca420 100644
--- a/doc/invargent-manual.tm
+++ b/doc/invargent-manual.tm
@@ -864,16 +864,20 @@
     <item*|<strong|<verbatim|-abd_pow_scaling>>>Scale the complexity cost of
     coefficients according to the given power.
 
-    <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|-prefer_bound_to_local>>Prefer a 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 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|-only_off_by_1>>Limit the effect of
+    <verbatim|-prefer_bound_to_local> and
+    <verbatim|-<no-break>prefer_bound_to_outer> to inequalities with a
+    constant 1. This corresponds to an upper bound of an index into a
+    zero-indexed array/matrix/etc.
 
     <item*|<verbatim|-concl_abd_penalty>>Penalize abductive guess when the
     supporting argument comes from the partial answer, instead of from the
diff --git a/examples/liquid_gauss_asserted.gadt b/examples/liquid_gauss_asserted.gadt
new file mode 100644
index 0000000..bd00791
--- /dev/null
+++ b/examples/liquid_gauss_asserted.gadt
@@ -0,0 +1,113 @@
+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
+  assert type n + 1 = matrix_dim2 data;
+
+  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
diff --git a/examples/liquid_gauss_harder_asserted.gadt b/examples/liquid_gauss_harder_asserted.gadt
new file mode 100644
index 0000000..bd00791
--- /dev/null
+++ b/examples/liquid_gauss_harder_asserted.gadt
@@ -0,0 +1,113 @@
+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
+  assert type n + 1 = matrix_dim2 data;
+
+  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
diff --git a/examples/liquid_gauss_simpler_asserted.gadt b/examples/liquid_gauss_simpler_asserted.gadt
new file mode 100644
index 0000000..4d112c1
--- /dev/null
+++ b/examples/liquid_gauss_simpler_asserted.gadt
@@ -0,0 +1,87 @@
+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"
+
+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 → ()
+
+let gauss data =
+  let n = matrix_dim1 data in
+  let m = matrix_dim2 data in
+  assert type n + 1 = m;
+
+  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) m i;
+      rowSwap data i mx;
+      let rec loop2 j =
+        if j + 1 <= n then (
+          rowElim (getRow data i) (getRow data j) m i;
+          loop2 (j+1))
+        else () in
+      loop2 (i+1);
+      loop1 (i+1)
+    else () in
+  loop1 0
diff --git a/examples/liquid_tower_asserted.gadt b/examples/liquid_tower_asserted.gadt
new file mode 100644
index 0000000..e421c20
--- /dev/null
+++ b/examples/liquid_tower_asserted.gadt
@@ -0,0 +1,75 @@
+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 n2i : ∀n. Num n → Int = "fun i -> i"
+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 print : String → () = "print_string"
+external let string_make : Int → String → String =
+  "fun n s -> String.make n s.[0]"
+external let string_of_int : Int → String = "string_of_int"
+
+external let abs : Int → Int = "fun i -> if i < 0 then ~-i else i"
+external let minus : Int → Int → Int = "(-)"
+external let plus : Int → Int → Int = "(+)"
+external let int0 : Int = "0"
+
+let play sz =
+  let leftPost = array_make sz int0 in
+  let middlePost = array_make sz int0 in
+  let rightPost = array_make sz int0 in
+
+  let initialize post =
+    let rec init_rec i =
+      if i + 1 <= sz - 1 then (
+        array_set post i (n2i (i+1));
+        init_rec (i+1))
+      else () in
+    init_rec 0 in
+
+  let showpiece n =
+    let rec r_rec i =
+      if leq (plus i (n2i 2)) n then (
+        print " "; r_rec (plus i (n2i 1)))
+      else () in
+    let rec r2_rec j =
+      if leq (plus j (n2i 1)) (n2i sz)
+      then (print "#"; r2_rec (plus j (n2i 1)))
+      else () in
+    r_rec (n2i 1);
+    r2_rec (plus n (n2i 1)) in
+
+  let showposts () =
+    let rec show_rec i =
+      if i + 1 <= sz - 1 then (
+        showpiece (array_get leftPost i); print " ";
+        showpiece (array_get middlePost i); print " ";
+        showpiece (array_get rightPost i); print "\n";
+        show_rec (i+1))
+      else () in
+    show_rec 0; print "\n" in
+
+  initialize leftPost;
+  let rec move n source s post p post' p' =
+    assert num s + n <= sz;
+    if n <= 1 then (
+      array_set post (p - 1) (array_get source s);
+      array_set source s int0; showposts ())
+    else (
+      move (n - 1) source s post' p' post p;
+      array_set post (p - 1) (array_get source (s + n - 1));
+      array_set source (s + n - 1) int0;
+      showposts ();
+      move (n - 1) post' ((p' - n) + 1) post (p - 1) source (s + n)) in
+
+  showposts ();
+  move sz leftPost 0 rightPost sz middlePost sz
diff --git a/examples/liquid_tower_asserted.gadti.target b/examples/liquid_tower_asserted.gadti.target
new file mode 100644
index 0000000..a67b6fe
--- /dev/null
+++ b/examples/liquid_tower_asserted.gadti.target
@@ -0,0 +1,33 @@
+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 n2i : ∀n. Num n → Int
+
+external val equal : ∀a. a → a → Bool
+
+external val leq : ∀a. a → a → Bool
+
+external val print : String → ()
+
+external val string_make : Int → String → String
+
+external val string_of_int : Int → String
+
+external val abs : Int → Int
+
+external val minus : Int → Int → Int
+
+external val plus : Int → Int → Int
+
+external val int0 : Int
+
+val play : ∀n[1 ≤ n]. Num n → ()
diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml
index ef1154c..564ed14 100644
--- a/src/InvarGenT.ml
+++ b/src/InvarGenT.ml
@@ -127,6 +127,9 @@ let main () =
     "-affine_penalty", Arg.Set_int NumS.affine_penalty,
     "How much to penalize an abduction candidate inequality for \
      containing a constant term (default 4)";
+    "-reward_constrn", Arg.Set_int NumS.reward_constrn,
+    "How much to reward introducing a constraint on so-far \
+     unconstrained varialbe, or penalize if negative (default 2)";
     "-complexity_penalty", Arg.Set_float NumS.complexity_penalty,
     "How much to penalize for complexity; the coefficient of either \
      the linear (default) or power scaling (default 2.5)";
@@ -136,11 +139,14 @@ let main () =
     "-abd_pow_scaling", Arg.Float set_pow_scaling,
     "Scale the complexity cost of coefficients according to the given power";
     "-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 a 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";
+    "Prefer a bound coming from outer scope, to inequality between \
+     two outer scope parameters";
+    "-only_off_by_1", Arg.Set NumS.only_off_by_1,
+    "Limit the effect of -prefer_bound_to_local and \
+     -prefer_bound_to_outer to inequalities with a constant 1";
     "-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)";
diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml
index 79a635a..d0f3c5e 100644
--- a/src/InvarGenTTest.ml
+++ b/src/InvarGenTTest.ml
@@ -20,6 +20,7 @@ let input_file file =
 let test_case ?(test_annot=false) ?(do_ml=true)
     ?richer_answers ?more_general_num
     ?prefer_guess ?prefer_bound_to_local ?prefer_bound_to_outer
+    ?only_off_by_1 ?reward_constrn
     ?abd_rotations ?num_abd_timeout
     ?num_abd_fail_timeout ?nodeadcode file () =
   if !debug then Printexc.record_backtrace true;
@@ -57,6 +58,16 @@ let test_case ?(test_annot=false) ?(do_ml=true)
    | None -> ()
    | Some prefer_bound_to_outer ->
      NumS.prefer_bound_to_outer := prefer_bound_to_outer);
+  let old_only_off_by_1 = !NumS.only_off_by_1 in
+  (match only_off_by_1 with
+   | None -> ()
+   | Some only_off_by_1 ->
+     NumS.only_off_by_1 := only_off_by_1);
+  let old_reward_constrn = !NumS.reward_constrn in
+  (match reward_constrn with
+   | None -> ()
+   | Some reward_constrn ->
+     NumS.reward_constrn := reward_constrn);
   let old_abd_rotations = !NumS.abd_rotations in
   (match abd_rotations with
    | None -> ()
@@ -101,6 +112,8 @@ let test_case ?(test_annot=false) ?(do_ml=true)
      Abduction.prefer_guess := old_prefer_guess;
      NumS.prefer_bound_to_local := old_prefer_bound_to_local;
      NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
+     NumS.only_off_by_1 := old_only_off_by_1;
+     NumS.reward_constrn := old_reward_constrn;
      NumS.abd_rotations := old_abd_rotations;
      NumS.abd_timeout_count := old_num_abd_timeout;
      NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -112,6 +125,8 @@ let test_case ?(test_annot=false) ?(do_ml=true)
      Abduction.prefer_guess := old_prefer_guess;
      NumS.prefer_bound_to_local := old_prefer_bound_to_local;
      NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
+     NumS.only_off_by_1 := old_only_off_by_1;
+     NumS.reward_constrn := old_reward_constrn;
      NumS.abd_rotations := old_abd_rotations;
      NumS.abd_timeout_count := old_num_abd_timeout;
      NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -122,6 +137,8 @@ let test_case ?(test_annot=false) ?(do_ml=true)
   Abduction.prefer_guess := old_prefer_guess;
   NumS.prefer_bound_to_local := old_prefer_bound_to_local;
   NumS.prefer_bound_to_outer := old_prefer_bound_to_outer;
+  NumS.only_off_by_1 := old_only_off_by_1;
+  NumS.reward_constrn := old_reward_constrn;
   NumS.abd_rotations := old_abd_rotations;
   NumS.abd_timeout_count := old_num_abd_timeout;
   NumS.abd_fail_timeout_count := old_num_abd_fail_timeout;
@@ -490,6 +507,11 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            skip_if !debug "debug";
            test_case "liquid_tower_simpler" ());
+      "liquid_tower_asserted" >::
+        (fun () ->
+           skip_if !debug "debug";
+           test_case ~prefer_bound_to_local:true
+             ~reward_constrn:(-1) "liquid_tower_asserted" ());
       "liquid_tower" >::
         (fun () ->
            skip_if !debug "debug";
@@ -553,7 +575,8 @@ 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_bound_to_local:true "liquid_simplex_step_3a" ());
+           test_case ~prefer_bound_to_local:true
+             ~only_off_by_1:true "liquid_simplex_step_3a" ());
       "liquid_simplex_step_4" >::
         (fun () ->
            todo "too hard for current InvarGenT";
@@ -627,10 +650,25 @@ let tests = "InvarGenT" >::: [
         (fun () ->
            skip_if !debug "debug";
            test_case "liquid_gauss_simpler" ());
+      "liquid_gauss_simpler_asserted" >::
+        (fun () ->
+           todo "FIXME";
+           skip_if !debug "debug";
+           test_case "liquid_gauss_simpler_asserted" ());
       "liquid_gauss" >::
         (fun () ->
            skip_if !debug "debug";
            test_case "liquid_gauss" ());
+      "liquid_gauss_asserted" >::
+        (fun () ->
+           todo "FIXME";
+           skip_if !debug "debug";
+           test_case "liquid_gauss_asserted" ());
+      "liquid_gauss_harder_asserted" >::
+        (fun () ->
+           todo "too hard for current numerical abudction";
+           skip_if !debug "debug";
+           test_case "liquid_gauss_harder_asserted" ());
       "liquid_gauss_harder" >::
         (fun () ->
            todo "too hard for current numerical abudction";
diff --git a/src/NumS.ml b/src/NumS.ml
index 3268aa7..96054cb 100644
--- a/src/NumS.ml
+++ b/src/NumS.ml
@@ -25,7 +25,7 @@ let general_reward = ref 2
 let affine_penalty = ref (* 4 *)3
 let affine_threshold = ref 2
 let affine_thresh_penalty = ref 2
-let reward_constrn = ref 2
+let reward_constrn = ref 2 (* (-1) *)
 let complexity_penalty = ref 2.5
 let reward_locality = ref 3
 let multi_levels_penalty = ref 4
@@ -39,6 +39,7 @@ let special_source_bonus = ref 7
 let uplevel_penalty = ref 9
 let prefer_bound_to_local = ref false
 let prefer_bound_to_outer = ref false
+let only_off_by_1 = ref false
 let concl_abd_penalty = ref 4
 let discourage_upper_bound = ref 6
 let discourage_already_bounded = ref 4
@@ -1506,7 +1507,8 @@ let abd_cands ~cmp_v ~qcmp_v ~cmp_w ~uni_v ~orig_ren ~b_of_v ~upward_of
     else [] in
   let down_v, skip_uplevel =
     match vars with
-    | [v, _; v2, _] -> v, upward_of v2 v && cst =/ !/1
+    | [v, _; v2, _] -> v, upward_of v2 v &&
+                          (not !only_off_by_1 || cst =/ !/1)
     | (v, _)::_ -> v, false
     | _ -> assert false in
   (*[* if !more_general
@@ -1663,7 +1665,8 @@ let abd_cands ~cmp_v ~qcmp_v ~cmp_w ~uni_v ~orig_ren ~b_of_v ~upward_of
            let i2f = float_of_int and f2i = int_of_float in
            let special_bonus () =
              if prem_abduced = None &&
-                cst =/ !/1 && List.tl score_ineqn = [] then
+                (not !only_off_by_1 || cst =/ !/1) &&
+                List.tl score_ineqn = [] then
                let nonlocal_pair =
                  match vars with
                  | (v, _)::(v2, _)::[] -> upward_of v2 v
@@ -2080,6 +2083,9 @@ let abd_simple ~qcmp_v ~cmp_w
           ()
       done; None
     with Result (ans_eqs, ans_ineqs, ans_optis, ans_suboptis) ->
+      (*[* Format.printf "NumS.abd_simple: result:\
+             @\neqs=@ %a@\nineqs=@ %a@\n%!"
+        pr_w_subst ans_eqs pr_ineqs ans_ineqs; *]*)
       Some (ans_eqs, ans_ineqs, ans_optis, ans_suboptis)
   with (* failed premise/\conclusion *)
   | Terms.Contradiction _ -> None
diff --git a/src/NumS.mli b/src/NumS.mli
index 039d2a9..bf09f3e 100644
--- a/src/NumS.mli
+++ b/src/NumS.mli
@@ -34,19 +34,25 @@ val discard_penalty : int ref
 (** How much to penalize an abduction candidate inequality for
     containing a constant term. Default [4]. *)
 val affine_penalty : int ref
+(** How much to reward introducing a constraint on so-far
+    unconstrained varialbe (or penalize, if negative). Default [2]. *)
+val reward_constrn : int ref
 (** How much to penalize for complexity; the coefficient $a$ in the
     description of {!complexity_scale}. Default [2.5]. *)
 val complexity_penalty : float ref
 (** How much to penalize for variables that are not parameters but
     instead instances from use sites of existential types. Default [6]. *)
 val nonparam_vars_penalty : int ref
-(** Prefer a zero-indexed array/matrix/etc. bound coming from outer
-    scope, to inequality between two local parameters. Default [false]. *)
+(** Prefer bound coming from outer scope, to inequality between two
+    local parameters. Default [false]. *)
 val prefer_bound_to_local : bool ref
-(** Prefer a zero-indexed array/matrix/etc. bound coming from outer
-    scope, to inequality between two outer scope parameters.
-    Default [false]. *)
+(** Prefer a bound coming from outer scope, to inequality between two
+    outer scope parameters. Default [false]. *)
 val prefer_bound_to_outer : bool ref
+(** Limit the effect of [prefer_bound_to_local] and
+    [prefer_bound_to_outer] to inequalities with a constant 1. This
+    corresponds to an upper bound of zero-indexed array/matrix/etc. *)
+val only_off_by_1 : bool ref
 (** Penalize abductive guess when the supporting argument comes from
     the partial answer, instead of from the current premise. Default [4]. *)
 val concl_abd_penalty : int ref