Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
30f16670
Commit
30f16670
authored
Jan 25, 2011
by
François Bobot
Browse files
Bench : add needed information in csv file
parent
2c5c9982
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/bench/bench.ml
View file @
30f16670
...
...
@@ -353,7 +353,7 @@ answer output time
let
transpose_sorted
=
function
|
[]
->
[]
|
(
_
,
lres
)
::_
as
l
->
let
lref
=
List
.
map
(
fun
r
->
r
.
prob
,
ref
[]
)
lres
in
let
lref
=
List
.
map
(
fun
r
->
(
r
.
prob
,
r
.
task
,
r
.
idtask
)
,
ref
[]
)
lres
in
let
l
=
List
.
rev
l
in
let
add
(
_
,
lr
)
res
=
lr
:=
res
::
!
lr
in
List
.
iter
(
fun
(
_
,
lres
)
->
List
.
iter2
add
lref
lres
)
l
;
...
...
@@ -380,8 +380,12 @@ answer output time
r
.
pr_time
|
InternalFailure
_
->
fprintf
fmt
"InternalFailure,
\"\"
"
in
let
print_line
fmt
(
b
,
l
)
=
fprintf
fmt
"%a ,"
print_prob
b
;
let
print_line
fmt
((
b
,
t
,
id
)
,
l
)
=
(* No printer for task since we want the same name evenif its
the same file with different environnement (loaded two times) *)
fprintf
fmt
"%a|%s|%i ,"
print_prob
b
(
Task
.
task_goal
t
)
.
Decl
.
pr_name
.
Ident
.
id_string
id
;
Pp
.
print_list
Pp
.
comma
print_cell
fmt
l
in
Pp
.
print_list
print_newline
print_line
fmt
l
...
...
src/bench/whybench.ml
View file @
30f16670
...
...
@@ -380,18 +380,20 @@ let () =
let
nb_scheduled
=
ref
0
in
let
nb_done
=
ref
0
in
let
nb_valid
=
ref
0
in
let
nb_failure
=
ref
0
in
let
callback
(
_
,
tool
)
(
_
,
file
,
prob
)
task
i
res
=
if
not
!
opt_quiet
then
begin
match
res
with
begin
begin
match
res
with
|
Scheduler
.
Scheduled
->
incr
nb_scheduled
|
Scheduler
.
Done
{
Call_provers
.
pr_answer
=
ans
}
->
incr
nb_done
;
begin
match
ans
with
|
Call_provers
.
Valid
->
incr
nb_valid
|
_
->
()
end
|
_
->
()
;
Format
.
printf
"%a(%i/%i) valid : %i%!"
Pp
.
Ansi
.
set_column
0
!
nb_done
!
nb_scheduled
!
nb_valid
|
Scheduler
.
InternalFailure
_
->
incr
nb_done
;
incr
nb_failure
|
Scheduler
.
Running
_
->
()
end
;
Format
.
printf
"%a(%i/%i) valid : %i failure : %i%!"
Pp
.
Ansi
.
set_column
0
!
nb_done
!
nb_scheduled
!
nb_valid
!
nb_failure
end
;
Debug
.
dprintf
debug
"%s.%s %a %i with %s : %a@."
file
prob
Pretty
.
print_pr
(
task_goal
task
)
i
tool
...
...
@@ -408,6 +410,6 @@ let () =
(*
Local Variables:
compile-command: "unset LANG; make -j -C ../.. bin/whybench.byte"
compile-command: "unset LANG; make -j -C ../.. bin/why
3
bench.byte"
End:
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment