diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index a242d84..40a2600 100644 Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index 25ca420..f730a1e 100644 --- a/doc/invargent-manual.tm +++ b/doc/invargent-manual.tm @@ -819,6 +819,10 @@ abduction. This makes it faster but less likely to find the correct solution. + >The iteration at which to start + truncating postconditions by only keeping atoms present in the previous + iteration, to force convergence (default 8). + >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 , which in the following step will force an answer , then , etc. + >How much to reward introducing a + constraint on so-far unconstrained varialbe, or penalize if negative + (default 2). + >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. + >Do not treat definitions with + positive assertions (, ) + specially. The special treatment is currently equivalent to passing + reward_constrn -1> and + . + >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 @@ file. - 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 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 @@ . On the other hand, 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 - \ \ >k, n, a[0 > n > n + - 1 > k]. + \; - \ \ Num k > Array (a, k) > Num n - > () + 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: -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 - \ \ >i, k, n, a[0 > n > - n + 1 > i > i > k]. + val main_step3_test : >k, n[1 > n + > 3 > k]. Matrix (n, k) + > Float - \ \ Num i > Array (a, k) > Num n - > () + 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 - Above, the type inferred with default parameter setting is insufficiently - general. Other examples that need the - option: , - . + The other examples that need the option, + but not the only_off_by_1> option: + , + . <\code> $ ./invargent -inform examples/pointwise_zip2_harder.gadt @@ -1322,14 +1341,8 @@ n + 1].Num n> instead of >k[k > n > 0 > k + 1].Num k>. The inference of the intended type succeeds after we introduce an appropriate assertion, - e.g. . - - The example creates too complex an - abduction problem at a late iteration of the type inference problem. - Paradoxically, the example is harder than , - despite the latter performing a joint inference of all the functions. The - example leads to more parameter sharing and - thus easier abduction problems. + e.g. . Alternatively, we could include a use + case for where the full postcondition is required. Examples , and @@ -1357,14 +1370,16 @@ intended postcondition. The example poses too big a challenge - for InvarGenT. To get the example 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 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 , which needs to be run + with the option . 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 + example. In , 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. <\initial> diff --git a/examples/avl_tree.gadti.target b/examples/avl_tree.gadti.target index d022904..5f82172 100644 --- a/examples/avl_tree.gadti.target +++ b/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) diff --git a/examples/liquid_gauss2.gadt b/examples/liquid_gauss2.gadt new file mode 100644 index 0000000..4de36f8 --- /dev/null +++ b/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 diff --git a/examples/liquid_gauss2.gadti.target b/examples/liquid_gauss2.gadti.target new file mode 100644 index 0000000..2ece992 --- /dev/null +++ b/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) → () diff --git a/examples/liquid_gauss_asserted.gadti.target b/examples/liquid_gauss_asserted.gadti.target new file mode 100644 index 0000000..caa45d5 --- /dev/null +++ b/examples/liquid_gauss_asserted.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 : ∀n[1 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_gauss_harder_asserted.gadti.target b/examples/liquid_gauss_harder_asserted.gadti.target new file mode 100644 index 0000000..caa45d5 --- /dev/null +++ b/examples/liquid_gauss_harder_asserted.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 : ∀n[1 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_gauss_simpler_asserted.gadti.target b/examples/liquid_gauss_simpler_asserted.gadti.target new file mode 100644 index 0000000..e536283 --- /dev/null +++ b/examples/liquid_gauss_simpler_asserted.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 : ∀n[1 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_tower_harder.gadti.target b/examples/liquid_tower_harder.gadti.target index d674c75..dcb20be 100644 --- a/examples/liquid_tower_harder.gadti.target +++ b/examples/liquid_tower_harder.gadti.target @@ -35,11 +35,11 @@ val initialize : ∀k, n[n ≤ k + 1]. Array (Int, k) → Num n → () val showpiece : Int → Int → () val showposts : - ∀i, k, n[i ≤ n + 1 ∧ i ≤ k + 1 ∧ 0 ≤ i]. + ∀i, k, n[1 ≤ k ∧ 0 ≤ i ∧ i ≤ n + 1 ∧ i ≤ k]. Array (Int, i) → Array (Int, k) → Array (Int, n) → () val move : - ∀i, j, k, n[n ≤ m ∧ k ≤ m ∧ i + j ≤ m ∧ i + 1 ≤ m ∧ - j ≤ k ∧ j ≤ n + 1 ∧ 0 ≤ i ∧ 1 ≤ k]. - Num j → Array (Int, m) → Num i → Array (Int, m) → - Num k → Array (Int, m) → Num n → () + ∀i, j, k, m, n[n ≤ k ∧ 1 ≤ i ∧ i ≤ k ∧ 0 ≤ j ∧ + j + 1 ≤ k ∧ 0 ≤ m ∧ m ≤ n + 1 ∧ j + m ≤ k ∧ m ≤ i]. + Num m → Array (Int, k) → Num j → Array (Int, k) → Num i → + Array (Int, k) → Num n → () diff --git a/src/Infer.ml b/src/Infer.ml index 25a0f68..9272a88 100644 --- a/src/Infer.ml +++ b/src/Infer.ml @@ -429,6 +429,8 @@ let impl prem concl = let letin_count = ref 0 +let uses_pos_assertions = ref false + let constr_gen_expr gamma e t = let elim_extype = ref [] and preserve = ref [] in let rec aux gamma t e : cnstrnt * iexpr = @@ -536,6 +538,7 @@ let constr_gen_expr gamma e t = | Letin (_, _, (RuntimeFailure _ as e1), _, _) -> aux gamma t e1 | AssertLeq (e1, e2, e3, loc) -> + uses_pos_assertions := true; let a1 = fresh_var Num_sort in let t1 = TVar a1 in let a2 = fresh_var Num_sort in @@ -552,6 +555,7 @@ let constr_gen_expr gamma e t = Ex (vars_of_list [a1; a2], cn), AssertLeq (e1, e2, e3, loc) | AssertEqty (e1, e2, e3, loc) -> + uses_pos_assertions := true; let a1 = fresh_typ_var () in let t1 = TVar a1 in let a2 = fresh_typ_var () in @@ -998,6 +1002,7 @@ let infer_prog solver prog = let pat_loc = match it with | LetVal (_, PVar (_, lc), _, _, _) -> Some lc | _ -> None in + uses_pos_assertions := false; let chi_id, _, cn, e, tests, elim_cells, preserve = constr_gen_letrec ~nonrec:(pat_loc<>None) !gamma x e sig_cn t tests in @@ -1005,7 +1010,9 @@ let infer_prog solver prog = pr_cnstrnt cn; *]*) let preserve = add_vars preserve (VarSet.union (fvs_typ t) (fvs_formula sig_cn)) in - let q, phi_res, sb_chi = solver ~new_ex_types ~preserve cn in + let q, phi_res, sb_chi = + solver ~uses_pos_assertions:!uses_pos_assertions + ~new_ex_types ~preserve cn in let elim_extypes = concat_map (!) elim_cells in let nice_sb, (vs, phi) = try nice_ans (List.assoc chi_id sb_chi) @@ -1063,6 +1070,7 @@ let infer_prog solver prog = let ta = TVar a in VarSet.singleton a, [], [], ta | Some (vs, phi, t) -> VarSet.empty, vs, phi, t in + uses_pos_assertions := false; let bs, exphi, env, cn, (p, e), elim_cell, preserve = constr_gen_let !gamma p e t in (*[* Format.printf "LetVal: p=%a@\ninit_cn=%a@\n%!" pr_pat p @@ -1077,7 +1085,9 @@ let infer_prog solver prog = if VarSet.is_empty avs then cn else Ex (avs, cn) in (*[* Format.printf "LetVal: p=%a@\ncn=%a@\n%!" pr_pat p pr_cnstrnt cn; *]*) - let q, phi, sb_chi = solver ~new_ex_types ~preserve cn in + let q, phi, sb_chi = solver + ~uses_pos_assertions:!uses_pos_assertions + ~new_ex_types ~preserve cn in let elim_extypes = !elim_cell in let sb, phi = separate_subst ~bvs:preserve ~apply:true q phi in diff --git a/src/Infer.mli b/src/Infer.mli index 899473d..bf443bb 100644 --- a/src/Infer.mli +++ b/src/Infer.mli @@ -50,8 +50,11 @@ type solution = (int * (Defs.var_name list * Terms.formula)) list val infer_prog_mockup : program -> (int * Defs.loc) list * Defs.VarSet.t * cnstrnt + +(** Exported only for testing purposes. *) +val uses_pos_assertions : bool ref val infer_prog : - (new_ex_types:(int * Defs.loc) list -> + (uses_pos_assertions:bool -> new_ex_types:(int * Defs.loc) list -> preserve:Defs.VarSet.t -> cnstrnt -> solution) -> program -> (string * Terms.typ_scheme) list * Terms.annot_item list diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index 564ed14..d6aa414 100644 --- a/src/InvarGenT.ml +++ b/src/InvarGenT.ml @@ -14,13 +14,13 @@ open Defs open Terms open Aux -let solver ~new_ex_types ~preserve cn = +let solver ~uses_pos_assertions ~new_ex_types ~preserve cn = let q_ops, cn = Infer.prenexize cn in (*[* Format.printf "solver: cn=@\n%a@\n%!" Infer.pr_cnstrnt cn; *]*) let exty_res_of_chi, brs = Infer.normalize q_ops cn in (*[* Format.printf "solver: normalized=@\n%a@\n%!" Infer.pr_brs brs; *]*) let brs = Infer.simplify preserve q_ops brs in - Invariants.solve q_ops new_ex_types exty_res_of_chi brs + Invariants.solve ~uses_pos_assertions q_ops new_ex_types exty_res_of_chi brs let process_file ?(do_sig=false) ?(do_ml=false) ?(verif_ml=true) ?(full_annot=false) fname = @@ -80,6 +80,8 @@ let main () = and full_annot = ref false in let num_is_mod s = OCaml.num_is := s; OCaml.num_is_mod := true in + let set_convergence_step i = + Invariants.disj_step.(5) <- i in let cli = [ "-inform", Arg.Set Infer.inform_toplevel, "Print type schemes of toplevel definitions as they are inferred"; @@ -114,6 +116,10 @@ let main () = "Do not include alien (e.g. numerical) premise info in term abduction"; "-early_num_abduction", Arg.Set NumS.early_num_abduction, "Include recursive branches in numerical abduction from the start"; + "-convergence_step", Arg.Int set_convergence_step, + "The iteration at which to start truncating postconditions to only \ + keep atoms present in the previous iteration, to force \ + convergence (default 8)"; "-early_postcond_abd", Arg.Set Invariants.early_postcond_abd, "Include postconditions from recursive calls in abduction from the start"; "-num_abduction_rotations", Arg.Set_int NumS.abd_rotations, @@ -147,6 +153,9 @@ let main () = "-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"; + "-same_with_assertions", Arg.Set Invariants.same_with_assertions, + "Do not treat definitions with positive assertions (assert num, \ + assert type) specially"; "-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)"; @@ -214,8 +223,9 @@ let main () = if !NumS.abd_fail_flag then Format.printf "Perhaps increase the -num_abduction_fail parameter.@\n%!"; if !Invariants.timeout_flag then Format.printf - "Perhaps increase the -iterations_timeout parameter or try the \ - -more_existential option.@\n%!"; + "Perhaps increase the -iterations_timeout parameter or try one \ + of the options: \ + -more_existential, -prefer_guess, -prefer_bound_to_local.@\n%!"; if !Invariants.unfinished_postcond_flag then Format.printf "Perhaps some definition is used with requirements on@ its \ inferred postcondition not warranted by the definition.@\n%!"; diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index d0f3c5e..66f589b 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -510,17 +510,15 @@ let tests = "InvarGenT" >::: [ "liquid_tower_asserted" >:: (fun () -> skip_if !debug "debug"; - test_case ~prefer_bound_to_local:true - ~reward_constrn:(-1) "liquid_tower_asserted" ()); + test_case "liquid_tower_asserted" ()); "liquid_tower" >:: (fun () -> skip_if !debug "debug"; test_case "liquid_tower" ()); "liquid_tower_harder" >:: (fun () -> - todo "too hard for current numerical abduction"; skip_if !debug "debug"; - test_case "liquid_tower_harder" ()); + test_case ~prefer_bound_to_local:true "liquid_tower_harder" ()); "liquid_matmult" >:: (fun () -> skip_if !debug "debug"; @@ -528,8 +526,7 @@ let tests = "InvarGenT" >::: [ "liquid_heapsort-heapify-simpler" >:: (fun () -> skip_if !debug "debug"; - test_case ~prefer_bound_to_local:true - "liquid_heapsort_heapify_simpler" ()); + test_case "liquid_heapsort_heapify_simpler" ()); "liquid_heapsort-heapify-simpler2" >:: (fun () -> (* TODO: improve time *) @@ -652,21 +649,22 @@ let tests = "InvarGenT" >::: [ 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_gauss2" >:: + (fun () -> + skip_if !debug "debug"; + test_case ~prefer_bound_to_local:true "liquid_gauss2" ()); "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" >:: diff --git a/src/Invariants.ml b/src/Invariants.ml index 7e586b3..8468d12 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -12,8 +12,9 @@ let timeout_flag = ref false let unfinished_postcond_flag = ref false let use_prior_discards = ref (* false *)true let use_solution_in_postcond = ref false (* true *) +let same_with_assertions = ref false (* Captures where the repeat step is/are. *) -let disj_step = [|1; 1; 2; 3; 4; 6|] +let disj_step = [|1; 1; 2; 3; 4; (* 6 *)8|] open Defs open Terms @@ -843,8 +844,15 @@ let neg_constrns = ref true let empty_disc = {at_typ=[],[]; at_num=[]; at_ord=[]; at_so=()} let empty_dl = {at_typ=[]; at_num=[]; at_ord=[]; at_so=()} -let solve q_ops new_ex_types exty_res_chi brs = +let solve ~uses_pos_assertions q_ops new_ex_types exty_res_chi brs = timeout_flag := false; + let old_reward_constrn = !NumS.reward_constrn in + let old_prefer_bound_to_local = !NumS.prefer_bound_to_local in + (*[* Format.printf + "solve: old_reward_constrn=%d, uses_pos_assertions=%b@\n%!" + old_reward_constrn uses_pos_assertions; *]*) + if uses_pos_assertions && not !same_with_assertions + then (NumS.reward_constrn := -1; NumS.prefer_bound_to_local := true); (* DEBUG *) (*[* List.iter (fun (prem,concl) -> @@ -1808,6 +1816,8 @@ let solve q_ops new_ex_types exty_res_chi brs = (!unfinished_postcond @ unfinished1 @ unfinished2 @ unfinished3) in timeout_flag := true; + NumS.reward_constrn := old_reward_constrn; + NumS.prefer_bound_to_local := old_prefer_bound_to_local; raise (NoAnswer (Type_sort, "Answers do not converge", None, loc)) else finish rol2 sol2 in match loop 0 empty_dl rolT solT [] with @@ -1911,5 +1921,7 @@ let solve q_ops new_ex_types exty_res_chi brs = let ety_n = Extype ex_i in Hashtbl.replace sigma ety_n (VarSet.elements allvs, rphi, [rty], ety_n, pvs)) new_ex_types; + NumS.reward_constrn := old_reward_constrn; + NumS.prefer_bound_to_local := old_prefer_bound_to_local; (*[* Format.printf "solve: returning@\n%!"; *]*) q.op, ans_res, sol diff --git a/src/Invariants.mli b/src/Invariants.mli index 631fca9..886d386 100644 --- a/src/Invariants.mli +++ b/src/Invariants.mli @@ -10,19 +10,26 @@ val timeout_count : int ref val timeout_flag : bool ref val unfinished_postcond_flag : bool ref val use_prior_discards : bool ref +(** If [true], do not use specific heuristic settings for definitions + with assertions. Currently, when [false], {!NumS.reward_constrn} + is set to [-1] for definitions with assertions. *) +val same_with_assertions : bool ref (** Breakdown of steps through the main iteration to achieve convergence, counting from 0. The iteration: * [disj_step.(0)] is * [disj_step.(1)] is * [disj_step.(2)] is - * [disj_step.(3)] is when convergence of postconditions is enforced. + * [disj_step.(3)] is + * [disj_step.(4)] is + * [disj_step.(5)] is when convergence of postconditions is enforced. *) val disj_step : int array type chi_subst = (int * (Defs.var_name list * Terms.formula)) list val neg_constrns : bool ref val solve : + uses_pos_assertions:bool -> Defs.quant_ops -> (int * Defs.loc) list -> (int, int) Hashtbl.t -> (Terms.formula * Terms.formula) list -> Defs.quant_ops * Terms.formula * chi_subst diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index 291d97e..3c0fbbb 100644 --- a/src/InvariantsTest.ml +++ b/src/InvariantsTest.ml @@ -69,7 +69,8 @@ let test_common ?more_general ?more_existential ?no_num_abduction (match prefer_guess with | None -> () | Some prefer_guess -> Abduction.prefer_guess := prefer_guess); let _, res, sol = - Invariants.solve q_ops new_ex_types exty_res_of_chi brs in + Invariants.solve ~uses_pos_assertions:!Infer.uses_pos_assertions + q_ops new_ex_types exty_res_of_chi brs in Defs.nodeadcode := old_nodeadcode; Defs.guess_from_postcond := old_guess_from_postcond; Defs.force_nodeadcode := old_force_nodeadcode; @@ -1900,7 +1901,7 @@ let rec zip = | UCons xs, UCons ys -> let zs = zip (xs, ys) in UCons zs" - [2,"∃n, k. δ = ((Unary n, Unary k) → ∃i[i=min (k, n)].Unary i)"] + [2,"∃n, k. δ = ((Unary n, Unary k) → ∃i[i=min (n, k)].Unary i)"] ); "unary minimum asserted 1" >:: @@ -1963,7 +1964,7 @@ let rec zip = | UCons xs, UCons ys -> let zs = zip (xs, ys) in UCons zs" - [2,"∃n, k. δ = ((Unary n, Unary k) → ∃i[i=min (n, k)].Unary i) ∧ + [2,"∃n, k. δ = ((Unary n, Unary k) → ∃i[i=min (k, n)].Unary i) ∧ 0 ≤ n ∧ 0 ≤ k"] ); @@ -1984,7 +1985,7 @@ let rec zip = let zs = zip (xs, ys) in LCons ((x, y), zs)" [2,"∃n, k, a, b. - δ = ((List (a, n), List (b, k)) → ∃i[i=min (n, k)].List ((a, b), i))"] + δ = ((List (a, n), List (b, k)) → ∃i[i=min (k, n)].List ((a, b), i))"] ); "unary maximum expanded" >:: @@ -2246,8 +2247,8 @@ let rec map2_filter = fun q r f g h -> [2,"∃n, k, a, b, c. δ = ((b → Bool) → (c → Bool) → (b → c → a) → (b → a) → - (c → a) → (List (b, n), List (c, k)) → ∃i[0 ≤ i ∧ - i ≤ n + k ∧ min (n, k)≤i ∧ i≤max (k, n)].List (a, i))"] + (c → a) → (List (b, n), List (c, k)) → ∃i[i ≤ n + k ∧ + 0 ≤ i ∧ i≤max (n, k) ∧ min (n, k)≤i].List (a, i))"] ); "avl_tree--height" >::