Commit 66b79960 authored by MARCHE Claude's avatar MARCHE Claude

Strategies: steplimit is not meaningfull -> removed

parent f64a0c8a
......@@ -1530,6 +1530,7 @@ let split_strategy =
let inline_strategy =
[| Strategy.Itransform(inline_transformation,1) |]
(*
let test_strategy () =
let config = gconfig.Gconfig.config in
let altergo =
......@@ -1541,12 +1542,13 @@ let test_strategy () =
Whyconf.filter_one_prover config fp
in
[|
Strategy.Icall_prover(altergo.Whyconf.prover,1,-1,1000);
Strategy.Icall_prover(cvc4.Whyconf.prover,1,0,1000);
Strategy.Icall_prover(altergo.Whyconf.prover,1,1000);
Strategy.Icall_prover(cvc4.Whyconf.prover,1,1000);
Strategy.Itransform(split_transformation,0); (* goto 0 on success *)
Strategy.Icall_prover(altergo.Whyconf.prover,10,-1,4000);
Strategy.Icall_prover(cvc4.Whyconf.prover,10,-1,4000);
Strategy.Icall_prover(altergo.Whyconf.prover,10,4000);
Strategy.Icall_prover(cvc4.Whyconf.prover,10,4000);
|]
*)
(*
let strategies () :
......
......@@ -940,7 +940,7 @@ let convert_unknown_prover =
Todo._done todo ()
else
match Array.get strat pc with
| Icall_prover(p,timelimit,steplimit,memlimit) ->
| Icall_prover(p,timelimit,memlimit) ->
let callback _pa res =
match res with
| Scheduled | Running ->
......@@ -957,7 +957,7 @@ let convert_unknown_prover =
(* should not happen *)
assert false
in
prover_on_goal es sched ~callback ~timelimit ~steplimit ~memlimit p g
prover_on_goal es sched ~callback ~timelimit ~steplimit:(-1) ~memlimit p g
| Itransform(trname,pcsuccess) ->
let callback ntr =
match ntr with
......
......@@ -12,7 +12,7 @@
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
......
......@@ -27,7 +27,7 @@
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int * int (** timelimit, steplimi, memlimit *)
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
......
......@@ -120,15 +120,13 @@ 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 s) space+ (integer as m)
| call space+ (ident as p) space+ (integer as t) 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, s, m));
add_instr code (Icall_prover (p.Whyconf.prover, t, m));
scan code lexbuf }
| transform space+ (ident as t) space+ (ident as l)
{ transform code t;
......
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