Commit 093df864 authored by Tuyen Nguyen's avatar Tuyen Nguyen
parents 199df4f4 1a5a0226
......@@ -131,7 +131,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eval_match instantiate_predicate
eval_match instantiate_predicate smoke_detector
LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 \
coq tptp simplify gappa cvc3 yices
......
......@@ -487,9 +487,12 @@ not and you have to use the IDE to update it.
\begin{itemize}
\item The exit code is 0 if no difference was detected, 1 if there
was. Other exit codes mean some failure in running the replay.
\item option \texttt{-s}: suppresses the output of the final tree view
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath
\item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.
\item option \texttt{-s}: suppresses the output of the final tree view.
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath.
\item option \texttt{-force}: force writing a new session file even if
some proofs did not replay correctly.
\item option \texttt{-smoke-detector \{none|top|deep\}} try to detect
if the context is self-contradicting.
\item option \texttt{-latex \textsl{<dir>}}: produce a summary of
the replay under the form of a tabular environment in LaTeX, one
tabular for each theory, one per file, in directory \texttt{\textsl{<dir>}}.
......@@ -499,6 +502,46 @@ not and you have to use the IDE to update it.
% the replay in HTML syntax.
\end{itemize}
\paragraph{Smoke Detector}
The smoke detector try to detect if the context is self-contradicting
and, thus, that anything can be proved in this context. The smoke
detector can't be run on outdated session and doesn't modify the session.
It has three possible configurations :
\begin{itemize}
\item \texttt{none} : don't run the smoke detector
\item \texttt{top} : The negation of each proved goals
tries to be proved with the same timeout and the same prover which
prove the goal.
\begin{verbatim}
[ ... ]
Goal G : forall x:int. q x -> (p1 x \/ p2 x)
\end{verbatim}
becomes
\begin{verbatim}
[ ... ]
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
\end{verbatim}
\item \texttt{deep} : The same technique as \texttt{top} but the
negation is pushed under the universal quantification (without
changing them) and under the implication. The previous example becomes
\begin{verbatim}
[ ... ]
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
\end{verbatim}
\end{itemize}
The name of the goals which triggered the smoke detector are printed :
\begin{verbatim}
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
\end{verbatim}
Moreover \texttt{Smoke detected} (exit code 1) is printed at the end if the smoke
detector has been trigged, or \texttt{No smoke detected} (exit code 0)
otherwise.
\paragraph{Customizing LaTeX output}
The generated LaTeX files contain some macros that must be defined
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="programs/fact/why3session.xml">
name="examples/programs/fact/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -9,43 +9,19 @@
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
version="8.2pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
name="Z3 smtv1"
version="2.2"/>
<file
name="../fact.mlw"
verified="true"
......
......@@ -123,12 +123,41 @@ version_regexp = "Version: \\([^ \n\r]+\\)"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/verit.drv"
[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "3.2"
version_old = "3.1"
version_old = "3.0"
version_bad = "2.19"
version_bad = "2.18"
version_bad = "2.17"
version_bad = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smtc \
-rs:42 \
PHASE_SELECTION=0 \
RESTART_STRATEGY=0 \
RESTART_FACTOR=1.5 \
QI_EAGER_THRESHOLD=100 \
ARITH_RANDOM_INITIAL_VALUE=true \
CASE_SPLIT=3 \
DELAY_UNITS=true \
DELAY_UNITS_THRESHOLD=16 \
%f"
[ATP z3]
name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.19"
version_old = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
......
......@@ -155,14 +155,6 @@ let load_config config =
env = env
}
let read_config () =
try
let config = Whyconf.read_config None in
load_config config
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "@.%a@." Exn_printer.exn_printer e;
exit 1
let save_config t =
let _save_prover _ pr acc =
Mstr.add pr.Session.prover_id
......@@ -200,15 +192,29 @@ let save_config t =
*)
save_config config
let config =
eprintf "[Info] reading IDE config file...@?";
let c = read_config () in
eprintf " done.@.";
c
let read_config conf_file =
try
let config = Whyconf.read_config conf_file in
load_config config
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "@.%a@." Exn_printer.exn_printer e;
exit 1
let config,read_config =
let config = ref None in
(fun () ->
match !config with
| None -> invalid_arg "configuration not yet loaded"
| Some conf -> conf),
(fun conf_file ->
eprintf "[Info] reading IDE config file...@?";
let c = read_config conf_file in
eprintf " done.@.";
config := Some c)
let save_config () = save_config config
let save_config () = save_config (config ())
let get_main () = (get_main config.config)
let get_main () = (get_main (config ()).config)
(*
......@@ -254,7 +260,7 @@ let iconname_reload = "movefile32"
let iconname_remove = "deletefile32"
let iconname_cleaning = "trashb32"
let image_default = ref (image ~size:20 iconname_default)
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ()) (** dumb pixbuf *)
let image_undone = ref !image_default
let image_scheduled = ref !image_default
let image_running = ref !image_default
......@@ -312,7 +318,7 @@ let resize_images size =
image_cleaning := image ~size iconname_cleaning;
()
let () =
let init () =
eprintf "[Info] reading icons...@?";
why_icon := image "logo-why";
resize_images 20;
......@@ -563,12 +569,15 @@ let run_auto_detection gconfig =
gconfig.config <- config;
let _provers = get_provers config in
(* TODO: store the result differently
gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers Mstr.empty
gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers
Mstr.empty
*)
()
*)
let () = eprintf "[Info] end of configuration initialization@."
(* let () = eprintf "[Info] end of configuration initialization@." *)
let read_config conf_file = read_config conf_file; init ()
(*
Local Variables:
......
......@@ -40,9 +40,14 @@ type t =
mutable config : Whyconf.config;
}
val read_config : string option -> unit
(** None use the default config *)
val save_config : unit -> unit
val config : t
val config : unit -> t
(** [config ()] raise [invalid_arg "configuration not yet loaded"]
if load_config is not called *)
val get_main : unit -> Whyconf.main
......
......@@ -37,11 +37,22 @@ open Gconfig
let includes = ref []
let file = ref None
let opt_version = ref false
let opt_config = ref None
let spec = Arg.align [
("-I",
("-L",
Arg.String (fun s -> includes := s :: !includes),
"<s> add s to loadpath") ;
("--library",
Arg.String (fun s -> includes := s :: !includes),
" same as -L") ;
("-I",
Arg.String (fun s -> includes := s :: !includes),
" same as -L (obsolete)") ;
"-C", Arg.String (fun s -> opt_config := Some s),
"<file> Read configuration from <file>";
"--config", Arg.String (fun s -> opt_config := Some s),
" same as -C";
(*
("-f",
Arg.String (fun s -> input_files := s :: !input_files),
......@@ -73,6 +84,8 @@ let () =
exit 0
end
let () = Gconfig.read_config !opt_config
let fname = match !file with
| None ->
Arg.usage spec usage_str;
......@@ -114,7 +127,7 @@ let source_text fname =
(********************************)
let gconfig =
let c = Gconfig.config in
let c = Gconfig.config () in
let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
c.env <- Env.create_env loadpath;
(*
......@@ -825,7 +838,7 @@ let exit_function ?(destroy=false) () =
let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
if ret = 0 then eprintf "DTD validation succeeded, good!@.";
*)
match config.saving_policy with
match (Gconfig.config ()).saving_policy with
| 0 -> save_session (); GMain.quit ()
| 1 -> GMain.quit ()
| 2 ->
......@@ -1530,7 +1543,7 @@ let select_row r =
let a = get_any_from_row_reference r in
match a with
| M.Goal g ->
if config.intro_premises then
if (Gconfig.config ()).intro_premises then
let callback = function
| [t] -> display_task g t
| _ -> assert false
......
......@@ -27,8 +27,16 @@ let opt_version = ref false
let opt_stats = ref true
let opt_latex = ref ""
let opt_latex2 = ref ""
let opt_longtable = ref false
let opt_html = ref ""
let opt_force = ref false
let opt_smoke = ref Session.SD_None
let set_opt_smoke = function
| "none" -> opt_smoke := Session.SD_None
| "top" -> opt_smoke := Session.SD_Top
| "deep" -> opt_smoke := Session.SD_Deep
| _ -> assert false
let spec = Arg.align [
("-I",
......@@ -37,6 +45,9 @@ let spec = Arg.align [
("-force",
Arg.Set opt_force,
" enforce saving of session even if replay failed") ;
("-smoke-detector",
Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
" try to detect if the context is self-contradicting") ;
("-s",
Arg.Clear opt_stats,
" do not print statistics") ;
......@@ -49,6 +60,9 @@ let spec = Arg.align [
("-latex2",
Arg.Set_string opt_latex2,
" [Dir_output] produce latex statistics") ;
("-longtable",
Arg.Set opt_longtable,
" produce latex statistics using longtable package") ;
("-html",
Arg.Set_string opt_html,
" [Dir_output] produce html statistics") ;
......@@ -75,6 +89,12 @@ let () =
exit 0
end
let () =
if !opt_smoke <> Session.SD_None && !opt_force then begin
Format.printf "You can't force when detecting smoke@.";
exit 1
end
let fname = match !file with
| None ->
Arg.usage spec usage_str;
......@@ -290,25 +310,22 @@ let file_statistics (files,n,m) f =
((f,ths,n1,m1)::files,n+n1,m+m1)
let print_statistics files =
List.iter
(fun (f,ths,n,m) ->
if n<m then
begin
printf " +--file %s: %d/%d@." f.M.file_name n m;
List.iter
(fun (th,goals,n,m) ->
if n<m then
begin
printf " +--theory %s: %d/%d@."
(M.theory_name th) n m;
List.iter
(fun g ->
printf " +--goal %s not proved@." (M.goal_name g))
(List.rev goals)
end)
(List.rev ths)
end)
(List.rev files)
let print_goal g =
printf " +--goal %s not proved@." (M.goal_name g)
in
let print_theory (th,goals,n,m) =
if n<m then begin
printf " +--theory %s: %d/%d@." (M.theory_name th) n m;
List.iter print_goal (List.rev goals)
end
in
let print_file (f,ths,n,m) =
if n<m then begin
printf " +--file %s: %d/%d@." f.M.file_name n m;
List.iter print_theory (List.rev ths)
end
in
List.iter print_file (List.rev files)
(* Statistics in LaTeX*)
......@@ -316,7 +333,8 @@ let rec transf_depth tr =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (tr.M.subgoals)
and goal_depth g =
Hashtbl.fold
(fun _st tr depth -> max depth (1 + transf_depth tr)) (M.transformations g) 0
(fun _st tr depth -> max depth (1 + transf_depth tr))
(M.transformations g) 0
let theory_depth t =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (M.goals t)
......@@ -331,7 +349,8 @@ let rec provers_latex_stats provers g =
let prover_name a =
match a with
M.Detected_prover d -> d.Session.prover_name ^ " " ^ d.Session.prover_version
M.Detected_prover d ->
d.Session.prover_name ^ " " ^ d.Session.prover_version
| M.Undetected_prover s -> s
let protect s =
......@@ -343,172 +362,234 @@ let protect s =
done;
Buffer.contents b
let rec goal_latex_stat n fmt prov depth depth_max column subgoal g =
let column n depth provers =
if n == 1 then
begin
if depth > 0 then
if subgoal > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
else ()
else
fprintf fmt "\\hline @.";
end
if depth > 1 then
(List.length provers) + depth
else
(List.length provers) + depth + 1
else
begin
if depth > 0 then
fprintf fmt "\\cline{%d-%d} @." 2 column
else
fprintf fmt "\\hline @."
end;
if(n ==1) then
begin
if depth_max > 1 then
begin
if subgoal > 0 then
(List.length provers) + 1
let print_result_prov proofs prov fmt=
List.iter (fun (p, _pr) ->
try
let pr = Hashtbl.find proofs p in
let s = pr.M.proof_state in
match s with
Session.Done res ->
begin
if(depth < depth_max) then
for i = 1 to depth do fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "done
else
for i = 1 to depth - 1 do fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
match res.Call_provers.pr_answer with
Call_provers.Valid ->
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid -> fprintf fmt "& \\invalid "
| Call_provers.Timeout -> fprintf fmt "& \\timeout "
| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
else
if(depth < depth_max) then
if depth > 0 then fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end
else
begin
if subgoal > 0 then
for i = 1 to depth do fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else
if depth > 0 then fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end
end
else
for i = 1 to depth do fprintf fmt "\\quad" done;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
else
if n == 2 then
fprintf fmt "\\explanation{%d} " (subgoal + 1)
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
let column = column 1 depth prov
in
if depth > 0 then
if subgoal > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
else ()
else
fprintf fmt "\\hline @.";
if depth_max > 1 then
begin
if subgoal > 0 then
begin
if(depth < depth_max) then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
else
for i = 1 to depth - 1 do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
end
else
if(depth < depth_max) then
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end
else
begin
if subgoal > 0 then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
else
fprintf fmt "\\explanation{%s}" " ";
let proofs = M.external_proofs g in
if (Hashtbl.length proofs) > 0 then
begin
if (n == 1) then
let proofs = M.external_proofs g in
if (Hashtbl.length proofs) > 0 then
begin
if depth_max <= 1 then
begin
if depth > 0 then
for i = depth to (depth_max - depth) do fprintf fmt "& \\explanation{%s}" " " done
for i = depth to (depth_max - depth) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 1) do fprintf fmt "& \\explanation{%s}" " " done
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
end
else
if depth > 0 then
for i = depth to (depth_max - depth - 1) do fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 2) do fprintf fmt "& \\explanation{%s}" " " done
if depth > 0 then
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 2) do
fprintf fmt "& \\explanation{%s}" " " done;
print_result_prov proofs prov fmt;
end;
List.iter (fun (p, _pr) ->
try
let pr = Hashtbl.find proofs p in
let s = pr.M.proof_state in
match s with
Session.Done res ->
begin
match res.Call_provers.pr_answer with
Call_provers.Valid -> fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid -> fprintf fmt "& \\invalid "
| Call_provers.Timeout -> fprintf fmt "& \\timeout "
| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
end;
let tr = M.transformations g in
if Hashtbl.length tr > 0 then
if n == 2 then
begin
if (Hashtbl.length proofs == 0) then
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov)
end
let tr = M.transformations g in
if Hashtbl.length tr > 0 then
if Hashtbl.length proofs > 0 then