type stats = { mutable pass : int;
tree_size : int;
mutable fetch_trans_cache_access : int;
- mutable fetch_trans_cache_hit : int;
+ mutable fetch_trans_cache_miss : int;
mutable eval_trans_cache_access : int;
- mutable eval_trans_cache_hit : int;
+ mutable eval_trans_cache_miss : int;
mutable nodes_per_run : int list;
}
((Obj.magic kind) lsl 4)
end
-let dummy_set = StateSet.singleton State.dummy
+let dummy_set = StateSet.singleton State.dummy_state
stats : stats;
}
-let dummy_form = Ata.Formula.stay State.dummy
+let dummy_form = Ata.Formula.stay State.dummy_state
-let get_form run tag q =
+let get_form run tag (q : State.t) =
let auto = run.auto in
let fetch_trans_cache = run.fetch_trans_cache in
let stats = run.stats in
if phi == dummy_form then
let phi = Ata.get_form auto tag q in
let () =
+ stats.fetch_trans_cache_miss <- stats.fetch_trans_cache_miss + 1;
Cache.N2.add
fetch_trans_cache
(tag.QName.id :> int)
(q :> int) phi
in phi
- else begin
- stats.fetch_trans_cache_hit <- stats.fetch_trans_cache_hit + 1;
+ else
phi
- end
+
let eval_form phi fcs nss ps ss summary =
let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in
stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;
- if res != dummy_set then begin
- stats.eval_trans_cache_hit <- 1 + stats.eval_trans_cache_hit;
+ if res != dummy_set then
res
- end else let new_sat =
+ else let new_sat =
eval_trans_fix run tag summary fcs nss ps ss todo
- in
- Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
- new_sat
+ in
+ stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss;
+ Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
+ new_sat
-module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
+module Make (T : Tree.S) (L : Deque.S with type elem = T.node) =
struct
let make auto tree =
{
tree = tree;
auto = auto;
- sat = (let a = Array.create len StateSet.empty in
+ sat = (let a = Array.make len StateSet.empty in
IFHTML([a], a));
pass = 0;
fetch_trans_cache = Cache.N2.create dummy_form;
pass = 0;
tree_size = len;
fetch_trans_cache_access = 0;
- fetch_trans_cache_hit = 0;
+ fetch_trans_cache_miss = 0;
eval_trans_cache_access = 0;
- eval_trans_cache_hit = 0;
+ eval_trans_cache_miss = 0;
nodes_per_run = [];
}
}