projects
/
tatoo.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c300293
)
Implement subtree-skipping optimisation (a one liner, really ~_~) that skips a whole...
author
Kim Nguyễn
<kn@lri.fr>
Sat, 11 Jan 2014 17:22:16 +0000
(18:22 +0100)
committer
Kim Nguyễn
<kn@lri.fr>
Sat, 11 Jan 2014 17:22:16 +0000
(18:22 +0100)
src/run.ml
patch
|
blob
|
history
diff --git
a/src/run.ml
b/src/run.ml
index
f9222f1
..
53f48c3
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-153,8
+153,8
@@
END
match m with
`First_child -> fcs
| `Next_sibling -> nss
match m with
`First_child -> fcs
| `Next_sibling -> nss
- | `Parent | `Previous_sibling ->
ps
- | `Stay ->
ss
+ | `Parent | `Previous_sibling -> ps
+ | `Stay -> ss
)
| Is_first_child -> b == is_left summary
| Is_next_sibling -> b == is_right summary
)
| Is_first_child -> b == is_left summary
| Is_next_sibling -> b == is_right summary
@@
-238,6
+238,7
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
let rec loop_td_and_bu node parent parent_sat =
if node == T.nil then StateSet.empty
else begin
let rec loop_td_and_bu node parent parent_sat =
if node == T.nil then StateSet.empty
else begin
+ let tag = T.tag tree node in
let node_id = T.preorder tree node in
let fc = T.first_child tree node in
let ns = T.next_sibling tree node in
let node_id = T.preorder tree node in
let fc = T.first_child tree node in
let ns = T.next_sibling tree node in
@@
-247,8
+248,8
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
if s != 0 then s else
let s =
NodeSummary.make
if s != 0 then s else
let s =
NodeSummary.make
- (node
_id == T.preorder tree
(T.first_child tree parent)) (*is_left *)
- (node
_id == T.preorder tree
(T.next_sibling tree parent))(*is_right *)
+ (node
==
(T.first_child tree parent)) (*is_left *)
+ (node
==
(T.next_sibling tree parent))(*is_right *)
(fc != T.nil) (* has_left *)
(ns != T.nil) (* has_right *)
(T.kind tree node) (* kind *)
(fc != T.nil) (* has_left *)
(ns != T.nil) (* has_right *)
(T.kind tree node) (* kind *)
@@
-258,7
+259,6
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
let status0 = unsafe_get run.sat node_id in
(* get the node_statuses for the first child, next sibling and parent *)
(* evaluate the transitions with all this statuses *)
let status0 = unsafe_get run.sat node_id in
(* get the node_statuses for the first child, next sibling and parent *)
(* evaluate the transitions with all this statuses *)
- let tag = T.tag tree node in
let status1 =
eval_trans
auto run.fetch_trans_cache run.td_cache tag
let status1 =
eval_trans
auto run.fetch_trans_cache run.td_cache tag
@@
-268,9
+268,10
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
parent_sat
status0 td_todo
in
parent_sat
status0 td_todo
in
-
- (* update the cache if the status of the node changed
- unsafe_set run.sat node_id status1 status0;*)
+ if status1 == StateSet.empty && status0 != StateSet.empty
+ then StateSet.empty else
+ (* update the cache if the status of the node changed
+ unsafe_set run.sat node_id status1 status0;*)
if bu_todo == StateSet.empty then begin
unsafe_set run.sat node_id status1 status0; (* write the td_states *)
update_res false status1 node;
if bu_todo == StateSet.empty then begin
unsafe_set run.sat node_id status1 status0; (* write the td_states *)
update_res false status1 node;
@@
-295,7
+296,7
@@
module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
status1 bu_todo
in
unsafe_set run.sat node_id status2 status0;
status1 bu_todo
in
unsafe_set run.sat node_id status2 status0;
- if last_run then update_res true status2 node;
+ if last_run
&& status2 != StateSet.empty
then update_res true status2 node;
status2
end
in
status2
end
in