Commit 94debda2 authored by David Hauzar's avatar David Hauzar

Controlling whether the counter-example will be got using metas.

It finished for why3prove but not finishedfor why3ide yet.
parent 620228a2
......@@ -38,7 +38,6 @@ type printer_args = {
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
cntexample : bool;
mutable printer_mapping : printer_mapping;
}
......
......@@ -36,8 +36,6 @@ type printer_args = {
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
cntexample : bool;
(* True if counter-example should be generated. *)
mutable printer_mapping : printer_mapping;
}
......
......@@ -34,7 +34,6 @@ type driver = {
drv_meta : (theory * Stdecl.t) Mid.t;
drv_res_parser : prover_result_parser;
drv_tag : int;
drv_cntexample : bool;
}
(** parse a driver file *)
......@@ -68,7 +67,7 @@ exception UnknownProp of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
let load_driver = let driver_tag = ref (-1) in fun ?(cntexample = false) env file extra_files ->
let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let prelude = ref [] in
let regexps = ref [] in
let exitcodes = ref [] in
......@@ -212,7 +211,6 @@ let load_driver = let driver_tag = ref (-1) in fun ?(cntexample = false) env fil
prp_model_parser = Model_parser.lookup_model_parser !model_parser
};
drv_tag = !driver_tag;
drv_cntexample = cntexample;
}
let syntax_map drv =
......@@ -295,7 +293,6 @@ let print_task_prepared ?old drv fmt task =
prelude = drv.drv_prelude;
th_prelude = drv.drv_thprelude;
blacklist = drv.drv_blacklist;
cntexample = drv.drv_cntexample;
printer_mapping = get_default_printer_mapping;
} in
let printer = lookup_printer p printer_args in
......
......@@ -15,9 +15,8 @@
type driver
val load_driver : ?cntexample:bool -> Env.env -> string -> string list -> driver
val load_driver : Env.env -> string -> string list -> driver
(** loads a driver from a file
@param bool true if the prover should be asked for a counter-example model
@param env environment to interpret theories
@param string driver file name
@param string list additional driver files containing only theories
......
......@@ -175,8 +175,6 @@ type main = {
(* max number of running prover processes *)
plugins : string list;
(* plugins to load, without extension, relative to [libdir]/plugins *)
cntexample : bool;
(* true provers should be asked for counter-example model *)
}
let libdir m =
......
......@@ -39,12 +39,15 @@ let debug = Debug.lookup_flag "ide_info"
let files = Queue.create ()
let opt_parser = ref None
let opt_cntexmp = ref false
let spec = Arg.align [
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
" same as -F";
"--get-ce", Arg.Set opt_cntexmp,
" gets the counter-example model";
(*
"-f",
Arg.String (fun s -> input_files := s :: !input_files),
......@@ -980,9 +983,10 @@ let prover_on_selected_goals pr =
try
let a = get_any_from_row_reference row in
M.run_prover
MA.keygen
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~timelimit ~memlimit ~cntexample
~timelimit ~memlimit
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......
......@@ -330,10 +330,10 @@ let print_logic_decl info fmt (ls,def) =
List.iter forget_var vsl
end
let print_info_model args fmt info =
let print_info_model cntexample fmt info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if info_model != [] && args.cntexample then
if info_model != [] && cntexample then
begin
(*
fprintf fmt "@[(get-value (%a))@]@\n"
......@@ -351,7 +351,7 @@ let print_info_model args fmt info =
info.info_model <- info_model
end
let print_prop_decl args info fmt k pr f = match k with
let print_prop_decl cntexample args info fmt k pr f = match k with
| Paxiom ->
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
pr.pr_name.id_string (* FIXME? collisions *)
......@@ -365,7 +365,7 @@ let print_prop_decl args info fmt k pr f = match k with
Loc.gen_report_position loc);
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
fprintf fmt "@[(check-sat)@]@\n";
print_info_model args fmt info;
print_info_model cntexample fmt info;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
queried_terms = info.info_model; }
......@@ -395,7 +395,7 @@ let print_data_decl info fmt (ts,cl) =
print_ident ts.ts_name
(print_list space (print_constructor_decl info)) cl
let print_decl args info fmt d = match d.d_node with
let print_decl cntexample args info fmt d = match d.d_node with
| Dtype ts ->
print_type_decl info fmt ts
| Ddata dl ->
......@@ -412,12 +412,12 @@ let print_decl args info fmt d = match d.d_node with
"smtv2 : inductive definition are not supported"
| Dprop (k,pr,f) ->
if Mid.mem pr.pr_name info.info_syn then () else
print_prop_decl args info fmt k pr f
print_prop_decl cntexample args info fmt k pr f
let print_decls args =
let print_decls cntexample args =
let print_decl (sm, cm, model) fmt d =
try let info = {info_syn = sm; info_converters = cm; info_model = model} in
print_decl args info fmt d; (sm, cm, info.info_model), []
print_decl cntexample args info fmt d; (sm, cm, info.info_model), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......@@ -432,13 +432,16 @@ let set_produce_models fmt cntexample =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
print_prelude fmt args.prelude;
set_produce_models fmt args.cntexample;
set_produce_models fmt cntexample;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
print (snd (Trans.apply (print_decls args) task));
print (snd (Trans.apply (print_decls cntexample args) task));
pp_print_flush fmt ()
let () = register_printer "smtv2" print_task
......
......@@ -1837,6 +1837,18 @@ let pos_of_metas lms =
List.fold_left (fun idpos (_,args) ->
List.fold_left look_for_ident idpos args) empty_idpos lms
let add_meta_to_task g meta meta_args =
(*let task = goal_task goal in
let task = Task.add_meta task meta meta_args in
goal.goal_task <- Some task
*)
let goal,task = Task.task_separate_goal (goal_task g) in
let task = Task.add_meta task meta meta_args in
g.goal_task <- Some task
let add_registered_metas ~keygen env added0 g =
let added = List.fold_left (fun ma (s,l) ->
Mstr.change (function
......@@ -1872,7 +1884,7 @@ let remove_metas ?(notify=notify) m =
(** Prover Loaded **)
(*****************************************************)
let load_prover ?(cntexample = false) eS prover =
let load_prover eS prover =
try
PHprover.find eS.loaded_provers prover
with Not_found ->
......@@ -1881,7 +1893,7 @@ let load_prover ?(cntexample = false) eS prover =
let r = match r with
| None -> None
| Some pr ->
let dr = Driver.load_driver ~cntexample eS.env
let dr = Driver.load_driver eS.env
pr.Whyconf.driver pr.Whyconf.extra_drivers in
Some { prover_config = pr;
prover_driver = dr}
......
......@@ -230,7 +230,7 @@ type 'a env_session = private
val update_env_session_config : 'a env_session -> Whyconf.config -> unit
(** updates the configuration *)
val load_prover : ?cntexample:bool -> 'a env_session -> Whyconf.prover -> loaded_prover option
val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
(** load a prover *)
val unload_provers : 'a env_session -> unit
......@@ -443,6 +443,8 @@ val remove_transformation : ?notify:'key notify -> 'key transf -> unit
(** Remove a transformation *)
(** {2 Metas} *)
val add_meta_to_task : 'key goal -> Theory.meta -> Theory.meta_arg list -> unit
val add_registered_metas :
keygen:'key keygen ->
'key env_session ->
......
......@@ -345,8 +345,8 @@ let add_file env_session ?format f =
(* method: run a given prover on each unproved goals *)
(*****************************************************)
let find_prover ?(cntexample = false) eS a =
match load_prover ~cntexample eS a.proof_prover with
let find_prover eS a =
match load_prover eS a.proof_prover with
| Some p -> Some (a.proof_prover, p,a)
| None ->
match O.uninstalled_prover eS a.proof_prover with
......@@ -362,7 +362,7 @@ let find_prover ?(cntexample = false) eS a =
with Not_found ->
(* we modify the prover in-place *)
Session.change_prover a new_p;
match load_prover ~cntexample eS new_p with
match load_prover eS new_p with
| Some p -> Some (new_p,p,a)
| None ->
(* should never happen because at loading, config
......@@ -385,7 +385,7 @@ let find_prover ?(cntexample = false) eS a =
~notify ~keygen:O.create ~prover:new_p ~env_session:eS a
in
O.init new_a.proof_key (Proof_attempt new_a);
match load_prover ~cntexample eS new_p with
match load_prover eS new_p with
| Some p -> Some (new_p,p,new_a)
| None ->
(* should never happen because at loading, config
......@@ -451,8 +451,8 @@ let dummy_limits = (0,0,0)
(** run_external_proof_v3 doesn't modify existing proof attempt, it can just
create new one by find_prover *)
let run_external_proof_v3 ?(cntexample = false) eS eT a callback =
match find_prover eS a ~cntexample with
let run_external_proof_v3 eS eT a callback =
match find_prover eS a with
| None ->
callback a a.proof_prover dummy_limits None Starting;
(* nothing to do *)
......@@ -500,7 +500,7 @@ let run_external_proof_v3 ?(cntexample = false) eS eT a callback =
end
(** run_external_proof_v2 modify the session according to the current state *)
let run_external_proof_v2 ?(cntexample = false) eS eT a callback =
let run_external_proof_v2 eS eT a callback =
let previous_res = ref (a.proof_state,a.proof_obsolete) in
let callback a ap limits previous state =
begin match state with
......@@ -522,19 +522,19 @@ let run_external_proof_v2 ?(cntexample = false) eS eT a callback =
end;
callback a ap limits previous state
in
run_external_proof_v3 eS eT a callback ~cntexample
run_external_proof_v3 eS eT a callback
let running = function
| Scheduled | Running -> true
| Unedited | JustEdited | Interrupted
| Done _ | InternalFailure _ -> false
let run_external_proof_v2 ?(cntexample = false) eS eT a callback =
let run_external_proof_v2 eS eT a callback =
(* Perhaps the test a.proof_archived should be done somewhere else *)
if a.proof_archived || running a.proof_state then () else
run_external_proof_v2 ~cntexample eS eT a callback
run_external_proof_v2 eS eT a callback
let run_external_proof ?(cntexample = false) eS eT ?callback a =
let run_external_proof eS eT ?callback a =
let callback =
match callback with
| None -> fun _ _ _ _ _ -> ()
......@@ -545,9 +545,9 @@ let run_external_proof ?(cntexample = false) eS eT ?callback a =
| MissingFile _ -> c a a.proof_state
| StatusChange s -> c a s
in
run_external_proof_v2 ~cntexample eS eT a callback
run_external_proof_v2 eS eT a callback
let prover_on_goal ?(cntexample = false) eS eT ?callback ~timelimit ~memlimit p g =
let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
......@@ -561,42 +561,49 @@ let prover_on_goal ?(cntexample = false) eS eT ?callback ~timelimit ~memlimit p
O.init ep.proof_key (Proof_attempt ep);
ep
in
run_external_proof ~cntexample eS eT ?callback a
run_external_proof eS eT ?callback a
let prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit p g ~cntexample =
~context_unproved_goals_only ~timelimit ~memlimit p g =
goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
(prover_on_goal ~cntexample eS eT ~timelimit ~memlimit p) g
(prover_on_goal eS eT ~timelimit ~memlimit p) g
let run_prover ~cntexample eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
let run_prover keygen eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
match a with
| Goal g ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr g ~cntexample
| Theory th ->
| Goal g ->
(*let cntexmp_meta = [("get_counterexmp", [])] in
ignore (add_registered_metas ~keygen eS cntexmp_meta g);*)
(*
let meta = Theory.lookup_meta "get_counterexmp" in
let () = Session.add_meta_to_task g meta [] in
*)
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr g
| Theory th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
~context_unproved_goals_only ~timelimit ~memlimit pr)
th.theory_goals
| File file ->
List.iter
(fun th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
~context_unproved_goals_only ~timelimit ~memlimit pr)
th.theory_goals)
file.file_theories
| Proof_attempt a ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent ~cntexample
~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent
| Transf tr ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
~context_unproved_goals_only ~timelimit ~memlimit pr)
tr.transf_goals
| Metas m ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal ~cntexample
~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
......
......@@ -130,7 +130,7 @@ module Make(O: OBSERVER) : sig
(** {2 Actions} *)
val run_prover :
cntexample:bool ->
O.key keygen ->
O.key env_session -> t ->
context_unproved_goals_only:bool ->
timelimit:int -> memlimit:int ->
......@@ -147,7 +147,6 @@ module Make(O: OBSERVER) : sig
val run_external_proof :
?cntexample:bool ->
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
O.key proof_attempt -> unit
......@@ -162,7 +161,6 @@ module Make(O: OBSERVER) : sig
| StatusChange of proof_attempt_status
val run_external_proof_v3 :
?cntexample:bool ->
O.key Session.env_session -> t -> O.key Session.proof_attempt ->
(O.key Session.proof_attempt -> Whyconf.prover ->
int * int * int -> Call_provers.prover_result option -> run_external_status -> unit) ->
......@@ -176,7 +174,6 @@ module Make(O: OBSERVER) : sig
val prover_on_goal :
?cntexample:bool ->
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
timelimit:int -> memlimit:int ->
......
......@@ -209,7 +209,9 @@ let () = try
in
Task.add_meta task meta args
in
opt_task := List.fold_left add_meta !opt_task !opt_metas
let metas = if !opt_cntexmp then (("get_counterexmp", None)::!opt_metas)
else !opt_metas in
opt_task := List.fold_left add_meta !opt_task metas
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
......@@ -379,7 +381,7 @@ let do_input env drv = function
let () =
try
let load (f,ef) = load_driver ~cntexample:!opt_cntexmp env f ef in
let load (f,ef) = load_driver env f ef in
let drv = Opt.map load !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not (Debug.test_flag Debug.stack_trace) ->
......
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