From 2d9352c1cd8cd3f73c60d0b7c50981f9b42ceb57 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Fri, 26 Jul 2013 17:16:13 +0200 Subject: [PATCH] Do not stupidely recompute a constant set of states for each node in the tree, compute it once and for all before the run and store it at each node as we traverse them. --- src/run.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/run.ml b/src/run.ml index f6812e4..9c8203b 100644 --- a/src/run.ml +++ b/src/run.ml @@ -299,6 +299,7 @@ DEFINE AND_(t1,t2) = let cache2 = run.cache2 in let cache5 = run.cache5 in let unstable = run.unstable in + let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in let rec loop node = let node_id = T.preorder tree node in if node == T.nil || not (Bitvector.get unstable node_id) then false else begin @@ -316,9 +317,7 @@ DEFINE AND_(t1,t2) = (* first time we visit the node *) NodeStatus.make { sat = StateSet.empty; - todo = StateSet.diff - (Ata.get_states auto) - (Ata.get_starting_states auto); + todo = init_todo; summary = NodeSummary.make (node == T.first_child tree parent) (* is_left *) (node == T.next_sibling tree parent) (* is_right *) -- 2.17.1