Commit d4c3cfbf authored by David Hauzar's avatar David Hauzar

Store steplimit in session file.

parent b5883169
......@@ -93,6 +93,7 @@ let add_proofs_attempts g =
~obsolete:true
~archived:false
~timelimit:5
~steplimit:(-1)
~memlimit:1000
~edit:None
g p.Whyconf.prover Session.Scheduled
......@@ -106,5 +107,3 @@ let () =
(* save the session on disk *)
let () = Session.save_session config env_session.Session.session
......@@ -1016,7 +1016,7 @@ let prover_on_selected_goals pr =
M.run_prover
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~cntexample ~timelimit ~memlimit
~cntexample ~timelimit ~steplimit:(-1) ~memlimit
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......@@ -1541,11 +1541,11 @@ let test_strategy () =
Whyconf.filter_one_prover config fp
in
[|
Strategy.Icall_prover(altergo.Whyconf.prover,1,1000);
Strategy.Icall_prover(cvc4.Whyconf.prover,1,1000);
Strategy.Icall_prover(altergo.Whyconf.prover,1,-1,1000);
Strategy.Icall_prover(cvc4.Whyconf.prover,1,0,1000);
Strategy.Itransform(split_transformation,0); (* goto 0 on success *)
Strategy.Icall_prover(altergo.Whyconf.prover,10,4000);
Strategy.Icall_prover(cvc4.Whyconf.prover,10,4000);
Strategy.Icall_prover(altergo.Whyconf.prover,10,-1,4000);
Strategy.Icall_prover(cvc4.Whyconf.prover,10,-1,4000);
|]
(*
......
This diff is collapsed.
......@@ -96,6 +96,7 @@ and 'a proof_attempt = private
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_steplimit : int;
mutable proof_memlimit : int;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
......@@ -346,6 +347,7 @@ val add_external_proof :
obsolete:bool ->
archived:bool ->
timelimit:int ->
steplimit:int ->
memlimit:int ->
edit:string option ->
'key goal ->
......@@ -388,6 +390,7 @@ val copy_external_proof :
?obsolete:bool ->
?archived:bool ->
?timelimit:int ->
?steplimit:int ->
?memlimit:int ->
?edit:string option ->
?goal:'key goal ->
......
......@@ -545,7 +545,7 @@ let run_external_proof eS eT ?(cntexample=false) ?callback a =
in
run_external_proof_v2 ~use_steps:false eS eT a ~cntexample callback
let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g =
let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~steplimit ~memlimit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
......@@ -554,7 +554,7 @@ let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g
a
with Not_found ->
let ep = add_external_proof ~keygen:O.create ~obsolete:false
~archived:false ~timelimit ~memlimit
~archived:false ~timelimit ~steplimit ~memlimit
~edit:None g p Interrupted in
O.init ep.proof_key (Proof_attempt ep);
ep
......@@ -562,39 +562,39 @@ let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g
run_external_proof eS eT ~cntexample ?callback a
let prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit p g =
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit p g =
goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
(prover_on_goal eS eT ~cntexample ~timelimit ~memlimit p) g
(prover_on_goal eS eT ~cntexample ~timelimit ~steplimit ~memlimit p) g
let run_prover eS eT ~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a =
let run_prover eS eT ~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr a =
match a with
| Goal g ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr g
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr g
| Theory th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
th.theory_goals
| File file ->
List.iter
(fun th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
th.theory_goals)
file.file_theories
| Proof_attempt a ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr a.proof_parent
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr a.proof_parent
| Transf tr ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr)
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr)
tr.transf_goals
| Metas m ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~cntexample ~timelimit ~memlimit pr m.metas_goal
~context_unproved_goals_only ~cntexample ~timelimit ~steplimit ~memlimit pr m.metas_goal
......@@ -741,16 +741,17 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
(* play all *)
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
let timelimit, memlimit, auto_proved =
PHprover.fold (fun _ pa (timelimit, memlimit, _ as acc) ->
let rec play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l g =
let timelimit, steplimit, memlimit, auto_proved =
PHprover.fold (fun _ pa (timelimit, steplimit, memlimit, _ as acc) ->
match pa.proof_edited_as, pa.proof_state with
| None, Done { Call_provers.pr_answer = Call_provers.Valid } ->
max timelimit pa.proof_timelimit,
max steplimit pa.proof_steplimit,
max memlimit pa.proof_memlimit,
true
| _ -> acc)
g.goal_external_proofs (timelimit, memlimit, false) in
g.goal_external_proofs (timelimit, steplimit, memlimit, false) in
let callback _key status =
if not (running status) then Todo._done todo () in
if auto_proved then begin
......@@ -760,21 +761,21 @@ let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
(* eprintf "todo increased to %d@." todo.Todo.todo; *)
(* eprintf "prover %a on goal %s@." *)
(* Whyconf.print_prover p g.goal_name.Ident.id_string; *)
prover_on_goal eS eT ~callback ~timelimit ~memlimit p g)
prover_on_goal eS eT ~callback ~timelimit ~steplimit ~memlimit p g)
l
end;
iter_goal
(fun _ -> ())
(iter_transf
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
(play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
)
(iter_metas
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
(play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
)
g
let play_all eS eT ~callback ~timelimit ~memlimit l =
let play_all eS eT ~callback ~timelimit ~steplimit ~memlimit l =
let todo = Todo.create () (fun () _ -> ()) callback in
Todo.start todo;
PHstr.iter
......@@ -782,7 +783,7 @@ let play_all eS eT ~callback ~timelimit ~memlimit l =
List.iter
(fun th ->
List.iter
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
(play_on_goal_and_children eS eT ~timelimit ~steplimit ~memlimit todo l)
th.theory_goals)
file.file_theories)
eS.session.session_files;
......@@ -939,7 +940,7 @@ let convert_unknown_prover =
Todo._done todo ()
else
match Array.get strat pc with
| Icall_prover(p,timelimit,memlimit) ->
| Icall_prover(p,timelimit,steplimit,memlimit) ->
let callback _pa res =
match res with
| Scheduled | Running ->
......@@ -956,7 +957,7 @@ let convert_unknown_prover =
(* should not happen *)
assert false
in
prover_on_goal es sched ~callback ~timelimit ~memlimit p g
prover_on_goal es sched ~callback ~timelimit ~steplimit ~memlimit p g
| Itransform(trname,pcsuccess) ->
let callback ntr =
match ntr with
......
......@@ -133,7 +133,7 @@ module Make(O: OBSERVER) : sig
O.key env_session -> t ->
context_unproved_goals_only:bool ->
cntexample : bool ->
timelimit:int -> memlimit:int ->
timelimit:int -> steplimit:int -> memlimit:int ->
Whyconf.prover -> O.key any -> unit
(** [run_prover es sched p a] runs prover [p] on all goals under [a]
the proof attempts are only scheduled for running, and they
......@@ -188,7 +188,7 @@ module Make(O: OBSERVER) : sig
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
?cntexample : bool ->
timelimit:int -> memlimit:int ->
timelimit:int -> steplimit:int -> memlimit:int ->
Whyconf.prover -> O.key goal -> unit
(** [prover_on_goal es sched ?cntexample ?timelimit p g] same as
{!redo_external_proof} but creates or reuses existing proof_attempt
......@@ -298,7 +298,7 @@ module Make(O: OBSERVER) : sig
val play_all :
O.key env_session -> t -> callback:(unit-> unit) ->
timelimit:int -> memlimit:int -> Whyconf.prover list -> unit
timelimit:int -> steplimit:int -> memlimit:int -> Whyconf.prover list -> unit
(** [play_all es sched l] runs every prover of list [l] on all
goals and sub-goals of the session, with the given time limit.
[callback] is called when all tasks are finished.
......
......@@ -12,7 +12,7 @@
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
......
......@@ -27,10 +27,8 @@
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type t = instruction array
......@@ -120,13 +120,15 @@ rule scan code = parse
| goto space+ (ident as id)
{ add_instr code (Igoto (find_label code id));
scan code lexbuf }
| call space+ (ident as p) space+ (integer as t) space+ (integer as m)
| call space+ (ident as p) space+ (integer as t) space+ (integer as s) space+ (integer as m)
{ let p = prover code p in
let t = integer "timelimit" t in
if t <= 0 then error "timelimit %d is invalid" t;
let s = integer "steplimit" s in
if s <= 0 then error "steplimit %d is invalid" s;
let m = integer "memlimit" m in
if m <= 0 then error "memlimit %d is invalid" m;
add_instr code (Icall_prover (p.Whyconf.prover, t, m));
add_instr code (Icall_prover (p.Whyconf.prover, t, s, m));
scan code lexbuf }
| transform space+ (ident as t) space+ (ident as l)
{ transform code t;
......
......@@ -397,7 +397,7 @@ let run_as_bench env_session =
eprintf " done.@.";
exit 0
in
M.play_all env_session sched ~callback ~timelimit:2 ~memlimit:0 provers;
M.play_all env_session sched ~callback ~timelimit:2 ~steplimit:(-1) ~memlimit:0 provers;
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
exit 1
......
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