Commit 029acee9 authored by MARCHE Claude's avatar MARCHE Claude

bisect continued

parent 18e1c2ce
......@@ -755,6 +755,13 @@ let schedule_tr_with_same_arguments
let callback = callback name args in
schedule_transformation c pn name args ~callback ~notification
let proof_is_complete pa =
match pa.Session_itp.proof_state with
| None -> false
| Some pr ->
not pa.Session_itp.proof_obsolete &&
Call_provers.(pr.pr_answer <> Valid)
let clean_session c ~removed =
(* clean should not change proved status *)
let notification _ = assert false in
......@@ -766,13 +773,8 @@ let clean_session c ~removed =
| APa pa ->
let pa = Session_itp.get_proof_attempt_node s pa in
if pn_proved s pa.parent then
(match pa.Session_itp.proof_state with
| None -> ()
| Some pr ->
if pa.Session_itp.proof_obsolete ||
Call_provers.(pr.pr_answer <> Valid)
then
Session_itp.remove_subtree ~notification ~removed s any)
if not (proof_is_complete pa) then
Session_itp.remove_subtree ~notification ~removed s any
| ATn tn ->
let pn = get_trans_parent s tn in
if pn_proved s pn && not (tn_proved s tn) then
......@@ -962,9 +964,21 @@ let replay ?(obsolete_only=true) ?(use_steps=false)
let debug = Debug.register_flag ~desc:"Task bisection" "bisect"
let create_rem_list rem =
let remove_ts acc ts = ts.Ty.ts_name.Ident.id_string :: acc in
let remove_ls acc ls = ls.Term.ls_name.Ident.id_string :: acc in
let remove_pr acc pr = pr.Decl.pr_name.Ident.id_string ::acc in
let acc = Ty.Sts.fold_left remove_ts [] rem.Eliminate_definition.rem_ts in
let acc = Term.Sls.fold_left remove_ls acc rem.Eliminate_definition.rem_ls in
let acc = Decl.Spr.fold_left remove_pr acc rem.Eliminate_definition.rem_pr in
acc
let bisect_proof_attempt ~notification c pa_id =
let ses = c.controller_session in
let pa = get_proof_attempt_node ses pa_id in
if not (proof_is_complete pa) then
invalid_arg "bisect: proof attempt should be valid";
let goal_id = pa.parent in
let prover = pa.prover in
let limit = { pa.limit with
......@@ -974,90 +988,99 @@ let bisect_proof_attempt ~notification c pa_id =
let timelimit = ref (-1) in
let set_timelimit res =
timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
let rec callback kont _pa_id = function
| Running | Scheduled -> ()
| Interrupted ->
Debug.dprintf debug "Bisecting interrupted.@."
| Detached | Uninstalled _ -> assert false
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
let b = res.Call_provers.pr_answer = Call_provers.Valid in
Debug.dprintf debug "Bisecting: %a.@."
Call_provers.print_prover_result res;
if b then set_timelimit res;
match kont b with
| Eliminate_definition.BSdone rem ->
if Decl.Spr.is_empty rem.Eliminate_definition.rem_pr &&
Term.Sls.is_empty rem.Eliminate_definition.rem_ls &&
Ty.Sts.is_empty rem.Eliminate_definition.rem_ts
then
Debug.dprintf debug "Bisecting doesn't reduced the task.@."
else
begin
Debug.dprintf debug "Bisecting done.@.";
()
(*
begin try
let keygen = MA.keygen in
let notify = MA.notify in
let reml = List.map (fun (m,l) -> m.Theory.meta_name,l) reml in
let metas = S.add_registered_metas ~keygen ses reml pa.S.proof_parent in
let trans = S.add_registered_transformation ~keygen
ses "eliminate_builtin" metas.S.metas_goal in
let goal = List.hd trans.S.transf_goals in (* only one *)
let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
~goal ~env_session:ses pa in
MA.init_any (S.Metas metas);
M.run_external_proof ses sched ~cntexample npa
with e ->
dprintf debug "Bisecting error:@\n%a@."
Exn_printer.exn_printer e end
*)
end
| Eliminate_definition.BSstep (_rem,kont) ->
schedule_proof_attempt
c goal_id prover
~counterexmp:false
~limit:{ limit with Call_provers.limit_time = !timelimit; }
~callback:(callback kont)
~notification
let bisect_end rem =
if Decl.Spr.is_empty rem.Eliminate_definition.rem_pr &&
Term.Sls.is_empty rem.Eliminate_definition.rem_ls &&
Ty.Sts.is_empty rem.Eliminate_definition.rem_ts
then
Debug.dprintf debug "Bisecting didn't reduce the task.@."
else
begin
Debug.dprintf debug "Bisecting done.@.";
(* apply again the transformation *)
let callback = function
| TSscheduled -> ()
| TSfailed _ -> assert false
| TSdone trid ->
match get_sub_tasks ses trid with
| [pn] ->
let limit = { limit with Call_provers.limit_time = !timelimit; } in
let callback _paid = function
| Scheduled | Running -> ()
| Detached | Uninstalled _ -> assert false
| Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
assert (res.Call_provers.pr_answer = Call_provers.Valid);
Debug.dprintf debug "Bisecting: %a.@."
Call_provers.print_prover_result res;
in
schedule_proof_attempt c pn prover ~counterexmp:false ~limit ~callback ~notification
| _ -> assert false
in
let rem = create_rem_list rem in
schedule_transformation c goal_id "remove" rem ~callback ~notification
end
in
(* Run once the complete goal in order to verify its validity and
update the proof attempt *)
let first_callback _pa_id = function
(* this pa_id can be different from the first pa_id *)
| Running | Scheduled -> ()
| Interrupted ->
Debug.dprintf debug "Bisecting interrupted.@."
| Detached | Uninstalled _ -> assert false
| InternalFailure exn ->
Debug.dprintf debug "proof of the initial task interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
if res.Call_provers.pr_answer <> Call_provers.Valid
then Debug.dprintf debug "Initial task can't be proved.@."
else
let t = get_raw_task ses goal_id in
let r = Eliminate_definition.bisect_step t in
match r with
| Eliminate_definition.BSdone _res ->
Debug.dprintf debug "Task can't be reduced.@."
| Eliminate_definition.BSstep (_rem,kont) ->
set_timelimit res;
schedule_proof_attempt
c goal_id prover
~counterexmp:false
~limit:{ limit with Call_provers.limit_time = !timelimit}
~callback:(callback kont)
~notification
let rec bisect_step rem kont =
(* we have to:
1) apply transformation remove with the given rem
2) on the generated sub-goal, run the prover with some callback
3) the callback should :
compute (next_iter success_value)
if result is done, do nothing more
if result is some new rem, remove the previous transformation
and recursively call bisect_step
*)
let callback = function
| TSscheduled -> ()
| TSfailed _ -> (* may happen if removing a type or a lsymbol
that is used later on. We do has if proof fails. *)
begin
match kont false with
| Eliminate_definition.BSstep (rem,kont) ->
bisect_step rem kont
| Eliminate_definition.BSdone rem ->
bisect_end rem
end
| TSdone trid ->
match get_sub_tasks ses trid with
| [pn] ->
let limit = { limit with Call_provers.limit_time = !timelimit; } in
let callback _paid = function
| Scheduled | Running -> ()
| Detached | Uninstalled _ -> assert false
| Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
Exn_printer.exn_printer exn
| Done res ->
let b = res.Call_provers.pr_answer = Call_provers.Valid in
Debug.dprintf debug "Bisecting: %a.@."
Call_provers.print_prover_result res;
if b then set_timelimit res;
match kont b with
| Eliminate_definition.BSstep (rem,kont) ->
remove_transformation ses trid;
bisect_step rem kont
| Eliminate_definition.BSdone rem ->
bisect_end rem
in
schedule_proof_attempt c pn prover ~counterexmp:false ~limit ~callback ~notification
| _ -> assert false
in
let rem = create_rem_list rem in
schedule_transformation c goal_id "remove" rem ~callback ~notification
in
Debug.dprintf debug "Bisecting with %a started.@."
Whyconf.print_prover prover;
schedule_proof_attempt
c goal_id prover ~counterexmp:false ~limit ~callback:first_callback ~notification
Whyconf.print_prover prover;
let t = get_raw_task ses goal_id in
match Eliminate_definition.bisect_step t with
| Eliminate_definition.BSdone _ -> assert false
| Eliminate_definition.BSstep(rem,kont) -> bisect_step rem kont
end
......@@ -220,6 +220,7 @@ let _print_rem fmt rem = Format.fprintf fmt
(Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) rem.rem_ls
(Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) rem.rem_ts
(*
let rec elim_task task rem =
match task with
| Some ({task_decl = {td_node = Decl decl}} as task) ->
......@@ -230,7 +231,7 @@ let rec elim_task task rem =
| Some task ->
Task.add_tdecl (elim_task task.task_prev rem) task.task_decl
| None -> None
*)
let add_rem rem decl =
let remove_ts rem ts =
......@@ -253,20 +254,6 @@ let _union_rem rem1 rem2 =
rem_pr = Spr.union rem1.rem_pr rem2.rem_pr;
}
(*
let create_meta_rem_list rem =
let remove_ts acc ts =
(Printer.meta_remove_type, [Theory.MAts ts])::acc in
let remove_ls acc ls =
(Printer.meta_remove_logic, [Theory.MAls ls])::acc in
let remove_pr acc pr =
(Printer.meta_remove_prop, [Theory.MApr pr])::acc in
let acc = Sts.fold_left remove_ts [] rem.rem_ts in
let acc = Sls.fold_left remove_ls acc rem.rem_ls in
let acc = Spr.fold_left remove_pr acc rem.rem_pr in
acc
*)
let fold_sub f acc a i1 i2 =
let acc = ref acc in
for i=i1 to i2-1 do
......@@ -323,11 +310,13 @@ let bisect_step task0 =
bisect_aux task0 a 0 n empty_rem
(fun rem -> BSdone rem)
(*
let bisect f task =
let rec run = function
| BSdone r -> r
| BSstep (rem,c) -> let t = elim_task task rem in run (c (f t)) in
run (bisect_step task)
*)
(** catch exception for debug *)
(* let bisect_step task0 = *)
......
......@@ -27,10 +27,12 @@ val eliminate_mutual_recursion: Task.task Trans.trans
type rem = { rem_pr : Decl.Spr.t; rem_ls : Term.Sls.t; rem_ts : Ty.Sts.t }
(* unused
val bisect : (Task.task -> bool) -> Task.task -> rem
(** [bisect test task] return metas that specify the symbols that
(** [bisect test task] return the symbols that
can be removed without making the task invalid for
the function test. *)
*)
type bisect_step =
| BSdone of rem
......
Markdown is supported
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