diff --git a/examples/programs/fact/why3session.xml b/examples/programs/fact/why3session.xml index 925dd7f5861e8845dc58470f214c7c6bb0e84676..a4f911819278793af958c390c4b222dc3764d5b3 100644 --- a/examples/programs/fact/why3session.xml +++ b/examples/programs/fact/why3session.xml @@ -1,7 +1,7 @@ + name="examples/programs/fact/why3session.xml"> + version="8.2pl2"/> - - - - - - + name="Z3 smtv1" + version="2.2"/> 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 - 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 + (List.length provers) + 1 + + +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}" " " " " - end - else - begin - if subgoal > 0 then - for i = 1 to depth do - fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done - else + 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 - 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) + 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 - begin - if depth_max <= 1 then - begin - if depth > 0 then - 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 - end + 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 + else + 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 - 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 + for i = depth to (depth_max - depth - 2) do + fprintf fmt "& \\explanation{%s}" " " done; + 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; - 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 + begin + if Hashtbl.length proofs > 0 then + fprintf fmt "\\cline{%d-%d} @." (depth + 2) column; + Hashtbl.iter (fun _st tr -> + let goals = tr.M.subgoals in + let _ = List.fold_left (fun subgoal g -> + goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g; + subgoal + 1) 0 goals in + () ) tr + end + else + if (Hashtbl.length proofs) = 0 then + fprintf fmt "\\\\ @." + + +let rec goal_latex2_stat fmt prov depth depth_max subgoal g = + let column = column 2 depth prov + in + if depth > 0 then + fprintf fmt "\\cline{%d-%d} @." 2 column + else + fprintf fmt "\\hline @."; + for i = 1 to depth do fprintf fmt "\\quad" done; + if (depth <= 1) then + fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g)) + else + fprintf fmt "\\explanation{%d} " (subgoal + 1); + let proofs = M.external_proofs g in + if (Hashtbl.length proofs) > 0 then + begin + 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 + begin + if (Hashtbl.length proofs == 0) then + fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov); + Hashtbl.iter (fun _st tr -> + let goals = tr.M.subgoals in + let _ = List.fold_left (fun subgoal g -> + goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g; + subgoal + 1) 0 goals in + () ) tr + end + else + if (Hashtbl.length proofs) == 0 then + fprintf fmt "\\\\ @." + + +let print_head n depth provers fmt = + if n == 1 then + if (depth > 1) then + fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } " + depth + else + fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } " + (depth + 1) else - if Hashtbl.length proofs > 0 then - fprintf fmt "\\cline{%d-%d} @." (depth + 2) column; - Hashtbl.iter (fun _st tr -> - let goals = tr.M.subgoals in - let _ = List.fold_left (fun subgoal g -> - goal_latex_stat n fmt prov (depth + 1) depth_max column (subgoal) g; - subgoal + 1) 0 goals in - () ) tr + fprintf fmt "\\hline Proof obligations "; + List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers; + fprintf fmt "\\\\ @." -let theory_latex_stat n dir t = - let provers = Hashtbl.create 9 in - List.iter (provers_latex_stats provers) (M.goals t); - let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc) - provers [] in - let provers = - List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in - let depth = theory_depth t in - let name = M.theory_name t in - let ch = open_out (Filename.concat dir(name^".tex")) in - let fmt = formatter_of_out_channel ch in - fprintf fmt "\\begin{longtable}"; +let latex_tabular n fmt depth provers t = +fprintf fmt "\\begin{tabular}"; +fprintf fmt "{| l |"; + for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done; + fprintf fmt "}@."; + print_head n depth provers fmt; + if n == 1 then + List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t) + else + List.iter (goal_latex2_stat fmt provers 0 depth 0) (M.goals t); + fprintf fmt "\\hline \\end{tabular}@." + + +let latex_longtable n fmt depth name provers t= + fprintf fmt "\\begin{longtable}"; fprintf fmt "{| l |"; for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done; fprintf fmt "}@."; - let print_head fmt = - if (n == 1) then - if (depth > 1) then - fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } " - depth - else - fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } " - (depth + 1) - else - fprintf fmt "\\hline Proof obligations "; - List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers; - fprintf fmt "\\\\ @."; - in (** First head *) - print_head fmt; + print_head n depth provers fmt; fprintf fmt "\\hline \\endfirsthead @."; (** Other heads : "Continued... " added *) fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \ \\\\ @." (List.length provers + 1) ; fprintf fmt "\\hline @."; - print_head fmt; + print_head n depth provers fmt; fprintf fmt "\\hline \\endhead @."; (** Other foots : "Continued..." added *) fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \ \\\\ @." (List.length provers); (** Last foot : nothing *) fprintf fmt "\\endfoot \\endlastfoot @."; + if n == 1 then + List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t) + else + List.iter (goal_latex2_stat fmt provers 0 depth 0) (M.goals t); + fprintf fmt "\\hline \\caption{%s statistics} @." (protect name); + fprintf fmt "\\label{%s} \\end{longtable}@." (protect name) - let column = - if n == 1 then - if depth > 1 - then - (List.length provers) + depth - else - (List.length provers) + depth + 1 + +let theory_latex_stat n table dir t = + let provers = Hashtbl.create 9 in + List.iter (provers_latex_stats provers) (M.goals t); + let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc) + provers [] in + let provers = + List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in + let depth = theory_depth t in + let name = M.theory_name t in + let ch = open_out (Filename.concat dir(name^".tex")) in + let fmt = formatter_of_out_channel ch in + if table = "tabular" then + latex_tabular n fmt depth provers t else - (List.length provers) + 1 - in - List.iter (goal_latex_stat n fmt provers 0 depth column 0) (M.goals t); - fprintf fmt "\\hline \\caption{%s statistics} @." (protect name); - fprintf fmt "\\label{%s} \\end{longtable}@." (protect name); - close_out ch + latex_longtable n fmt depth name provers t; + close_out ch -let file_latex_stat n dir f = - List.iter (theory_latex_stat n dir) f.M.theories +let file_latex_stat n table dir f = + List.iter (theory_latex_stat n table dir) f.M.theories -let print_latex_statistics n dir = +let print_latex_statistics n table dir = let files = M.get_all_files () in - List.iter (file_latex_stat n dir) files + List.iter (file_latex_stat n table dir) files let print_report (g,p,r) = printf " goal '%s', prover '%s': " g p; @@ -636,24 +691,24 @@ let () = M.maximum_running_proofs := Whyconf.running_provers_max (Whyconf.get_main config); M.smoke_detector := !opt_smoke; - eprintf " done@."; - if !opt_longtable && !opt_latex = " " && !opt_latex2 = " " then + eprintf " done."; + if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then begin - eprintf - "[Error] I can't use option longtable without latex ou latex2"; - exit 1 + eprintf + "[Error] I can't use option longtable without latex ou latex2@."; + exit 1 end; - if !opt_latex <> "" then - if !opt_longtable then - print_latex_statistics 1 !opt_latex - else - print_latex_statistics 1 !opt_latex + if !opt_latex <> "" then + if !opt_longtable then + print_latex_statistics 1 "longtable" !opt_latex + else + print_latex_statistics 1 "tabular" !opt_latex else - if !opt_latex2 <> "" then - if !opt_longtable then - print_latex_statistics 2 !opt_latex2 - else - print_latex_statistics 2 !opt_latex2 + if !opt_latex2 <> "" then + if !opt_longtable then + print_latex_statistics 2 "longtable" !opt_latex2 + else + print_latex_statistics 2 "tabular "!opt_latex2 else begin add_to_check found_obs;