Commit ce93b961 authored by MARCHE Claude's avatar MARCHE Claude

counterexample generation as a prover alternative

# Conflicts:
#	share/provers-detection-data.conf
#	src/driver/driver.ml
#	src/session/controller_itp.ml
#	src/session/controller_itp.mli
#	src/session/itp_server.ml
parent 76958dd8
......@@ -30,11 +30,11 @@ fi
run () {
printf " $2 ($1)... "
f="$2_$1"
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1,counterexamples" --timelimit 1 -a split_intros_goal_wp "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' > "$f.out"
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 --debug fast_wp -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1,counterexamples" --timelimit 1 --debug fast_wp -a split_intros_goal_wp "$2.mlw" | \
sed 's/ ([0-9]\+\.[0-9]\+s)//' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
......
......@@ -45,6 +45,21 @@ command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
# CVC4 version 1.5, with counterexamples
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.5"
driver = "cvc4_15_ce"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version 1.5
[ATP cvc4]
name = "CVC4"
......@@ -373,6 +388,25 @@ command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 >= 4.6.0, with counterexamples
[ATP z3-ce]
name = "Z3"
alternative = "counterexamples"
exec = "z3"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.6.0"
version_ok = "4.5.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_440_ce"
command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 >= 4.4.0, with BV support
[ATP z3]
name = "Z3"
......
......@@ -285,16 +285,7 @@ let update_task = let ht = Hint.create 5 in fun drv ->
add_tdecl task goal
| task -> update task
let add_cntexample_meta task cntexample =
if not (cntexample) then task
else
let cnt_meta = lookup_meta "get_counterexmp" in
let g,task = Task.task_separate_goal task in
let task = Task.add_meta task cnt_meta [] in
Task.add_tdecl task g
let prepare_task ~cntexample drv task =
let task = add_cntexample_meta task cntexample in
let prepare_task drv task =
let lookup_transform t = lookup_transform t drv.drv_env in
let transl = List.map lookup_transform drv.drv_transform in
let apply task tr = Trans.apply tr task in
......@@ -316,8 +307,8 @@ let print_task_prepared ?old drv fmt task =
fprintf fmt "@[%a@]@?" (printer ?old) task;
printer_args.printer_mapping
let print_task ?old ?(cntexample=false) drv fmt task =
let task = prepare_task ~cntexample drv task in
let print_task ?old drv fmt task =
let task = prepare_task drv task in
let _ = print_task_prepared ?old drv fmt task in
()
......@@ -375,9 +366,8 @@ let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
Buffer.reset buf;
res
let prove_task ~command ~limit ?(cntexample=false) ?old
?inplace ?interactive drv task =
let task = prepare_task ~cntexample drv task in
let prove_task ~command ~limit ?old ?inplace ?interactive drv task =
let task = prepare_task drv task in
prove_task_prepared ~command ~limit ?interactive ?old ?inplace drv task
(* exception report *)
......
......@@ -46,7 +46,6 @@ val call_on_buffer :
val print_task :
?old : in_channel ->
?cntexample : bool ->
driver -> Format.formatter -> Task.task -> unit
val print_theory :
......@@ -57,14 +56,13 @@ val print_theory :
val prove_task :
command : string ->
limit : Call_provers.resource_limit ->
?cntexample : bool ->
?old : string ->
?inplace : bool ->
?interactive : bool ->
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
......
......@@ -356,7 +356,7 @@ let fuzzy_proof_time nres ores =
else nres
let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
let build_prover_call ?proof_script c id pr limit callback ores =
let (config_pr,driver) = Hprover.find c.controller_provers pr in
let with_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let command =
......@@ -369,7 +369,7 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
let interactive = config_pr.Whyconf.interactive in
try
let call =
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace ~command
Driver.prove_task ?old:proof_script ~inplace ~command
~limit ~interactive driver task
in
let pa = (c.controller_session,id,pr,callback,false,call,ores) in
......@@ -454,10 +454,10 @@ let timeout_handler () =
try
for _i = Hashtbl.length prover_tasks_in_progress
to S.multiplier * !session_max_tasks do
let (c,id,pr,limit,proof_script,callback,cntexample,ores) =
let (c,id,pr,limit,proof_script,callback,ores) =
Queue.pop scheduled_proof_attempts in
try
build_prover_call ?proof_script ~cntexample c id pr limit callback ores
build_prover_call ?proof_script c id pr limit callback ores
with e when not (Debug.test_flag Debug.stack_trace) ->
callback (InternalFailure e)
done
......@@ -481,7 +481,7 @@ let interrupt () =
*)
number_of_running_provers := 0;
while not (Queue.is_empty scheduled_proof_attempts) do
let (_c,_id,_pr,_limit,_proof_script,callback,_cntexample,_ores) =
let (_c,_id,_pr,_limit,_proof_script,callback,_ores) =
Queue.pop scheduled_proof_attempts in
callback Interrupted
done;
......@@ -494,8 +494,7 @@ let run_timeout_handler () =
S.timeout ~ms:default_delay_ms timeout_handler;
end
let schedule_proof_attempt c id pr ?save_to
~counterexmp ~limit ~callback ~notification =
let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
let ses = c.controller_session in
let callback panid s =
begin
......@@ -544,7 +543,7 @@ let schedule_proof_attempt c id pr ?save_to
with Not_found | Session_itp.BadID -> limit,None,save_to
in
let panid = graft_proof_attempt ~limit ses id pr in
Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,counterexmp,ores)
Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,ores)
scheduled_proof_attempts;
callback panid Scheduled;
run_timeout_handler ()
......@@ -619,7 +618,7 @@ let prepare_edition c ?file pn pr ~notification =
let fmt = formatter_of_out_channel ch in
let task = Session_itp.get_task session pn in
let driver = snd (Hprover.find c.controller_provers pr) in
Driver.print_task ~cntexample:false ?old driver fmt task;
Driver.print_task ?old driver fmt task;
Opt.iter close_in old;
close_out ch;
panid,file,old_res
......@@ -714,7 +713,7 @@ let schedule_transformation c id name args ~callback ~notification =
open Strategy
let run_strategy_on_goal
c id strat ~counterexmp ~callback_pa ~callback_tr ~callback ~notification =
c id strat ~callback_pa ~callback_tr ~callback ~notification =
let rec exec_strategy pc strat g =
if pc < 0 || pc >= Array.length strat then
callback STShalt
......@@ -742,7 +741,7 @@ let run_strategy_on_goal
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ?save_to:None ~counterexmp ~limit ~callback ~notification
schedule_proof_attempt c g p ?save_to:None ~limit ~callback ~notification
| Itransform(trname,pcsuccess) ->
let callback ntr =
callback_tr trname [] ntr;
......@@ -858,7 +857,7 @@ let rec copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any =
*)
| APn from_pn, APn to_pn ->
let from_pa_list = get_proof_attempts s from_pn in
List.iter (fun x -> schedule_pa_with_same_arguments ?save_to:None c x to_pn ~counterexmp:false
List.iter (fun x -> schedule_pa_with_same_arguments ?save_to:None c x to_pn
~callback:callback_pa ~notification) from_pa_list;
let from_tr_list = get_transformations s from_pn in
let callback x tr args st = callback_tr tr args st;
......@@ -955,7 +954,7 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
try
if pr' <> pr then callback id (UpgradeProver pr');
let _ = get_task c.controller_session parid in
schedule_proof_attempt ?save_to:None c parid pr' ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c parid pr' ~limit ~callback ~notification
with Not_found ->
callback id Detached
......@@ -1160,7 +1159,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
Call_provers.print_prover_result res
end
in
schedule_proof_attempt ?save_to:None c pn prover ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c pn prover ~limit ~callback ~notification
| _ -> assert false
end
in
......@@ -1240,7 +1239,7 @@ later on. We do has if proof fails. *)
in
Debug.dprintf
debug "[Bisect] running the prover on subtask@.";
schedule_proof_attempt ?save_to:None c pn prover ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c pn prover ~limit ~callback ~notification
| _ -> assert false
end
in
......
......@@ -198,7 +198,6 @@ val schedule_proof_attempt :
proofNodeID ->
Whyconf.prover ->
?save_to:string ->
counterexmp:bool ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:notifier -> unit
......@@ -252,7 +251,6 @@ val run_strategy_on_goal :
controller ->
proofNodeID ->
Strategy.t ->
counterexmp:bool ->
callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
callback_tr:(string -> string list -> transformation_status -> unit) ->
callback:(strategy_status -> unit) ->
......
......@@ -1054,12 +1054,12 @@ end
Format.eprintf "Fatal anomaly in Itp_server.notify_change_proved@.";
exit 1
let schedule_proof_attempt ~counterexmp nid (p: Whyconf.config_prover) limit =
let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
let d = get_server_data () in
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id prover ~counterexmp
List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id prover
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
......@@ -1164,7 +1164,7 @@ end
let debug_strat = Debug.register_flag "strategy_exec" ~desc:"Trace strategies execution"
let run_strategy_on_task ~counterexmp nid s =
let run_strategy_on_task nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
try
......@@ -1176,7 +1176,7 @@ end
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr tr args st = callback_update_tree_transform tr args st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~counterexmp
C.run_strategy_on_goal d.cont id st
~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
with
......@@ -1312,7 +1312,6 @@ end
let treat_request r =
let d = get_server_data () in
let config = d.cont.controller_config in
(* Check that the request does not refer to obsolete node_ids *)
if not (request_is_valid r) then
begin
......@@ -1366,11 +1365,9 @@ end
| Transform (s, _t, args) -> apply_transform nid s args
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
schedule_proof_attempt ~counterexmp nid p limit
schedule_proof_attempt nid p limit
| Strategies st ->
let counterexmp = Whyconf.cntexample (Whyconf.get_main config) in
run_strategy_on_task ~counterexmp nid st
run_strategy_on_task nid st
| Edit p -> schedule_edition nid p
| Bisect -> schedule_bisection nid
| Replay valid_only -> replay ~valid_only snid
......
......@@ -90,8 +90,6 @@ 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";
......@@ -143,9 +141,7 @@ let option_list = [
"parse_only" "--parse-only" " stop after parsing";
Debug.Args.desc_shortcut
"type_only" "--type-only" " stop after type checking";
Termcode.arg_extra_expl_prefix;
"--get-ce", Arg.Set opt_cntexmp,
" gets the counter-example model" ]
Termcode.arg_extra_expl_prefix ]
let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg
......@@ -250,14 +246,14 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
match !opt_output, !opt_command with
| None, Some command ->
let call =
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv task in
Driver.prove_task ~command ~limit drv task in
let res = Call_provers.wait_on_call call in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res;
if res.Call_provers.pr_answer <> Call_provers.Valid then unproved := true
| None, None ->
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
Driver.print_task drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
let do_tasks env drv fname tname th task =
......
......@@ -15,7 +15,7 @@ let debug = Debug.register_info_flag "prepare_for_counterexmp"
~desc:"Print@ debugging@ messages@ about@ preparing@ the@ task@ for@ getting@ counter-example."
let meta_get_counterexmp =
Theory.register_meta_excl "get_counterexmp" []
Theory.register_meta_excl "get_counterexmp" [Theory.MTstring]
~desc:"Set@ when@ counter-example@ should@ be@ get."
let get_counterexmp task =
......
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