Commit f59f4b8d authored by David Hauzar's avatar David Hauzar

Option "--get-counterexample" added to why3prove and "cntexample" option added to why3.conf.

If these are set, the prover is asked for counter-example and if the counter-example is got, it is displayed.
parent 371633fc
......@@ -12,10 +12,6 @@ prelude "(set-logic AUFBVDTLIRA)"
does not seem to include DT
*)
(* Counterexamples: enable model construction *)
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_intro" *)
......
......@@ -92,7 +92,7 @@ let rec print_model fmt model =
match model with
| [] -> ()
| m_element::t -> begin
fprintf fmt "%s at %a = %a\n"
fprintf fmt "\n%s at %a = %a"
m_element.me_name print_location m_element print_model_value m_element.me_value;
print_model fmt t
end
......
......@@ -38,6 +38,7 @@ type printer_args = {
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
cntexample : bool;
mutable printer_mapping : printer_mapping;
}
......
......@@ -36,6 +36,8 @@ 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;
}
......
......@@ -131,8 +131,12 @@ let print_steps fmt s =
if s >= 0 then fprintf fmt ", %d steps)" s
let print_prover_result fmt
{pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s} =
{pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s; pr_model=m} =
fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
if m <> [] then begin
fprintf fmt "\nCounter-example model:";
Model_parser.print_model fmt m
end;
if ans == HighFailure then
fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
print_prover_status status out
......
......@@ -34,6 +34,7 @@ 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 *)
......@@ -67,7 +68,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 env file extra_files ->
let load_driver = let driver_tag = ref (-1) in fun ?(cntexample = false) env file extra_files ->
let prelude = ref [] in
let regexps = ref [] in
let exitcodes = ref [] in
......@@ -211,6 +212,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
prp_model_parser = Model_parser.lookup_model_parser !model_parser
};
drv_tag = !driver_tag;
drv_cntexample = cntexample;
}
let syntax_map drv =
......@@ -292,6 +294,7 @@ 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,8 +15,9 @@
type driver
val load_driver : Env.env -> string -> string list -> driver
val load_driver : ?cntexample:bool -> 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,6 +175,8 @@ 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 =
......@@ -203,6 +205,7 @@ let loadpath m =
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let cntexample m = m.cntexample
exception StepsCommandNotSpecified of string
......@@ -256,6 +259,7 @@ let empty_main =
memlimit = 1000; (* 1 Mb *)
running_provers_max = 2; (* two provers run in parallel *)
plugins = [];
cntexample = true;
}
let default_main =
......@@ -274,6 +278,7 @@ let set_main rc main =
let section =
set_int section "running_provers_max" main.running_provers_max in
let section = set_stringl section "plugin" main.plugins in
let section = set_bool section "cntexample" main.cntexample in
set_section rc "main" section
exception NonUniqueId
......@@ -424,7 +429,7 @@ let load_shortcut acc section =
let shortcuts = get_stringl section "shortcut" in
let prover = { prover_name = name;
prover_version = version;
prover_altern= altern} in
prover_altern = altern} in
add_prover_shortcuts acc prover shortcuts
with MissingField s ->
Warning.emit "[Warning] cannot load shortcut: missing field '%s'@." s;
......@@ -507,6 +512,7 @@ let load_main dirname section =
running_provers_max = get_int ~default:default_main.running_provers_max
section "running_provers_max";
plugins = get_stringl ~default:[] section "plugin";
cntexample = get_bool ~default:default_main.cntexample section "cntexample"
}
let read_config_rc conf_file =
......
......@@ -75,6 +75,7 @@ val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val cntexample: main -> bool
val set_limits: main -> int -> int -> int -> main
val plugins : main -> string list
......
......@@ -609,7 +609,7 @@ let update_tabs a =
"Edited interactive proof. Run it with \"Replay\" button"
| S.Done
({Call_provers.pr_answer = Call_provers.HighFailure} as r) ->
fprintf str_formatter "%a" Call_provers.print_prover_result r;
Call_provers.print_prover_result str_formatter r;
flush_str_formatter ()
| S.Done r ->
let out = r.Call_provers.pr_output in
......@@ -974,6 +974,7 @@ let () = Queue.iter (open_file ~start:true) files
let prover_on_selected_goals pr =
let timelimit = gconfig.session_time_limit in
let memlimit = gconfig.session_mem_limit in
let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
List.iter
(fun row ->
try
......@@ -981,7 +982,7 @@ let prover_on_selected_goals pr =
M.run_prover
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~timelimit ~memlimit
~timelimit ~memlimit ~cntexample
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 fmt info =
let print_info_model args fmt info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if info_model != [] then
if info_model != [] && args.cntexample then
begin
(*
fprintf fmt "@[(get-value (%a))@]@\n"
......@@ -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 fmt info;
print_info_model args fmt info;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
queried_terms = info.info_model; }
......@@ -425,10 +425,15 @@ let print_decls args =
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm, []),[])))
let set_produce_models fmt cntexample =
if cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt args.prelude;
set_produce_models fmt args.cntexample;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
......
......@@ -1871,7 +1871,7 @@ let remove_metas ?(notify=notify) m =
(** Prover Loaded **)
(*****************************************************)
let load_prover eS prover =
let load_prover ?(cntexample = false) eS prover =
try
PHprover.find eS.loaded_provers prover
with Not_found ->
......@@ -1880,7 +1880,7 @@ let load_prover eS prover =
let r = match r with
| None -> None
| Some pr ->
let dr = Driver.load_driver eS.env
let dr = Driver.load_driver ~cntexample 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 : 'a env_session -> Whyconf.prover -> loaded_prover option
val load_prover : ?cntexample:bool -> 'a env_session -> Whyconf.prover -> loaded_prover option
(** load a prover *)
val unload_provers : 'a env_session -> unit
......
......@@ -345,8 +345,8 @@ let add_file env_session ?format f =
(* method: run a given prover on each unproved goals *)
(*****************************************************)
let find_prover eS a =
match load_prover eS a.proof_prover with
let find_prover ?(cntexample = false) eS a =
match load_prover ~cntexample 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 eS a =
with Not_found ->
(* we modify the prover in-place *)
Session.change_prover a new_p;
match load_prover eS new_p with
match load_prover ~cntexample 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 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 eS new_p with
match load_prover ~cntexample 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 eS eT a callback =
match find_prover eS a with
let run_external_proof_v3 ?(cntexample = false) eS eT a callback =
match find_prover eS a ~cntexample with
| None ->
callback a a.proof_prover dummy_limits None Starting;
(* nothing to do *)
......@@ -500,7 +500,7 @@ let run_external_proof_v3 eS eT a callback =
end
(** run_external_proof_v2 modify the session according to the current state *)
let run_external_proof_v2 eS eT a callback =
let run_external_proof_v2 ?(cntexample = false) 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 eS eT a callback =
end;
callback a ap limits previous state
in
run_external_proof_v3 eS eT a callback
run_external_proof_v3 eS eT a callback ~cntexample
let running = function
| Scheduled | Running -> true
| Unedited | JustEdited | Interrupted
| Done _ | InternalFailure _ -> false
let run_external_proof_v2 eS eT a callback =
let run_external_proof_v2 ?(cntexample = false) 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 eS eT a callback
run_external_proof_v2 ~cntexample eS eT a callback
let run_external_proof eS eT ?callback a =
let run_external_proof ?(cntexample = false) eS eT ?callback a =
let callback =
match callback with
| None -> fun _ _ _ _ _ -> ()
......@@ -545,9 +545,9 @@ let run_external_proof eS eT ?callback a =
| MissingFile _ -> c a a.proof_state
| StatusChange s -> c a s
in
run_external_proof_v2 eS eT a callback
run_external_proof_v2 ~cntexample eS eT a callback
let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
let prover_on_goal ?(cntexample = false) eS eT ?callback ~timelimit ~memlimit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
......@@ -561,42 +561,42 @@ let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
O.init ep.proof_key (Proof_attempt ep);
ep
in
run_external_proof eS eT ?callback a
run_external_proof ~cntexample eS eT ?callback a
let prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit p g =
~context_unproved_goals_only ~timelimit ~memlimit p g ~cntexample =
goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
(prover_on_goal eS eT ~timelimit ~memlimit p) g
(prover_on_goal ~cntexample eS eT ~timelimit ~memlimit p) g
let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
let run_prover ~cntexample 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
~context_unproved_goals_only ~timelimit ~memlimit pr g ~cntexample
| Theory th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr)
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
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)
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
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
~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent ~cntexample
| Transf tr ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr)
~context_unproved_goals_only ~timelimit ~memlimit pr ~cntexample)
tr.transf_goals
| Metas m ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal ~cntexample
......
......@@ -130,6 +130,7 @@ module Make(O: OBSERVER) : sig
(** {2 Actions} *)
val run_prover :
cntexample:bool ->
O.key env_session -> t ->
context_unproved_goals_only:bool ->
timelimit:int -> memlimit:int ->
......@@ -139,10 +140,14 @@ module Make(O: OBSERVER) : sig
will be started asynchronously when processors are available.
~context_unproved_goals_only indicates if prover must be run
on already proved goals or not *)
on already proved goals or not
~cntexample indicates if prover should be asked to get counter-example
model
*)
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
......@@ -157,6 +162,7 @@ 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) ->
......@@ -170,6 +176,7 @@ 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 ->
......
......@@ -91,6 +91,8 @@ let opt_task = ref None
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_cntexmp = ref false
let option_list = [
"-", Arg.Unit (fun () -> add_opt_file "-"),
" read the input file from stdin";
......@@ -141,7 +143,9 @@ let option_list = [
Debug.Args.desc_shortcut
"parse_only" "--parse-only" " stop after parsing";
Debug.Args.desc_shortcut
"type_only" "--type-only" " stop after type checking" ]
"type_only" "--type-only" " stop after type checking";
"--get-counterexample", Arg.Set opt_cntexmp,
" gets the counter-example model" ]
let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg
......@@ -375,7 +379,7 @@ let do_input env drv = function
let () =
try
let load (f,ef) = load_driver env f ef in
let load (f,ef) = load_driver ~cntexample:!opt_cntexmp 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