From 14c1d5e9f96b8dcaec44f7e1163e3bd0674a7ec4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 11 May 2022 15:15:25 +0200
Subject: [PATCH] [wp] The session can now track scripts usage
---
src/plugins/wp/ProofSession.ml | 59 +++++-
src/plugins/wp/ProofSession.mli | 7 +
src/plugins/wp/register.ml | 191 +++++++++++++-----
.../oracle_qualif/user_init.1.res.oracle | 133 ++++++------
4 files changed, 273 insertions(+), 117 deletions(-)
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index d102a9a49bb..0df94afce70 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -32,8 +32,11 @@ let files : (string,script) Hashtbl.t = Hashtbl.create 32
let jsonfile (dir:Datatype.Filepath.t) =
Format.sprintf "%s/%s.json" (dir :> string)
+let get_script_dir ~force =
+ Wp_parameters.get_session_dir ~force "script"
+
let filename ~force wpo =
- let dscript = Wp_parameters.get_session_dir ~force "script" in
+ let dscript = get_script_dir ~force in
jsonfile dscript wpo.po_sid (* no model in name *)
let legacies wpo =
@@ -121,3 +124,57 @@ let save ~stdout wpo js =
Json.save_file f js ;
Hashtbl.replace files f (Script f) ;
end
+
+let get_marks_dir ~force =
+ let scripts = Wp_parameters.get_session_dir ~force "script" in
+ let path = Datatype.Filepath.concat scripts ".marks" in
+ if force then Wp_parameters.make_output_dir (path :> string) ;
+ path
+
+let remove_marks ~dry =
+ let marks = get_marks_dir ~force:false in
+ let as_str = (marks :> string) in
+ if Sys.file_exists as_str && Sys.is_directory as_str then
+ if dry
+ then Wp_parameters.feedback "[dry] remove marks"
+ else Extlib.safe_remove_dir as_str
+
+let reset_marks () =
+ remove_marks ~dry:false ;
+ ignore @@ get_marks_dir ~force:true
+
+let mark goal =
+ let marks = get_marks_dir ~force:false in
+ let as_str = (marks :> string) in
+ if Sys.file_exists as_str && Sys.is_directory as_str then
+ let mark = Datatype.Filepath.concat marks (goal.po_sid ^ ".json") in
+ if Sys.file_exists (mark :> string) then ()
+ else close_out @@ open_out (mark :> string)
+
+module StringSet = Datatype.String.Set
+
+let remove_unmarked_files ~dry =
+ let dir = (get_script_dir ~force:false :> string) in
+ if Sys.file_exists dir && Sys.is_directory dir then
+ let marks = (get_marks_dir ~force:false :> string) in
+ if Sys.file_exists marks && Sys.is_directory marks then
+ begin
+ let files =
+ Array.fold_left
+ (fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir dir)
+ in
+ let marks =
+ Array.fold_left
+ (fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir marks)
+ in
+ let orphans = StringSet.diff files marks in
+ let orphans = StringSet.remove ".marks" orphans in
+ let remove file =
+ let path = dir ^ "/" ^ file in
+ if dry
+ then Wp_parameters.feedback "[dry] rm %s" path
+ else Sys.remove path
+ in
+ StringSet.iter remove orphans ;
+ remove_marks ~dry
+ end
diff --git a/src/plugins/wp/ProofSession.mli b/src/plugins/wp/ProofSession.mli
index 9d0f127fca1..1957f78eb49 100644
--- a/src/plugins/wp/ProofSession.mli
+++ b/src/plugins/wp/ProofSession.mli
@@ -25,6 +25,7 @@ type script =
| Script of string
| Deprecated of string
+val pp_file : Format.formatter -> string -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit
val get : Wpo.t -> script
@@ -33,4 +34,10 @@ val save : stdout:bool -> Wpo.t -> Json.t -> unit
val load : Wpo.t -> Json.t
val remove : Wpo.t -> unit
+val filename : force:bool -> Wpo.t -> string
+
+val mark : Wpo.t -> unit
+val reset_marks : unit -> unit
+val remove_unmarked_files : dry:bool -> unit
+
(**************************************************************************)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 69f8a7c0d65..cb51b2fed00 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -22,6 +22,12 @@
let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised"
+let dkey_script_removed =
+ Wp_parameters.register_category "script:show-removed"
+let dkey_script_updated =
+ Wp_parameters.register_category "script:show-updated"
+let dkey_script_incomplete =
+ Wp_parameters.register_category "script:show-incomplete"
(* ------------------------------------------------------------------------ *)
(* --- Memory Model Hypotheses --- *)
@@ -585,60 +591,128 @@ let compute_auto ~script =
if script.auto <> [] then script.tactical <- true ;
end
-let do_update_session ~script goals =
- if script.update then
- begin
- let removed = ref 0 in
- let updated = ref 0 in
- let invalid = ref 0 in
- Bag.iter
- begin fun goal ->
- let results = Wpo.get_results goal in
- let autoproof (p,r) =
- (p=VCS.Qed) || (VCS.is_auto p && VCS.is_valid r && VCS.autofit r) in
- if List.exists autoproof results then
+type session_scripts = {
+ updated: (Wpo.t * string * Json.t) list;
+ incomplete: (Wpo.t * string * Json.t) list;
+ removed: (Wpo.t * string) list;
+}
+
+let do_collect_session goals =
+ let updated = ref [] in
+ let incomplete = ref [] in
+ let removed = ref [] in
+ let file goal =
+ Format.asprintf "%a"
+ ProofSession.pp_file @@ ProofSession.filename ~force:false goal
+ in
+ Bag.iter
+ begin fun goal ->
+ let results = Wpo.get_results goal in
+ let autoproof (p,r) =
+ (p=VCS.Qed) || (VCS.is_auto p && VCS.is_valid r && VCS.autofit r) in
+ if List.exists autoproof results then
+ begin
+ if ProofSession.exists goal then
begin
- if ProofSession.exists goal then
- (incr removed ; ProofSession.remove goal)
+ let file = file goal in
+ removed := (goal, file) :: !removed
end
- else
- let scripts = ProofEngine.script (ProofEngine.proof ~main:goal) in
- if scripts <> [] then
+ end
+ else
+ let scripts = ProofEngine.script (ProofEngine.proof ~main:goal) in
+ if scripts <> [] then
+ begin
+ let keep = function
+ | ProofScript.Prover(p,r) -> VCS.is_auto p && VCS.is_valid r
+ | ProofScript.Tactic(n,_,_) -> n=0
+ | ProofScript.Error _ -> false in
+ let strategy = List.filter keep scripts in
+ if strategy <> [] then
+ begin
+ let file = file goal in
+ let json = ProofScript.encode strategy in
+ updated := (goal, file, json) :: !updated
+ end
+ else
+ if not (ProofSession.exists goal) then
begin
- let keep = function
- | ProofScript.Prover(p,r) -> VCS.is_auto p && VCS.is_valid r
- | ProofScript.Tactic(n,_,_) -> n=0
- | ProofScript.Error _ -> false in
- let strategy = List.filter keep scripts in
- let stdout = script.on_stdout in
- if strategy <> [] then
- begin
- incr updated ;
- ProofSession.save ~stdout goal (ProofScript.encode strategy)
- end
- else
- if not (ProofSession.exists goal) then
- begin
- incr invalid ;
- ProofSession.save ~stdout goal (ProofScript.encode scripts)
- end
+ let file = file goal in
+ let json = ProofScript.encode scripts in
+ incomplete := (goal, file, json) :: !incomplete
end
- end goals ;
- let r = !removed in
- let u = !updated in
- let f = !invalid in
- ( if r = 0 && u = 0 && f = 0 then
- Wp_parameters.result "No updated script." ) ;
- ( if r > 0 then
- let s = if r > 1 then "s" else "" in
- Wp_parameters.result "Updated session with %d new automated proof%s." r s );
- ( if u > 0 then
- let s = if u > 1 then "s" else "" in
- Wp_parameters.result "Updated session with %d new valid script%s." u s ) ;
- ( if f > 0 then
- let s = if f > 1 then "s" else "" in
- Wp_parameters.result "Updated session with %d new script%s to complete." f s );
+ end
+ end goals ;
+ { updated = !updated ;
+ incomplete = !incomplete ;
+ removed = !removed ; }
+
+let do_update_session script session =
+ let stdout = script.on_stdout in
+ List.iter
+ begin fun (g, _, s) ->
+ (* we always mark existing scripts *)
+ ProofSession.mark g ;
+ if script.update then ProofSession.save ~stdout g s
+ end
+ session.updated ;
+ List.iter
+ begin fun (g, _, s) ->
+ (* we mark new incomplete scripts only if we save such files *)
+ if script.update then
+ (ProofSession.mark g ; ProofSession.save ~stdout g s)
end
+ session.incomplete ;
+ List.iter (fun (g, _) -> ProofSession.remove g) session.removed ;
+ ()
+
+let do_show_session updated_session session =
+ let show enabled kind dkey file =
+ if enabled then
+ Wp_parameters.result ~dkey "[%s] %a" kind ProofSession.pp_file file
+ in
+ (* Note: we display new (in)valid scripts only when updating *)
+ List.iter
+ (fun (_,f,_) -> show updated_session "UPDATED" dkey_script_updated f)
+ session.updated ;
+ List.iter
+ (fun (_,f,_) -> show updated_session "INCOMPLETE" dkey_script_incomplete f)
+ session.incomplete ;
+ let txt_removed = if updated_session then "REMOVED" else "UNUSED" in
+ List.iter
+ (fun (_,f) -> show true txt_removed dkey_script_removed f)
+ session.removed ;
+
+ let r = List.length session.removed in
+ let u = List.length session.updated in
+ let f = List.length session.incomplete in
+
+ (* Note: we display new (in)valid scripts only when updating *)
+ if (updated_session && (f > 0 || u > 0)) || r > 0 then
+ let updated_s =
+ let s = if u > 1 then "s" else "" in
+ if u = 0 || (not updated_session) then ""
+ else Format.asprintf "\n - %d new valid script%s" u s
+ in
+ let invalid_s =
+ let s = if f > 1 then "s" else "" in
+ if f = 0 || (not updated_session) then ""
+ else Format.asprintf "\n - %d new script%s to complete" f s
+ in
+ let removed_s =
+ let s = if r > 1 then "s" else "" in
+ let txt_removed = String.lowercase_ascii txt_removed in
+ if r = 0 then ""
+ else Format.asprintf "\n - %d script%s %s (now automated)" r s txt_removed
+ in
+ Wp_parameters.result
+ "%s%s%s%s"
+ (if updated_session then "Updated session" else "Session can be updated")
+ removed_s updated_s invalid_s
+
+let do_session ~script goals =
+ let session = do_collect_session goals in
+ do_update_session script session ;
+ do_show_session script.update session
let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
let script = default_script_mode () in
@@ -662,7 +736,7 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
if spawned then
begin
do_list_scheduled_result () ;
- do_update_session ~script goals ;
+ do_session ~script goals ;
end
else if not (Wp_parameters.Print.get ()) then
Bag.iter do_wpo_display goals
@@ -816,6 +890,21 @@ let sequence jobs () =
then List.iter (fun f -> f ()) jobs
else try_sequence jobs ()
+let prepare_scripts () =
+ if Wp_parameters.PrepareScripts.get () then begin
+ Wp_parameters.feedback "Prepare" ;
+ ProofSession.reset_marks () ;
+ Wp_parameters.PrepareScripts.clear ()
+ end
+
+let finalize_scripts () =
+ if Wp_parameters.FinalizeScripts.get () then begin
+ Wp_parameters.feedback "Finalize" ;
+ ProofSession.remove_unmarked_files
+ ~dry:(Wp_parameters.DryFinalizeScripts.get()) ;
+ Wp_parameters.FinalizeScripts.clear ()
+ end
+
let tracelog () =
let active_keys = Wp_parameters.get_debug_keys () in
if active_keys <> [] then begin
@@ -828,8 +917,10 @@ let tracelog () =
let main = sequence [
(fun () -> Wp_parameters.debug ~dkey:dkey_main "Start WP plugin...@.") ;
do_prover_detect ;
+ prepare_scripts ;
cmdline_run ;
tracelog ;
+ finalize_scripts ;
Wp_parameters.reset ;
(fun () -> Wp_parameters.debug ~dkey:dkey_main "Stop WP plugin...@.") ;
]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 4221a029a04..cf4d5306048 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -30,54 +30,54 @@
Qed: 11
Script: 12
Alt-Ergo: 0 (unsuccess: 12)
-[wp] Proof script for typed_init_t2_v2_loop_assigns_part2:
+[wp] Proof script for typed_init_t2_bis_v2_assigns_normal_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0098,
- "steps": 35 } ],
+ "verdict": "valid", "time": 0.0088,
+ "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0048,
- "steps": 35 } ] } } ]
-[wp] Proof script for typed_init_t2_v2_loop_assigns_part3:
+ "verdict": "valid", "time": 0.0116,
+ "steps": 24 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_assigns_exit_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0098,
- "steps": 35 } ],
+ "verdict": "valid", "time": 0.0088,
+ "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0048,
- "steps": 35 } ] } } ]
-[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part2:
+ "verdict": "valid", "time": 0.0116,
+ "steps": 24 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (i_2<=i_3) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (i_3<=i_2) /\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0099,
- "steps": 42 } ],
+ "verdict": "valid", "time": 0.0074,
+ "steps": 31 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0124,
- "steps": 42 } ] } } ]
-[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part3:
+ "verdict": "valid", "time": 0.0078,
+ "steps": 31 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_1<=i_2) /\\ (i_2<=j_1) /\\ (i_0<=9)",
- "pattern": "\\E$i0$i$j$j9" },
+ "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0094,
- "steps": 26 } ],
+ "verdict": "valid", "time": 0.0124,
+ "steps": 43 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0101,
- "steps": 26 } ] } } ]
-[wp] Proof script for typed_init_t2_v2_assigns_part2:
+ "verdict": "valid", "time": 0.0121,
+ "steps": 43 } ] } } ]
+[wp] Proof script for typed_init_t2_v3_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_158) /\\ (i_1<=i_159) /\\ (0<=i_0) /\\ (i_158<=i_0) /\\ (i_159<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_149) /\\ (i_1<=i_150) /\\ (0<=i_0) /\\ (i_149<=i_0) /\\ (i_150<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
@@ -85,17 +85,6 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0092,
"steps": 16 } ] } } ]
-[wp] Proof script for typed_init_t2_v3_loop_assigns_part2:
- [ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0139,
- "steps": 45 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0127,
- "steps": 45 } ] } } ]
[wp] Proof script for typed_init_t2_v3_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
@@ -107,10 +96,21 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0081,
"steps": 33 } ] } } ]
-[wp] Proof script for typed_init_t2_v3_assigns_part2:
+[wp] Proof script for typed_init_t2_v3_loop_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_149) /\\ (i_1<=i_150) /\\ (0<=i_0) /\\ (i_149<=i_0) /\\ (i_150<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E$i$i0$i$i9" },
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0139,
+ "steps": 45 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0127,
+ "steps": 45 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_assigns_part2:
+ [ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_158) /\\ (i_1<=i_159) /\\ (0<=i_0) /\\ (i_158<=i_0) /\\ (i_159<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
@@ -118,51 +118,52 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0092,
"steps": 16 } ] } } ]
-[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part2:
+[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E$i$i0$i$i9" },
+ "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_1<=i_2) /\\ (i_2<=j_1) /\\ (i_0<=9)",
+ "pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0124,
- "steps": 43 } ],
+ "verdict": "valid", "time": 0.0094,
+ "steps": 26 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0121,
- "steps": 43 } ] } } ]
-[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part3:
+ "verdict": "valid", "time": 0.0101,
+ "steps": 26 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (i_2<=i_3) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (i_3<=i_2) /\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0074,
- "steps": 31 } ],
+ "verdict": "valid", "time": 0.0099,
+ "steps": 42 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0078,
- "steps": 31 } ] } } ]
-[wp] Proof script for typed_init_t2_bis_v2_assigns_exit_part2:
+ "verdict": "valid", "time": 0.0124,
+ "steps": 42 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0088,
- "steps": 24 } ],
+ "verdict": "valid", "time": 0.0098,
+ "steps": 35 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0116,
- "steps": 24 } ] } } ]
-[wp] Proof script for typed_init_t2_bis_v2_assigns_normal_part2:
+ "verdict": "valid", "time": 0.0048,
+ "steps": 35 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0088,
- "steps": 24 } ],
+ "verdict": "valid", "time": 0.0098,
+ "steps": 35 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0116,
- "steps": 24 } ] } } ]
-[wp] Updated session with 12 new valid scripts.
+ "verdict": "valid", "time": 0.0048,
+ "steps": 35 } ] } } ]
+[wp] Updated session
+ - 12 new valid scripts
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v2 3 - 8 100%
--
GitLab