From cfef2deaf1a17df7bcb153c3b92e28e14edd912b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Fri, 26 Jul 2013 16:38:26 +0200 Subject: [PATCH] Improve performances by moving the caching outside of the saturation of the set of states of the current node (instead of caching and looking-up at each step) --- src/run.ml | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/run.ml b/src/run.ml index 726a483..f6812e4 100644 --- a/src/run.ml +++ b/src/run.ml @@ -250,7 +250,7 @@ DEFINE AND_(t1,t2) = loop phi - let eval_trans_aux auto cache2 cache4 tag fcs nss ps old_status = + let eval_trans_aux auto cache2 tag fcs nss ps old_status = let { sat = old_sat; todo = old_todo; summary = old_summary } as os_node = old_status.NodeStatus.node @@ -273,26 +273,22 @@ DEFINE AND_(t1,t2) = let eval_trans auto cache2 cache5 tag fcs nss ps ss = + let rec loop old_status = + let new_status = + eval_trans_aux auto cache2 tag fcs nss ps old_status + in + if new_status == old_status then old_status else loop new_status + in let fcsid = (fcs.NodeStatus.id :> int) in let nssid = (nss.NodeStatus.id :> int) in let psid = (ps.NodeStatus.id :> int) in + let ssid = (ss.NodeStatus.id :> int) in let tagid = (tag.QName.id :> int) in - let rec loop old_status = - let oid = (old_status.NodeStatus.id :> int) in - let res = - let res = Cache.N5.find cache5 tagid oid fcsid nssid psid in - if res != dummy_status then res - else - let new_status = - eval_trans_aux auto cache2 cache5 tag fcs nss ps old_status - in - Cache.N5.add cache5 tagid oid fcsid nssid psid new_status; - new_status - in - if res == old_status then res else loop res - in - loop ss - + let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in + if res != dummy_status then res + else let new_status = loop ss in + Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status; + new_status -- 2.17.1