Commit a229dcf0 authored by MARCHE Claude's avatar MARCHE Claude

few improvements in CE bench

* time limit set to 1 sec. Quicker, and results are the same !

* use Stdlib whenever possible

* FIXME: the use of StringMap.bindings should not be useful, and wastes time and memory
parent 9ac6d394
......@@ -16,7 +16,7 @@ cd $dir
run_cvc4_15 () {
echo -n " $1... "
../bin/why3prove.opt -P "CVC4,1.5-prerelease" --timelimit 5 --get-ce $1 | \
../bin/why3prove.opt -P "CVC4,1.5-prerelease" --timelimit 1 --get-ce $1 | \
# 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)//' > $1.out
......
......@@ -237,8 +237,8 @@ let print_location fmt m_element =
** Model definitions
***************************************************************
*)
module IntMap = Map.Make(struct type t = int let compare = compare end)
module StringMap = Map.Make(String)
module IntMap = Stdlib.Mint
module StringMap = Stdlib.Mstr
type model_file = model_element list IntMap.t
type model_files = model_file StringMap.t
......@@ -278,10 +278,9 @@ let print_model_elements ?(sep = "\n") me_name_trans fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element me_name_trans) fmt m_elements
let print_model_file fmt me_name_trans filename model_file =
(* Relativize does not work on nighly bench: using path_of_file instead. It
(* Relativize does not work on nighly bench: using basename instead. It
hides the local paths. *)
let path = Sysutil.path_of_file filename in
let filename = List.hd (List.rev path) in
let filename = Filename.basename filename in
fprintf fmt "File %s:" filename;
IntMap.iter
(fun line m_elements ->
......@@ -300,7 +299,9 @@ let print_model
?(me_name_trans = why_name_trans)
fmt
model =
(* Simple and easy way to print file sorted alphabetically *)
(* Simple and easy way to print file sorted alphabetically
FIXME: but StringMap.iter is supposed to iter in alphabetic order, so waste of time and memory here !
*)
let l = StringMap.bindings model.model_files in
List.iter (fun (k, e) -> print_model_file fmt me_name_trans k e) l
......
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