projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
ajout d'un compteur pour compter le nombre de noeuds évalués
[tatoo.git]
/
src
/
tatoo.ml
diff --git
a/src/tatoo.ml
b/src/tatoo.ml
index
485d8e1
..
9fb7045
100644
(file)
--- a/
src/tatoo.ml
+++ b/
src/tatoo.ml
@@
-123,10
+123,10
@@
let main () =
let s = Naive.stats () in
Run.(
Logger.msg `STATS
let s = Naive.stats () in
Run.(
Logger.msg `STATS
- "@[tree size: %d@\ntraversals: %d@\n
cache2 hit ratio: %f@\ncache5
hit ratio: %f@]"
+ "@[tree size: %d@\ntraversals: %d@\n
transition fetch cache hit ratio: %f@\ntransition eval cache
hit ratio: %f@]"
s.tree_size s.run
s.tree_size s.run
- (float s.
cache2_hit /. float s.cache2
_access)
- (float s.
cache5_hit /. float s.cache5
_access));
+ (float s.
fetch_trans_cache_hit /. float s.fetch_trans_cache
_access)
+ (float s.
eval_trans_cache_hit /. float s.eval_trans_cache
_access));
time (fun () ->
let count = ref 1 in
List.iter (fun results ->
time (fun () ->
let count = ref 1 in
List.iter (fun results ->