projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Split the formula cache into a top-down and bottom-up cache.
[tatoo.git]
/
src
/
tatoo.ml
diff --git
a/src/tatoo.ml
b/src/tatoo.ml
index
485d8e1
..
6464cb4
100644
(file)
--- a/
src/tatoo.ml
+++ b/
src/tatoo.ml
@@
-15,6
+15,8
@@
open Format
open Format
+
+
let time f arg msg =
let t1 = Unix.gettimeofday () in
let r = f arg in
let time f arg msg =
let t1 = Unix.gettimeofday () in
let r = f arg in
@@
-123,10
+125,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 ->