Commit 00d39290 authored by MARCHE Claude's avatar MARCHE Claude

Strategies parsed from Why3 config file

parent d13b981a
......@@ -128,6 +128,43 @@ type config_editor = {
editor_options : string list;
}
(** Strategies *)
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
}
(* a default set of strategies *)
let default_strategies =
List.map
(fun (name,desc,instrs) ->
let s = ref Rc.empty_section in
s := Rc.set_string !s "name" name;
s := Rc.set_string !s "desc" desc;
for i = 0 to Array.length instrs - 1 do
s := Rc.set_string !s ("l" ^ (string_of_int i)) instrs.(i);
done;
!s)
[ "Split", "Split@ conjunctions@ in@ goal",
[|"t split_goal_wp 1"|];
"Inline", "Inline@ function@ symbols@ once",
[|"t inline_goal 1"|];
"Blaster", "The@ blaster",
[|"c Alt-Ergo,0.95.2 1 1000";
"c CVC4,1.4 1 1000";
"t split_goal_wp 0";
"c Alt-Ergo,0.95.2 10 4000";
"c CVC4,1.4 10 4000" |];
]
let get_strategies rc =
match get_simple_family rc "strategy" with
| [] -> default_strategies
| s -> s
(** Main record *)
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
......@@ -202,6 +239,7 @@ type config = {
prover_shortcuts : prover Mstr.t;
editors : config_editor Meditor.t;
provers_upgrade_policy : prover_upgrade_policy Mprover.t;
strategies : config_strategy Mstr.t;
}
let empty_main =
......@@ -428,6 +466,32 @@ let load_policy provers acc (_,section) =
eprintf "[Warning] cannot load a policy: missing field '%s'@." s;
acc
let load_strategy strategies section =
try
let name = get_string section "name" in
let desc = get_string section "desc" in
let desc = Scanf.format_from_string desc "" in
let code = ref [] and i = ref 0 in
try
while true do
let instr = get_string section ("l" ^ (string_of_int !i)) in
code := instr :: !code;
incr i
done;
assert false
with MissingField _ ->
Mstr.add
name
{ strategy_name = name;
strategy_desc = desc;
strategy_code = Array.of_list (List.rev !code);
}
strategies
with
MissingField s ->
eprintf "[Warning] cannot load a strategy: missing field '%s'@." s;
strategies
let load_main dirname section =
if get_int ~default:0 section "magic" <> magicnumber then
raise WrongMagicNumber;
......@@ -476,6 +540,8 @@ let get_config (filename,rc) =
let editors = List.fold_left load_editor Meditor.empty editors in
let policy = get_family rc "uninstalled_prover" in
let policy = List.fold_left (load_policy provers) Mprover.empty policy in
let strategies = get_strategies rc in
let strategies = List.fold_left load_strategy Mstr.empty strategies in
{ conf_file = filename;
config = rc;
main = main;
......@@ -483,6 +549,7 @@ let get_config (filename,rc) =
prover_shortcuts = shortcuts;
editors = editors;
provers_upgrade_policy = policy;
strategies = strategies;
}
let default_config conf_file =
......@@ -709,6 +776,8 @@ let get_editors c = c.editors
let editor_by_id whyconf id =
Meditor.find id whyconf.editors
let get_strategies config = config.strategies
(******)
let get_section config name = assert (name <> "main");
......
......@@ -177,6 +177,16 @@ val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config -> prover_upgrade_policy Mprover.t -> config
(** strategies *)
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
}
val get_strategies : config -> config_strategy Mstr.t
(** filter prover *)
type filter_prover
......
......@@ -1447,20 +1447,49 @@ let test_strategy () =
M.Icall_prover(cvc4.Whyconf.prover,10,4000);
|]
let strategies () :
(string * Pp.formatted * M.strategy *
(*
let strategies () :
(string * Pp.formatted * M.strategy *
(string * Gdk.keysym) option) list =
[ "Split", "Splits@ conjunctions@ of@ the@ goal", split_strategy,
[ "Split", "Splits@ conjunctions@ of@ the@ goal", split_strategy,
Some("s",GdkKeysyms._s);
"Inline", "Inline@ defined@ symbols", inline_strategy,
Some("i",GdkKeysyms._i);
"Blaster", "Blaster@ strategy", test_strategy (),
Some("b",GdkKeysyms._b);
]
*)
let loaded_strategies = ref []
let strategies () =
match !loaded_strategies with
| [] ->
let config = gconfig.Gconfig.config in
let strategies = Whyconf.get_strategies config in
let strategies =
Mstr.fold_left
(fun acc _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let len = Array.length code in
let code = Array.map (M.parse_instr (env_session()) len) code in
Format.eprintf "Strategy '%s' loaded.@." name;
(name, st.Whyconf.strategy_desc,code, None) :: acc
with M.SyntaxError msg ->
Format.eprintf "Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
loaded_strategies := strategies;
strategies
| l -> l
let escape_text = Glib.Markup.escape_text
let sanitize_markup x =
let remove = function
| '_' -> "__"
......@@ -1471,7 +1500,7 @@ let string_of_desc desc =
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n%a@]" x Pp.formatted r
in Pp.string_of print_trans_desc desc
let () =
let add_submenu_transform name get_trans () =
let submenu = tools_factory#add_submenu name in
......@@ -1513,7 +1542,7 @@ let () =
let iter (name,desc,strat,k) =
let callback () = apply_strategy_on_selection strat in
let ii = submenu#add_image_item
~label:(sanitize_markup name) ~callback ()
~label:(sanitize_markup name) ~callback ()
in
let name =
match k with
......@@ -1532,7 +1561,7 @@ let () =
let () =
let iter (name,desc,strat,k) =
let b = GButton.button ~packing:strategies_box#add
let b = GButton.button ~packing:strategies_box#add
~label:(sanitize_markup name) ()
in
let name =
......@@ -2150,8 +2179,8 @@ let () =
if key = GdkKeysyms._x then begin confirm_remove_selection (); true end else
(* strategy shortcuts *)
let rec iter l =
match l with
| [] -> false (* otherwise, use the default event handler *)
match l with
| [] -> false (* otherwise, use the default event handler *)
| (_,_,_,None) :: rem -> iter rem
| (_,_,s,Some(_,k)) :: rem ->
if key = k then begin apply_strategy_on_selection s; true end else
......
......@@ -129,7 +129,7 @@ let init max =
let notify_timer_state t continue =
O.notify_timer_state
(Queue.length t.actions_queue)
(Queue.length t.proof_attempts_queue)
(Queue.length t.proof_attempts_queue)
(List.length t.running_proofs);
continue
......@@ -925,6 +925,86 @@ let convert_unknown_prover =
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
exception SyntaxError of string
let parse_instr env max s =
match Strings.split s ' ' with
| [] -> raise (SyntaxError "unexpected empty instruction")
| ["g";n] ->
let g =
try int_of_string n
with Failure _ ->
raise
(SyntaxError
("unable to parse goto argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
raise
(SyntaxError ("goto index " ^ n ^ " is invalid"));
Igoto g
| "g" :: _ ->
raise (SyntaxError "'g' expects exactly one argument")
| ["c";p;t;m] ->
let p =
try
let fp = Whyconf.parse_filter_prover p in
Whyconf.filter_one_prover env.whyconf fp
with Whyconf.ProverNotFound _ ->
raise
(SyntaxError
("Prover " ^ p ^ " not installed or not configured"))
in
let timelimit =
try int_of_string t
with Failure _ ->
raise
(SyntaxError
("unable to parse timelimit argument '" ^ t ^ "'"))
in
if timelimit <= 0 then
raise
(SyntaxError ("timelimit " ^ t ^ " is invalid"));
let memlimit =
try int_of_string m
with Failure _ ->
raise
(SyntaxError
("unable to parse memlimit argument '" ^ m ^ "'"))
in
if memlimit <= 0 then
raise
(SyntaxError ("memlimit " ^ m ^ " is invalid"));
Icall_prover(p.Whyconf.prover,timelimit,memlimit)
| "c" :: _ ->
raise (SyntaxError "'c' expects exactly three arguments")
| ["t";t;n] ->
let () =
try
let _ = Trans.lookup_transform t env.env in
()
with Trans.UnknownTrans _ ->
try
let _ = Trans.lookup_transform_l t env.env in
()
with Trans.UnknownTrans _->
raise (SyntaxError ("transformation '" ^ t ^ "' is unknown"))
in
let g =
try int_of_string n
with Failure _ ->
raise
(SyntaxError
("unable to parse argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
raise
(SyntaxError ("index " ^ n ^ " is invalid"));
Itransform(t,g)
| "t" :: _ ->
raise (SyntaxError "'t' expects exactly one argument")
| s :: _ ->
raise (SyntaxError ("unknown instruction '" ^ s ^ "'"))
type strategy = instruction array
let rec exec_strategy es sched pc strat g =
......
......@@ -319,6 +319,10 @@ module Make(O: OBSERVER) : sig
type strategy = instruction array
exception SyntaxError of string
val parse_instr : O.key Session.env_session -> int -> string -> instruction
val run_strategy_on_goal:
O.key Session.env_session -> t ->
strategy -> O.key Session.goal -> unit
......
......@@ -20,6 +20,8 @@ let rev_split s c =
| Invalid_argument _ -> ""::acc in
aux [] 0
let split s c = List.rev (rev_split s c)
let ends_with s suf =
let rec aux s suf suflen offset i =
i >= suflen || (s.[i + offset] = suf.[i]
......
......@@ -13,6 +13,8 @@
val rev_split : string -> char -> string list
val split : string -> char -> string list
val ends_with : string -> string -> bool
(** test if a string ends with another *)
......
......@@ -2,8 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="10" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.3" timelimit="10" memlimit="4000"/>
<file name="../test_compute.why" expanded="true">
<theory name="Test" expanded="true">
<goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531">
......@@ -11,14 +9,6 @@
</transf>
</goal>
<goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891" expanded="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="unknown" time="0.01"/></proof>
<proof prover="1" timelimit="1" memlimit="1000"><result status="unknown" time="0.00"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="g2.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
<proof prover="1"><result status="unknown" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="g3" sum="059bfb681820ff98c7d4f1682433c247">
<transf name="compute_in_goal">
......
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