From d3800e9e5c3e41aa4865edb9ce7574ea80f19146 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Sun, 15 Mar 2015 05:09:42 +0100 Subject: [PATCH] Two small bug fixes. More logging. --- examples/liquid_bsearch2_harder3.ml.target | 8 +- examples/liquid_gauss_asserted.gadti.target | 2 +- ...liquid_gauss_simpler_asserted.gadti.target | 2 +- examples/liquid_simplex_step_3a.gadti.target | 2 +- examples/mutual_recursion_eval_docs.ml.target | 6 +- src/Abduction.ml | 4 +- src/Infer.ml | 44 +++- src/InvarGenTTest.ml | 36 +-- src/Invariants.ml | 16 +- src/InvariantsTest.ml | 3 +- src/Joint.ml | 4 +- src/NumS.ml | 216 +++++++++++------- src/Terms.ml | 2 +- 13 files changed, 206 insertions(+), 139 deletions(-) diff --git a/examples/liquid_bsearch2_harder3.ml.target b/examples/liquid_bsearch2_harder3.ml.target index 278b19e..e564e9c 100644 --- a/examples/liquid_bsearch2_harder3.ml.target +++ b/examples/liquid_bsearch2_harder3.ml.target @@ -30,9 +30,9 @@ let bsearch (fun key vec -> let Ex3 xcase = let rec look : - type (*i*) (*k*) (*n*) a (*0 ≤ n + 1 ∧ 0 ≤ k ∧ - n + 1 ≤ i*). (a -> (a (* i *)) array -> (* k *) num -> (* n *) num -> - (* n *) ex3) + type (*i*) (*j*) (*k*) b (*0 ≤ k + 1 ∧ 0 ≤ i ∧ + k + 1 ≤ j*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num -> + (* k *) ex3) = (fun key vec lo hi -> (if lo <= hi then @@ -44,6 +44,6 @@ let bsearch | EQ -> (if equal key x then let xcase = m in Ex3 xcase else let xcase = -1 in Ex3 xcase))) : - (* n *) ex3) else let xcase = -1 in Ex3 xcase)) in + (* k *) ex3) else let xcase = -1 in Ex3 xcase)) in look key vec 0 (array_length vec + -1) in Ex4 xcase) diff --git a/examples/liquid_gauss_asserted.gadti.target b/examples/liquid_gauss_asserted.gadti.target index c23387a..fb69a69 100644 --- a/examples/liquid_gauss_asserted.gadti.target +++ b/examples/liquid_gauss_asserted.gadti.target @@ -71,4 +71,4 @@ val rowElim : ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j]. Array (Float, j) → Array (Float, i) → Num k → Num n → () -val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → () +val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_gauss_simpler_asserted.gadti.target b/examples/liquid_gauss_simpler_asserted.gadti.target index 85fd0d9..e536283 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[0 ≤ n]. Matrix (n, n + 1) → () +val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → () diff --git a/examples/liquid_simplex_step_3a.gadti.target b/examples/liquid_simplex_step_3a.gadti.target index 798c347..9e9f098 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 ∧ 2 ≤ k]. Matrix (n, k) → Float +val main_step3_test : ∀k, n[1 ≤ n ∧ 3 ≤ k]. Matrix (n, k) → Float diff --git a/examples/mutual_recursion_eval_docs.ml.target b/examples/mutual_recursion_eval_docs.ml.target index 23daeb5..d37b15e 100644 --- a/examples/mutual_recursion_eval_docs.ml.target +++ b/examples/mutual_recursion_eval_docs.ml.target @@ -35,7 +35,7 @@ type ex3 = be easier to only expose the external one. *) let (calc, eval) (*: type a . ((calc -> ex3) * (a term -> a))*) = (** [eval] has to expose its "helper" function. *) - let rec eval : type a . ((calc -> ex3) * (a term -> a)) = + let rec eval : type b . ((calc -> ex3) * (b term -> b)) = let rec calc : (calc -> ex3) = ((function Lit i -> let xcase = i in Ex3 xcase | Plus (x, y) -> @@ -58,7 +58,7 @@ let (calc, eval) (*: type a . ((calc -> ex3) * (a term -> a))*) = let Ex3 r = calc x in is_zero r | If (b, t, e) -> (if snd eval b then snd eval t else snd eval e) | Pair (x, y) -> (snd eval x, snd eval y) - | Fst p -> let ((x, y): (a * _)) = snd eval p in x - | Snd p -> let ((x, y): (_ * a)) = snd eval p in y): a term -> a)) in + | Fst p -> let ((x, y): (b * _)) = snd eval p in x + | Snd p -> let ((x, y): (_ * b)) = snd eval p in y): b term -> b)) in eval diff --git a/src/Abduction.ml b/src/Abduction.ml index 6db1333..8d94a44 100644 --- a/src/Abduction.ml +++ b/src/Abduction.ml @@ -952,9 +952,9 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars with Contradiction _ -> None) neg_brs in let verif_brs = List.map2 - (fun (prem, concl_ty) (_, _, _, concl_num) -> + (fun (prem, concl_ty) (_, _, prem_num, concl_num) -> VarSet.union (fvs_sb concl_ty) (NumDefs.fvs_formula concl_num), - prem, concl_ty, concl_num) + prem, concl_ty, prem_num @ concl_num) brs_typ brs_num in let validation = map_some diff --git a/src/Infer.ml b/src/Infer.ml index cf8f82d..e05f776 100644 --- a/src/Infer.ml +++ b/src/Infer.ml @@ -820,9 +820,15 @@ let annotate_expr q res_sb chi_sb nice_sb e : texpr = let _, ans = try List.find (fun (k,_) -> List.mem k ns) chi_sb with Not_found -> assert false in + (*[* Format.printf + "annotate_expr-typ_sch: ans=@ %a@\n%!" pr_ans ans; *]*) let nice_sb, (vs, phi) = nice_ans ~sb:nice_sb ans in + (*[* Format.printf + "annotate_expr-typ_sch: phi=@ %a@\n%!" pr_formula phi; *]*) let sb, phi = separate_subst ~bvs:(vars_of_list vs) ~apply:true q phi in + (*[* Format.printf + "annotate_expr-typ_sch: sb=@ %a@\n%!" pr_subst sb; *]*) let res, _ = VarMap.find delta sb in let vs = VarSet.inter (VarSet.union (fvs_formula phi) (fvs_typ res)) @@ -1019,15 +1025,31 @@ let infer_prog solver prog = let nice_sb, (vs, phi) = try nice_ans (List.assoc chi_id sb_chi) with Not_found -> assert false in + (*[* Format.printf + "Infer: nice_sb=%a@\n%!" pr_hvsubst nice_sb; *]*) + (*[* Format.printf + "Infer: [1] phi_res=%a@\n%!" + pr_formula phi_res; *]*) let sb_res, phi_res = separate_subst ~bvs:(vars_of_list (vs @ bvs)) ~apply:true q phi_res in + (*[* Format.printf + "Infer: [2] sb_res=%a@ phi_res=%a@\n%!" + pr_subst sb_res pr_formula phi_res; *]*) + (*[* Format.printf + "Infer: [3] phi=%a@\n%!" + pr_formula phi; *]*) let more_sb, phi = separate_subst ~bvs:(vars_of_list (vs @ bvs)) ~apply:true q phi in + (*[* Format.printf + "Infer: [4] more_sb=%a@ phi=%a@\n%!" + pr_subst more_sb pr_formula phi; *]*) let sb = update_sb ~more_sb sb_res in - let e = annotate_expr q sb sb_chi nice_sb e - and tests = List.map (annotate_expr q sb sb_chi nice_sb) tests in + (*[* Format.printf + "Infer: [5] sb=%a@\n%!" pr_subst sb; *]*) + let e = annotate_expr q sb sb_chi nice_sb e in + let tests = List.map (annotate_expr q sb sb_chi nice_sb) tests in let res, _ = VarMap.find delta sb in let gvs = VarSet.elements (VarSet.union (fvs_formula phi) (fvs_typ res)) in @@ -1091,8 +1113,14 @@ let infer_prog solver prog = ~uses_pos_assertions:!uses_pos_assertions ~new_ex_types ~preserve cn in let elim_extypes = !elim_cell in + (*[* Format.printf "Infer: solved.@\n%!"; *]*) + (*[* Format.printf + "Infer: [6] phi=%a@\n%!" + pr_formula phi; *]*) let sb, phi = separate_subst ~bvs:preserve ~apply:true q phi in + (*[* Format.printf + "Infer: [7] sb=%a@\n%!" pr_subst sb; *]*) let res = subst_typ sb t in let gvs = VarSet.union (fvs_formula phi) (fvs_typ res) in (*[* Format.printf "LetVal: res=%a@ gvs=%a@ phi=%a@\n%!" @@ -1100,6 +1128,8 @@ let infer_prog solver prog = let gvs = VarSet.elements gvs in let nice_sb, (gvs, phi) = nice_ans ~fvs:(fvs_typ res) (gvs, phi) in + (*[* Format.printf + "Infer: [8] nice_sb=%a@\n%!" pr_hvsubst nice_sb; *]*) let sb = hvsubst_sb nice_sb sb in let res = hvsubst_typ nice_sb res in (*[* Format.printf @@ -1109,8 +1139,13 @@ let infer_prog solver prog = let top_sch = gvs, phi, res in let e = annotate_expr q sb sb_chi nice_sb e in let exphi = subst_formula sb exphi in + (*[* Format.printf + "Infer: [9] exphi=%a@\n%!" + pr_formula exphi; *]*) let exsb, exphi = separate_subst ~bvs:(add_vars gvs preserve) ~apply:true q exphi in + (*[* Format.printf + "Infer: [10] exsb=%a@\n%!" pr_subst sb; *]*) let exsb = update_sb ~more_sb:exsb sb in let ex_items = update_new_ex_types q new_ex_types sb sb_chi in @@ -1142,9 +1177,14 @@ let infer_prog solver prog = let res = subst_typ exsb res in let gvs, phi = prepare_scheme phi res in let exvs, exphi = prepare_scheme exphi res in + (*[* Format.printf + "Infer: [11] exphi=%a@\n%!" + pr_formula exphi; *]*) let more_sb, exphi = separate_subst ~bvs:(VarSet.union exvs gvs) ~apply:true q exphi in + (*[* Format.printf + "Infer: [12] more_sb=%a@\n%!" pr_subst sb; *]*) let sb = update_sb ~more_sb sb in let exvs = VarSet.diff exvs (vars_of_list [delta; delta']) in let gvs = VarSet.diff gvs (vars_of_list [delta; delta']) in diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 4028b79..2cc3173 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -206,7 +206,6 @@ let tests = "InvarGenT" >::: [ test_case "flatten_quadrs" ()); "flatten_septs" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case ~ty_abd_timeout:3000 ~abd_rotations:4 "flatten_septs" ()); @@ -447,7 +446,6 @@ let tests = "InvarGenT" >::: [ test_case "liquid_bsearch" ()); "liquid_bsearch-harder" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_bsearch_harder" ()); "liquid_bsearch2-simpler" >:: @@ -485,7 +483,6 @@ let tests = "InvarGenT" >::: [ test_case "liquid_queen_simpler" ()); "liquid_queen" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_queen" ()); "liquid_isort-simpler1" >:: @@ -494,7 +491,6 @@ let tests = "InvarGenT" >::: [ test_case "liquid_isort_simpler1" ()); "liquid_isort-simpler2" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_isort_simpler2" ()); "liquid_isort-simpler3" >:: @@ -507,17 +503,16 @@ let tests = "InvarGenT" >::: [ test_case "liquid_isort_simpler" ()); "liquid_isort" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_isort" ()); "liquid_isort-harder" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_isort_harder" ()); "liquid_vecswap_simpler" >:: (fun () -> - skip_if !debug "debug"; + todo "FIXME"; + (* skip_if !debug "debug"; *) test_case "liquid_vecswap_simpler" ()); "liquid_vecswap" >:: (fun () -> @@ -525,7 +520,6 @@ let tests = "InvarGenT" >::: [ test_case "liquid_vecswap" ()); "liquid_isort-full" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_isort_full" ()); "liquid_tower_showposts" >:: @@ -538,7 +532,8 @@ let tests = "InvarGenT" >::: [ test_case "liquid_tower_simpler" ()); "liquid_tower_asserted" >:: (fun () -> - skip_if !debug "debug"; + todo "FIXME"; + (* skip_if !debug "debug"; *) test_case "liquid_tower_asserted" ()); "liquid_tower" >:: (fun () -> @@ -546,7 +541,8 @@ let tests = "InvarGenT" >::: [ test_case "liquid_tower" ()); "liquid_tower_harder" >:: (fun () -> - skip_if !debug "debug"; + todo "FIXME"; + (* skip_if !debug "debug"; *) test_case ~prefer_bound_to_local:true "liquid_tower_harder" ()); "liquid_matmult" >:: (fun () -> @@ -570,12 +566,10 @@ let tests = "InvarGenT" >::: [ test_case "liquid_heapsort_heapify" ()); "liquid_heapsort-heapsort-simpler" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_heapsort_heapsort_simpler" ()); "liquid_heapsort-heapsort" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_heapsort_heapsort" ()); "liquid_heapsort" >:: @@ -599,8 +593,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_3" ()); "liquid_simplex_step_3a" >:: (fun () -> - todo "FIXME"; - 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 @@ -616,12 +609,10 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_4a" ()); "liquid_simplex_step_5a" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_simplex_step_5a" ()); "liquid_simplex_step_6a_1" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_simplex_step_6a_1" ()); "liquid_simplex_step_6_2" >:: @@ -630,7 +621,6 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_6_2" ()); "liquid_simplex_step_6a_2" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case ~prefer_bound_to_local:true "liquid_simplex_step_6a_2" ()); @@ -640,12 +630,10 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_6_3" ()); "liquid_simplex_step_6a_3" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_simplex_step_6a_3" ()); "liquid_simplex_step_6a" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_simplex_step_6a" ()); "liquid_simplex_step_7a" >:: @@ -654,12 +642,10 @@ let tests = "InvarGenT" >::: [ test_case "liquid_simplex_step_7a" ()); "liquid_simplex" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case ~test_annot:true "liquid_simplex" ()); "liquid_simplex-harder" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; skip_if !short_tests_only "long test: 53s"; test_case "liquid_simplex_harder" ()); @@ -687,8 +673,7 @@ let tests = "InvarGenT" >::: [ test_case "liquid_gauss_simpler" ()); "liquid_gauss_simpler_asserted" >:: (fun () -> - todo "FIXME"; - skip_if !debug "debug"; + (* skip_if !debug "debug"; *) test_case "liquid_gauss_simpler_asserted" ()); "liquid_gauss" >:: (fun () -> @@ -697,17 +682,16 @@ let tests = "InvarGenT" >::: [ "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 () -> - todo "FIXME"; skip_if !debug "debug"; 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/Invariants.ml b/src/Invariants.ml index 0a627fb..29cfa6b 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -1423,10 +1423,12 @@ let solve ~uses_pos_assertions q_ops new_ex_types exty_res_chi brs = | TVar b -> (try let vs, _ = List.assoc i sol1 in + (* Should not have variables not already in + the quantifier. *) let renaming = - matchup_vars ~self_owned:false q b vs in + matchup_vars ~self_owned:true(* false *) q b vs in (*[* Format.printf - "sb_chi_pos: chi%d(%s)@ lvs=%a;@ rvs=%a@\n%!" + "br_chi_pos: chi%d(%s)@ lvs=%a;@ rvs=%a@\n%!" i (var_str b) pr_vars (varmap_domain renaming) pr_vars (vars_of_list (varmap_codom renaming)); @@ -1450,11 +1452,13 @@ let solve ~uses_pos_assertions q_ops new_ex_types exty_res_chi brs = (fun x xvs acc -> try (*[* Format.printf - "xbvs: x=%s xvs=%a@ %!" - (var_str x) pr_vars xvs; + "xbvs: ? x=%s pos=%b xvs=%a@ %!" + (var_str x) (q.positive_b x) pr_vars xvs; Format.printf "b=%d@\n%!" (q.find_chi x); *]*) - (*if q.positive_b x then acc - else*) (q.find_chi x, xvs)::acc + (* FIXME: make sure to include postconditions with + original parameters. *) + if q.positive_b x then acc + else (q.find_chi x, xvs)::acc with Not_found -> acc) q.b_vs [] in let answer = diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index e91eda6..4ad258a 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 -> () @@ -815,7 +815,6 @@ let rec plus = "binary plus asserted" >:: (fun () -> - todo "FIXE"; skip_if !debug "debug"; test_case "binary plus" "datatype Binary : num diff --git a/src/Joint.ml b/src/Joint.ml index 474cee8..bcf2019 100644 --- a/src/Joint.ml +++ b/src/Joint.ml @@ -44,7 +44,7 @@ module JointAbduction (P : ABD_PARAMS) = struct P.abd_fail_flag := false; let culprit = ref None and best_done = ref (-1) in - let rec loop fails discard acc (validation : P.validation) + let rec loop fails discard acc validation done_brs aside_brs = function | [] -> let best = @@ -82,7 +82,7 @@ module JointAbduction (P : ABD_PARAMS) = struct loop (fails+1) discard acc validation done_brs (br::aside_brs) more_brs - and check_aside fails best discard acc (validation : P.validation) + and check_aside fails best discard acc validation done_brs = function | [] -> acc | br::aside_brs as all_aside -> diff --git a/src/NumS.ml b/src/NumS.ml index c945d36..607226e 100644 --- a/src/NumS.ml +++ b/src/NumS.ml @@ -63,6 +63,7 @@ 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 abd_fail_flag = ref false let abd_timeout_flag = ref false @@ -1979,31 +1980,29 @@ let subst_chi chi_sb pos_chi = optis @ acc_optis, suboptis @ acc_suboptis) ([], [], [], []) pos_chi -(* Alternative approach, did not work well enough *) -let subst_chi ~cmp_v ~bvs ~xbvs pos_chi a = +let subst_chi_incr ~cmp_v ~bvs ~xbvs pos_chi a = let leq x y = (* let c = cmp_v x y in if c = Same_quant then VarSet.mem x bvs else c <> Right_of *) cmp_v x y >= 0 in let v = maximum ~leq (VarSet.elements (fvs_w_atom a)) in (*[* Format.printf - "subst_chi: pos_chi=%a@ xbvs=@ %a@\n%!" pr_ints - (ints_of_list (List.map fst pos_chi)) + "subst_chi: v=%s pos_chi=%a@ xbvs=@ %a@\n%!" (var_str v) + pr_ints (ints_of_list (List.map fst pos_chi)) (pr_sep_list "| " (fun ppf (i, vs) -> Format.fprintf ppf "%d->%a" i pr_vars vs)) xbvs; *]*) List.fold_left (fun acc (i, renaming) -> - let xvs = try List.assoc i xbvs with Not_found -> assert false in - if VarSet.mem v xvs + if List.exists (fun (j, xvs) -> i=j && VarSet.mem v xvs) xbvs then rename_w_atom renaming a::acc else acc) [] pos_chi -let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = +let validate_incr ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = let added_vs = fvs_w_atom a in (*[* Format.printf - "NumS.abd-validate:@ a=%a@\n%!" pr_w_atom a; *]*) + "NumS.abd-validate-incr:@ a=%a@\n%!" pr_w_atom a; *]*) (* TODO: introduce use-site substitutions *) try let validation = @@ -2015,9 +2014,9 @@ let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = (dc_eqs, dc_ineqs, dc_optis, dc_suboptis)) as br) -> let prem_state = (*[* Format.printf - "NumS.abd-validate: brs_r=%d; brs_n=%d\ - @\nd_eqs=%a@\nd_ineqs=%a\ - @\nd_optis=%a@\nd_suboptis=%a@\n%!" !brs_r brs_n + "NumS.abd-validate-incr: brs_r=%d; brs_n=%d\ + @\nv-d_eqs=%a@\nv-d_ineqs=%a\ + @\nv-d_optis=%a@\nv-d_suboptis=%a@\n%!" !brs_r brs_n pr_w_subst d_eqs pr_ineqs d_ineqs pr_optis d_optis pr_suboptis d_suboptis; *]*) try @@ -2028,17 +2027,28 @@ let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = with Terms.Contradiction _ as e -> Left e in match prem_state with | Right (d_eqs, d_ineqs, d_optis, d_suboptis) -> - let u = subst_chi ~cmp_v ~bvs ~xbvs chi_pos a in (*[* Format.printf - "NumS.abd-validate: u=%a@\n%!" pr_w_formula u; *]*) + "v-d_eqs'=%a@\nv-d_ineqs'=%a@\n\ + v-d_optis'=%a@\nv-d_suboptis'=%a@\n%!" + pr_w_subst d_eqs pr_ineqs d_ineqs pr_optis d_optis + pr_suboptis d_suboptis; *]*) + let u = subst_chi_incr ~cmp_v ~bvs ~xbvs chi_pos a in + (*[* Format.printf + "v-dc_eqs=%a@\nv-dc_ineqs=%a@\n\ + v-dc_optis=%a@\nv-dc_suboptis=%a@\n%!" + pr_w_subst dc_eqs pr_ineqs dc_ineqs pr_optis dc_optis + pr_suboptis dc_suboptis; *]*) + (*[* Format.printf + "NumS.abd-validate-incr: trying u=%a@\n%!" + pr_w_formula u; *]*) let dc_eqs, dc_ineqs, dc_optis, dc_suboptis = solve ~eqs:dc_eqs ~ineqs:dc_ineqs ~optis:dc_optis ~suboptis:dc_suboptis ~cnj':(a::u) ~cmp_v ~cmp_w uni_v in (*[* Format.printf - "dc_eqs'=%a@\ndc_ineqs'=%a@\n\ - dc_optis'=%a@\ndc_suboptis'=%a@\n%!" + "v-dc_eqs'=%a@\nv-dc_ineqs'=%a@\n\ + v-dc_optis'=%a@\nv-dc_suboptis'=%a@\n%!" pr_w_subst dc_eqs pr_ineqs dc_ineqs pr_optis dc_optis pr_suboptis dc_suboptis; *]*) (VarSet.union added_vs br_vs, @@ -2046,13 +2056,16 @@ let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = chi_pos, (d_eqs, d_ineqs, d_optis, d_suboptis), (dc_eqs, dc_ineqs, dc_optis, dc_suboptis))) | Left e -> + (*[* Format.printf + "NumS.abd-validate-incr: dead premise, brs_r=%d nodead=%b@\n%!" + !brs_r !nodeadcode; *]*) if !nodeadcode then ( decr brs_r; if !brs_r <= 0 then (deadcode_flag := true; raise e) else br) else br) validation in - (*[* Format.printf "NumS.abd-validate: passed@\n%!"; *]*) + (*[* Format.printf "NumS.abd-validate-incr: passed@\n%!"; *]*) List.iter (fun (_, ((brs_r, brs_n), _, _, _)) -> brs_r := brs_n) validation; validation @@ -2065,7 +2078,7 @@ let validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a = (* TODO: guess equalities between parameters. *) let abd_simple ~qcmp_v ~cmp_w ~orig_ren ~b_of_v ~upward_of cmp_v uni_v - ~bvs ~xbvs ~nonparam_vars ~discard ~validation ~validate:_ + ~bvs ~xbvs ~nonparam_vars ~discard ~validation ~validate ~neg_validate:_ skip (eqs_i, ineqs_i, optis_i, suboptis_i) (opti_lhs, (d_eqn, d_ineqn), (c_eqn, c_ineqn, c_optis, c_suboptis)) = @@ -2169,7 +2182,7 @@ let abd_simple ~qcmp_v ~cmp_w "NumS.abd_simple: reverted c_eqn0=@ %a@\n%!" pr_eqn c_eqn0; *]*) (* 4 *) - let rec loop valiation eq_trs + let rec loop validation eq_trs eqs_acc0 ineqs_acc0 optis_acc suboptis_acc c0eqn c0ineqn c0optis c0suboptis = (*[* let ddepth = incr debug_dep; !debug_dep in *]*) @@ -2207,6 +2220,10 @@ let abd_simple ~qcmp_v ~cmp_w "NumS.abd_simple: [%d] 5.@ a=%a @\nd_eqn=@ %a@\nineqn=@ %a@\n%!" ddepth pr_w_atom a pr_eqn d_eqn pr_ineqn (c0ineqn @ d_ineqn); *]*) + (*[* Format.printf + "NumS.abd_simple: loop-validation-prems:@\n%a@\n%!" + (pr_line_list "| " + (fun ppf (_, (_, _, s, _)) -> pr_state ppf s)) validation; *]*) let b_eqs, b_ineqs, b_optis, b_suboptis = solve ~eqs:eqs_acc0 ~ineqs:ineqs_acc0 ~eqn:(c0eqn @ d_eqn) ~ineqn:(c0ineqn @ d_ineqn) @@ -2236,7 +2253,7 @@ let abd_simple ~qcmp_v ~cmp_w "NumS.abd_simple: [%d] loop at:@\neqs=@ %a@\nineqs=@ %a@\n%!" ddepth pr_w_subst eqs_acc0 pr_ineqs ineqs_acc0; *]*) - loop valiation eq_trs eqs_acc0 + loop validation eq_trs eqs_acc0 ineqs_acc0 optis_acc suboptis_acc c0eqn c0ineqn c0optis c0suboptis) else @@ -2251,68 +2268,75 @@ let abd_simple ~qcmp_v ~cmp_w let try_trans validation (((eqs_acc, ineqs_acc, optis_acc, suboptis_acc), new_eqn, new_ineqn, _, _), optin, suboptin) = - if !aggressive_discard && - List.exists - (fun (r_eqn, r_ineqn, r_optin, r_suboptin) -> - List.exists (fun eqn -> - let a'vs = fvs_w eqn in - VarSet.cardinal a'vs > 1 && - VarSet.is_empty (VarSet.diff a'vs bvs) && - List.exists (equal_w ~cmp_v eqn) r_eqn) - new_eqn || - List.exists (fun ineqn -> - let a'vs = fvs_w ineqn in - VarSet.cardinal a'vs > 1 && - VarSet.is_empty (VarSet.diff a'vs bvs) && - List.exists (equal_w ~cmp_v ineqn) r_ineqn) - new_ineqn || - List.exists (fun optin -> - let a'vs = fvs_2w optin in - VarSet.cardinal a'vs > 1 && - VarSet.is_empty (VarSet.diff a'vs bvs) && - List.exists (equal_2w ~cmp_v optin) r_optin) - optin || - List.exists (fun suboptin -> - let a'vs = fvs_2w suboptin in - VarSet.cardinal a'vs > 1 && - VarSet.is_empty (VarSet.diff a'vs bvs) && - List.exists (equal_2w ~cmp_v suboptin) r_suboptin) - suboptin) - discard - then raise Omit_trans; - (*[* Format.printf - "NumS.abd_simple: [%d] 7a. validating a'=@ %a@ ...@\n%!" - ddepth pr_formula - (ans_to_num_formula - (eqs_acc, ineqs_acc, optis_acc, suboptis_acc)); - *]*) - let all_new_vs = - VarSet.union (vars_of_map fvs_w new_eqn) - ((* VarSet.union *) (vars_of_map fvs_w new_ineqn) - (* (VarSet.union (vars_of_map fvs_2w optin) *) - (* (vars_of_map fvs_2w suboptin)) *)) in - let new_vs = VarSet.inter bvs all_new_vs in - (*[* Format.printf - "NumS.abd_simple: [%d] approaching 7. new_vs=@ %a\ - @ crosses=%b@\n%!" - ddepth pr_vars new_vs (crosses_xparams ~cmp_v:qcmp_v ~bvs new_vs); - *]*) - (* 7b *) - if crosses_xparams ~cmp_v:qcmp_v ~bvs new_vs then raise Omit_trans; - passes := true; - (*[* Format.printf - "NumS.abd_simple: [%d] 7a. validated@\n%!" ddepth; *]*) - (* 7d *) - (*[* Format.printf - "NumS.abd_simple: [%d] 7 OK@\n%!" ddepth; *]*) - (*[* Format.printf - "NumS.abd_simple: [%d] loop at:\ - @\neqs=@ %a@\nineqs=@ %a@\n%!" - ddepth pr_w_subst eqs_acc pr_ineqs ineqs_acc; - *]*) - (* (try *) - loop valiation eq_trs eqs_acc ineqs_acc optis_acc suboptis_acc - c0eqn c0ineqn c0optis c0suboptis in + (*[* Format.printf + "NumS.abd_simple: trans-validation-prems:@\n%a@\n%!" + (pr_line_list "| " + (fun ppf (_, (_, _, s, _)) -> pr_state ppf s)) validation; *]*) + if !aggressive_discard && + List.exists + (fun (r_eqn, r_ineqn, r_optin, r_suboptin) -> + List.exists (fun eqn -> + let a'vs = fvs_w eqn in + VarSet.cardinal a'vs > 1 && + VarSet.is_empty (VarSet.diff a'vs bvs) && + List.exists (equal_w ~cmp_v eqn) r_eqn) + new_eqn || + List.exists (fun ineqn -> + let a'vs = fvs_w ineqn in + VarSet.cardinal a'vs > 1 && + VarSet.is_empty (VarSet.diff a'vs bvs) && + List.exists (equal_w ~cmp_v ineqn) r_ineqn) + new_ineqn || + List.exists (fun optin -> + let a'vs = fvs_2w optin in + VarSet.cardinal a'vs > 1 && + VarSet.is_empty (VarSet.diff a'vs bvs) && + List.exists (equal_2w ~cmp_v optin) r_optin) + optin || + List.exists (fun suboptin -> + let a'vs = fvs_2w suboptin in + VarSet.cardinal a'vs > 1 && + VarSet.is_empty (VarSet.diff a'vs bvs) && + List.exists (equal_2w ~cmp_v suboptin) r_suboptin) + suboptin) + discard + then raise Omit_trans; + (*[* Format.printf + "NumS.abd_simple: [%d] 7a. validating=%b a'=@ %a@ ...@\n%!" + ddepth (not !verif_incremental) pr_formula + (ans_to_num_formula + (eqs_acc, ineqs_acc, optis_acc, suboptis_acc)); + *]*) + let all_new_vs = + VarSet.union (vars_of_map fvs_w new_eqn) + ((* VarSet.union *) (vars_of_map fvs_w new_ineqn) + (* (VarSet.union (vars_of_map fvs_2w optin) *) + (* (vars_of_map fvs_2w suboptin)) *)) in + let new_vs = VarSet.inter bvs all_new_vs in + (*[* Format.printf + "NumS.abd_simple: [%d] approaching 7. new_vs=@ %a\ + @ crosses=%b@\n%!" + ddepth pr_vars new_vs (crosses_xparams ~cmp_v:qcmp_v ~bvs new_vs); + *]*) + (* 7b *) + if crosses_xparams ~cmp_v:qcmp_v ~bvs new_vs then raise Omit_trans; + if not !verif_incremental then + ignore (validate all_new_vs + (eqs_acc, ineqs_acc, optis_acc, suboptis_acc)); + passes := true; + (*[* Format.printf + "NumS.abd_simple: [%d] 7a. validated@\n%!" ddepth; *]*) + (* 7d *) + (*[* Format.printf + "NumS.abd_simple: [%d] 7 OK@\n%!" ddepth; *]*) + (*[* Format.printf + "NumS.abd_simple: [%d] loop at:\ + @\neqs=@ %a@\nineqs=@ %a@\n%!" + ddepth pr_w_subst eqs_acc pr_ineqs ineqs_acc; + *]*) + (* (try *) + loop validation eq_trs eqs_acc ineqs_acc optis_acc suboptis_acc + c0eqn c0ineqn c0optis c0suboptis in let try_trans_a a' = try (* 7a *) @@ -2323,7 +2347,10 @@ let abd_simple ~qcmp_v ~cmp_w if not (no_scope_viol_atom ~cmp_v:qcmp_v ~upward_of ~bvs a') then raise Omit_trans; let validation = - validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a' in + if !verif_incremental + then validate_incr + ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation a' + else validation in let eqn, ineqn, optin, suboptin = split_w_atom a' in (* [new_eqn, new_ineqn] are only used to determine the variables contributed to the answer. *) @@ -2357,7 +2384,10 @@ let abd_simple ~qcmp_v ~cmp_w if not (no_scope_viol ~cmp_v:qcmp_v ~upward_of ~bvs w') then raise Omit_trans; let validation = - validate ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation (Leq_w w') in + if !verif_incremental + then validate_incr + ~cmp_v ~cmp_w uni_v ~bvs ~xbvs validation (Leq_w w') + else validation in try_trans validation (acc', [], []) (* with Contradiction _ -> ()) *) with @@ -2412,6 +2442,10 @@ let abd_simple ~qcmp_v ~cmp_w (Num_sort, no_pass_msg, None, dummy_loc))) in (* 2 *) + (*[* Format.printf + "NumS.abd_simple: init-validation-prems:@\n%a@\n%!" + (pr_line_list "| " + (fun ppf (_, (_, _, s, _)) -> pr_state ppf s)) validation; *]*) try for rot = 1 to !abd_rotations do let big_k = Array.init (rot - 1) (fun k -> !/(k+2)) in @@ -2439,8 +2473,12 @@ let abd_simple ~qcmp_v ~cmp_w done; None with Result (ans_eqs, ans_ineqs, ans_optis, ans_suboptis, validation) -> (*[* Format.printf "NumS.abd_simple: result:\ - @\neqs=@ %a@\nineqs=@ %a@\n%!" + @\neqs=@ %a@\nineqs=@ %a@\n%!" pr_w_subst ans_eqs pr_ineqs ans_ineqs; *]*) + (*[* Format.printf + "NumS.abd_simple: result-validation-prems:@\n%a@\n%!" + (pr_line_list "| " + (fun ppf (_, (_, _, s, _)) -> pr_state ppf s)) validation; *]*) Some ((ans_eqs, ans_ineqs, ans_optis, ans_suboptis), validation) with (* failed premise/\conclusion *) | Terms.Contradiction _ -> None @@ -2685,7 +2723,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) brs in let brs, validate_brs = List.split brs in (*[* Format.printf "NumS.abd: brs processing past merging@\n%!"; *]*) - (* let validate added_vs (eqs, ineqs, optis, suboptis) = + let validate added_vs (eqs, ineqs, optis, suboptis) = let chi_sb = local_split ~cmp_v:q.cmp_v ~bvs ~xbvs (unsubst eqs) (unsolve ineqs) optis suboptis in (*[* Format.printf @@ -2740,9 +2778,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) List.iter (fun (_, brs_r, brs_n, _) -> brs_r := brs_n) validate_brs with e -> List.iter (fun (_, brs_r, brs_n, _) -> brs_r := brs_n) validate_brs; - raise e in*) - let validate _ _ = () in - (* Alternative approach not working well: *) + raise e in let validation = map_some (fun (br_vs, brs_r, brs_n, @@ -2760,6 +2796,10 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) Some (br_vs, ((brs_r, brs_n), chi_pos, prem, prem_n_concl)) with Terms.Contradiction _ -> None) validate_brs in + (*[* Format.printf + "validation:@ %a@\n%!" + (pr_line_list "| " + (fun ppf (_, (_, _, _, s)) -> pr_state ppf s)) validation; *]*) (* We currently do not make use of negative constraints. *) let neg_validate _ = 0 in let brs, unproc_brs = diff --git a/src/Terms.ml b/src/Terms.ml index 98f6dea..1923fee 100644 --- a/src/Terms.ml +++ b/src/Terms.ml @@ -1690,7 +1690,7 @@ let nice_ans ?sb ?(fvs=VarSet.empty) (vs, phi) = let fvs, sb = match sb with | None -> fvs, VarMap.empty - | Some sb -> VarSet.union (varmap_domain sb) fvs, sb in + | Some sb -> add_vars (varmap_codom sb) fvs, sb in let vs = List.filter (fun v -> VarSet.mem v fvs || VarMap.mem v sb) vs in let allvs, rn = fold_map