Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit e847147b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

strategies: first step


Signed-off-by: MARCHE Claude's avatarClaude Marche <Claude.Marche@inria.fr>
parent d098414b
......@@ -919,7 +919,7 @@ let set_archive_proofs b () =
(get_selected_row_references ())
(*****************************************************)
(* method: split selected goals *)
(* method: apply strategy on selected goals *)
(*****************************************************)
......@@ -933,6 +933,19 @@ let apply_trans_on_selection tr =
a)
(get_selected_row_references ())
let apply_strategy_on_selection str =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
match a with
| S.Goal g ->
M.run_strategy_on_goal (env_session()) sched
str g
| _ -> ())
(get_selected_row_references ())
(*****************************************************)
(* method: bisect goal *)
(*****************************************************)
......@@ -1421,6 +1434,28 @@ let split_selected_goals () =
let inline_selected_goals () =
apply_trans_on_selection inline_transformation
let run_test_strategy () =
let strat =
let config = gconfig.Gconfig.config in
let altergo =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
Whyconf.filter_one_prover config fp
in
let cvc4 =
let fp = Whyconf.parse_filter_prover "CVC4" in
Whyconf.filter_one_prover config fp
in
[|
M.Icall_prover(altergo.Whyconf.prover,1,1000);
M.Icall_prover(cvc4.Whyconf.prover,1,1000);
M.Icall_prover(altergo.Whyconf.prover,10,4000);
M.Icall_prover(cvc4.Whyconf.prover,10,4000);
|]
in
apply_strategy_on_selection strat
let escape_text = Glib.Markup.escape_text
let sanitize_markup x =
let remove = function
......@@ -1470,6 +1505,7 @@ let () =
add_tool_separator ();
add_tool_item "Split in selection" split_selected_goals;
add_tool_item "Inline in selection" inline_selected_goals;
add_tool_item "Test strategy" run_test_strategy;
add_gui_item add_non_splitting_1;
add_gui_item add_non_splitting_2;
add_gui_item add_splitting;
......@@ -1499,6 +1535,17 @@ to the <b>selected goals</b>";
in
()
let () =
let b = GButton.button ~packing:transf_box#add ~label:"Test Strategy" () in
b#misc#set_tooltip_markup "Apply the strategy <tt>test</tt> \
to the <b>selected goals</b>";
let i = GMisc.image ~pixbuf:(!image_transf) () in
let () = b#set_image i#coerce in
let (_ : GtkSignal.id) =
b#connect#pressed ~callback:run_test_strategy
in
()
......
......@@ -310,7 +310,7 @@ let update_session ?release ~allow_obsolete old_session env whyconf =
O.reset ();
let (env_session,_,_) as res =
update_session ?release
~keygen:O.create ~allow_obsolete old_session env whyconf
~keygen:O.create ~allow_obsolete old_session env whyconf
in
Debug.dprintf debug "Init_session@\n";
init_session env_session.session;
......@@ -491,7 +491,8 @@ let run_external_proof_v2 eS eT a callback =
end
| _ -> ()
end;
callback a ap timelimit previous state in
callback a ap timelimit previous state
in
run_external_proof_v3 eS eT a callback
let running = function
......@@ -513,7 +514,8 @@ let run_external_proof eS eT ?callback a =
| Starting -> ()
| MissingProver -> c a Interrupted
| MissingFile _ -> c a a.proof_state
| StatusChange s -> c a s in
| StatusChange s -> c a s
in
run_external_proof_v2 eS eT a callback
let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
......@@ -908,6 +910,50 @@ let rec clean = function
let convert_unknown_prover =
Session_tools.convert_unknown_prover ~keygen:O.create
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type strategy = instruction array
let rec exec_strategy es sched pc strat g =
if pc < 0 || pc >= Array.length strat then
(* halt the strategy *)
()
else
match Array.get strat pc with
| Icall_prover(p,timelimit,memlimit) ->
let callback _pa res =
match res with
| Scheduled | Running ->
(* nothing to do yet *)
()
| Done { Call_provers.pr_answer = Call_provers.Valid } ->
(* proof succeeded, nothing more to do *)
()
| Interrupted | InternalFailure _ | Done _ ->
(* proof did not succeed, goto to next step *)
let callback () = exec_strategy es sched (pc+1) strat g in
schedule_delayed_action sched callback
| Unedited | JustEdited ->
(* should not happen *)
assert false
in
prover_on_goal es sched ~callback ~timelimit ~memlimit p g
| Itransform(_tr,_pcsuccess) ->
assert false (* TODO *)
| Igoto pc ->
exec_strategy es sched pc strat g
let run_strategy_on_goal es sched strat g =
let callback () = exec_strategy es sched 0 strat g in
schedule_delayed_action sched callback
end
......
......@@ -295,6 +295,34 @@ module Make(O: OBSERVER) : sig
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
(** {2 User-defined strategies} *)
(** A strategy is defined by a program declared under a simple
assembly-like form: instructions are indexed by integers
starting from 0 (the initial instruction counter). An
instruction is either
1) a call to a prover, with given time and mem limits
. on success, the program execution ends
. on any other result, the program execution continues on the next index
2) a application of a transformation
. on success, the execution continues to a explicitly given index
. on failure, execution continues on the next index
3) a goto instruction.
the execution halts when reaching a non-existing state
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type strategy = instruction array
val run_strategy_on_goal:
O.key Session.env_session -> t ->
strategy -> O.key Session.goal -> unit
end
......
......@@ -6,15 +6,6 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
*)
theory W
use int.Int
predicate f (x:int) = Int.(<=) x
end
theory TestProp
goal Test0 : true
......
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