Skip to content
Snippets Groups Projects
Commit 14c1d5e9 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] The session can now track scripts usage

parent bf85e4cc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/ProofSession.ml
+ 58
− 1
View file @ 14c1d5e9
...@@ -32,8 +32,11 @@ let files : (string,script) Hashtbl.t = Hashtbl.create 32 ...@@ -32,8 +32,11 @@ let files : (string,script) Hashtbl.t = Hashtbl.create 32
let jsonfile (dir:Datatype.Filepath.t) = let jsonfile (dir:Datatype.Filepath.t) =
Format.sprintf "%s/%s.json" (dir :> string) Format.sprintf "%s/%s.json" (dir :> string)
let get_script_dir ~force =
Wp_parameters.get_session_dir ~force "script"
let filename ~force wpo = 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 *) jsonfile dscript wpo.po_sid (* no model in name *)
let legacies wpo = let legacies wpo =
...@@ -121,3 +124,57 @@ let save ~stdout wpo js = ...@@ -121,3 +124,57 @@ let save ~stdout wpo js =
Json.save_file f js ; Json.save_file f js ;
Hashtbl.replace files f (Script f) ; Hashtbl.replace files f (Script f) ;
end 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
src/plugins/wp/ProofSession.mli
+ 7
− 0
View file @ 14c1d5e9
...@@ -25,6 +25,7 @@ type script = ...@@ -25,6 +25,7 @@ type script =
| Script of string | Script of string
| Deprecated of string | Deprecated of string
val pp_file : Format.formatter -> string -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit val pp_script_for : Format.formatter -> Wpo.t -> unit
val get : Wpo.t -> script val get : Wpo.t -> script
...@@ -33,4 +34,10 @@ val save : stdout:bool -> Wpo.t -> Json.t -> unit ...@@ -33,4 +34,10 @@ val save : stdout:bool -> Wpo.t -> Json.t -> unit
val load : Wpo.t -> Json.t val load : Wpo.t -> Json.t
val remove : Wpo.t -> unit 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
(**************************************************************************) (**************************************************************************)
src/plugins/wp/register.ml
+ 141
− 50
View file @ 14c1d5e9
...@@ -22,6 +22,12 @@ ...@@ -22,6 +22,12 @@
let dkey_main = Wp_parameters.register_category "main" let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised" 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 --- *) (* --- Memory Model Hypotheses --- *)
...@@ -585,60 +591,128 @@ let compute_auto ~script = ...@@ -585,60 +591,128 @@ let compute_auto ~script =
if script.auto <> [] then script.tactical <- true ; if script.auto <> [] then script.tactical <- true ;
end end
let do_update_session ~script goals = type session_scripts = {
if script.update then updated: (Wpo.t * string * Json.t) list;
begin incomplete: (Wpo.t * string * Json.t) list;
let removed = ref 0 in removed: (Wpo.t * string) list;
let updated = ref 0 in }
let invalid = ref 0 in
Bag.iter let do_collect_session goals =
begin fun goal -> let updated = ref [] in
let results = Wpo.get_results goal in let incomplete = ref [] in
let autoproof (p,r) = let removed = ref [] in
(p=VCS.Qed) || (VCS.is_auto p && VCS.is_valid r && VCS.autofit r) in let file goal =
if List.exists autoproof results then 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 begin
if ProofSession.exists goal then let file = file goal in
(incr removed ; ProofSession.remove goal) removed := (goal, file) :: !removed
end end
else end
let scripts = ProofEngine.script (ProofEngine.proof ~main:goal) in else
if scripts <> [] then 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 begin
let keep = function let file = file goal in
| ProofScript.Prover(p,r) -> VCS.is_auto p && VCS.is_valid r let json = ProofScript.encode scripts in
| ProofScript.Tactic(n,_,_) -> n=0 incomplete := (goal, file, json) :: !incomplete
| 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
end end
end goals ; end
let r = !removed in end goals ;
let u = !updated in { updated = !updated ;
let f = !invalid in incomplete = !incomplete ;
( if r = 0 && u = 0 && f = 0 then removed = !removed ; }
Wp_parameters.result "No updated script." ) ;
( if r > 0 then let do_update_session script session =
let s = if r > 1 then "s" else "" in let stdout = script.on_stdout in
Wp_parameters.result "Updated session with %d new automated proof%s." r s ); List.iter
( if u > 0 then begin fun (g, _, s) ->
let s = if u > 1 then "s" else "" in (* we always mark existing scripts *)
Wp_parameters.result "Updated session with %d new valid script%s." u s ) ; ProofSession.mark g ;
( if f > 0 then if script.update then ProofSession.save ~stdout g s
let s = if f > 1 then "s" else "" in end
Wp_parameters.result "Updated session with %d new script%s to complete." f s ); 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 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 do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
let script = default_script_mode () in let script = default_script_mode () in
...@@ -662,7 +736,7 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) = ...@@ -662,7 +736,7 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
if spawned then if spawned then
begin begin
do_list_scheduled_result () ; do_list_scheduled_result () ;
do_update_session ~script goals ; do_session ~script goals ;
end end
else if not (Wp_parameters.Print.get ()) then else if not (Wp_parameters.Print.get ()) then
Bag.iter do_wpo_display goals Bag.iter do_wpo_display goals
...@@ -816,6 +890,21 @@ let sequence jobs () = ...@@ -816,6 +890,21 @@ let sequence jobs () =
then List.iter (fun f -> f ()) jobs then List.iter (fun f -> f ()) jobs
else try_sequence 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 tracelog () =
let active_keys = Wp_parameters.get_debug_keys () in let active_keys = Wp_parameters.get_debug_keys () in
if active_keys <> [] then begin if active_keys <> [] then begin
...@@ -828,8 +917,10 @@ let tracelog () = ...@@ -828,8 +917,10 @@ let tracelog () =
let main = sequence [ let main = sequence [
(fun () -> Wp_parameters.debug ~dkey:dkey_main "Start WP plugin...@.") ; (fun () -> Wp_parameters.debug ~dkey:dkey_main "Start WP plugin...@.") ;
do_prover_detect ; do_prover_detect ;
prepare_scripts ;
cmdline_run ; cmdline_run ;
tracelog ; tracelog ;
finalize_scripts ;
Wp_parameters.reset ; Wp_parameters.reset ;
(fun () -> Wp_parameters.debug ~dkey:dkey_main "Stop WP plugin...@.") ; (fun () -> Wp_parameters.debug ~dkey:dkey_main "Stop WP plugin...@.") ;
] ]
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+ 67
− 66
View file @ 14c1d5e9
...@@ -30,54 +30,54 @@ ...@@ -30,54 +30,54 @@
Qed: 11 Qed: 11
Script: 12 Script: 12
Alt-Ergo: 0 (unsuccess: 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": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0098, "verdict": "valid", "time": 0.0088,
"steps": 35 } ], "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0048, "verdict": "valid", "time": 0.0116,
"steps": 35 } ] } } ] "steps": 24 } ] } } ]
[wp] Proof script for typed_init_t2_v2_loop_assigns_part3: [wp] Proof script for typed_init_t2_bis_v2_assigns_exit_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0098, "verdict": "valid", "time": 0.0088,
"steps": 35 } ], "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0048, "verdict": "valid", "time": 0.0116,
"steps": 35 } ] } } ] "steps": 24 } ] } } ]
[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part2: [wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0099, "verdict": "valid", "time": 0.0074,
"steps": 42 } ], "steps": 31 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0124, "verdict": "valid", "time": 0.0078,
"steps": 42 } ] } } ] "steps": 31 } ] } } ]
[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part3: [wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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)", "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$i0$i$j$j9" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0094, "verdict": "valid", "time": 0.0124,
"steps": 26 } ], "steps": 43 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0101, "verdict": "valid", "time": 0.0121,
"steps": 26 } ] } } ] "steps": 43 } ] } } ]
[wp] Proof script for typed_init_t2_v2_assigns_part2: [wp] Proof script for typed_init_t2_v3_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011, "verdict": "valid", "time": 0.011,
...@@ -85,17 +85,6 @@ ...@@ -85,17 +85,6 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0092, "verdict": "valid", "time": 0.0092,
"steps": 16 } ] } } ] "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: [wp] Proof script for typed_init_t2_v3_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
...@@ -107,10 +96,21 @@ ...@@ -107,10 +96,21 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0081, "verdict": "valid", "time": 0.0081,
"steps": 33 } ] } } ] "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": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011, "verdict": "valid", "time": 0.011,
...@@ -118,51 +118,52 @@ ...@@ -118,51 +118,52 @@
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0092, "verdict": "valid", "time": 0.0092,
"steps": 16 } ] } } ] "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": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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)", "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$i$i0$i$i9" }, "pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0124, "verdict": "valid", "time": 0.0094,
"steps": 43 } ], "steps": 26 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0121, "verdict": "valid", "time": 0.0101,
"steps": 43 } ] } } ] "steps": 26 } ] } } ]
[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part3: [wp] Proof script for typed_init_t2_v2_loop_assigns_2_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0074, "verdict": "valid", "time": 0.0099,
"steps": 31 } ], "steps": 42 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0078, "verdict": "valid", "time": 0.0124,
"steps": 31 } ] } } ] "steps": 42 } ] } } ]
[wp] Proof script for typed_init_t2_bis_v2_assigns_exit_part2: [wp] Proof script for typed_init_t2_v2_loop_assigns_part3:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0088, "verdict": "valid", "time": 0.0098,
"steps": 24 } ], "steps": 35 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0116, "verdict": "valid", "time": 0.0048,
"steps": 24 } ] } } ] "steps": 35 } ] } } ]
[wp] Proof script for typed_init_t2_bis_v2_assigns_normal_part2: [wp] Proof script for typed_init_t2_v2_loop_assigns_part2:
[ { "header": "Split", "tactic": "Wp.split", "params": {}, [ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal", "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" }, "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0", "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0088, "verdict": "valid", "time": 0.0098,
"steps": 24 } ], "steps": 35 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0", "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0116, "verdict": "valid", "time": 0.0048,
"steps": 24 } ] } } ] "steps": 35 } ] } } ]
[wp] Updated session with 12 new valid scripts. [wp] Updated session
- 12 new valid scripts
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
init_t2_v2 3 - 8 100% init_t2_v2 3 - 8 100%
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment