From a9bba32bcde92883a4b2bea66e5439eafcccbe12 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Wed, 18 Mar 2015 02:34:30 +0100 Subject: [PATCH] Return to non-incremental validation in numerical abduction. Map-based numerical substitutions and normal form inequalities. --- examples/avl_tree.gadti.target | 12 +- examples/binary_upper_bound.gadti.target | 4 +- examples/filter.gadti.target | 2 +- examples/filter_map.gadti.target | 4 +- examples/liquid_bcopy.gadti.target | 2 +- examples/liquid_bcopy_simpler.gadti.target | 2 +- examples/liquid_bsearch.gadti.target | 2 +- examples/liquid_bsearch2.gadti.target | 8 +- examples/liquid_bsearch2_harder1.gadti.target | 8 +- examples/liquid_bsearch2_harder2.gadti.target | 2 +- examples/liquid_bsearch2_harder3.gadti.target | 2 +- examples/liquid_bsearch2_harder3.ml.target | 8 +- examples/liquid_bsearch2_simpler.gadti.target | 6 +- examples/liquid_fft.gadti.target | 2 +- examples/liquid_fft_ffor.gadti.target | 2 +- examples/liquid_fft_full.gadti.target | 4 +- .../liquid_fft_full_asserted.gadti.target | 2 +- examples/liquid_gauss.gadti.target | 14 +- examples/liquid_gauss2.gadti.target | 14 +- examples/liquid_gauss_asserted.gadti.target | 12 +- .../liquid_gauss_harder_asserted.gadti.target | 14 +- examples/liquid_gauss_rowElim.gadti.target | 2 +- examples/liquid_gauss_rowMax_2.gadti.target | 4 +- examples/liquid_gauss_rowSwap.gadti.target | 4 +- examples/liquid_gauss_simpler.gadti.target | 2 +- ...liquid_gauss_simpler_asserted.gadti.target | 2 +- examples/liquid_heapsort.gadti.target | 6 +- examples/liquid_heapsort_heapify.gadti.target | 2 +- ...quid_heapsort_heapify_simpler.gadti.target | 2 +- ...uid_heapsort_heapify_simpler2.gadti.target | 2 +- ...uid_heapsort_heapify_simpler3.gadti.target | 2 +- .../liquid_heapsort_heapsort.gadti.target | 2 +- ...uid_heapsort_heapsort_simpler.gadti.target | 2 +- examples/liquid_isort.gadti.target | 2 +- examples/liquid_isort_full.gadti.target | 2 +- examples/liquid_isort_harder.gadti.target | 2 +- examples/liquid_isort_simpler.gadti.target | 2 +- examples/liquid_isort_simpler3.gadti.target | 2 +- examples/liquid_matmult.gadti.target | 4 +- examples/liquid_queen_simpler.gadti.target | 4 +- examples/liquid_simplex.gadti.target | 24 +- examples/liquid_simplex.ml.target | 63 ++- examples/liquid_simplex_harder.gadti.target | 2 +- examples/liquid_simplex_step_2.gadti.target | 6 +- examples/liquid_simplex_step_2a.gadti.target | 6 +- examples/liquid_simplex_step_3a.gadti.target | 2 +- examples/liquid_simplex_step_4a.gadti.target | 2 +- examples/liquid_simplex_step_5a.gadti.target | 2 +- examples/liquid_simplex_step_6_2.gadti.target | 8 +- examples/liquid_simplex_step_6_3.gadti.target | 2 +- examples/liquid_simplex_step_6a.gadti.target | 2 +- .../liquid_simplex_step_6a_1.gadti.target | 2 +- .../liquid_simplex_step_6a_2.gadti.target | 2 +- .../liquid_simplex_step_6a_3.gadti.target | 2 +- examples/liquid_simplex_step_7a.gadti.target | 2 +- examples/liquid_tower_harder.gadti.target | 6 +- examples/liquid_tower_showposts.gadti.target | 2 +- examples/liquid_tower_simpler.gadti.target | 4 +- examples/liquid_vecswap.gadti.target | 4 +- examples/liquid_vecswap_simpler.gadti.target | 2 +- src/InvarGenTTest.ml | 19 +- src/InvariantsTest.ml | 61 ++- src/NumS.ml | 328 ++++++------ test.log | 472 ++++++++---------- 64 files changed, 602 insertions(+), 599 deletions(-) diff --git a/examples/avl_tree.gadti.target b/examples/avl_tree.gadti.target index af87285..8b0c049 100644 --- a/examples/avl_tree.gadti.target +++ b/examples/avl_tree.gadti.target @@ -21,18 +21,18 @@ external val compare : ∀a. a → a → LinOrder val height : ∀n, a. Avl (a, n) → Num n val create : - ∀k, n, a[0 ≤ n ∧ n ≤ k + 2 ∧ 0 ≤ k ∧ k ≤ n + 2]. + ∀k, n, a[k ≤ n + 2 ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ 0 ≤ n]. Avl (a, k) → a → Avl (a, n) → ∃i[i=max (k + 1, n + 1)].Avl (a, i) val singleton : ∀a. a → Avl (a, 1) val rotr : - ∀k, n, a[0 ≤ n ∧ n + 2 ≤ k ∧ k ≤ n + 3]. + ∀k, n, a[k ≤ n + 3 ∧ n + 2 ≤ k ∧ 0 ≤ n]. Avl (a, k) → a → Avl (a, n) → ∃n[k ≤ n ∧ n ≤ k + 1].Avl (a, n) val rotl : - ∀k, n, a[n ≤ k + 3 ∧ 0 ≤ k ∧ k + 2 ≤ n]. + ∀k, n, a[k + 2 ≤ n ∧ 0 ≤ k ∧ n ≤ k + 3]. Avl (a, k) → a → Avl (a, n) → ∃k[k ≤ n + 1 ∧ n ≤ k].Avl (a, k) @@ -46,13 +46,13 @@ val min_binding : ∀n, a[1 ≤ n]. Avl (a, n) → a val remove_min_binding : ∀n, a[1 ≤ n]. - Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ k ≤ n].Avl (a, k) + Avl (a, n) → ∃k[k + 2 ≤ 2 n ∧ k ≤ n ∧ n ≤ k + 1].Avl (a, k) val merge : - ∀k, n, a[n ≤ k + 2 ∧ k ≤ n + 2]. + ∀k, n, a[k ≤ n + 2 ∧ n ≤ k + 2]. (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[n ≤ k + 1 ∧ 0 ≤ k ∧ k ≤ n].Avl (a, k) + a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ k ≤ n ∧ 0 ≤ k].Avl (a, k) diff --git a/examples/binary_upper_bound.gadti.target b/examples/binary_upper_bound.gadti.target index 2375971..1c0ae21 100644 --- a/examples/binary_upper_bound.gadti.target +++ b/examples/binary_upper_bound.gadti.target @@ -8,5 +8,5 @@ datacons POne : ∀n[0 ≤ n].Binary n ⟶ Binary (2 n + 1) val ub : ∀k, n. - Binary k → Binary n → ∃i[k ≤ i ∧ n ≤ i ∧ - i ≤ n + k].Binary i + Binary k → Binary n → ∃i[i ≤ n + k ∧ n ≤ i ∧ + k ≤ i].Binary i diff --git a/examples/filter.gadti.target b/examples/filter.gadti.target index 274bf93..dc66ef4 100644 --- a/examples/filter.gadti.target +++ b/examples/filter.gadti.target @@ -6,4 +6,4 @@ datacons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1) val filter : ∀n, a. - (a → Bool) → List (a, n) → ∃k[0 ≤ k ∧ k ≤ n].List (a, k) + (a → Bool) → List (a, n) → ∃k[k ≤ n ∧ 0 ≤ k].List (a, k) diff --git a/examples/filter_map.gadti.target b/examples/filter_map.gadti.target index 2bd1156..395f48f 100644 --- a/examples/filter_map.gadti.target +++ b/examples/filter_map.gadti.target @@ -6,5 +6,5 @@ datacons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1) val filter : ∀n, a, b. - (a → Bool) → (a → b) → List (a, n) → ∃k[0 ≤ k ∧ - k ≤ n].List (b, k) + (a → Bool) → (a → b) → List (a, n) → ∃k[k ≤ n ∧ + 0 ≤ k].List (b, k) diff --git a/examples/liquid_bcopy.gadti.target b/examples/liquid_bcopy.gadti.target index bc375e0..bae2b97 100644 --- a/examples/liquid_bcopy.gadti.target +++ b/examples/liquid_bcopy.gadti.target @@ -17,7 +17,7 @@ external val prod : Int → Int → Int external val int0 : Int val bcopy_aux : - ∀i, j, k, n, a[0 ≤ n ∧ k ≤ i ∧ k ≤ j]. + ∀i, j, k, n, a[k ≤ j ∧ k ≤ i ∧ 0 ≤ n]. Array (a, j) → Array (a, i) → (Num n, Num k) → () val bcopy : ∀k, n, a[k ≤ n]. Array (a, k) → Array (a, n) → () diff --git a/examples/liquid_bcopy_simpler.gadti.target b/examples/liquid_bcopy_simpler.gadti.target index bc375e0..bae2b97 100644 --- a/examples/liquid_bcopy_simpler.gadti.target +++ b/examples/liquid_bcopy_simpler.gadti.target @@ -17,7 +17,7 @@ external val prod : Int → Int → Int external val int0 : Int val bcopy_aux : - ∀i, j, k, n, a[0 ≤ n ∧ k ≤ i ∧ k ≤ j]. + ∀i, j, k, n, a[k ≤ j ∧ k ≤ i ∧ 0 ≤ n]. Array (a, j) → Array (a, i) → (Num n, Num k) → () val bcopy : ∀k, n, a[k ≤ n]. Array (a, k) → Array (a, n) → () diff --git a/examples/liquid_bsearch.gadti.target b/examples/liquid_bsearch.gadti.target index 57e6e0b..32ee49a 100644 --- a/examples/liquid_bsearch.gadti.target +++ b/examples/liquid_bsearch.gadti.target @@ -31,7 +31,7 @@ datacons NotFound : ∀a. Answer a datacons Found : ∀a.a ⟶ Answer a val look : - ∀i, k, n, a[0 ≤ k ∧ n + 1 ≤ i]. + ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k]. a → Array (a, i) → Num k → Num n → Answer a val bsearch : ∀n, a[0 ≤ n]. a → Array (a, n) → Answer a diff --git a/examples/liquid_bsearch2.gadti.target b/examples/liquid_bsearch2.gadti.target index 295ca61..f934802 100644 --- a/examples/liquid_bsearch2.gadti.target +++ b/examples/liquid_bsearch2.gadti.target @@ -25,10 +25,10 @@ external val equal : ∀a. a → a → Bool external val div2 : ∀n. Num (2 n) → Num n val look : - ∀i, k, n, a[0 ≤ n + 1 ∧ 0 ≤ k ∧ n + 1 ≤ i]. - a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧ - k ≤ n].Num k + ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n + 1]. + a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧ + 0 ≤ k + 1].Num k val bsearch : ∀n, a[0 ≤ n + 1]. - a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k + a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k diff --git a/examples/liquid_bsearch2_harder1.gadti.target b/examples/liquid_bsearch2_harder1.gadti.target index 295ca61..f934802 100644 --- a/examples/liquid_bsearch2_harder1.gadti.target +++ b/examples/liquid_bsearch2_harder1.gadti.target @@ -25,10 +25,10 @@ external val equal : ∀a. a → a → Bool external val div2 : ∀n. Num (2 n) → Num n val look : - ∀i, k, n, a[0 ≤ n + 1 ∧ 0 ≤ k ∧ n + 1 ≤ i]. - a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧ - k ≤ n].Num k + ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n + 1]. + a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧ + 0 ≤ k + 1].Num k val bsearch : ∀n, a[0 ≤ n + 1]. - a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k + a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k diff --git a/examples/liquid_bsearch2_harder2.gadti.target b/examples/liquid_bsearch2_harder2.gadti.target index ef58fd7..f7ee48b 100644 --- a/examples/liquid_bsearch2_harder2.gadti.target +++ b/examples/liquid_bsearch2_harder2.gadti.target @@ -26,4 +26,4 @@ external val div2 : ∀n. Num (2 n) → Num n val bsearch : ∀n, a[0 ≤ n + 1]. - a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k + a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k diff --git a/examples/liquid_bsearch2_harder3.gadti.target b/examples/liquid_bsearch2_harder3.gadti.target index 903a075..9ec1fe6 100644 --- a/examples/liquid_bsearch2_harder3.gadti.target +++ b/examples/liquid_bsearch2_harder3.gadti.target @@ -26,4 +26,4 @@ external val div2 : ∀n. Num (2 n) → Num n val bsearch : ∀n, a[0 ≤ n]. - a → Array (a, n) → ∃k[0 ≤ k + 1 ∧ k + 1 ≤ n].Num k + a → Array (a, n) → ∃k[k + 1 ≤ n ∧ 0 ≤ k + 1].Num k diff --git a/examples/liquid_bsearch2_harder3.ml.target b/examples/liquid_bsearch2_harder3.ml.target index e564e9c..186c197 100644 --- a/examples/liquid_bsearch2_harder3.ml.target +++ b/examples/liquid_bsearch2_harder3.ml.target @@ -21,17 +21,17 @@ let compare : ('a -> 'a -> linOrder) = let equal : ('a -> 'a -> bool) = fun a b -> a = b let div2 : ((* 2 n *) num -> (* n *) num) = fun x -> x / 2 type ex4 = - | Ex4 : (*∀'k, 'n[0 ≤ k + 1 ∧ k + 1 ≤ n].*)(* k *) num -> + | Ex4 : (*∀'k, 'n[k + 1 ≤ n ∧ 0 ≤ k + 1].*)(* k *) num -> (* n *) ex4 type ex3 = - | Ex3 : (*∀'k, 'n[0 ≤ k + 1 ∧ k ≤ n].*)(* k *) num -> (* n *) ex3 + | Ex3 : (*∀'k, 'n[k ≤ n ∧ 0 ≤ k + 1].*)(* k *) num -> (* n *) ex3 let bsearch : type (*n*) a (*0 ≤ n*). (a -> (a (* n *)) array -> (* n *) ex4) = (fun key vec -> let Ex3 xcase = let rec look : - type (*i*) (*j*) (*k*) b (*0 ≤ k + 1 ∧ 0 ≤ i ∧ - k + 1 ≤ j*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num -> + type (*i*) (*j*) (*k*) b (*k + 1 ≤ j ∧ 0 ≤ i ∧ + 0 ≤ k + 1*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num -> (* k *) ex3) = (fun key vec lo hi -> diff --git a/examples/liquid_bsearch2_simpler.gadti.target b/examples/liquid_bsearch2_simpler.gadti.target index 89f7d83..443f086 100644 --- a/examples/liquid_bsearch2_simpler.gadti.target +++ b/examples/liquid_bsearch2_simpler.gadti.target @@ -25,6 +25,6 @@ external val equal : ∀a. a → a → Bool external val div2 : ∀n. Num (2 n) → Num n val look : - ∀i, k, n, a[0 ≤ k ∧ k ≤ n + 1 ∧ n + 1 ≤ i]. - a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧ - k ≤ n].Num k + ∀i, k, n, a[n + 1 ≤ i ∧ k ≤ n + 1 ∧ 0 ≤ k]. + a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧ + 0 ≤ k + 1].Num k diff --git a/examples/liquid_fft.gadti.target b/examples/liquid_fft.gadti.target index 2493ea4..1129aa8 100644 --- a/examples/liquid_fft.gadti.target +++ b/examples/liquid_fft.gadti.target @@ -69,5 +69,5 @@ external val asgn : ∀a. Ref a → a → () external val deref : ∀a. Ref a → a val fft : - ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. + ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Array (Float, n + 1) → Array (Float, k) → Num n diff --git a/examples/liquid_fft_ffor.gadti.target b/examples/liquid_fft_ffor.gadti.target index 84328d6..ca2705e 100644 --- a/examples/liquid_fft_ffor.gadti.target +++ b/examples/liquid_fft_ffor.gadti.target @@ -3,5 +3,5 @@ datatype Bounded : num * num datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) val ffor : - ∀i, j, k, n[j ≤ i ∧ k ≤ n]. + ∀i, j, k, n[k ≤ n ∧ j ≤ i]. Num n → Num j → (Bounded (k, i) → ()) → () diff --git a/examples/liquid_fft_full.gadti.target b/examples/liquid_fft_full.gadti.target index 9ff4037..4c4ec4b 100644 --- a/examples/liquid_fft_full.gadti.target +++ b/examples/liquid_fft_full.gadti.target @@ -63,7 +63,7 @@ datatype Bounded : num * num datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) val ffor : - ∀i, j, k, n[j ≤ i ∧ k ≤ n]. + ∀i, j, k, n[k ≤ n ∧ j ≤ i]. Num n → Num j → (Bounded (k, i) → ()) → () external val ref : ∀a. a → Ref a @@ -73,7 +73,7 @@ external val asgn : ∀a. Ref a → a → () external val deref : ∀a. Ref a → a val fft : - ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. + ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Array (Float, n + 1) → Array (Float, k) → Num n val ffttest : ∀n[2 ≤ n]. Num n → Float diff --git a/examples/liquid_fft_full_asserted.gadti.target b/examples/liquid_fft_full_asserted.gadti.target index 82f278b..edc1c13 100644 --- a/examples/liquid_fft_full_asserted.gadti.target +++ b/examples/liquid_fft_full_asserted.gadti.target @@ -63,7 +63,7 @@ datatype Bounded : num * num datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) val ffor : - ∀i, j, k, n[j ≤ i ∧ k ≤ n]. + ∀i, j, k, n[k ≤ n ∧ j ≤ i]. Num n → Num j → (Bounded (k, i) → ()) → () external val ref : ∀a. a → Ref a diff --git a/examples/liquid_gauss.gadti.target b/examples/liquid_gauss.gadti.target index fa0190a..5bad05e 100644 --- a/examples/liquid_gauss.gadti.target +++ b/examples/liquid_gauss.gadti.target @@ -52,23 +52,23 @@ external val fl0 : Float external val fl1 : Float val getRow : - ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i]. + ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, n) → Num k → Array (Float, n) val putRow : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j]. + ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. 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 → () + ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n]. Matrix (i, j) → Num k → Num n → () val norm : - ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i]. + ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, i) → Num k → Num n → () val rowElim : - ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. + ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, j) → Array (Float, i) → Num k → Num n → () -val gauss : ∀k, n[0 ≤ n ∧ n ≤ k ∧ 1 ≤ k]. Matrix (n, k) → () +val gauss : ∀k, n[n ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_gauss2.gadti.target b/examples/liquid_gauss2.gadti.target index 7dd4c70..10adf5e 100644 --- a/examples/liquid_gauss2.gadti.target +++ b/examples/liquid_gauss2.gadti.target @@ -52,23 +52,23 @@ external val fl0 : Float external val fl1 : Float val getRow : - ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i]. + ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, n) → Num k → Array (Float, n) val putRow : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j]. + ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. 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 → () + ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n]. Matrix (i, j) → Num k → Num n → () val norm : - ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i]. + ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, i) → Num k → Num n → () val rowElim : - ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. + ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, j) → Array (Float, i) → Num k → Num n → () -val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → () +val gauss : ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_gauss_asserted.gadti.target b/examples/liquid_gauss_asserted.gadti.target index fb69a69..7b04cf8 100644 --- a/examples/liquid_gauss_asserted.gadti.target +++ b/examples/liquid_gauss_asserted.gadti.target @@ -52,23 +52,23 @@ external val fl0 : Float external val fl1 : Float val getRow : - ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i]. + ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, n) → Num k → Array (Float, n) val putRow : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j]. + ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. 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 → () + ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n]. Matrix (i, j) → Num k → Num n → () val norm : - ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i]. + ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, i) → Num k → Num n → () val rowElim : - ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. + ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. 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 index 7dd4c70..10adf5e 100644 --- a/examples/liquid_gauss_harder_asserted.gadti.target +++ b/examples/liquid_gauss_harder_asserted.gadti.target @@ -52,23 +52,23 @@ external val fl0 : Float external val fl1 : Float val getRow : - ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i]. + ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, n) → Num k → Array (Float, n) val putRow : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j]. + ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. 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 → () + ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n]. Matrix (i, j) → Num k → Num n → () val norm : - ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i]. + ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, i) → Num k → Num n → () val rowElim : - ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. + ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, j) → Array (Float, i) → Num k → Num n → () -val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → () +val gauss : ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_gauss_rowElim.gadti.target b/examples/liquid_gauss_rowElim.gadti.target index 29c8683..a029e2f 100644 --- a/examples/liquid_gauss_rowElim.gadti.target +++ b/examples/liquid_gauss_rowElim.gadti.target @@ -52,5 +52,5 @@ external val fl0 : Float external val fl1 : Float val rowElim : - ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. + ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Float, j) → Array (Float, i) → Num k → Num n → () diff --git a/examples/liquid_gauss_rowMax_2.gadti.target b/examples/liquid_gauss_rowMax_2.gadti.target index 3351861..3c8d937 100644 --- a/examples/liquid_gauss_rowMax_2.gadti.target +++ b/examples/liquid_gauss_rowMax_2.gadti.target @@ -68,8 +68,8 @@ external norm : Array (Float, i) → Num k → Num n → () val rowMax : - ∀i, j, k, m, n[0 ≤ i ∧ i + 1 ≤ j ∧ i + 1 ≤ m ∧ 0 ≤ k ∧ - 0 ≤ n]. + ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ i + 1 ≤ m ∧ i + 1 ≤ j ∧ + 0 ≤ i]. Matrix (j, m) → Num i → (Num k → Float → Num n → ∃k[0 ≤ k ∧ k≤max (n, j + -1)].Num k, diff --git a/examples/liquid_gauss_rowSwap.gadti.target b/examples/liquid_gauss_rowSwap.gadti.target index ca6b9fb..7253520 100644 --- a/examples/liquid_gauss_rowSwap.gadti.target +++ b/examples/liquid_gauss_rowSwap.gadti.target @@ -60,5 +60,5 @@ external putRow : Matrix (n, k) → Num i → Array (Float, j) → () 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 → () + ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n]. Matrix (i, j) → Num k → Num n → () diff --git a/examples/liquid_gauss_simpler.gadti.target b/examples/liquid_gauss_simpler.gadti.target index 317c481..dcc0900 100644 --- a/examples/liquid_gauss_simpler.gadti.target +++ b/examples/liquid_gauss_simpler.gadti.target @@ -71,4 +71,4 @@ 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) → () +val gauss : ∀k, n[n + 1 ≤ k ∧ 0 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_gauss_simpler_asserted.gadti.target b/examples/liquid_gauss_simpler_asserted.gadti.target index e536283..85fd0d9 100644 --- a/examples/liquid_gauss_simpler_asserted.gadti.target +++ b/examples/liquid_gauss_simpler_asserted.gadti.target @@ -71,4 +71,4 @@ 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) → () +val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_heapsort.gadti.target b/examples/liquid_heapsort.gadti.target index 56780ed..0a0cea5 100644 --- a/examples/liquid_heapsort.gadti.target +++ b/examples/liquid_heapsort.gadti.target @@ -35,15 +35,15 @@ external val plus : Int → Int → Int external val int0 : Int val heapify : - ∀i, k, n, a[0 ≤ n ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ 0 ≤ n]. Num i → Array (a, k) → Num n → () val buildheap : ∀k, n, a[k ≤ n]. Num k → Array (a, n) → () val heapsort : - ∀i, k, n, a[k ≤ n ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ k ≤ n]. Num i → Num k → Array (a, n) → () val print_array : - ∀i, k, n[k ≤ i ∧ 0 ≤ n]. + ∀i, k, n[0 ≤ n ∧ k ≤ i]. Array (String, i) → Num n → Num k → () diff --git a/examples/liquid_heapsort_heapify.gadti.target b/examples/liquid_heapsort_heapify.gadti.target index 8e9db15..39fdef6 100644 --- a/examples/liquid_heapsort_heapify.gadti.target +++ b/examples/liquid_heapsort_heapify.gadti.target @@ -35,5 +35,5 @@ external val plus : Int → Int → Int external val int0 : Int val heapify : - ∀i, k, n, a[0 ≤ n ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ 0 ≤ n]. Num i → Array (a, k) → Num n → () diff --git a/examples/liquid_heapsort_heapify_simpler.gadti.target b/examples/liquid_heapsort_heapify_simpler.gadti.target index f1c9250..3162bbb 100644 --- a/examples/liquid_heapsort_heapify_simpler.gadti.target +++ b/examples/liquid_heapsort_heapify_simpler.gadti.target @@ -35,5 +35,5 @@ external val plus : Int → Int → Int external val int0 : Int val heapify : - ∀i, k, n, a[0 ≤ n ∧ n + 1 ≤ i ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ n + 1 ≤ i ∧ 0 ≤ n]. Num i → Array (a, k) → Num n → () diff --git a/examples/liquid_heapsort_heapify_simpler2.gadti.target b/examples/liquid_heapsort_heapify_simpler2.gadti.target index 3cffd74..422c01d 100644 --- a/examples/liquid_heapsort_heapify_simpler2.gadti.target +++ b/examples/liquid_heapsort_heapify_simpler2.gadti.target @@ -35,5 +35,5 @@ external val plus : Int → Int → Int external val int0 : Int val heapify : - ∀i, k, n, a[0 ≤ n ∧ 0 ≤ k ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ 0 ≤ k ∧ 0 ≤ n]. Num i → Array (a, k) → Num n → () diff --git a/examples/liquid_heapsort_heapify_simpler3.gadti.target b/examples/liquid_heapsort_heapify_simpler3.gadti.target index 3cffd74..422c01d 100644 --- a/examples/liquid_heapsort_heapify_simpler3.gadti.target +++ b/examples/liquid_heapsort_heapify_simpler3.gadti.target @@ -35,5 +35,5 @@ external val plus : Int → Int → Int external val int0 : Int val heapify : - ∀i, k, n, a[0 ≤ n ∧ 0 ≤ k ∧ i ≤ k]. + ∀i, k, n, a[i ≤ k ∧ 0 ≤ k ∧ 0 ≤ n]. Num i → Array (a, k) → Num n → () diff --git a/examples/liquid_heapsort_heapsort.gadti.target b/examples/liquid_heapsort_heapsort.gadti.target index d63638a..74c791f 100644 --- a/examples/liquid_heapsort_heapsort.gadti.target +++ b/examples/liquid_heapsort_heapsort.gadti.target @@ -42,5 +42,5 @@ external buildheap : ∀k, n, a[k ≤ n ∧ 0 ≤ k]. Num k → Array (a, n) → () val heapsort : - ∀i, k, n, a[0 ≤ k ∧ k ≤ n ∧ i ≤ n]. + ∀i, k, n, a[i ≤ n ∧ k ≤ n ∧ 0 ≤ k]. Num i → Num k → Array (a, n) → () diff --git a/examples/liquid_heapsort_heapsort_simpler.gadti.target b/examples/liquid_heapsort_heapsort_simpler.gadti.target index eee7d39..f590232 100644 --- a/examples/liquid_heapsort_heapsort_simpler.gadti.target +++ b/examples/liquid_heapsort_heapsort_simpler.gadti.target @@ -42,4 +42,4 @@ external buildheap : ∀k, n, a[k ≤ n ∧ 0 ≤ k]. Num k → Array (a, n) → () val heapsort : - ∀k, n, a[0 ≤ k ∧ k ≤ n]. Num k → Array (a, n) → () + ∀k, n, a[k ≤ n ∧ 0 ≤ k]. Num k → Array (a, n) → () diff --git a/examples/liquid_isort.gadti.target b/examples/liquid_isort.gadti.target index f17df7d..0cd9c9c 100644 --- a/examples/liquid_isort.gadti.target +++ b/examples/liquid_isort.gadti.target @@ -23,5 +23,5 @@ external val compare : ∀a. a → a → LinOrder external val equal : ∀a. a → a → Bool val insertSort : - ∀i, k, n, a[0 ≤ n ∧ 0 ≤ k ∧ n + 1 ≤ i]. + ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Array (a, i) → Num k → Num n → () diff --git a/examples/liquid_isort_full.gadti.target b/examples/liquid_isort_full.gadti.target index 37cb59e..16b42f5 100644 --- a/examples/liquid_isort_full.gadti.target +++ b/examples/liquid_isort_full.gadti.target @@ -23,5 +23,5 @@ external val compare : ∀a. a → a → LinOrder external val equal : ∀a. a → a → Bool val sortRange : - ∀i, k, n, a[1 ≤ i ∧ 0 ≤ n ∧ k + n ≤ i]. + ∀i, k, n, a[k + n ≤ i ∧ 0 ≤ n ∧ 1 ≤ i]. Array (a, i) → Num n → Num k → () diff --git a/examples/liquid_isort_harder.gadti.target b/examples/liquid_isort_harder.gadti.target index c46ccce..e13830c 100644 --- a/examples/liquid_isort_harder.gadti.target +++ b/examples/liquid_isort_harder.gadti.target @@ -23,5 +23,5 @@ external val compare : ∀a. a → a → LinOrder external val equal : ∀a. a → a → Bool val insertSort : - ∀i, k, n, a[0 ≤ k ∧ k + n ≤ i ∧ 1 ≤ i]. + ∀i, k, n, a[1 ≤ i ∧ k + n ≤ i ∧ 0 ≤ k]. Array (a, i) → Num k → Num n → () diff --git a/examples/liquid_isort_simpler.gadti.target b/examples/liquid_isort_simpler.gadti.target index abb6770..5d62f83 100644 --- a/examples/liquid_isort_simpler.gadti.target +++ b/examples/liquid_isort_simpler.gadti.target @@ -27,5 +27,5 @@ external swap : Array (a, i) → Num k → Num n → () val insertSort : - ∀i, k, n, a[0 ≤ k ∧ k + n ≤ i]. + ∀i, k, n, a[k + n ≤ i ∧ 0 ≤ k]. Array (a, i) → Num k → Num n → () diff --git a/examples/liquid_isort_simpler3.gadti.target b/examples/liquid_isort_simpler3.gadti.target index 47e34a4..1a8419f 100644 --- a/examples/liquid_isort_simpler3.gadti.target +++ b/examples/liquid_isort_simpler3.gadti.target @@ -27,5 +27,5 @@ external swap : Array (a, i) → Num k → Num n → () val insertSort : - ∀i, k, n, a[0 ≤ k ∧ n + 1 ≤ i]. + ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k]. Array (a, i) → Num k → Num n → () diff --git a/examples/liquid_matmult.gadti.target b/examples/liquid_matmult.gadti.target index 56a20f9..36b110a 100644 --- a/examples/liquid_matmult.gadti.target +++ b/examples/liquid_matmult.gadti.target @@ -34,8 +34,8 @@ external val mult : Int → Int → Int external val int0 : Int val fillar : - ∀k, n[0 ≤ n ∧ 0 ≤ k]. Matrix (n, k) → (() → Int) → () + ∀k, n[0 ≤ k ∧ 0 ≤ n]. Matrix (n, k) → (() → Int) → () val matmul : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ j ∧ j ≤ i]. + ∀i, j, k, n[j ≤ i ∧ 0 ≤ j ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (n, j) → Matrix (i, k) → Matrix (n, k) diff --git a/examples/liquid_queen_simpler.gadti.target b/examples/liquid_queen_simpler.gadti.target index 5a3a279..7c2fff7 100644 --- a/examples/liquid_queen_simpler.gadti.target +++ b/examples/liquid_queen_simpler.gadti.target @@ -31,10 +31,10 @@ val print_row : ∀n. Num n → Int → () val print_queens : ∀k, n[n ≤ k]. Array (Int, k) → Num n → () val solved : - ∀k, n[0 ≤ n ∧ n + 1 ≤ k]. Array (Int, k) → Num n → Bool + ∀k, n[n + 1 ≤ k ∧ 0 ≤ n]. Array (Int, k) → Num n → Bool val loop : - ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i]. + ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n]. Array (Int, i) → Num k → Num n → () val queens : ∀n[1 ≤ n]. Num n → () diff --git a/examples/liquid_simplex.gadti.target b/examples/liquid_simplex.gadti.target index aab2791..160f95f 100644 --- a/examples/liquid_simplex.gadti.target +++ b/examples/liquid_simplex.gadti.target @@ -36,39 +36,39 @@ external val div : Float → Float → Float external val fl0 : Float val is_neg_aux : - ∀i, k, n[0 ≤ n ∧ 1 ≤ k ∧ 0 ≤ i]. + ∀i, k, n[0 ≤ i ∧ 1 ≤ k ∧ 0 ≤ n]. Matrix (k, i) → Num n → Bool -val is_neg : ∀k, n[1 ≤ n ∧ 0 ≤ k]. Matrix (n, k) → Bool +val is_neg : ∀k, n[0 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → Bool val unb1 : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k + 1 ∧ 1 ≤ i ∧ 0 ≤ j]. + ∀i, j, k, n[0 ≤ j ∧ 1 ≤ i ∧ 0 ≤ k + 1 ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → Bool val norm_aux : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ 0 ≤ j]. + ∀i, j, k, n[0 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, j) → Num k → Float → Num n → () val norm : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ j]. + ∀i, j, k, n[n + 1 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → () val row_op_aux1 : - ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ 0 ≤ m]. + ∀i, j, k, m, n[0 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ 0 ≤ i ∧ + 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Float → Num n → () val row_op_aux2 : - ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ n + 1 ≤ m]. + ∀i, j, k, m, n[n + 1 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ + 0 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Num n → () val row_op_aux3 : - ∀i, j, k, m, n[0 ≤ k ∧ 0 ≤ i ∧ 0 ≤ j ∧ k + 1 ≤ m]. + ∀i, j, k, m, n[k + 1 ≤ m ∧ 0 ≤ j ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Num n → () val row_op : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ j]. + ∀i, j, k, n[n + 1 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → () -val simplex : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val simplex : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex.ml.target b/examples/liquid_simplex.ml.target index c25d650..620b313 100644 --- a/examples/liquid_simplex.ml.target +++ b/examples/liquid_simplex.ml.target @@ -28,23 +28,22 @@ let mult : (float -> float -> float) = ( *. ) let div : (float -> float -> float) = ( /. ) let fl0 : float = 0.0 let rec is_neg_aux : - (*type i k n [0 ≤ n ∧ 1 ≤ k ∧ - 0 ≤ i].*) ((* k, i *) matrix -> (* n *) num -> bool) = + (*type i k n [0 ≤ i ∧ 1 ≤ k ∧ + 0 ≤ n].*) ((* k, i *) matrix -> (* n *) num -> bool) = (fun a j -> (if j + 2 <= matrix_dim2 a then (if less (matrix_get a 0 j) fl0 then true else is_neg_aux a (j + 1)) else false)) let is_neg - : (*type k n [1 ≤ n ∧ 0 ≤ k].*) ((* n, k *) matrix -> bool) = + : (*type k n [0 ≤ k ∧ 1 ≤ n].*) ((* n, k *) matrix -> bool) = (fun a -> is_neg_aux a 1) let rec unb1 : - (*type i j k n [0 ≤ n ∧ 0 ≤ k + 1 ∧ 1 ≤ i ∧ - 0 ≤ j].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> bool) = + (*type i j k n [0 ≤ j ∧ 1 ≤ i ∧ 0 ≤ k + 1 ∧ + 0 ≤ n].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> bool) = (fun a i j -> let rec unb2 : - (*type k1 l m n1 [0 ≤ m ∧ 0 ≤ l ∧ 0 ≤ n1 ∧ - m + 1 ≤ k1].*) ((* n1, k1 *) matrix -> (* l *) num -> (* m *) num -> - bool) + (*type k1 l m n1 [m + 1 ≤ k1 ∧ 0 ≤ n1 ∧ 0 ≤ l ∧ + 0 ≤ m].*) ((* n1, k1 *) matrix -> (* l *) num -> (* m *) num -> bool) = (fun a i j -> (if i + 1 <= matrix_dim1 a then @@ -54,21 +53,21 @@ let rec unb1 : (if less (matrix_get a 0 j) fl0 then unb2 a (i + 1) j else unb1 a 0 (j + 1)) else false)) let rec norm_aux : - (*type i j k n [0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ - 0 ≤ j].*) ((* i, j *) matrix -> (* k *) num -> float -> (* n *) num -> + (*type i j k n [0 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n].*) ((* i, j *) matrix -> (* k *) num -> float -> (* n *) num -> unit) = (fun a i c j -> (if j + 1 <= matrix_dim2 a then (matrix_set a i j (div (matrix_get a i j) c) ; norm_aux a i c (j + 1)) else ())) let rec norm : - (*type i j k n [0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ - n + 1 ≤ j].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> unit) = + (*type i j k n [n + 1 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> unit) = (fun a i j -> let c = matrix_get a i j in norm_aux a i c 1) let rec row_op_aux1 : - (*type i j k m n [0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ - 0 ≤ m].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> float -> + (*type i j k m n [0 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ 0 ≤ i ∧ + 0 ≤ k ∧ + 0 ≤ n].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> float -> (* n *) num -> unit) = (fun a i i' c j -> (if j + 1 <= matrix_dim2 a then @@ -76,26 +75,26 @@ let rec row_op_aux1 : (minus (matrix_get a i' j) (mult (matrix_get a i j) c)) ; row_op_aux1 a i i' c (j + 1)) else ())) let rec row_op_aux2 : - (*type i j k m n [0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ - n + 1 ≤ m].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> - (* n *) num -> unit) = + (*type i j k m n [n + 1 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ + 0 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> + (* n *) num -> unit) = (fun a i i' j -> row_op_aux1 a i i' (matrix_get a i' j) 1) let rec row_op_aux3 : - (*type i j k m n [0 ≤ k ∧ 0 ≤ i ∧ 0 ≤ j ∧ - k + 1 ≤ m].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> - (* n *) num -> unit) = + (*type i j k m n [k + 1 ≤ m ∧ 0 ≤ j ∧ 0 ≤ k ∧ + 0 ≤ n].*) ((* j, m *) matrix -> (* i *) num -> (* k *) num -> + (* n *) num -> unit) = (fun a i j i' -> (if i' + 1 <= matrix_dim1 a then (if i <= i'&& i' <= i then (row_op_aux2 a i i' j ; row_op_aux3 a i j (i' + 1)) else row_op_aux3 a i j (i' + 1)) else ())) let rec row_op : - (*type i j k n [0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ - n + 1 ≤ j].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> unit) = + (*type i j k n [n + 1 ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ + 0 ≤ n].*) ((* i, j *) matrix -> (* k *) num -> (* n *) num -> unit) = (fun a i j -> (norm a i j ; row_op_aux3 a i j 0)) type ex7 = - | Ex7 : (*∀'i, 'k, 'n[k ≤ i ∧ i + 1 ≤ n].*)((* i *) num * float) -> + | Ex7 : (*∀'i, 'k, 'n[i + 1 ≤ n ∧ k ≤ i].*)((* i *) num * float) -> (* n, k *) ex7 type ex5 = | Ex5 : (*∀'i, 'k, 'n[0 ≤ k ∧ k≤max (i, n + -1)].*)(* k *) num -> @@ -104,11 +103,11 @@ type ex2 = | Ex2 : (*∀'i, 'k, 'n[0 ≤ k ∧ k≤max (i, n + -1)].*)(* k *) num -> (* n, i *) ex2 let rec simplex : - (*type k n [1 ≤ n ∧ 2 ≤ k].*) ((* n, k *) matrix -> unit) = + (*type k n [2 ≤ k ∧ 1 ≤ n].*) ((* n, k *) matrix -> unit) = (fun a -> let rec enter_var : - (*type i j [0 ≤ j ∧ - 0 ≤ i].*) ((* i *) num -> float -> (* j *) num -> (* k, i *) ex2) + (*type i j [0 ≤ i ∧ + 0 ≤ j].*) ((* i *) num -> float -> (* j *) num -> (* k, i *) ex2) = (fun j c j' -> (if j' + 2 <= matrix_dim2 a then @@ -118,8 +117,8 @@ let rec simplex : let Ex2 xcase = enter_var j c (j' + 1) in Ex2 xcase) else let xcase = j in Ex2 xcase)) in let rec depart_var : - (*type l m n1 [0 ≤ l ∧ 0 ≤ n1 ∧ n1 + 1 ≤ k ∧ - 0 ≤ m].*) ((* n1 *) num -> (* m *) num -> float -> (* l *) num -> + (*type l m n1 [0 ≤ m ∧ n1 + 1 ≤ k ∧ 0 ≤ n1 ∧ + 0 ≤ l].*) ((* n1 *) num -> (* m *) num -> float -> (* l *) num -> (* n, m *) ex5) = (fun j i r i' -> @@ -133,8 +132,8 @@ let rec simplex : let Ex5 xcase = depart_var j i r (i' + 1) in Ex5 xcase) else let xcase = i in Ex5 xcase)) in let rec init_ratio : - (*type i1 k1 [0 ≤ k1 ∧ 0 ≤ i1 ∧ - i1 + 1 ≤ k].*) ((* i1 *) num -> (* k1 *) num -> (* n, k1 *) ex7) + (*type i1 k1 [i1 + 1 ≤ k ∧ 0 ≤ i1 ∧ + 0 ≤ k1].*) ((* i1 *) num -> (* k1 *) num -> (* n, k1 *) ex7) = (fun j i -> (if i + 1 <= matrix_dim1 a then diff --git a/examples/liquid_simplex_harder.gadti.target b/examples/liquid_simplex_harder.gadti.target index 88de1eb..4bf49d0 100644 --- a/examples/liquid_simplex_harder.gadti.target +++ b/examples/liquid_simplex_harder.gadti.target @@ -35,4 +35,4 @@ external val div : Float → Float → Float external val fl0 : Float -val main_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex_step_2.gadti.target b/examples/liquid_simplex_step_2.gadti.target index ddfc184..ef6d59c 100644 --- a/examples/liquid_simplex_step_2.gadti.target +++ b/examples/liquid_simplex_step_2.gadti.target @@ -38,12 +38,12 @@ external val fl0 : Float val snd : ∀a, b. (b, a) → a val is_neg_aux : - ∀i, j, k, n[0 ≤ n ∧ 1 ≤ i ∧ k ≤ j + 1]. + ∀i, j, k, n[k ≤ j + 1 ∧ 1 ≤ i ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → Bool val is_neg : - ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool + ∀i, k, n[n ≤ i + 1 ∧ 1 ≤ k]. Matrix (k, i) → Num n → Bool val unb1 : - ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k + 1 ∧ 1 ≤ i ∧ 0 ≤ j]. + ∀i, j, k, n[0 ≤ j ∧ 1 ≤ i ∧ 0 ≤ k + 1 ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → Bool diff --git a/examples/liquid_simplex_step_2a.gadti.target b/examples/liquid_simplex_step_2a.gadti.target index e0877ff..6b89365 100644 --- a/examples/liquid_simplex_step_2a.gadti.target +++ b/examples/liquid_simplex_step_2a.gadti.target @@ -38,10 +38,10 @@ external val fl0 : Float val snd : ∀a, b. (b, a) → a val is_neg_aux : - ∀i, j, k, n[0 ≤ n ∧ 1 ≤ i ∧ k ≤ j + 1]. + ∀i, j, k, n[k ≤ j + 1 ∧ 1 ≤ i ∧ 0 ≤ n]. Matrix (i, j) → Num k → Num n → Bool val is_neg : - ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool + ∀i, k, n[n ≤ i + 1 ∧ 1 ≤ k]. Matrix (k, i) → Num n → Bool -val main_step6_test : ∀k, n[1 ≤ n ∧ 1 ≤ k]. Matrix (n, k) → Bool +val main_step6_test : ∀k, n[1 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → Bool diff --git a/examples/liquid_simplex_step_3a.gadti.target b/examples/liquid_simplex_step_3a.gadti.target index 9e9f098..5f7ec6e 100644 --- a/examples/liquid_simplex_step_3a.gadti.target +++ b/examples/liquid_simplex_step_3a.gadti.target @@ -44,4 +44,4 @@ external is_neg_aux : external is_neg : ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool -val main_step3_test : ∀k, n[1 ≤ n ∧ 3 ≤ k]. Matrix (n, k) → Float +val main_step3_test : ∀k, n[3 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → Float diff --git a/examples/liquid_simplex_step_4a.gadti.target b/examples/liquid_simplex_step_4a.gadti.target index 8b380b2..2ac283c 100644 --- a/examples/liquid_simplex_step_4a.gadti.target +++ b/examples/liquid_simplex_step_4a.gadti.target @@ -46,4 +46,4 @@ external is_neg_aux : external is_neg : ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool -val main_step3_test : ∀k, n[2 ≤ n ∧ 4 ≤ k]. Matrix (n, k) → Float +val main_step3_test : ∀k, n[4 ≤ k ∧ 2 ≤ n]. Matrix (n, k) → Float diff --git a/examples/liquid_simplex_step_5a.gadti.target b/examples/liquid_simplex_step_5a.gadti.target index d3c75bf..4951c30 100644 --- a/examples/liquid_simplex_step_5a.gadti.target +++ b/examples/liquid_simplex_step_5a.gadti.target @@ -49,4 +49,4 @@ external enter_var : Matrix (i, j) → Num n → Float → Num m → ∃l[0 ≤ l ∧ l≤max (j + -1, n)].Num l -val main_step3_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → Float +val main_step3_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → Float diff --git a/examples/liquid_simplex_step_6_2.gadti.target b/examples/liquid_simplex_step_6_2.gadti.target index f348bfc..fab9c5a 100644 --- a/examples/liquid_simplex_step_6_2.gadti.target +++ b/examples/liquid_simplex_step_6_2.gadti.target @@ -64,11 +64,11 @@ external norm : Matrix (i, j) → Num k → Num n → () val row_op_aux1 : - ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ 0 ≤ m]. + ∀i, j, k, m, n[0 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ 0 ≤ i ∧ + 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Float → Num n → () val row_op_aux2 : - ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ i ∧ i + 1 ≤ j ∧ - k + 1 ≤ j ∧ n + 1 ≤ m]. + ∀i, j, k, m, n[n + 1 ≤ m ∧ k + 1 ≤ j ∧ i + 1 ≤ j ∧ + 0 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Num n → () diff --git a/examples/liquid_simplex_step_6_3.gadti.target b/examples/liquid_simplex_step_6_3.gadti.target index 08995bf..09e93a4 100644 --- a/examples/liquid_simplex_step_6_3.gadti.target +++ b/examples/liquid_simplex_step_6_3.gadti.target @@ -69,5 +69,5 @@ external row_op_aux2 : Matrix (i, j) → Num k → Num n → Num m → () val row_op_aux3 : - ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ 0 ≤ j ∧ k + 1 ≤ m]. + ∀i, j, k, m, n[k + 1 ≤ m ∧ 0 ≤ j ∧ 0 ≤ k ∧ 0 ≤ n]. Matrix (j, m) → Num i → Num k → Num n → () diff --git a/examples/liquid_simplex_step_6a.gadti.target b/examples/liquid_simplex_step_6a.gadti.target index bffcc4c..af82f26 100644 --- a/examples/liquid_simplex_step_6a.gadti.target +++ b/examples/liquid_simplex_step_6a.gadti.target @@ -59,4 +59,4 @@ external init_ratio : Matrix (i, j) → Num k → Num n → ∃l[0 ≤ l ∧ l + 1 ≤ i].(Num l, Float) -val main_step6_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_step6_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex_step_6a_1.gadti.target b/examples/liquid_simplex_step_6a_1.gadti.target index bffcc4c..af82f26 100644 --- a/examples/liquid_simplex_step_6a_1.gadti.target +++ b/examples/liquid_simplex_step_6a_1.gadti.target @@ -59,4 +59,4 @@ external init_ratio : Matrix (i, j) → Num k → Num n → ∃l[0 ≤ l ∧ l + 1 ≤ i].(Num l, Float) -val main_step6_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_step6_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex_step_6a_2.gadti.target b/examples/liquid_simplex_step_6a_2.gadti.target index bffcc4c..af82f26 100644 --- a/examples/liquid_simplex_step_6a_2.gadti.target +++ b/examples/liquid_simplex_step_6a_2.gadti.target @@ -59,4 +59,4 @@ external init_ratio : Matrix (i, j) → Num k → Num n → ∃l[0 ≤ l ∧ l + 1 ≤ i].(Num l, Float) -val main_step6_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_step6_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex_step_6a_3.gadti.target b/examples/liquid_simplex_step_6a_3.gadti.target index e2c0314..b5c6b65 100644 --- a/examples/liquid_simplex_step_6a_3.gadti.target +++ b/examples/liquid_simplex_step_6a_3.gadti.target @@ -68,4 +68,4 @@ external row_op_aux2 : k + 1 ≤ i ∧ n + 1 ≤ i]. Matrix (i, j) → Num k → Num n → Num m → () -val main_step6_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_step6_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_simplex_step_7a.gadti.target b/examples/liquid_simplex_step_7a.gadti.target index cbd5fbc..b776596 100644 --- a/examples/liquid_simplex_step_7a.gadti.target +++ b/examples/liquid_simplex_step_7a.gadti.target @@ -67,4 +67,4 @@ external row_op : ∀i, j, k, n[0 ≤ k ∧ k + 1 ≤ i ∧ 0 ≤ n ∧ n + 1 ≤ j]. Matrix (i, j) → Num k → Num n → () -val main_step6_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → () +val main_step6_test : ∀k, n[2 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → () diff --git a/examples/liquid_tower_harder.gadti.target b/examples/liquid_tower_harder.gadti.target index 9c71bbd..48dd5c0 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[1 ≤ k ∧ 0 ≤ i ∧ i ≤ k ∧ i ≤ n + 1]. + ∀i, k, n[i ≤ n + 1 ∧ i ≤ k ∧ 0 ≤ i ∧ 1 ≤ k]. Array (Int, i) → Array (Int, k) → Array (Int, n) → () val move : - ∀i, j, k, m, n[n ≤ k ∧ 1 ≤ i ∧ i ≤ k ∧ 0 ≤ j ∧ - j + 1 ≤ k ∧ 0 ≤ m ∧ j + m ≤ k ∧ m ≤ i ∧ m ≤ n + 1]. + ∀i, j, k, m, n[m ≤ n + 1 ∧ m ≤ i ∧ j + m ≤ k ∧ 0 ≤ m ∧ + j + 1 ≤ k ∧ 0 ≤ j ∧ i ≤ k ∧ 1 ≤ i ∧ n ≤ k]. Num m → Array (Int, k) → Num j → Array (Int, k) → Num i → Array (Int, k) → Num n → () diff --git a/examples/liquid_tower_showposts.gadti.target b/examples/liquid_tower_showposts.gadti.target index afbe1b9..40845f0 100644 --- a/examples/liquid_tower_showposts.gadti.target +++ b/examples/liquid_tower_showposts.gadti.target @@ -35,5 +35,5 @@ external showpiece : Int → Int → () (** We use [i + 1 <= sz - 1] instead of [i <= sz - 1] to make inference harder. *) val showposts : - ∀i, k, n[0 ≤ i ∧ i ≤ k + 1 ∧ i ≤ n + 1]. + ∀i, k, n[i ≤ n + 1 ∧ i ≤ k + 1 ∧ 0 ≤ i]. Array (Int, i) → Array (Int, k) → Array (Int, n) → () diff --git a/examples/liquid_tower_simpler.gadti.target b/examples/liquid_tower_simpler.gadti.target index 95da153..6fb80c8 100644 --- a/examples/liquid_tower_simpler.gadti.target +++ b/examples/liquid_tower_simpler.gadti.target @@ -35,7 +35,7 @@ external showposts : Array (Int, n) → Array (Int, n) → Array (Int, n) → Num n → () val move : - ∀i, j, k, m, n[n ≤ k ∧ 1 ≤ i ∧ i ≤ k ∧ 0 ≤ j ∧ - j + 1 ≤ k ∧ j + m ≤ k ∧ m ≤ i ∧ m ≤ n + 1]. + ∀i, j, k, m, n[m ≤ n + 1 ∧ m ≤ i ∧ j + m ≤ k ∧ + j + 1 ≤ k ∧ 0 ≤ j ∧ i ≤ k ∧ 1 ≤ i ∧ n ≤ k]. Num k → Num m → Array (Int, k) → Num j → Array (Int, k) → Num i → Array (Int, k) → Num n → () diff --git a/examples/liquid_vecswap.gadti.target b/examples/liquid_vecswap.gadti.target index 02c64f9..59cb43b 100644 --- a/examples/liquid_vecswap.gadti.target +++ b/examples/liquid_vecswap.gadti.target @@ -11,5 +11,5 @@ external val array_set : external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n val swap_interval : - ∀i, j, k, n, a[1 ≤ j ∧ 0 ≤ n ∧ 0 ≤ k ∧ i + k ≤ j ∧ - i + n ≤ j]. Array (a, j) → Num n → Num k → Num i → () + ∀i, j, k, n, a[i + n ≤ j ∧ i + k ≤ j ∧ 0 ≤ k ∧ 0 ≤ n ∧ + 1 ≤ j]. Array (a, j) → Num n → Num k → Num i → () diff --git a/examples/liquid_vecswap_simpler.gadti.target b/examples/liquid_vecswap_simpler.gadti.target index 3d01671..d676dcb 100644 --- a/examples/liquid_vecswap_simpler.gadti.target +++ b/examples/liquid_vecswap_simpler.gadti.target @@ -11,5 +11,5 @@ external val array_set : external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n val swap_interval : - ∀i, j, k, n, a[1 ≤ j ∧ 0 ≤ n ∧ i + n ≤ k ∧ i + k ≤ j]. + ∀i, j, k, n, a[i + k ≤ j ∧ i + n ≤ k ∧ 0 ≤ n ∧ 1 ≤ j]. Array (a, j) → Num n → Num k → Num i → () diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 2cc3173..81ea133 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -511,8 +511,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_isort_harder" ()); "liquid_vecswap_simpler" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "liquid_vecswap_simpler" ()); "liquid_vecswap" >:: (fun () -> @@ -532,8 +531,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_tower_simpler" ()); "liquid_tower_asserted" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "liquid_tower_asserted" ()); "liquid_tower" >:: (fun () -> @@ -541,8 +539,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_tower" ()); "liquid_tower_harder" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case ~prefer_bound_to_local:true "liquid_tower_harder" ()); "liquid_matmult" >:: (fun () -> @@ -593,7 +590,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_3" ()); "liquid_simplex_step_3a" >:: (fun () -> - (* skip_if !debug "debug"; *) + 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 @@ -673,7 +670,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_gauss_simpler" ()); "liquid_gauss_simpler_asserted" >:: (fun () -> - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "liquid_gauss_simpler_asserted" ()); "liquid_gauss" >:: (fun () -> @@ -681,8 +678,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_gauss" ()); "liquid_gauss2" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case ~prefer_bound_to_local:true "liquid_gauss2" ()); "liquid_gauss_asserted" >:: (fun () -> @@ -690,8 +686,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_gauss_asserted" ()); "liquid_gauss_harder_asserted" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "liquid_gauss_harder_asserted" ()); "liquid_gauss_harder" >:: (fun () -> diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index 4ad258a..d70f155 100644 --- a/src/InvariantsTest.ml +++ b/src/InvariantsTest.ml @@ -52,7 +52,7 @@ let test_common ?more_general ?more_existential ?no_num_abduction i pr_vars (vars_of_list pvs) pr_vars (vars_of_list allvs) pr_ty ty pr_formula phi) !all_ex_types; - (*]*) + *]*) let old_more_general = !Abduction.more_general in (match more_general with | None -> () @@ -704,8 +704,8 @@ let rec append = | LCons (x, xs) -> (function l when (length l + 1) <= 0 -> assert false | l -> LCons (x, append xs l))" - [1,"∃n, k. δ = (List k → List n → List (n + k)) ∧ 0 ≤ n ∧ - 0 ≤ n + k"]; + [1,"∃n, k. δ = (List k → List n → List (n + k)) ∧ 0 ≤ n + k ∧ + 0 ≤ n"]; ); "interleave" >:: @@ -1500,7 +1500,7 @@ let rec filter = LCons (x, ys) | False -> filter xs" - [2,"∃n. δ = (List n → ∃k[0 ≤ k ∧ k ≤ n].List k)"]; + [2,"∃n. δ = (List n → ∃k[k ≤ n ∧ 0 ≤ k].List k)"]; ); @@ -1524,7 +1524,7 @@ let rec filter = LCons (x, ys) | False -> filter xs" - [2,"∃n. δ = (List (Bar, n) → ∃k[0 ≤ k ∧ k ≤ n].List (Bar, k))"]; + [2,"∃n. δ = (List (Bar, n) → ∃k[k ≤ n ∧ 0 ≤ k].List (Bar, k))"]; ); "filter poly" >:: @@ -1546,7 +1546,7 @@ let rec filter = fun f -> filter f xs" [2,"∃n, a. δ = - ((a → Bool) → List (a, n) → ∃k[0 ≤ k ∧ k ≤ n].List (a, k))"]; + ((a → Bool) → List (a, n) → ∃k[k ≤ n ∧ 0 ≤ k].List (a, k))"]; ); "poly filter map" >:: @@ -1568,9 +1568,8 @@ let rec filter = fun f g -> filter f g xs" [2,"∃n, a, b. δ = - ((a → Bool) → (a → b) → List (a, n) → ∃k[0 ≤ k ∧ - k ≤ n].List (b, k))"]; - + ((a → Bool) → (a → b) → List (a, n) → ∃k[k ≤ n ∧ + 0 ≤ k].List (b, k))"]; ); "binary upper bound-wrong" >:: @@ -1604,7 +1603,7 @@ let rec ub = efunction let r = ub a1 b1 in POne r)" [2,"∃n, k. - δ = (Binary k → Binary n → ∃i[n ≤ i ∧ i ≤ n + k].Binary i)"] + δ = (Binary k → Binary n → ∃i[i ≤ n + k ∧ n ≤ i].Binary i)"] ); "binary upper bound expanded" >:: @@ -1642,8 +1641,8 @@ let rec ub = efunction POne r)" [2,"∃n, k. δ = - (Binary k → Binary n → ∃i[k ≤ i ∧ n ≤ i ∧ - i ≤ n + k].Binary i)"] + (Binary k → Binary n → ∃i[i ≤ n + k ∧ n ≤ i ∧ + k ≤ i].Binary i)"] ); "nested recursion simple eval" >:: @@ -2020,7 +2019,7 @@ let rec zip = let zs = zip (xs, ys) in UCons zs" [2,"∃n, k. δ = ((Unary n, Unary k) → ∃i[i=min (k, n)].Unary i) ∧ - 0 ≤ n ∧ 0 ≤ k"] + 0 ≤ k ∧ 0 ≤ n"] ); "list zip prefix expanded" >:: @@ -2110,8 +2109,8 @@ let rec filter_zip = fun f -> | False -> zs" [2,"∃n, k, a, b. δ = - ((a → b → Bool) → (List (a, n), List (b, k)) → ∃i[0 ≤ i ∧ - i ≤ k ∧ i ≤ n].List ((a, b), i))"] + ((a → b → Bool) → (List (a, n), List (b, k)) → ∃i[i ≤ n ∧ + i ≤ k ∧ 0 ≤ i].List ((a, b), i))"] ); "list filter-map2 with postfix" >:: @@ -2171,7 +2170,7 @@ let rec filter_map2 = | False -> zs" [2,"∃n, k. δ = - ((List n, List k) → ∃i[0 ≤ i ∧ i ≤ n + k ∧ + ((List n, List k) → ∃i[i ≤ n + k ∧ 0 ≤ i ∧ i≤max (k, n)].List i)"] ); @@ -2271,7 +2270,7 @@ let rec filter_map2 = fun p q r f g h -> δ = ((b → c → Bool) → (b → Bool) → (c → Bool) → (b → c → a) → (b → a) → (c → a) → - (List (b, n), List (c, k)) → ∃i[0 ≤ i ∧ i ≤ n + k ∧ + (List (b, n), List (c, k)) → ∃i[i ≤ n + k ∧ 0 ≤ i ∧ i≤max (k, n)].List (a, i))"] ); @@ -2302,8 +2301,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[i ≤ n + k ∧ - 0 ≤ i ∧ i≤max (n, k) ∧ min (n, k)≤i].List (a, i))"] + (c → a) → (List (b, n), List (c, k)) → ∃i[0 ≤ i ∧ + i ≤ n + k ∧ i≤max (n, k) ∧ min (n, k)≤i].List (a, i))"] ); "avl_tree--height" >:: @@ -2342,7 +2341,7 @@ let create = fun l x r -> δ = (Avl (a, k) → a → Avl (a, n) → ∃i[i=max (k + 1, n + 1)].Avl (a, i)) ∧ - 0 ≤ n ∧ n ≤ k + 2 ∧ 0 ≤ k ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ 0 ≤ n"]; ); "avl_tree--create2" >:: @@ -2364,7 +2363,7 @@ let create = fun l x r -> δ = (Avl (a, k) → a → Avl (a, n) → ∃i[i=max (n + 1, k + 1)].Avl (a, i)) ∧ - 0 ≤ n ∧ n ≤ k + 2 ∧ 0 ≤ k ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ 0 ≤ n"]; ); "avl_tree--singleton" >:: @@ -2559,7 +2558,7 @@ let rotr = fun l x r -> (* hl = hr + 3 *) δ = (Avl (a, k) → a → Avl (a, n) → ∃n[k ≤ n ∧ n ≤ k + 1].Avl (a, n)) ∧ - 0 ≤ n ∧ n + 2 ≤ k ∧ k ≤ n + 3"]; + k ≤ n + 3 ∧ n + 2 ≤ k ∧ 0 ≤ n"]; ); (* The [rotl] functions are symmetrical to [rotr]. *) @@ -2682,7 +2681,7 @@ let rotl = fun l x r -> (* hl + 3 = hr *) δ = (Avl (a, k) → a → Avl (a, n) → ∃k[k ≤ n + 1 ∧ n ≤ k].Avl (a, k)) ∧ - n ≤ k + 3 ∧ 0 ≤ k ∧ k + 2 ≤ n"]; + k + 2 ≤ n ∧ 0 ≤ k ∧ n ≤ k + 3"]; ); "avl_tree--add-simple" >:: @@ -2980,7 +2979,7 @@ let rec remove_min_binding = efunction (* The inequality [k + 2 ≤ 2 n] corresponds to the fact [n=1 ==> k=0]. *) [2,"∃n, a. δ = - (Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ + (Avl (a, n) → ∃k[k + 2 ≤ 2 n ∧ n ≤ k + 1 ∧ k ≤ n].Avl (a, k)) ∧ 1 ≤ n"]; ); @@ -3026,7 +3025,7 @@ let rec remove_min_binding = efunction (* The inequality [k + 2 ≤ 2 n] corresponds to the fact [n=1 ==> k=0]. *) [2,"∃n, a. δ = - (Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ + (Avl (a, n) → ∃k[k + 2 ≤ 2 n ∧ n ≤ k + 1 ∧ k ≤ n].Avl (a, k)) ∧ 1 ≤ n"]; ); @@ -3071,8 +3070,8 @@ let rec remove_min_binding = efunction (* The inequality [k + 2 ≤ 2 n] corresponds to the fact [n=1 ==> k=0]. *) [2,"∃n, a. δ = - (Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ - k ≤ n].Avl (a, k)) ∧ + (Avl (a, n) → ∃k[k ≤ n ∧ n ≤ k + 1 ∧ + k + 2 ≤ 2 n].Avl (a, k)) ∧ 1 ≤ n"]; ); @@ -3127,7 +3126,7 @@ let merge = efunction δ = ((Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ i ≤ n + k ∧ k ≤ i ∧ i≤max (k + 1, n + 1)].Avl (a, i)) ∧ - n ≤ k + 2 ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ n ≤ k + 2"]; ); "avl_tree--merge" >:: @@ -3181,7 +3180,7 @@ let merge = efunction δ = ((Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ i ≤ n + k ∧ k ≤ i ∧ i≤max (k + 1, n + 1)].Avl (a, i)) ∧ - n ≤ k + 2 ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ n ≤ k + 2"]; ); "avl_tree--merge2" >:: @@ -3235,7 +3234,7 @@ let merge = efunction δ = ((Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ i ≤ n + k ∧ k ≤ i ∧ i≤max (k + 1, n + 1)].Avl (a, i)) ∧ - n ≤ k + 2 ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ n ≤ k + 2"]; ); "avl_tree--merge3" >:: @@ -3341,7 +3340,7 @@ let merge = efunction δ = ((Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ k ≤ i ∧ i ≤ n + k ∧ i≤max (k + 1, n + 1)].Avl (a, i)) ∧ - n ≤ k + 2 ∧ k ≤ n + 2"]; + k ≤ n + 2 ∧ n ≤ k + 2"]; ); "avl_tree--remove-simple" >:: diff --git a/src/NumS.ml b/src/NumS.ml index 607226e..0476100 100644 --- a/src/NumS.ml +++ b/src/NumS.ml @@ -62,8 +62,8 @@ let max_subopti_postcond = ref 5 let opti_postcond_reward = ref 5 let primary_only_target = ref true let excuse_case_by_common = ref (* true *)false -let verif_all_brs = ref false -let verif_incremental = ref true(* false *) +let verif_all_brs = ref false(* true *) +let verif_incremental = ref (* true *)false let abd_fail_flag = ref false let abd_timeout_flag = ref false @@ -102,7 +102,7 @@ let sort_of_subst sb = sort_of_assoc (varmap_to_assoc sb) let (!/) i = num_of_int i type w = (var_name * num) list * num * loc -type w_subst = (var_name * w) list +type w_subst = w VarMap.t let w_size (vars, cst, _) = (if cst =/ !/0 then 0 else 1) + @@ -231,7 +231,7 @@ let add_to_affine ~is_lhs l af = let affine_exists f af = CombMap.exists (fun vars (cst, lc) -> f (vars, cst, lc)) af -type ineqs = (var_name * (affine * affine)) list +type ineqs = (affine * affine) VarMap.t type optis = (w * w) list type suboptis = (w * w) list @@ -247,7 +247,8 @@ let pr_sw ppf (v, w) = Format.fprintf ppf "@[<2>%s@ =@ %a@]" (var_str v) pr_w w let pr_w_subst ppf sb = - Format.fprintf ppf "@[<2>%a@]" (pr_sep_list "," pr_sw) sb + Format.fprintf ppf "@[<2>%a@]" (pr_sep_list "," pr_sw) + (varmap_to_assoc sb) let pr_ineq ppf (v, (wl, wr)) = let wl = affine_to_ineqn wl @@ -257,7 +258,10 @@ let pr_ineq ppf (v, (wl, wr)) = (pr_sep_list ";" pr_w) wr let pr_ineqs ppf (ineqs : ineqs) = - pr_sep_list "," pr_ineq ppf ineqs + pr_sep_list "," pr_ineq ppf (varmap_to_assoc ineqs) + +let pr_hineqs ppf ineqs = + pr_sep_list "," pr_ineq ppf (hashtbl_to_assoc ineqs) let pr_opti ppf (w1, w2) = Format.fprintf ppf "@[<2>opti(%a,@ %a)@]" pr_w w1 pr_w w2 @@ -401,11 +405,13 @@ let nonq_cmp_w (vars1,cst1,_) (vars2,cst2,_) = aux (vars1, vars2) let unsubst sb = - List.map (fun (v, (vars, cst, loc)) -> (v, !/(-1))::vars, cst, loc) sb + VarMap.fold + (fun v (vars, cst, loc) acc -> ((v, !/(-1))::vars, cst, loc)::acc) + sb [] (* FIXME: no need to sort the variables? *) -let unsolve (ineqs : ineqs) : w list = concat_map - (fun (v, (left, right)) -> +let unsolve (ineqs : ineqs) : w list = concat_varmap + (fun v (left, right) -> let left = affine_to_ineqn left and right = affine_to_ineqn right in List.map (fun (vars, cst, loc) -> (v, !/(-1))::vars, cst, loc) @@ -455,7 +461,7 @@ let flatten_formula ~cmp_v cnj = List.map (flatten ~cmp_v) cnj let subst_w ~cmp_v (eqs : w_subst) (vars, cst, loc : w) : w = let sums = List.map (fun (v,k) -> - try let vars, cst, _ = mult k (List.assoc v eqs) in vars, cst + try let vars, cst, _ = mult k (VarMap.find v eqs) in vars, cst with Not_found -> [v,k], !/0) vars in let vars, csts = List.split sums in @@ -491,8 +497,8 @@ let subst_ineqs ~cmp_v eqs ineqs = List.map wset_map (subst_w ~cmp_v eqs) right)) ineqs -let subst_eqs ~cmp_v ~sb eqs = List.map - (fun (v, eq) -> v, subst_w ~cmp_v sb eq) eqs +let subst_eqs ~cmp_v ~sb eqs = VarMap.map + (fun eq -> subst_w ~cmp_v sb eq) eqs let subst_one ~cmp_v (v, w) (vars, cst, loc as arg) = try @@ -627,44 +633,46 @@ let extract_v_subst v (vars, cst, loc) = v, mult (!/(-1) // j) (vars, cst, loc) let expand_subst ~keep ~bvs eqs = - List.split - (List.map - (fun (v, (vars, cst, loc as w) as sw) -> - let w' = (v, !/(-1))::vars, cst, loc in - (*[* Format.printf "expand_subst: v=%s w=%a@ norm=%a@\n%!" - (var_str v) pr_w w pr_w - (norm_by_lcd ((v, !/(-1))::vars, cst, loc)); *]*) - if not (VarSet.mem v bvs) then (v, (expand_w w, loc)), sw - else match expand_sides - (norm_by_lcd ((v, !/(-1))::vars, cst, loc)) with - | Lin (1, 1, v), t when not (VarSet.mem v keep) -> - (*[* Format.printf - "expand_subst: [1] v=%s t=%a@\n%!" (var_str v) pr_term t; *]*) - (v, (t, loc)), extract_v_subst v w' - | t, Lin (1, 1, v) when not (VarSet.mem v keep) -> - (*[* Format.printf - "expand_subst: [2] v=%s t=%a@\n%!" (var_str v) pr_term t; *]*) - (v, (t, loc)), extract_v_subst v w' - | _ when not (VarSet.mem v keep) -> - (*[* Format.printf - "expand_subst: [3] v=%s t=%a@\n%!" (var_str v) - pr_term (expand_w w); *]*) - (v, (expand_w w, loc)), sw - | _ -> - (*[* Format.printf - "expand_subst: [3] orig_v=%s orig_t=%a@\n%!" (var_str v) - pr_term (expand_w w); *]*) - let keep_vars, cands = List.partition - (fun (v, _) -> VarSet.mem v keep) vars in - match cands with - | [] -> (v, (expand_w w, loc)), sw - | (v, j)::vars -> - let w = mult (!/1 // j) (vars @ cands, cst, loc) in + let sb, sb' = + List.split + (List.map + (fun (v, (vars, cst, loc as w) as sw) -> + let w' = (v, !/(-1))::vars, cst, loc in + (*[* Format.printf "expand_subst: v=%s w=%a@ norm=%a@\n%!" + (var_str v) pr_w w pr_w + (norm_by_lcd ((v, !/(-1))::vars, cst, loc)); *]*) + if not (VarSet.mem v bvs) then (v, (expand_w w, loc)), sw + else match expand_sides + (norm_by_lcd ((v, !/(-1))::vars, cst, loc)) with + | Lin (1, 1, v), t when not (VarSet.mem v keep) -> + (*[* Format.printf + "expand_subst: [1] v=%s t=%a@\n%!" (var_str v) pr_term t; *]*) + (v, (t, loc)), extract_v_subst v w' + | t, Lin (1, 1, v) when not (VarSet.mem v keep) -> + (*[* Format.printf + "expand_subst: [2] v=%s t=%a@\n%!" (var_str v) pr_term t; *]*) + (v, (t, loc)), extract_v_subst v w' + | _ when not (VarSet.mem v keep) -> (*[* Format.printf "expand_subst: [3] v=%s t=%a@\n%!" (var_str v) pr_term (expand_w w); *]*) - (v, (expand_w w, loc)), extract_v_subst v w') - eqs) + (v, (expand_w w, loc)), sw + | _ -> + (*[* Format.printf + "expand_subst: [3] orig_v=%s orig_t=%a@\n%!" (var_str v) + pr_term (expand_w w); *]*) + let keep_vars, cands = List.partition + (fun (v, _) -> VarSet.mem v keep) vars in + match cands with + | [] -> (v, (expand_w w, loc)), sw + | (v, j)::vars -> + let w = mult (!/1 // j) (vars @ cands, cst, loc) in + (*[* Format.printf + "expand_subst: [3] v=%s t=%a@\n%!" (var_str v) + pr_term (expand_w w); *]*) + (v, (expand_w w, loc)), extract_v_subst v w') + (varmap_to_assoc eqs)) in + varmap_of_assoc sb, varmap_of_assoc sb' let expand_formula = List.map (function @@ -698,7 +706,8 @@ let cnj_to_w_formula (eqn, ineqn, optis, suboptis) = let num_to_formula phi = List.map (fun a -> Terms.A (Terms.Num_atom a)) phi let eqn_of_eqs eqs = - List.map (fun (v,(vars,cst,loc)) -> (v,!/(-1))::vars,cst,loc) eqs + VarMap.fold + (fun v (vars,cst,loc) acc -> ((v,!/(-1))::vars,cst,loc)::acc) eqs [] let eqineq_loc_union (eqn, ineqn) = List.fold_left loc_union dummy_loc @@ -903,7 +912,7 @@ let trans_affine ~cmp_v (ineqs : ineqs) ~is_lhs wn = | ([], _, _ as w)::wn -> proj (affine_add ~is_lhs w acc) wn | ((v,k)::vars, cst, loc as w)::wn -> let left, right = - try List.assoc v ineqs + try VarMap.find v ineqs with Not_found -> affine_empty, affine_empty in let is_left = if k true, true, bvs | Fail_viol bvs -> false, true, bvs in let eqs = - if eqs' = [] then eqs else subst_eqs ~cmp_v ~sb:eqs' eqs @ eqs' in + if VarMap.is_empty eqs' then eqs + else varmap_merge (subst_eqs ~cmp_v ~sb:eqs' eqs) eqs' in let eqs_implicits = ref [] in let subst_side_ineq ~is_lhs v sb ohs w = let vars, cst, lc as w' = subst_w ~cmp_v sb w in if affine_mem ~is_lhs:(not is_lhs) w' ohs then eqs_implicits := ((v,!/(-1))::vars,cst,lc) :: !eqs_implicits; w' in - let ineqs = if eqs' = [] then ineqs else List.map - (fun (v,(wl,wr)) -> v, - (affine_map ~is_lhs:true - (subst_side_ineq ~is_lhs:true v eqs' wr) wl, - affine_map ~is_lhs:false - (subst_side_ineq ~is_lhs:false v eqs' wl) wr)) + let ineqs = if VarMap.is_empty eqs' then ineqs else VarMap.mapi + (fun v (wl,wr) -> + affine_map ~is_lhs:true + (subst_side_ineq ~is_lhs:true v eqs' wr) wl, + affine_map ~is_lhs:false + (subst_side_ineq ~is_lhs:false v eqs' wl) wr) ineqs in let more_eqn, more_ineqn, more_optis, more_suboptis = split_flatten ~cmp_v cnj in @@ -954,9 +964,12 @@ let solve_aux ~use_quants ?(strict=false) (*[* Format.printf "NumS.solve: start ineqn0=@ %a@\n%!" pr_ineqn ineqn0; *]*) assert (not strict || eqn = []); - let eqn = if eqs=[] then eqn else List.map (subst_w ~cmp_v eqs) eqn in + let eqn = + if VarMap.is_empty eqs then eqn + else List.map (subst_w ~cmp_v eqs) eqn in let ineqn0 = - if eqs=[] then ineqn0 else List.map (subst_w ~cmp_v eqs) ineqn0 in + if VarMap.is_empty eqs then ineqn0 + else List.map (subst_w ~cmp_v eqs) ineqn0 in let optis1 = List.map (subst_w ~cmp_v eqs) (flat2 optis) in let ineqn = ineqn0 @ optis1 in (*[* Format.printf "NumS.solve: subst1 ineqn0=@ %a@\n%!" @@ -1006,35 +1019,40 @@ let solve_aux ~use_quants ?(strict=false) (* [eqn0] and [ineqn0] store the unprocessed but substituted new equations and inequalities. *) let eqn0 = eqn in - let eqn = List.rev (elim [] eqn) in + let eqn = varmap_of_assoc (elim [] eqn) in + let new_eqvars = + VarSet.union (varmap_domain eqn) (varmap_domain eqs') in (*[* Format.printf "NumS.solve: solved eqn=@ %a@\n%!" pr_w_subst eqn; *]*) - let ineqn = if eqn=[] then ineqn else List.map (subst_w ~cmp_v eqn) ineqn in + let ineqn = if VarMap.is_empty eqn then ineqn + else List.map (subst_w ~cmp_v eqn) ineqn in (*[* Format.printf "NumS.solve: subst2 ineqn=@ %a@\n%!" pr_ineqn ineqn; *]*) - let eqs = if eqn=[] then eqs else subst_eqs ~cmp_v ~sb:eqn eqs in + let eqs = if VarMap.is_empty eqn then eqs + else subst_eqs ~cmp_v ~sb:eqn eqs in (* inequalities [left <= v] and [v <= right] *) - let ineqs = if eqn=[] then ineqs else - List.map (fun (v, (wl, wr)) -> - v, - (affine_map ~is_lhs:true - (subst_side_ineq ~is_lhs:true v eqn wr) wl, - affine_map ~is_lhs:false - (subst_side_ineq ~is_lhs:false v eqn wl) wr)) ineqs in + let ineqs = if VarMap.is_empty eqn then ineqs else + VarMap.mapi (fun v (wl, wr) -> + affine_map ~is_lhs:true + (subst_side_ineq ~is_lhs:true v eqn wr) wl, + affine_map ~is_lhs:false + (subst_side_ineq ~is_lhs:false v eqn wl) wr) ineqs in (*[* Format.printf "NumS.solve: simplified eqn=@ %a@\n%!" pr_w_subst eqn; *]*) let more_ineqn = - concat_map - (fun (v, w) -> + concat_varmap + (fun v w -> try - let left, right = List.assoc v ineqs in + let left, right = VarMap.find v ineqs in affine_map_to_list (fun lhs -> diff ~cmp_v lhs w) left @ affine_map_to_list (fun rhs -> diff ~cmp_v w rhs) right with Not_found -> []) eqn in + let ineqs = VarMap.filter + (fun v _ -> not (VarSet.mem v new_eqvars)) ineqs in let ineqn = List.sort cmp_w (more_ineqn @ ineqn) in (*[* Format.printf "NumS.solve:@\neqs=%a@\nsimplified ineqn=@ %a@\n%!" - pr_w_subst (eqn @ eqs) pr_ineqn ineqn; *]*) + pr_w_subst (varmap_merge eqn eqs) pr_ineqn ineqn; *]*) let project v (vars, cst, loc as lhs) rhs = if equal_w ~cmp_v lhs rhs then @@ -1056,9 +1074,9 @@ let solve_aux ~use_quants ?(strict=false) pr_ineqs ineqs pr_eqn implicits pr_ineqn ineqn0; *]*) let handle_proj v k vars cst loc ineqn = let trans_affine = trans_affine ~cmp_v ineqs in - let (left, right), ineqs = - try pop_assoc v ineqs - with Not_found -> (affine_empty, affine_empty), ineqs in + let left, right = + try VarMap.find v ineqs + with Not_found -> affine_empty, affine_empty in let ineq_l, ineq_r, (more_ineqn, more_implicits) = (* Change sides wrt. to variable [v]. *) let ohs = mult (!/(-1) // k) (vars, cst, loc) in @@ -1095,14 +1113,15 @@ let solve_aux ~use_quants ?(strict=false) let ineqn = merge_one_nonredund ~cmp_v ~cmp_w (List.sort cmp_w more_ineqn) ineqn in let more_ineqs = - v, (affine_union ~is_lhs:true - (trans_affine ~is_lhs:true ineq_l) left, - affine_union ~is_lhs:false - (trans_affine ~is_lhs:false ineq_r) right) in + affine_union ~is_lhs:true + (trans_affine ~is_lhs:true ineq_l) left, + affine_union ~is_lhs:false + (trans_affine ~is_lhs:false ineq_r) right in (*[* Format.printf "NumS.solve-project: res v=%s@\nmore_ineqn=@ %a@\nineqs_v=@ %a@\n%!" - (var_str v) pr_ineqn more_ineqn pr_ineqs [more_ineqs]; *]*) - let ineqs = more_ineqs::ineqs in + (var_str v) pr_ineqn more_ineqn + pr_ineqs (VarMap.singleton v more_ineqs); *]*) + let ineqs = VarMap.add v more_ineqs ineqs in proj ineqs (more_implicits @ implicits) ineqn in match ineqn0 with | [] -> ineqs, implicits @@ -1121,7 +1140,7 @@ let solve_aux ~use_quants ?(strict=false) when storeable && quant_viol uni_v cmp_v ~storeable bvs v vars -> let old_ineq = try - let lhs, rhs = List.assoc v ineqs in + let lhs, rhs = VarMap.find v ineqs in let ohs = mult (!/(-1) // k) (vars, cst, loc) in if k >/ !/0 then affine_mem ~is_lhs:false ohs rhs else affine_mem ~is_lhs:true ohs lhs @@ -1157,11 +1176,11 @@ let solve_aux ~use_quants ?(strict=false) else Some (Left (m, n)) in (*[* Format.printf "NumS.solve: solving optis...@\n%!"; *]*) let optis, more_implicits = - if eqn = [] then optis, [] + if VarMap.is_empty eqn then optis, [] else partition_choice (map_some propagate optis) in (*[* Format.printf "NumS.solve: solving suboptis...@\n%!"; *]*) let suboptis, more_ineqn = - if eqn = [] then suboptis, [] + if VarMap.is_empty eqn then suboptis, [] else partition_choice (map_some propagate suboptis) in (*[* Format.printf "NumS.solve: solving ineqs...@\nineqn=%a@\n%!" pr_ineqn ineqn; *]*) @@ -1170,14 +1189,14 @@ let solve_aux ~use_quants ?(strict=false) (*[* Format.printf "NumS.solve: done@\nineqs=@ %a@\n%!" pr_ineqs ineqs; *]*) - (eqn @ eqs, ineqs, + (varmap_merge eqn eqs, ineqs, optis, suboptis), eqn0, ineqn0, WSet.elements (wset_of_list implicits), !quant_viol_cnj type num_solution = w_subst * ineqs * optis * suboptis let solve_get_eqn ~use_quants ?strict - ?(eqs=[]) ?(ineqs=[]) ?(eqs'=[]) + ?(eqs=VarMap.empty) ?(ineqs=VarMap.empty) ?(eqs'=VarMap.empty) ?(optis=[]) ?(suboptis=[]) ?(eqn=[]) ?(ineqn=[]) ?(cnj=[]) ?(cnj'=[]) ~cmp_v ~cmp_w uni_v = (*[* Format.printf @@ -1206,10 +1225,12 @@ let solve_get_eqn ~use_quants ?strict loop (solve_aux ~use_quants ?strict ~eqs ~ineqs ~optis ~suboptis ~eqn:implicits - ~eqs':[] ~ineqn:[] ~cnj:[] ~cnj':[] ~cmp_v ~cmp_w uni_v)) in - if eqn=[] && (eqs=[] || eqs'=[]) && ineqn=[] && optis=[] && + ~eqs':VarMap.empty + ~ineqn:[] ~cnj:[] ~cnj':[] ~cmp_v ~cmp_w uni_v)) in + if eqn=[] && (VarMap.is_empty eqs || VarMap.is_empty eqs') && + ineqn=[] && optis=[] && suboptis=[] && cnj=[] && cnj'=[] - then (eqs @ eqs', ineqs, [], []), [], [], [], [] + then (varmap_merge eqs eqs', ineqs, [], []), [], [], [], [] else let (eqs,ineqs,optis,suboptis as res) = loop (solve_aux ~use_quants ?strict ~eqs ~ineqs ~eqs' ~optis ~suboptis @@ -1355,11 +1376,11 @@ let implies_discard ~cmp_v ~cmp_w uni_v ~bvs (eqs, ineqs, optis, suboptis) (c_eqn, c_ineqn, c_optis, c_suboptis) = let eqs' = if !abd_discard_param_only - then List.filter (fun (v, _) -> VarSet.mem v bvs) eqs + then VarMap.filter (fun v _ -> VarSet.mem v bvs) eqs else eqs in let ineqs' = if !abd_discard_param_only - then List.filter (fun (v, _) -> VarSet.mem v bvs) ineqs + then VarMap.filter (fun v _ -> VarSet.mem v bvs) ineqs else ineqs in let c_eqn' = if !abd_discard_param_only @@ -1407,9 +1428,9 @@ let implies_ineq ~cmp_v ~cmp_w ineqs ineq = let rec proj (ineqs : ineqs) ineqn0 = let handle_proj v k vars cst loc ineqn = let trans_affine = trans_affine ~cmp_v ineqs in - let (left, right), ineqs = - try pop_assoc v ineqs - with Not_found -> (affine_empty, affine_empty), ineqs in + let left, right = + try VarMap.find v ineqs + with Not_found -> affine_empty, affine_empty in let ineq_l, ineq_r, more_ineqn = (* Change sides wrt. to variable [v]. *) let ohs = mult (!/(-1) // k) (vars, cst, loc) in @@ -1439,14 +1460,15 @@ let implies_ineq ~cmp_v ~cmp_w ineqs ineq = let ineqn = merge_one_nonredund ~cmp_v ~cmp_w (List.sort cmp_w more_ineqn) ineqn in let more_ineqs = - v, (affine_union ~is_lhs:true - (trans_affine ~is_lhs:true ineq_l) left, - affine_union ~is_lhs:false - (trans_affine ~is_lhs:false ineq_r) right) in + affine_union ~is_lhs:true + (trans_affine ~is_lhs:true ineq_l) left, + affine_union ~is_lhs:false + (trans_affine ~is_lhs:false ineq_r) right in (*[* Format.printf "NumS.impl-project: res v=%s@\nmore_ineqn=@ %a@\nineqs_v=@ %a@\n%!" - (var_str v) pr_ineqn more_ineqn pr_ineqs [more_ineqs]; *]*) - let ineqs = more_ineqs::ineqs in + (var_str v) pr_ineqn more_ineqn + pr_ineqs (VarMap.singleton v more_ineqs); *]*) + let ineqs = VarMap.add v more_ineqs ineqs in proj ineqs ineqn in match ineqn0 with | [] -> () @@ -1506,8 +1528,8 @@ let trans_w_atom ~cmp_v tr = function [c]], output [[] <= a <= [b]; [a] <= b <= [c]; [b] <= c <= []]. *) let complete_ineqs ~cmp_v ineqs = let ineqn = unsolve ineqs in - let res = Hashtbl.create (List.length ineqs) in - List.iter (fun (v, v_ineqs) -> Hashtbl.add res v v_ineqs) ineqs; + let res = Hashtbl.create (VarMap.cardinal ineqs) in + VarMap.iter (fun v v_ineqs -> Hashtbl.add res v v_ineqs) ineqs; List.iter (fun (vars, cst, lc) -> List.iter @@ -1536,7 +1558,7 @@ let revert_uni ~cmp_v ~cmp_w ~uni_v ~bvs eqn = let rev_sb, _, _, _ = (* Do not use quantifiers. *) solve ~eqn ~cmp_v ~cmp_w uni_v in - List.filter (fun (v, (vars, _, _)) -> + VarMap.filter (fun v (vars, _, _) -> uni_v v && not (VarSet.mem v bvs) && not (List.exists (fun (v', _) -> uni_v v' && not (VarSet.mem v' bvs)) vars)) rev_sb @@ -1577,8 +1599,8 @@ let abd_cands ~cmp_v ~qcmp_v ~cmp_w ~uni_v ~orig_ren ~b_of_v ~upward_of "NumS.abd_cands: w=%a@ bvs=%a@\nnonparam_vars=%a@\n\ d_ineqs=%a@ d_ineqn=%a@\nbh_ineqs=@ %a@\n%!" pr_w w pr_vars bvs pr_vars nonparam_vars - pr_ineqs (hashtbl_to_assoc d_ineqs) pr_ineqn d_ineqn - pr_ineqs (hashtbl_to_assoc bh_ineqs); *]*) + pr_hineqs d_ineqs pr_ineqn d_ineqn + pr_hineqs bh_ineqs; *]*) let cands_vs = concat_map (fun ((v, coef), vars1) -> @@ -2097,7 +2119,7 @@ let abd_simple ~qcmp_v ~cmp_w conflicts with a live-code branch, should be discarded. *) let (d_eqs0, d_ineqs0, _, _), _, _, d_implicits, _ = (* TODO: could we speed up abduction by using Store_viol? *) - solve_get_eqn ~use_quants:Ignore_viol ~eqs:eqs_i ~eqs':[] + solve_get_eqn ~use_quants:Ignore_viol ~eqs:eqs_i ~eqs':VarMap.empty ~ineqs:ineqs_i ~eqn:d_eqn' ~ineqn:d_ineqn' ~optis:[] ~suboptis:[] ~cnj:[] ~cmp_v ~cmp_w uni_v in (*[* Format.printf @@ -2545,7 +2567,7 @@ module NumAbd = struct num_to_formula (cnj_to_num_formula concl) let is_taut (eqs, ineqs, optis, suboptis) = - eqs=[] && ineqs=[] && optis=[] && suboptis=[] + VarMap.is_empty eqs && VarMap.is_empty ineqs && optis=[] && suboptis=[] let pr_branch pp (_, (d_eqn, d_ineqn), (c_eqn, c_ineqn, c_optis, c_suboptis)) = @@ -2556,7 +2578,8 @@ module NumAbd = struct let pr_ans pp (eqs, ineqs, optis, suboptis) = Format.fprintf pp "eqs=%a@\nineqs=%a@\noptis=%a@\nsuboptis=%a@\n%!" - pr_w_subst eqs pr_ineqs ineqs pr_optis optis pr_suboptis suboptis + pr_w_subst eqs pr_ineqs ineqs + pr_optis optis pr_suboptis suboptis end module JCA = Joint.JointAbduction (NumAbd) @@ -2606,7 +2629,8 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) try let (d_eqs,d_ineqs,d_optis,d_suboptis), _, _, d_opti_eqn, _ = solve_aux ~cmp_v ~cmp_w q.uni_v ~use_quants:Ignore_viol - ~eqs:[] ~ineqs:[] ~eqs':[] ~cnj:[] ~cnj':[] + ~eqs:VarMap.empty ~ineqs:VarMap.empty + ~eqs':VarMap.empty ~cnj:[] ~cnj':[] ~eqn:d_eqn ~ineqn:d_ineqn ~optis:d_optis ~suboptis:d_suboptis in (*[* Format.printf @@ -2736,7 +2760,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) (fun (br_vs, brs_r, (_ (*[* as brs_n *]*)), (_, chi_pos, _, (d_eqn, d_ineqn), (c_eqn, c_ineqn, c_optis, c_suboptis))) -> - if chi_pos <> [] || + if !verif_all_brs || chi_pos <> [] || VarSet.exists (fun v -> VarSet.mem v br_vs) added_vs then let prem_state = @@ -2752,9 +2776,20 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) with Terms.Contradiction _ as e -> Left e in match prem_state with | Right (eqs,ineqs,optis,suboptis) -> + (*[* Format.printf + "v_eqs=%a@\nv_ineqs=%a@\nv_optis=%a@\nv_suboptis=%a@\n%!" + pr_w_subst eqs pr_ineqs ineqs pr_optis optis + pr_suboptis suboptis; *]*) let u_eqn, u_ineqn, u_optis, u_suboptis as u = subst_chi chi_sb chi_pos in - if VarSet.exists (fun v -> VarSet.mem v br_vs) added_vs || + (*[* Format.printf + "brc_eqn=%a@\nbrc_ineqn=%a@\nbrc_optis=%a@\n\ + brc_suboptis=%a@\n%!" + pr_eqn (u_eqn @ c_eqn) pr_ineqn (u_ineqn @ c_ineqn) + pr_optis (u_optis @ c_optis) + pr_suboptis (suboptis @ u_suboptis @ c_suboptis); *]*) + if !verif_all_brs || + VarSet.exists (fun v -> VarSet.mem v br_vs) added_vs || VarSet.exists (fun v -> VarSet.mem v br_vs) (fvs_sep_w_formula u) then @@ -2846,7 +2881,8 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) let ans = JCA.abd {cmp_v; cmp_w; NumAbd.qcmp_v = q.cmp_v; orig_ren; b_of_v; upward_of; uni_v = q.uni_v; bvs; xbvs; nonparam_vars} - ~discard validation ~validate ~neg_validate ([], [], [], []) brs in + ~discard validation ~validate ~neg_validate + (VarMap.empty, VarMap.empty, [], []) brs in [], elim_uni @ ans_to_num_formula ans @@ -2937,9 +2973,9 @@ let project ~cmp_v ~cmp_w ineqs ineqn = | [] -> ineqs | ([], cst, _)::ineqn (* when cst <=/ !/0 *) -> proj ineqs ineqn | ((v,k)::vars, cst, loc)::ineqn -> - let (left, right), ineqs = - try pop_assoc v ineqs - with Not_found -> (affine_empty, affine_empty), ineqs in + let left, right = + try VarMap.find v ineqs + with Not_found -> affine_empty, affine_empty in let ineq_l, ineq_r, more_ineqn = let ohs = mult (!/(-1) // k) (vars, cst, loc) in if k >/ !/0 @@ -2961,8 +2997,9 @@ let project ~cmp_v ~cmp_w ineqs ineqn = let ineqn = merge cmp_w (List.sort cmp_w more_ineqn) ineqn in let ineqs = - (v, (add_to_affine ~is_lhs:true ineq_l left, - add_to_affine ~is_lhs:false ineq_r right))::ineqs in + VarMap.add v + (add_to_affine ~is_lhs:true ineq_l left, + add_to_affine ~is_lhs:false ineq_r right) ineqs in proj ineqs ineqn in proj ineqs ineqn @@ -2983,9 +3020,9 @@ let strict_sat ~cmp_v ~cmp_w (ineqs : ineqs) | ([], cst, loc)::_ -> raise Not_satisfiable | ((v,k)::vars, cst, loc)::ineqn -> - let (left, right), ineqs = - try pop_assoc v ineqs - with Not_found -> (affine_empty, affine_empty), ineqs in + let left, right = + try VarMap.find v ineqs + with Not_found -> affine_empty, affine_empty in let ohs = mult (!/(-1) // k) (vars, cst, loc) in let ineq_l, ineq_r, more_ineqn = if k >/ !/0 @@ -3018,8 +3055,10 @@ let strict_sat ~cmp_v ~cmp_w (ineqs : ineqs) let ineqn = merge cmp_w (List.sort cmp_w more_ineqn) ineqn in let ineqs = - (v, (add_to_affine ~is_lhs:true ineq_l left, - add_to_affine ~is_lhs:false ineq_r right))::ineqs in + VarMap.add v + (add_to_affine ~is_lhs:true ineq_l left, + add_to_affine ~is_lhs:false ineq_r right) + ineqs in proj strict ineqs ineqn in let res = try @@ -3239,7 +3278,7 @@ let prune_redund ~cmp_v ~cmp_w guard_cnj cnj = [g_ineqn]) in (*[* Format.printf "NumS.prune_redund:@\ninit_ineqn=@ %a@\n%!" pr_ineqn init_ineqn; *]*) - let init_ineqs = project ~cmp_v ~cmp_w [] + let init_ineqs = project ~cmp_v ~cmp_w VarMap.empty (List.sort cmp_w init_ineqn) in let init_ineqs_for_subopti = project ~cmp_v ~cmp_w init_ineqs (List.sort cmp_w ineqn) in @@ -3381,14 +3420,14 @@ let disjelim_aux q ~target_vs ~preserve ~bvs ~param_bvs "NumS.disjelim: substituted p_ineqs=@\n%a@\n%!" pr_ineqs p_ineqs; *]*) (* Simplify downto preserved variables. *) - let eqs = List.filter - (fun (v,_) -> VarSet.mem v preserved) eqs in - let ineqs = List.filter - (fun (v,_) -> VarSet.mem v preserved) ineqs in - let p_eqs = List.filter - (fun (v,_) -> VarSet.mem v preserved) p_eqs in - let p_ineqs = List.filter - (fun (v,_) -> VarSet.mem v preserved) p_ineqs in + let eqs = VarMap.filter + (fun v _ -> VarSet.mem v preserved) eqs in + let ineqs = VarMap.filter + (fun v _ -> VarSet.mem v preserved) ineqs in + let p_eqs = VarMap.filter + (fun v _ -> VarSet.mem v preserved) p_eqs in + let p_ineqs = VarMap.filter + (fun v _ -> VarSet.mem v preserved) p_ineqs in (*[* Format.printf "NumS.disjelim: success opti_choice=@\n%a@\n%!" pr_w_formula opti_subopti; *]*) @@ -3459,7 +3498,8 @@ let disjelim_aux q ~target_vs ~preserve ~bvs ~param_bvs let faces, equations = split_map (fun (eqs, ineqs) -> let eq_classes = collect ~cmp_k:(compare_w ~cmp_v) - (List.map (fun (v, rhs) -> rhs, v) eqs) in + (List.map (fun (v, rhs) -> rhs, v) + (varmap_to_assoc eqs)) in let eq_sides = concat_map (fun (rhs, lvs) -> let ws = @@ -3478,7 +3518,7 @@ let disjelim_aux q ~target_vs ~preserve ~bvs ~param_bvs let ineqs = unsolve ineqs in let faces = ineqs @ eq_sides @ List.map (mult !/(-1)) eq_sides in - let _, res, _ = keep_nonredund ~cmp_v ~cmp_w [] faces in + let _, res, _ = keep_nonredund ~cmp_v ~cmp_w VarMap.empty faces in (*[* Format.printf "ptop-ineqs=%a@\nptop-faces=%a@\nptop-res=%a@\n%!" pr_ineqn ineqs pr_ineqn faces pr_ineqn res; *]*) @@ -3937,7 +3977,7 @@ let simplify q ?(keepvs=VarSet.empty) ?localvs ?(guard=[]) elimvs cnj = let eqs, ineqs, optis, suboptis = solve ~cnj ~cmp_v ~cmp_w q.uni_v in let eqs = - List.filter (fun (v,_) -> + VarMap.filter (fun v _ -> VarSet.mem v keepvs || not (VarSet.mem v elimvs)) eqs in (*let ineqs = List.filter (fun (v,_) -> @@ -3997,7 +4037,7 @@ let converge q ?localvs ?(guard=[]) ~initstep cnj1 cnj2 = type state = w_subst * ineqs * optis * suboptis -let empty_state = [], [], [], [] +let empty_state = VarMap.empty, VarMap.empty, [], [] let formula_of_state (eqs, ineqs, optis, suboptis) = let cnj = expand_eqineqs eqs ineqs in @@ -4115,10 +4155,8 @@ let negation_elim q ~bvs ~verif_cns neg_cns = let rev_sb, _, _, _ = (* Do not use quantifiers. *) solve ~cnj ~cmp_v ~cmp_w q.uni_v in - let rev_sb = - map_some (fun (v, w) -> - if uni_v v then Some (v, expand_w w) else None) rev_sb in - varmap_of_assoc rev_sb in + VarMap.map expand_w + (VarMap.filter (fun v _ -> uni_v v) rev_sb) in (* The formula will be conjoined to the branches. Note that the branch will be non-recursive. *) let res = concat_map @@ -4227,8 +4265,8 @@ let separate_subst_aux q ~no_csts ~keep ~bvs ~apply cnj = (function | v, ([], cst, lc) -> Left (cst, (v, lc)) | eq -> Right eq) - eqs - else [], eqs in + (varmap_to_assoc eqs) + else [], varmap_to_assoc eqs in let c_eqn = collect ~cmp_k:Num.compare_num c_eqn in let leq (v1, _) (v2, _) = cmp_v v1 v2 >= 0 in @@ -4252,11 +4290,11 @@ let separate_subst_aux q ~no_csts ~keep ~bvs ~apply cnj = c_eqs in let eqs, more_eqs = List.partition (fun (v,_) -> not (VarSet.mem v keep)) (c_eqs @ eqs) in + let eqs = varmap_of_assoc eqs in let sb, eqs = expand_subst ~keep ~bvs eqs in - let sb = varmap_of_assoc sb in (*[* Format.printf "NumS.separate_subst: no_csts=%b@ eq-keys=%a@ sb=%a@\n%!" - no_csts pr_vars (vars_of_list (List.map fst eqs)) + no_csts pr_vars (varmap_domain eqs) pr_num_subst sb; *]*) if not apply then @@ -4274,10 +4312,10 @@ let separate_subst_aux q ~no_csts ~keep ~bvs ~apply cnj = (*[* Format.printf "NumS.separate_subst: bvs=%a@ phi=%a@\n%!" pr_vars bvs pr_formula phi_num; *]*) let more_sb, _ = - expand_subst ~keep ~bvs more_eqs in + expand_subst ~keep ~bvs (varmap_of_assoc more_eqs) in let more = List.map (fun (v,(t,lc)) -> Eq (Lin (1,1,v), t, lc)) - more_sb in + (varmap_to_assoc more_sb) in sb, more @ phi_num (* TODO: move to VarMap-based solutions? *) diff --git a/test.log b/test.log index 9713150..9c1b6eb 100644 --- a/test.log +++ b/test.log @@ -1,36 +1,8 @@ -Compilation started at Tue Mar 3 18:24:59 +Compilation started at Wed Mar 18 02:26:37 make testnative ocamlbuild src/Tests.native -lib nums -pkg oUnit -- Warning: tag "package" does not expect a parameter, but is used with parameter "oUnit" -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/Abduction.ml > src/Abduction.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/NumS.ml > src/NumS.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/Joint.ml > src/Joint.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/Joint.mli > src/Joint.mli.depends -/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Joint.cmi src/Joint.mli -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Joint.cmx src/Joint.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumS.cmx src/NumS.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Infer.cmx src/Infer.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Abduction.cmx src/Abduction.ml -+ /home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Abduction.cmx src/Abduction.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Lexer.cmx src/Lexer.ml -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/DisjElim.ml > src/DisjElim.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/DisjElim.cmx src/DisjElim.ml -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/Invariants.ml > src/Invariants.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/OCaml.ml > src/OCaml.ml.depends -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Invariants.cmx src/Invariants.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/OCaml.cmx src/OCaml.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvarGenT.cmx src/InvarGenT.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/AbductionTest.cmx src/AbductionTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/DisjElimTest.cmx src/DisjElimTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InferTest.cmx src/InferTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvarGenTTest.cmx src/InvarGenTTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvariantsTest.cmx src/InvariantsTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumSTest.cmx src/NumSTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/OrderSTest.cmx src/OrderSTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/TermsTest.cmx src/TermsTest.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Tests.cmx src/Tests.ml -/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt nums.cmxa -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml unix.cmxa oUnit.cmxa src/Aux.cmx src/Defs.cmx src/NumDefs.cmx src/OrderDefs.cmx src/Terms.cmx src/Joint.cmx src/NumS.cmx src/OrderS.cmx src/Infer.cmx src/Abduction.cmx src/Parser.cmx src/Lexer.cmx src/AbductionTest.cmx src/DisjElim.cmx src/DisjElimTest.cmx src/InferTest.cmx src/Invariants.cmx src/OCaml.cmx src/InvarGenT.cmx src/InvarGenTTest.cmx src/InvariantsTest.cmx src/NumSTest.cmx src/OrderSTest.cmx src/TermsTest.cmx src/Tests.cmx -o src/Tests.native InvarGenT:0:Terms:0:parsing and printing ... ok InvarGenT:0:Terms:1:parsing existentials ... @@ -58,9 +30,9 @@ ok InvarGenT:5:DisjElim:1:simplified eval ... ok InvarGenT:6:Invariants:0:simple eval ... - t=0.013s ok + t=0.009s ok InvarGenT:6:Invariants:1:simple assert false ... - t=0.002s ok + t=0.003s ok InvarGenT:6:Invariants:2:foo without when 1 ... t=0.001s ok InvarGenT:6:Invariants:3:foo without when 2 ... @@ -68,27 +40,27 @@ InvarGenT:6:Invariants:3:foo without when 2 ... InvarGenT:6:Invariants:4:foo with when 1 ... t=0.004s ok InvarGenT:6:Invariants:5:foo with when 2 ... - t=0.002s ok + t=0.003s ok InvarGenT:6:Invariants:6:deadcode foo ... t=0.002s ok InvarGenT:6:Invariants:7:deadcode foo fail ... ok InvarGenT:6:Invariants:8:abs ... - t=0.011s ok + t=0.010s ok InvarGenT:6:Invariants:9:abs2 ... - t=0.012s ok + t=0.011s ok InvarGenT:6:Invariants:10:eval ... - t=0.090s ok + t=0.050s ok InvarGenT:6:Invariants:11:eval hard ... - t=0.076s ok + t=0.046s ok InvarGenT:6:Invariants:12:equal1 wrong type ... - t=0.226s ok + t=0.140s ok InvarGenT:6:Invariants:13:equal with test ... - t=0.428s ok + t=0.251s ok InvarGenT:6:Invariants:14:equal with assert ... - t=1.319s ok + t=2.158s ok InvarGenT:6:Invariants:15:equal with assert and test ... - t=0.634s ok + t=1.216s ok InvarGenT:6:Invariants:16:SPJ non-principal 1 ... t=0.002s ok InvarGenT:6:Invariants:17:SPJ non-principal 2 ... @@ -96,234 +68,234 @@ InvarGenT:6:Invariants:17:SPJ non-principal 2 ... InvarGenT:6:Invariants:18:TS infinitely non-principal ... t=0.002s ok InvarGenT:6:Invariants:19:TS non-principal subexpr ... - t=0.003s ok + t=0.002s ok InvarGenT:6:Invariants:20:TS non-principal subexpr 2 ... ok InvarGenT:6:Invariants:21:simple existential ... - t=0.019s ok + t=0.017s ok InvarGenT:6:Invariants:22:simple universal ... t=0.004s ok InvarGenT:6:Invariants:23:simple existential 2 ... - t=0.033s ok + t=0.031s ok InvarGenT:6:Invariants:24:map mono ... t=0.006s ok InvarGenT:6:Invariants:25:append expanded ... - t=0.019s ok + t=0.020s ok InvarGenT:6:Invariants:26:append asserted ... t=0.022s ok InvarGenT:6:Invariants:27:interleave ... - t=0.015s ok + t=0.017s ok InvarGenT:6:Invariants:28:interleave 3 ... - t=0.146s ok + t=0.133s ok InvarGenT:6:Invariants:29:binary increment ... - t=0.008s ok + t=0.009s ok InvarGenT:6:Invariants:30:binary plus expanded ... - t=0.744s ok + t=0.655s ok InvarGenT:6:Invariants:31:binary plus asserted ... - t=0.861s ok + t=0.772s ok InvarGenT:6:Invariants:32:binary plus with test ... - t=0.848s ok + t=0.717s ok InvarGenT:6:Invariants:33:flatten_pairs ... t=0.013s ok InvarGenT:6:Invariants:34:escape castle ... - t=0.126s ok + t=0.098s ok InvarGenT:6:Invariants:35:easy nested universal ... - t=0.024s ok + t=0.018s ok InvarGenT:6:Invariants:36:equational nested universal ... - t=1.575s ok + t=0.655s ok InvarGenT:6:Invariants:37:double nested universal ... - t=0.043s ok + t=0.030s ok InvarGenT:6:Invariants:38:find castle ... - t=0.017s ok + t=0.015s ok InvarGenT:6:Invariants:39:find castle big ... - t=0.034s ok + t=0.031s ok InvarGenT:6:Invariants:40:search castle shortcut ... - t=0.021s ok + t=0.019s ok InvarGenT:6:Invariants:41:search castle distance ... - t=0.037s ok + t=0.030s ok InvarGenT:6:Invariants:42:search castle distance A/B ... - t=0.053s ok + t=0.050s ok InvarGenT:6:Invariants:43:castle not existential ... - t=0.010s ok + t=0.011s ok InvarGenT:6:Invariants:44:castle nested not existential ... - t=0.017s ok + t=0.015s ok InvarGenT:6:Invariants:45:castle nested existential factored ... - t=0.019s ok + t=0.018s ok InvarGenT:6:Invariants:46:castle nested existential ... - t=0.021s ok + t=0.020s ok InvarGenT:6:Invariants:47:existential by hand ... - t=0.017s ok + t=0.016s ok InvarGenT:6:Invariants:48:existential with param ... - t=0.067s ok + t=0.049s ok InvarGenT:6:Invariants:49:universal option ... t=0.005s ok InvarGenT:6:Invariants:50:existential option ... - t=0.019s ok + t=0.016s ok InvarGenT:6:Invariants:51:not existential option ... - t=0.035s ok + t=0.022s ok InvarGenT:6:Invariants:52:non-num map not existential poly ... - t=0.034s ok + t=0.023s ok InvarGenT:6:Invariants:53:non-num map not existential mono ... - t=0.012s ok + t=0.013s ok InvarGenT:6:Invariants:54:map not existential mono ... - t=0.012s ok + t=0.014s ok InvarGenT:6:Invariants:55:map not existential poly ... - t=0.053s ok + t=0.037s ok InvarGenT:6:Invariants:56:map not existential instance ... t=0.024s ok InvarGenT:6:Invariants:57:filter mono ... - t=0.101s ok + t=0.100s ok InvarGenT:6:Invariants:58:filter Bar ... - t=0.126s ok + t=0.119s ok InvarGenT:6:Invariants:59:filter poly ... - t=0.278s ok + t=0.178s ok InvarGenT:6:Invariants:60:poly filter map ... - t=0.403s ok + t=0.228s ok InvarGenT:6:Invariants:61:binary upper bound-wrong ... - t=1.044s ok + t=0.893s ok InvarGenT:6:Invariants:62:binary upper bound expanded ... - t=1.512s ok + t=1.249s ok InvarGenT:6:Invariants:63:nested recursion simple eval ... - t=0.011s ok + t=0.010s ok InvarGenT:6:Invariants:64:nested recursion eval ... - t=0.096s ok + t=0.059s ok InvarGenT:6:Invariants:65:mutual recursion simple calc ... - t=0.072s ok + t=0.063s ok InvarGenT:6:Invariants:66:mutual recursion medium calc ... - t=0.120s ok + t=0.094s ok InvarGenT:6:Invariants:67:mutual recursion calc ... - t=0.570s ok + t=0.419s ok InvarGenT:6:Invariants:68:local defs simple ... t=0.004s ok InvarGenT:6:Invariants:69:local recursion simple ... - t=0.015s ok + t=0.011s ok InvarGenT:6:Invariants:70:nonrec simple ... - t=0.000s ok + t=0.001s ok InvarGenT:6:Invariants:71:binomial heap--rank ... t=0.002s ok InvarGenT:6:Invariants:72:binomial heap--link ... t=0.021s ok InvarGenT:6:Invariants:73:unary minimum expanded ... - t=0.212s ok + t=0.207s ok InvarGenT:6:Invariants:74:unary minimum asserted 1 ... - t=0.275s ok + t=0.276s ok InvarGenT:6:Invariants:75:unary minimum asserted 2 ... - t=0.273s ok + t=0.274s ok InvarGenT:6:Invariants:76:unary minimum asserted 3 ... - t=0.427s ok + t=0.431s ok InvarGenT:6:Invariants:77:list zip prefix expanded ... - t=0.648s ok + t=0.381s ok InvarGenT:6:Invariants:78:unary maximum expanded ... - t=0.075s ok + t=0.073s ok InvarGenT:6:Invariants:79:list map2 with postfix expanded ... - t=0.207s ok + t=0.136s ok InvarGenT:6:Invariants:80:list filter-zip prefix ... - t=1.070s ok + t=0.582s ok InvarGenT:6:Invariants:81:list filter-map2 with postfix ... - t=0.961s ok + t=0.615s ok InvarGenT:6:Invariants:82:list filter-map2 with filter postfix mono ... - t=1.159s ok + t=0.930s ok InvarGenT:6:Invariants:83:non-num no postcond list filter-map2 with filter postfix ... - t=0.223s ok + t=0.103s ok InvarGenT:6:Invariants:84:non-num list filter-map2 with filter postfix ... - t=1.533s ok + t=0.653s ok InvarGenT:6:Invariants:85:list filter-map2 with filter postfix ... - t=6.263s ok + t=2.492s ok InvarGenT:6:Invariants:86:list map2 with filter postfix ... - t=5.046s ok + t=2.106s ok InvarGenT:6:Invariants:87:avl_tree--height ... t=0.005s ok InvarGenT:6:Invariants:88:avl_tree--create ... - t=0.100s ok + t=0.085s ok InvarGenT:6:Invariants:89:avl_tree--create2 ... - t=0.106s ok + t=0.089s ok InvarGenT:6:Invariants:90:avl_tree--singleton ... t=0.004s ok InvarGenT:6:Invariants:91:avl_tree--min_binding ... - t=0.031s ok + t=0.037s ok InvarGenT:6:Invariants:92:avl_tree--rotr-simple ... - t=3.266s ok + t=3.111s ok InvarGenT:6:Invariants:93:avl_tree--rotr-simple2 ... - t=1.515s ok + t=1.440s ok InvarGenT:6:Invariants:94:avl_tree--rotr-simple3 ... - t=1.647s ok + t=1.569s ok InvarGenT:6:Invariants:95:avl_tree--rotr ... - t=1.170s ok + t=1.072s ok InvarGenT:6:Invariants:96:avl_tree--rotl-simple ... - t=3.276s ok + t=3.075s ok InvarGenT:6:Invariants:97:avl_tree--rotl-simple2 ... - t=1.124s ok + t=1.086s ok InvarGenT:6:Invariants:98:avl_tree--rotl ... - t=1.179s ok + t=1.081s ok InvarGenT:6:Invariants:99:avl_tree--add-simple ... - t=0.690s ok + t=0.452s ok InvarGenT:6:Invariants:100:avl_tree--add-simple2 ... - t=0.604s ok + t=0.432s ok InvarGenT:6:Invariants:101:avl_tree--add ... - t=1.060s ok + t=0.690s ok InvarGenT:6:Invariants:102:avl_tree--add2 ... - t=0.960s ok + t=0.687s ok InvarGenT:6:Invariants:103:avl_tree--add-harder ... - t=0.928s ok + t=0.625s ok InvarGenT:6:Invariants:104:avl_tree--remove_min_binding-simple ... - t=0.853s ok + t=0.327s ok InvarGenT:6:Invariants:105:avl_tree--remove_min_binding ... - t=2.367s ok + t=0.659s ok InvarGenT:6:Invariants:106:avl_tree--remove_min_binding-harder ... - t=2.210s ok + t=0.587s ok InvarGenT:6:Invariants:107:avl_tree--merge-simple ... - t=1.029s ok + t=1.016s ok InvarGenT:6:Invariants:108:avl_tree--merge ... - t=1.802s ok + t=1.694s ok InvarGenT:6:Invariants:109:avl_tree--merge2 ... - t=1.286s ok + t=1.206s ok InvarGenT:6:Invariants:110:avl_tree--merge3 ... TODO InvarGenT:6:Invariants:111:avl_tree--merge4 ... - t=1.055s ok + t=0.932s ok InvarGenT:6:Invariants:112:avl_tree--remove-simple ... - t=0.467s ok + t=0.332s ok InvarGenT:6:Invariants:113:avl_tree--remove ... - t=0.637s ok + t=0.431s ok InvarGenT:6:Invariants:114:avl_tree--remove2 ... - t=0.640s ok + t=0.439s ok InvarGenT:6:Invariants:115:avl_tree--remove-harder ... - t=0.579s ok + t=0.380s ok InvarGenT:7:InvarGenT:0:simple eval ... InvarGenT: Generated file ./examples/simple_eval.gadti InvarGenT: Generated file ./examples/simple_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_eval.ml" exited with code 0 - t=0.012s ok + t=0.010s ok InvarGenT:7:InvarGenT:1:eval ... InvarGenT: Generated file ./examples/eval.gadti InvarGenT: Generated file ./examples/eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/eval.ml" exited with code 0 - t=0.091s ok + t=0.053s ok InvarGenT:7:InvarGenT:2:simple when ... InvarGenT: Generated file ./examples/simple_when.gadti InvarGenT: Generated file ./examples/simple_when.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_when.ml" exited with code 0 - t=0.005s ok + t=0.006s ok InvarGenT:7:InvarGenT:3:equal1_wrong ... InvarGenT: Generated file ./examples/equal1_wrong.gadti InvarGenT: Generated file ./examples/equal1_wrong.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal1_wrong.ml" exited with code 0 - t=0.225s ok + t=0.139s ok InvarGenT:7:InvarGenT:4:equal_test ... InvarGenT: Generated file ./examples/equal_test.gadti InvarGenT: Generated file ./examples/equal_test.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal_test.ml" exited with code 0 - t=0.408s ok + t=0.251s ok InvarGenT:7:InvarGenT:5:equal_assert ... InvarGenT: Generated file ./examples/equal_assert.gadti InvarGenT: Generated file ./examples/equal_assert.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal_assert.ml" exited with code 0 - t=1.317s ok + t=2.141s ok InvarGenT:7:InvarGenT:6:binary_plus ... InvarGenT: Generated file ./examples/binary_plus.gadti InvarGenT: Generated file ./examples/binary_plus.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binary_plus.ml" exited with code 0 - t=0.749s ok + t=0.657s ok InvarGenT:7:InvarGenT:7:binary_plus-harder ... TODO InvarGenT:7:InvarGenT:8:flatten_pairs ... @@ -335,77 +307,77 @@ InvarGenT:7:InvarGenT:9:flatten_quadrs ... InvarGenT: Generated file ./examples/flatten_quadrs.gadti InvarGenT: Generated file ./examples/flatten_quadrs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/flatten_quadrs.ml" exited with code 0 - t=0.068s ok + t=0.060s ok InvarGenT:7:InvarGenT:10:flatten_septs ... InvarGenT: Generated file ./examples/flatten_septs.gadti InvarGenT: Generated file ./examples/flatten_septs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/flatten_septs.ml" exited with code 0 - t=0.953s ok + t=0.915s ok InvarGenT:7:InvarGenT:11:equational_reas ... InvarGenT: Generated file ./examples/equational_reas.gadti InvarGenT: Generated file ./examples/equational_reas.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equational_reas.ml" exited with code 0 - t=1.588s ok + t=0.658s ok InvarGenT:7:InvarGenT:12:filter ... InvarGenT: Generated file ./examples/filter.gadti InvarGenT: Generated file ./examples/filter.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/filter.ml" exited with code 0 - t=0.286s ok + t=0.179s ok InvarGenT:7:InvarGenT:13:filter_map ... InvarGenT: Generated file ./examples/filter_map.gadti InvarGenT: Generated file ./examples/filter_map.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/filter_map.ml" exited with code 0 - t=0.417s ok + t=0.232s ok InvarGenT:7:InvarGenT:14:binary_upper_bound ... InvarGenT: Generated file ./examples/binary_upper_bound.gadti InvarGenT: Generated file ./examples/binary_upper_bound.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binary_upper_bound.ml" exited with code 0 - t=1.532s ok + t=1.214s ok InvarGenT:7:InvarGenT:15:ex_config_pc ... InvarGenT: Generated file ./examples/ex_config_pc.gadti InvarGenT: Generated file ./examples/ex_config_pc.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/ex_config_pc.ml" exited with code 0 - t=0.059s ok + t=0.049s ok InvarGenT:7:InvarGenT:16:mutual_simple_recursion_eval ... InvarGenT: Generated file ./examples/mutual_simple_recursion_eval.gadti InvarGenT: Generated file ./examples/mutual_simple_recursion_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_simple_recursion_eval.ml" exited with code 0 - t=0.142s ok + t=0.120s ok InvarGenT:7:InvarGenT:17:binomial_heap_nonrec ... InvarGenT: Generated file ./examples/binomial_heap_nonrec.gadti InvarGenT: Generated file ./examples/binomial_heap_nonrec.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binomial_heap_nonrec.ml" exited with code 0 - t=0.026s ok + t=0.025s ok InvarGenT:7:InvarGenT:18:mutual_recursion_eval ... InvarGenT: Generated file ./examples/mutual_recursion_eval.gadti InvarGenT: Generated file ./examples/mutual_recursion_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_recursion_eval.ml" exited with code 0 - t=0.970s ok + t=0.676s ok InvarGenT:7:InvarGenT:19:simple eval-annot ... InvarGenT: Generated file ./examples/simple_eval.gadti InvarGenT: Generated file ./examples/simple_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_eval.ml" exited with code 0 - t=0.021s ok + t=0.010s ok InvarGenT:7:InvarGenT:20:eval-annot ... InvarGenT: Generated file ./examples/eval.gadti InvarGenT: Generated file ./examples/eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/eval.ml" exited with code 0 - t=0.101s ok + t=0.058s ok InvarGenT:7:InvarGenT:21:equational_reas-annot ... InvarGenT: Generated file ./examples/equational_reas.gadti InvarGenT: Generated file ./examples/equational_reas.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equational_reas.ml" exited with code 0 - t=1.710s ok + t=0.715s ok InvarGenT:7:InvarGenT:22:mutual_recursion_eval-annot ... InvarGenT: Generated file ./examples/mutual_recursion_eval_docs.gadti InvarGenT: Generated file ./examples/mutual_recursion_eval_docs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_recursion_eval_docs.ml" exited with code 0 - t=0.971s ok + t=0.672s ok InvarGenT:7:InvarGenT:23:concat_strings-export ... InvarGenT: Generated file ./examples/concat_strings.gadti InvarGenT: Generated file ./examples/concat_strings.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/concat_strings.ml" exited with code 0 - t=0.013s ok + t=0.006s ok InvarGenT:7:InvarGenT:24:list-head ... InvarGenT: Generated file ./examples/list_head.gadti InvarGenT: Generated file ./examples/list_head.ml @@ -421,22 +393,22 @@ InvarGenT:7:InvarGenT:26:pointwise-refine ... InvarGenT: Generated file ./examples/pointwise_refine.gadti InvarGenT: Generated file ./examples/pointwise_refine.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_refine.ml" exited with code 0 - t=0.013s ok + t=0.008s ok InvarGenT:7:InvarGenT:27:pointwise-rbtree_rotate ... InvarGenT: Generated file ./examples/pointwise_rbtree_rotate.gadti InvarGenT: Generated file ./examples/pointwise_rbtree_rotate.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_rbtree_rotate.ml" exited with code 0 - t=0.030s ok + t=0.019s ok InvarGenT:7:InvarGenT:28:pointwise-zip2-simpler1 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler1.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler1.ml" exited with code 0 - t=0.013s ok + t=0.011s ok InvarGenT:7:InvarGenT:29:pointwise-zip2-simpler2 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler2.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler2.ml" exited with code 0 - t=0.024s ok + t=0.019s ok InvarGenT:7:InvarGenT:30:pointwise-zip2-simpler3 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler3.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler3.ml @@ -446,60 +418,60 @@ InvarGenT:7:InvarGenT:31:pointwise-zip2-simpler4 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler4.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler4.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler4.ml" exited with code 0 - t=0.172s ok + t=0.124s ok InvarGenT:7:InvarGenT:32:pointwise-zip2 ... InvarGenT: Generated file ./examples/pointwise_zip2.gadti InvarGenT: Generated file ./examples/pointwise_zip2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2.ml" exited with code 0 - t=0.271s ok + t=0.186s ok InvarGenT:7:InvarGenT:33:pointwise-zip2-harder ... InvarGenT: Generated file ./examples/pointwise_zip2_harder.gadti - t=0.242s ok + t=0.162s ok InvarGenT:7:InvarGenT:34:pointwise-avl_rotl ... InvarGenT: Generated file ./examples/pointwise_avl_rotl.gadti InvarGenT: Generated file ./examples/pointwise_avl_rotl.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_avl_rotl.ml" exited with code 0 - t=0.030s ok + t=0.025s ok InvarGenT:7:InvarGenT:35:pointwise-avl_ins ... InvarGenT: Generated file ./examples/pointwise_avl_ins.gadti InvarGenT: Generated file ./examples/pointwise_avl_ins.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_avl_ins.ml" exited with code 0 - t=0.746s ok + t=0.408s ok InvarGenT:7:InvarGenT:36:pointwise-extract0 ... InvarGenT: Generated file ./examples/pointwise_extract0.gadti InvarGenT: Generated file ./examples/pointwise_extract0.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract0.ml" exited with code 0 - t=0.028s ok + t=0.015s ok InvarGenT:7:InvarGenT:37:pointwise-extract1 ... InvarGenT: Generated file ./examples/pointwise_extract1.gadti InvarGenT: Generated file ./examples/pointwise_extract1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract1.ml" exited with code 0 - t=0.505s ok + t=0.066s ok InvarGenT:7:InvarGenT:38:pointwise-extract2 ... InvarGenT: Generated file ./examples/pointwise_extract2.gadti InvarGenT: Generated file ./examples/pointwise_extract2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract2.ml" exited with code 0 - t=0.293s ok + t=0.036s ok InvarGenT:7:InvarGenT:39:pointwise-extract ... InvarGenT: Generated file ./examples/pointwise_extract.gadti InvarGenT: Generated file ./examples/pointwise_extract.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract.ml" exited with code 0 - t=0.376s ok + t=0.058s ok InvarGenT:7:InvarGenT:40:pointwise-run_state ... InvarGenT: Generated file ./examples/pointwise_run_state.gadti InvarGenT: Generated file ./examples/pointwise_run_state.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_run_state.ml" exited with code 0 - t=0.023s ok + t=0.013s ok InvarGenT:7:InvarGenT:41:non_outsidein-rx ... InvarGenT: Generated file ./examples/non_outsidein_rx.gadti InvarGenT: Generated file ./examples/non_outsidein_rx.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_outsidein_rx.ml" exited with code 0 - t=0.003s ok + t=0.002s ok InvarGenT:7:InvarGenT:42:non_pointwise-split ... InvarGenT: Generated file ./examples/non_pointwise_split.gadti InvarGenT: Generated file ./examples/non_pointwise_split.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_split.ml" exited with code 0 - t=0.004s ok + t=0.003s ok InvarGenT:7:InvarGenT:43:non_pointwise-avl_small_rec ... InvarGenT: Generated file ./examples/non_pointwise_avl_small_rec.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_small_rec.ml @@ -508,7 +480,7 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (Less, _, _, _) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_small_rec.ml" exited with code 0 - t=0.014s ok + t=0.011s ok InvarGenT:7:InvarGenT:44:non_pointwise-avl_small ... InvarGenT: Generated file ./examples/non_pointwise_avl_small.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_small.ml @@ -517,7 +489,7 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (Less, _, _, _) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_small.ml" exited with code 0 - t=0.016s ok + t=0.012s ok InvarGenT:7:InvarGenT:45:non_pointwise-avl_rotr ... InvarGenT: Generated file ./examples/non_pointwise_avl.gadti InvarGenT: Generated file ./examples/non_pointwise_avl.ml @@ -526,103 +498,103 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (More, _, _, Leaf) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl.ml" exited with code 0 - t=0.113s ok + t=0.090s ok InvarGenT:7:InvarGenT:46:avl_delmin-simpler ... InvarGenT: Generated file ./examples/avl_delmin_simpler.gadti InvarGenT: Generated file ./examples/avl_delmin_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/avl_delmin_simpler.ml" exited with code 0 - t=0.182s ok + t=0.130s ok InvarGenT:7:InvarGenT:47:non_pointwise-avl_delmin-modified ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin_modified.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin_modified.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin_modified.ml" exited with code 0 - t=0.282s ok + t=0.187s ok InvarGenT:7:InvarGenT:48:non_pointwise-avl_delmin ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin.ml" exited with code 0 - t=0.473s ok + t=0.307s ok InvarGenT:7:InvarGenT:49:non_pointwise-avl_delmin2 ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin2.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin2.ml" exited with code 0 - t=0.452s ok + t=0.306s ok InvarGenT:7:InvarGenT:50:non_pointwise-fd_comp ... InvarGenT: Generated file ./examples/non_pointwise_fd_comp.gadti InvarGenT: Generated file ./examples/non_pointwise_fd_comp.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_fd_comp.ml" exited with code 0 - t=0.538s ok + t=0.175s ok InvarGenT:7:InvarGenT:51:non_pointwise-fd_comp2 ... InvarGenT: Generated file ./examples/non_pointwise_fd_comp2.gadti InvarGenT: Generated file ./examples/non_pointwise_fd_comp2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_fd_comp2.ml" exited with code 0 - t=0.106s ok + t=0.052s ok InvarGenT:7:InvarGenT:52:non_pointwise-fd_comp-harder ... TODO InvarGenT:7:InvarGenT:53:non_pointwise-zip1-simpler ... InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_simpler.ml" exited with code 0 - t=0.041s ok + t=0.017s ok InvarGenT:7:InvarGenT:54:non_pointwise-zip1-simpler2 ... InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler2.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_simpler2.ml" exited with code 0 - t=0.047s ok + t=0.017s ok InvarGenT:7:InvarGenT:55:non_pointwise-zip1-modified ... InvarGenT: Generated file ./examples/non_pointwise_zip1_modified.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_modified.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_modified.ml" exited with code 0 - t=0.079s ok + t=0.031s ok InvarGenT:7:InvarGenT:56:non_pointwise-zip1 ... InvarGenT: Generated file ./examples/non_pointwise_zip1.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1.ml" exited with code 0 - t=0.133s ok + t=0.076s ok InvarGenT:7:InvarGenT:57:non_pointwise-leq ... InvarGenT: Generated file ./examples/non_pointwise_leq.gadti InvarGenT: Generated file ./examples/non_pointwise_leq.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_leq.ml" exited with code 0 - t=0.013s ok + t=0.005s ok InvarGenT:7:InvarGenT:58:non_pointwise-run_state ... InvarGenT: Generated file ./examples/non_pointwise_run_state.gadti InvarGenT: Generated file ./examples/non_pointwise_run_state.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_run_state.ml" exited with code 0 - t=0.053s ok + t=0.025s ok InvarGenT:7:InvarGenT:59:non_pointwise-run_state2 ... InvarGenT: Generated file ./examples/non_pointwise_run_state2.gadti InvarGenT: Generated file ./examples/non_pointwise_run_state2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_run_state2.ml" exited with code 0 - t=0.042s ok + t=0.023s ok InvarGenT:7:InvarGenT:60:avl_tree ... InvarGenT: Generated file ./examples/avl_tree.gadti InvarGenT: Generated file ./examples/avl_tree.ml -File "./examples/avl_tree.ml", line 43, characters 4-161: +File "./examples/avl_tree.ml", line 42, characters 4-161: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty -File "./examples/avl_tree.ml", line 39, characters 4-322: +File "./examples/avl_tree.ml", line 38, characters 4-322: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty -File "./examples/avl_tree.ml", line 59, characters 4-161: +File "./examples/avl_tree.ml", line 58, characters 4-161: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty -File "./examples/avl_tree.ml", line 55, characters 4-322: +File "./examples/avl_tree.ml", line 54, characters 4-322: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty -File "./examples/avl_tree.ml", line 88, characters 2-101: +File "./examples/avl_tree.ml", line 87, characters 2-101: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty -File "./examples/avl_tree.ml", line 95, characters 2-310: +File "./examples/avl_tree.ml", line 94, characters 2-310: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty InvarGenT: Command "ocamlc -w -25 -c ./examples/avl_tree.ml" exited with code 0 - t=7.415s ok + t=4.924s ok InvarGenT:7:InvarGenT:61:binomial_heap ... TODO InvarGenT:7:InvarGenT:62:liquid_dotprod-simpler ... @@ -634,37 +606,37 @@ InvarGenT:7:InvarGenT:63:liquid_dotprod ... InvarGenT: Generated file ./examples/liquid_dotprod.gadti InvarGenT: Generated file ./examples/liquid_dotprod.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_dotprod.ml" exited with code 0 - t=0.051s ok + t=0.049s ok InvarGenT:7:InvarGenT:64:liquid_bcopy-simpler ... InvarGenT: Generated file ./examples/liquid_bcopy_simpler.gadti InvarGenT: Generated file ./examples/liquid_bcopy_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bcopy_simpler.ml" exited with code 0 - t=0.027s ok + t=0.026s ok InvarGenT:7:InvarGenT:65:liquid_bcopy ... InvarGenT: Generated file ./examples/liquid_bcopy.gadti InvarGenT: Generated file ./examples/liquid_bcopy.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bcopy.ml" exited with code 0 - t=0.034s ok + t=0.032s ok InvarGenT:7:InvarGenT:66:liquid_bsearch-simpler ... InvarGenT: Generated file ./examples/liquid_bsearch_simpler.gadti InvarGenT: Generated file ./examples/liquid_bsearch_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch_simpler.ml" exited with code 0 - t=0.096s ok + t=0.074s ok InvarGenT:7:InvarGenT:67:liquid_bsearch ... InvarGenT: Generated file ./examples/liquid_bsearch.gadti InvarGenT: Generated file ./examples/liquid_bsearch.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch.ml" exited with code 0 - t=0.055s ok + t=0.044s ok InvarGenT:7:InvarGenT:68:liquid_bsearch-harder ... InvarGenT: Generated file ./examples/liquid_bsearch_harder.gadti InvarGenT: Generated file ./examples/liquid_bsearch_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch_harder.ml" exited with code 0 - t=0.093s ok + t=0.071s ok InvarGenT:7:InvarGenT:69:liquid_bsearch2-simpler ... InvarGenT: Generated file ./examples/liquid_bsearch2_simpler.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_simpler.ml" exited with code 0 - t=0.950s ok + t=0.799s ok InvarGenT:7:InvarGenT:70:liquid_bsearch2-simpler2 ... InvarGenT: Generated file ./examples/liquid_bsearch2_simpler2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_simpler2.ml @@ -674,158 +646,158 @@ InvarGenT:7:InvarGenT:71:liquid_bsearch2 ... InvarGenT: Generated file ./examples/liquid_bsearch2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2.ml" exited with code 0 - t=0.849s ok + t=0.707s ok InvarGenT:7:InvarGenT:72:liquid_bsearch2-harder1 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder1.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder1.ml" exited with code 0 - t=0.845s ok + t=0.710s ok InvarGenT:7:InvarGenT:73:liquid_bsearch2-harder2 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder2.ml" exited with code 0 - t=1.376s ok + t=1.122s ok InvarGenT:7:InvarGenT:74:liquid_bsearch2-harder3 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder3.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder3.ml" exited with code 0 - t=1.806s ok + t=1.394s ok InvarGenT:7:InvarGenT:75:liquid_bsearch2-harder4 ... TODO InvarGenT:7:InvarGenT:76:liquid_queen-simpler ... InvarGenT: Generated file ./examples/liquid_queen_simpler.gadti InvarGenT: Generated file ./examples/liquid_queen_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_queen_simpler.ml" exited with code 0 - t=0.184s ok + t=0.168s ok InvarGenT:7:InvarGenT:77:liquid_queen ... InvarGenT: Generated file ./examples/liquid_queen.gadti InvarGenT: Generated file ./examples/liquid_queen.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_queen.ml" exited with code 0 - t=0.480s ok + t=0.421s ok InvarGenT:7:InvarGenT:78:liquid_isort-simpler1 ... InvarGenT: Generated file ./examples/liquid_isort_simpler1.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler1.ml" exited with code 0 - t=0.102s ok + t=0.092s ok InvarGenT:7:InvarGenT:79:liquid_isort-simpler2 ... InvarGenT: Generated file ./examples/liquid_isort_simpler2.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler2.ml" exited with code 0 - t=0.318s ok + t=0.252s ok InvarGenT:7:InvarGenT:80:liquid_isort-simpler3 ... InvarGenT: Generated file ./examples/liquid_isort_simpler3.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler3.ml" exited with code 0 - t=0.154s ok + t=0.140s ok InvarGenT:7:InvarGenT:81:liquid_isort-simpler ... InvarGenT: Generated file ./examples/liquid_isort_simpler.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler.ml" exited with code 0 - t=0.164s ok + t=0.149s ok InvarGenT:7:InvarGenT:82:liquid_isort ... InvarGenT: Generated file ./examples/liquid_isort.gadti InvarGenT: Generated file ./examples/liquid_isort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort.ml" exited with code 0 - t=0.334s ok + t=0.300s ok InvarGenT:7:InvarGenT:83:liquid_isort-harder ... InvarGenT: Generated file ./examples/liquid_isort_harder.gadti InvarGenT: Generated file ./examples/liquid_isort_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_harder.ml" exited with code 0 - t=0.446s ok + t=0.372s ok InvarGenT:7:InvarGenT:84:liquid_vecswap_simpler ... InvarGenT: Generated file ./examples/liquid_vecswap_simpler.gadti InvarGenT: Generated file ./examples/liquid_vecswap_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_vecswap_simpler.ml" exited with code 0 - t=0.325s ok + t=0.277s ok InvarGenT:7:InvarGenT:85:liquid_vecswap ... InvarGenT: Generated file ./examples/liquid_vecswap.gadti InvarGenT: Generated file ./examples/liquid_vecswap.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_vecswap.ml" exited with code 0 - t=0.299s ok + t=0.267s ok InvarGenT:7:InvarGenT:86:liquid_isort-full ... InvarGenT: Generated file ./examples/liquid_isort_full.gadti InvarGenT: Generated file ./examples/liquid_isort_full.ml File "./examples/liquid_isort_full.ml", line 35, characters 12-19: Warning 26: unused variable vecswap. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_full.ml" exited with code 0 - t=1.244s ok + t=1.047s ok InvarGenT:7:InvarGenT:87:liquid_tower_showposts ... InvarGenT: Generated file ./examples/liquid_tower_showposts.gadti InvarGenT: Generated file ./examples/liquid_tower_showposts.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_showposts.ml" exited with code 0 - t=0.051s ok + t=0.047s ok InvarGenT:7:InvarGenT:88:liquid_tower_simpler ... InvarGenT: Generated file ./examples/liquid_tower_simpler.gadti InvarGenT: Generated file ./examples/liquid_tower_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_simpler.ml" exited with code 0 - t=0.659s ok + t=0.912s ok InvarGenT:7:InvarGenT:89:liquid_tower_asserted ... InvarGenT: Generated file ./examples/liquid_tower_asserted.gadti InvarGenT: Generated file ./examples/liquid_tower_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_asserted.ml" exited with code 0 - t=4.499s ok + t=3.928s ok InvarGenT:7:InvarGenT:90:liquid_tower ... InvarGenT: Generated file ./examples/liquid_tower.gadti InvarGenT: Generated file ./examples/liquid_tower.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower.ml" exited with code 0 - t=1.093s ok + t=0.835s ok InvarGenT:7:InvarGenT:91:liquid_tower_harder ... InvarGenT: Generated file ./examples/liquid_tower_harder.gadti InvarGenT: Generated file ./examples/liquid_tower_harder.ml File "./examples/liquid_tower_harder.ml", line 69, characters 8-10: Warning 26: unused variable sz. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_harder.ml" exited with code 0 - t=7.106s ok + t=10.936s ok InvarGenT:7:InvarGenT:92:liquid_matmult ... InvarGenT: Generated file ./examples/liquid_matmult.gadti InvarGenT: Generated file ./examples/liquid_matmult.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_matmult.ml" exited with code 0 - t=0.354s ok + t=0.335s ok InvarGenT:7:InvarGenT:93:liquid_heapsort-heapify-simpler ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler.ml" exited with code 0 - t=2.478s ok + t=2.280s ok InvarGenT:7:InvarGenT:94:liquid_heapsort-heapify-simpler2 ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler2.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler2.ml" exited with code 0 - t=6.682s ok + t=6.464s ok InvarGenT:7:InvarGenT:95:liquid_heapsort-heapify-simpler3 ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler3.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler3.ml" exited with code 0 - t=3.611s ok + t=3.525s ok InvarGenT:7:InvarGenT:96:liquid_heapsort-heapify ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify.ml" exited with code 0 - t=2.614s ok + t=2.241s ok InvarGenT:7:InvarGenT:97:liquid_heapsort-heapsort-simpler ... InvarGenT: Generated file ./examples/liquid_heapsort_heapsort_simpler.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapsort_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapsort_simpler.ml" exited with code 0 - t=0.053s ok + t=0.061s ok InvarGenT:7:InvarGenT:98:liquid_heapsort-heapsort ... InvarGenT: Generated file ./examples/liquid_heapsort_heapsort.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapsort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapsort.ml" exited with code 0 - t=0.076s ok + t=0.075s ok InvarGenT:7:InvarGenT:99:liquid_heapsort ... InvarGenT: Generated file ./examples/liquid_heapsort.gadti InvarGenT: Generated file ./examples/liquid_heapsort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort.ml" exited with code 0 - t=2.707s ok + t=2.342s ok InvarGenT:7:InvarGenT:100:liquid_simplex_step_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_2.ml" exited with code 0 - t=0.238s ok + t=0.207s ok InvarGenT:7:InvarGenT:101:liquid_simplex_step_2a ... InvarGenT: Generated file ./examples/liquid_simplex_step_2a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_2a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_2a.ml" exited with code 0 - t=0.186s ok + t=0.170s ok InvarGenT:7:InvarGenT:102:liquid_simplex_step_3 ... TODO InvarGenT:7:InvarGenT:103:liquid_simplex_step_3a ... @@ -834,119 +806,119 @@ InvarGenT: Generated file ./examples/liquid_simplex_step_3a.ml File "./examples/liquid_simplex_step_3a.ml", line 43, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_3a.ml" exited with code 0 - t=4.277s ok + t=4.047s ok InvarGenT:7:InvarGenT:104:liquid_simplex_step_4 ... TODO InvarGenT:7:InvarGenT:105:liquid_simplex_step_4a ... InvarGenT: Generated file ./examples/liquid_simplex_step_4a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_4a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_4a.ml" exited with code 0 - t=0.580s ok + t=0.421s ok InvarGenT:7:InvarGenT:106:liquid_simplex_step_5a ... InvarGenT: Generated file ./examples/liquid_simplex_step_5a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_5a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_5a.ml" exited with code 0 - t=5.056s ok + t=3.290s ok InvarGenT:7:InvarGenT:107:liquid_simplex_step_6a_1 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_1.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_1.ml File "./examples/liquid_simplex_step_6a_1.ml", line 59, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_1.ml" exited with code 0 - t=0.531s ok + t=0.505s ok InvarGenT:7:InvarGenT:108:liquid_simplex_step_6_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6_2.ml" exited with code 0 - t=0.071s ok + t=0.066s ok InvarGenT:7:InvarGenT:109:liquid_simplex_step_6a_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_2.ml File "./examples/liquid_simplex_step_6a_2.ml", line 59, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_2.ml" exited with code 0 - t=0.887s ok + t=0.824s ok InvarGenT:7:InvarGenT:110:liquid_simplex_step_6_3 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6_3.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6_3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6_3.ml" exited with code 0 - t=0.066s ok + t=0.060s ok InvarGenT:7:InvarGenT:111:liquid_simplex_step_6a_3 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_3.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_3.ml File "./examples/liquid_simplex_step_6a_3.ml", line 67, characters 8-9: Warning 26: unused variable n. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_3.ml" exited with code 0 - t=0.615s ok + t=0.580s ok InvarGenT:7:InvarGenT:112:liquid_simplex_step_6a ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a.ml" exited with code 0 - t=2.536s ok + t=2.213s ok InvarGenT:7:InvarGenT:113:liquid_simplex_step_7a ... InvarGenT: Generated file ./examples/liquid_simplex_step_7a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_7a.ml File "./examples/liquid_simplex_step_7a.ml", line 65, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_7a.ml" exited with code 0 - t=0.212s ok + t=0.215s ok InvarGenT:7:InvarGenT:114:liquid_simplex ... InvarGenT: Generated file ./examples/liquid_simplex.gadti InvarGenT: Generated file ./examples/liquid_simplex.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex.ml" exited with code 0 - t=13.215s ok + t=8.109s ok InvarGenT:7:InvarGenT:115:liquid_simplex-harder ... InvarGenT: Generated file ./examples/liquid_simplex_harder.gadti InvarGenT: Generated file ./examples/liquid_simplex_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_harder.ml" exited with code 0 - t=52.970s ok + t=31.395s ok InvarGenT:7:InvarGenT:116:liquid_gauss_rowSwap ... InvarGenT: Generated file ./examples/liquid_gauss_rowSwap.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowSwap.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowSwap.ml" exited with code 0 - t=0.022s ok + t=0.031s ok InvarGenT:7:InvarGenT:117:liquid_gauss_rowElim ... InvarGenT: Generated file ./examples/liquid_gauss_rowElim.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowElim.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowElim.ml" exited with code 0 - t=0.043s ok + t=0.052s ok InvarGenT:7:InvarGenT:118:liquid_gauss_rowMax ... TODO InvarGenT:7:InvarGenT:119:liquid_gauss_rowMax_2 ... InvarGenT: Generated file ./examples/liquid_gauss_rowMax_2.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowMax_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowMax_2.ml" exited with code 0 - t=0.597s ok + t=0.463s ok InvarGenT:7:InvarGenT:120:liquid_gauss_simpler ... InvarGenT: Generated file ./examples/liquid_gauss_simpler.gadti InvarGenT: Generated file ./examples/liquid_gauss_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_simpler.ml" exited with code 0 - t=4.009s ok + t=2.782s ok InvarGenT:7:InvarGenT:121:liquid_gauss_simpler_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_simpler_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_simpler_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_simpler_asserted.ml" exited with code 0 - t=2.322s ok + t=1.953s ok InvarGenT:7:InvarGenT:122:liquid_gauss ... InvarGenT: Generated file ./examples/liquid_gauss.gadti InvarGenT: Generated file ./examples/liquid_gauss.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss.ml" exited with code 0 - t=3.368s ok + t=2.665s ok InvarGenT:7:InvarGenT:123:liquid_gauss2 ... InvarGenT: Generated file ./examples/liquid_gauss2.gadti InvarGenT: Generated file ./examples/liquid_gauss2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss2.ml" exited with code 0 - t=3.281s ok + t=1.020s ok InvarGenT:7:InvarGenT:124:liquid_gauss_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_asserted.ml" exited with code 0 - t=2.488s ok + t=0.962s ok InvarGenT:7:InvarGenT:125:liquid_gauss_harder_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_harder_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_harder_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_harder_asserted.ml" exited with code 0 - t=3.546s ok + t=2.722s ok InvarGenT:7:InvarGenT:126:liquid_gauss_harder ... TODO InvarGenT:7:InvarGenT:127:liquid_fft_ffor ... @@ -958,28 +930,28 @@ InvarGenT:7:InvarGenT:128:liquid_fft_simpler ... InvarGenT: Generated file ./examples/liquid_fft_simpler.gadti InvarGenT: Generated file ./examples/liquid_fft_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_simpler.ml" exited with code 0 - t=35.198s ok + t=29.912s ok InvarGenT:7:InvarGenT:129:liquid_fft ... InvarGenT: Generated file ./examples/liquid_fft.gadti InvarGenT: Generated file ./examples/liquid_fft.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft.ml" exited with code 0 - t=34.286s ok + t=29.564s ok InvarGenT:7:InvarGenT:130:liquid_fft_tests ... InvarGenT: Generated file ./examples/liquid_fft_tests.gadti InvarGenT: Generated file ./examples/liquid_fft_tests.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_tests.ml" exited with code 0 - t=7.321s ok + t=6.233s ok InvarGenT:7:InvarGenT:131:liquid_fft_full ... InvarGenT: Generated file ./examples/liquid_fft_full.gadti InvarGenT: Generated file ./examples/liquid_fft_full.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_full.ml" exited with code 0 - t=42.282s ok + t=36.416s ok InvarGenT:7:InvarGenT:132:liquid_fft_full_asserted ... InvarGenT: Generated file ./examples/liquid_fft_full_asserted.gadti InvarGenT: Generated file ./examples/liquid_fft_full_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_full_asserted.ml" exited with code 0 - t=43.453s ok -Ran: 262 tests in: 396.20 seconds. + t=37.541s ok +Ran: 262 tests in: 311.19 seconds. FAILED: Cases: 262 Tried: 262 Errors: 0 Failures: 0 Skip:0 Todo:10 -Compilation finished at Tue Mar 3 18:31:38 +Compilation finished at Wed Mar 18 02:31:49