Commit 2484e7b9 authored by MARCHE Claude's avatar MARCHE Claude

improved interaction with external provers

parent fd402ea5
......@@ -19,7 +19,8 @@ transformations
"eliminate_algebraic"
"eliminate_let"
"inline_trivial"
"split_goal_pos_neg_goal" (*"split_goal_pos_neg_all"*)
(* "split_goal_pos_neg_goal"*)
(*"split_goal_pos_neg_all"*)
end
......
......@@ -2,6 +2,10 @@
printer "coq"
filename "%f_%t_%g.v"
valid "Success"
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
prelude "(* generated by Why3's Coq driver *)"
theory BuiltIn
......
(* Why driver for SMT syntax *)
prelude "(* this is a prelude for smtlib*)"
prelude ";;; this is a prelude for Z3"
printer "smtv1"
filename "%f-%t-%g.smt"
......@@ -32,7 +32,7 @@ end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
prelude ";;; this is a prelude for Z3, Arithmetic"
syntax logic zero "0"
......
......@@ -40,14 +40,14 @@ let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
| Timeout -> fprintf fmt "Timeout"
| Unknown s -> pp_print_string fmt s
| Failure s -> pp_print_string fmt s
| Unknown s -> fprintf fmt "Unknown: %s" s
| Failure s -> fprintf fmt "Failure: %s" s
| HighFailure -> fprintf fmt "HighFailure"
let print_prover_result fmt pr =
fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time;
if pr.pr_answer == HighFailure then
fprintf fmt "@\n@stdout-stderr:@\n%s@." pr.pr_output
fprintf fmt "@\nstdout-stderr:@\n%s@." pr.pr_output
let rec grep out l = match l with
| [] -> HighFailure
......@@ -72,13 +72,16 @@ let call_prover debug command regexps opt_cout buffer =
if debug then Format.eprintf "Call_provers: Command output:@\n%s@." out;
let ans = match ret with
| Unix.WSTOPPED n ->
if debug then Format.eprintf "Call_provers: stopped on signal %d" n;
if debug then Format.eprintf "Call_provers: stopped on signal %d@." n;
HighFailure
| Unix.WSIGNALED 24 (* SIGXCPU signal cf. /usr/include/bits/signum.h *) ->
if debug then Format.eprintf "Call_provers: killed by signal SIGXCPU@.";
Timeout
| Unix.WSIGNALED n ->
if debug then Format.eprintf "Call_provers: killed by signal %d" n;
if debug then Format.eprintf "Call_provers: killed by signal %d@." n;
HighFailure
| Unix.WEXITED n ->
if debug then Format.eprintf "Call_provers: exited with status %d" n;
if debug then Format.eprintf "Call_provers: exited with status %d@." n;
grep out regexps
in
{ pr_answer = ans;
......
......@@ -111,6 +111,7 @@ type proof_attempt_status =
type prover_data =
{ prover_name : string;
command : string;
driver : Why.Driver.driver;
}
......@@ -1176,6 +1177,7 @@ let root_goals () =
(*
let string_from_result = function
| Why.Driver.Valid -> "Valid"
| Why.Driver.Invalid -> "Invalid"
......@@ -1183,6 +1185,7 @@ let string_from_result = function
| Why.Driver.Failure s -> "Failure " ^ s
| Why.Driver.Timeout -> "Timeout"
| Why.Driver.HighFailure -> "HighFailure"
*)
exception AlreadyAttempted
......@@ -1194,15 +1197,31 @@ let try_prover ~timelimit ?memlimit (g : goal) (d: prover_data) : unit -> unit =
match memlimit with None -> ()
| Some _ -> Format.eprintf "Db.try_prover warning: memlimit is ignored@."
end;
Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
let [task] = Why.Driver.apply_transforms d.driver g.task in
Format.eprintf "Task for prover: %a@." (Why.Driver.print_task d.driver) task;
(*
let callback = Why.Driver.call_prover_ext ~debug:true ~timeout:timelimit d.driver g.task
in
*)
let callback =
let dest =
Why.Driver.file_of_task d.driver "" "" task
in
let print_task fmt =
Format.fprintf fmt "@[%a@]@?" (Why.Driver.print_task d.driver) task
in
let regexps = Why.Driver.get_regexps d.driver in
Why.Call_provers.call_on_formatter ~debug:true ~suffix:dest
~command:d.command ~timelimit ~memlimit:0 ~regexps print_task
in
fun () ->
let r = callback () in
Format.eprintf "prover returned %s in %f seconds@."
(string_from_result r.Why.Call_provers.pr_answer)
r.Why.Call_provers.pr_time;
Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
(*
Format.eprintf "stdout: %s@." r.Why.Call_provers.pr_stdout;
Format.eprintf "stderr: %s@." r.Why.Call_provers.pr_stderr;
*)
(* TODO : update attempt depending on r = Valid *)
()
......
......@@ -64,6 +64,7 @@ type proof_attempt_status =
type prover_data =
{ prover_name : string;
command : string;
driver : Why.Driver.driver;
}
......
......@@ -71,6 +71,7 @@ let provers_data =
let name = conf.Whyconf.name in
printf " %s, " name;
{ Db.prover_name = name;
Db.command = conf.Whyconf.command;
Db.driver = get_driver id; } :: acc
) config.provers []
in
......
......@@ -148,6 +148,8 @@ let rec print_fmla drv fmt f = match f.f_node with
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
and print_triggers drv fmt tl =
let tl = List.map (List.filter (function Term _ -> true | Fmla _ -> false)) tl in
let tl = List.filter (function [] -> false | _::_ -> true) tl in
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma (print_expr drv))) tl
......
......@@ -319,7 +319,7 @@ let print_pkind fmt = function
let print_proof fmt = function
| Paxiom -> ()
| Plemma | Pgoal -> fprintf fmt "Admitted.@\n"
| Plemma | Pgoal -> fprintf fmt "Qed.@\n"
let print_decl drv fmt d = match d.d_node with
| Dtype tl -> print_list nothing (print_type_decl drv) fmt tl
......
......@@ -9,7 +9,7 @@ driver = "drivers/alt_ergo.drv"
[prover coq]
name = "Coq"
command = "coqc %f"
command = "coqc %f && echo Success"
driver = "drivers/coq.drv"
[prover cvc3]
......@@ -18,7 +18,7 @@ command = "cvc3 -lang smt"
driver = "drivers/cvc3.drv"
[prover z3]
name = "Z3"
command = "z3 -smt -in"
name = "Z3 en mieux"
command = "why-cpulimit %t z3 -smt %f"
driver = "drivers/z3.drv"
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