From a96c64d15866719b4c8eb6d98ad7f1fc948e7636 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 12 Apr 2017 08:51:31 +0200 Subject: [PATCH] Add a generic deque module. --- src/deque.ml | 114 ++++++++++++++++++++++++++++++++ src/{node_list.ml => deque.mli} | 14 ++-- src/naive_node_list.ml | 74 +-------------------- src/naive_node_list.mli | 2 +- src/run.ml | 28 ++++---- src/run.mli | 6 +- src/tatoo.ml | 6 +- 7 files changed, 144 insertions(+), 100 deletions(-) create mode 100644 src/deque.ml rename src/{node_list.ml => deque.mli} (83%) diff --git a/src/deque.ml b/src/deque.ml new file mode 100644 index 0000000..64e7188 --- /dev/null +++ b/src/deque.ml @@ -0,0 +1,114 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + + +module type S = + sig + type elem + type t + type iterator + + val create : unit -> t + val add : elem -> t -> unit + val push_front : elem -> t -> unit + val push_back : elem -> t -> unit + val iter : (elem -> unit) -> t -> unit + val length : t -> int + val is_empty : t -> bool + val head : t -> iterator + val last : t -> iterator + val next : iterator -> iterator + val value : iterator -> elem + val finished : iterator -> bool + val copy : t -> t + end + +module Make (E : sig type t end) = +struct + + + type elem = E.t + type cell = { node : elem; + mutable next : cell } + + type iterator = cell + + type t = { mutable length : int; + mutable head : cell; + mutable last : cell; } + + let rec nil = { node = Obj.magic (); + next = nil } + + let create () = { length = 0; + head = nil; + last = nil } + + let iter f l = + let rec loop c = + if c != nil then begin + f c.node; + loop c.next + end + in + loop l.head + + + let length l = l.length + let is_empty l = l.head == nil + + let add n l = + let ncell = { node = n; + next = nil } + in + if l.head == nil then begin + l.head <- ncell; + l.last <- ncell; + l.length <- 1 + end else begin + l.last.next <- ncell; + l.last <- ncell; + l.length <- l.length + 1 + end + + let push_back n l = add n l + let push_front n l = + let ncell = { node = n; + next = l.head } + in + if l.head == nil then begin + l.head <- ncell; + l.last <- ncell; + l.length <- 1; + end else begin + l.head <- ncell; + l.length <- l.length + 1; + end + + let head l = l.head + let last l = l.last + let next i = i.next + let value i = i.node + let finished i = i == nil + + let copy l = + let rec loop l2 i = + if finished i then l2 else begin + add (value i) l2; + loop l2 (next i) + end + in + loop (create ()) (head l) +end diff --git a/src/node_list.ml b/src/deque.mli similarity index 83% rename from src/node_list.ml rename to src/deque.mli index e9bb58a..fecf60c 100644 --- a/src/node_list.ml +++ b/src/deque.mli @@ -15,21 +15,23 @@ module type S = sig - type node + type elem type t type iterator val create : unit -> t - val add : node -> t -> unit - val push_front : node -> t -> unit - val push_back : node -> t -> unit - val iter : (node -> unit) -> t -> unit + val add : elem -> t -> unit + val push_front : elem -> t -> unit + val push_back : elem -> t -> unit + val iter : (elem -> unit) -> t -> unit val length : t -> int val is_empty : t -> bool val head : t -> iterator val last : t -> iterator val next : iterator -> iterator - val value : iterator -> node + val value : iterator -> elem val finished : iterator -> bool val copy : t -> t end + +module Make (E : sig type t end) : S with type elem = E.t diff --git a/src/naive_node_list.ml b/src/naive_node_list.ml index b6f0ae4..91d07e0 100644 --- a/src/naive_node_list.ml +++ b/src/naive_node_list.ml @@ -13,76 +13,4 @@ (* *) (***********************************************************************) - -type node = Naive_tree.node -type cell = { node : node; - mutable next : cell } - -type iterator = cell - -type t = { mutable length : int; - mutable head : cell; - mutable last : cell; } - -let rec nil = { node = Naive_tree.nil; - next = nil } - -let create () = { length = 0; - head = nil; - last = nil } - -let iter f l = - let rec loop c = - if c != nil then begin - f c.node; - loop c.next - end - in - loop l.head - - -let length l = l.length -let is_empty l = l.head == nil - -let add n l = - let ncell = { node = n; - next = nil } - in - if l.head == nil then begin - l.head <- ncell; - l.last <- ncell; - l.length <- 1 - end else begin - l.last.next <- ncell; - l.last <- ncell; - l.length <- l.length + 1 - end - -let push_back n l = add n l -let push_front n l = - let ncell = { node = n; - next = l.head } - in - if l.head == nil then begin - l.head <- ncell; - l.last <- ncell; - l.length <- 1; - end else begin - l.head <- ncell; - l.length <- l.length + 1; - end - -let head l = l.head -let last l = l.last -let next i = i.next -let value i = i.node -let finished i = i == nil - -let copy l = - let rec loop l2 i = - if finished i then l2 else begin - add (value i) l2; - loop l2 (next i) - end - in - loop (create ()) (head l) +include Deque.Make (struct type t = Naive_tree.node end) diff --git a/src/naive_node_list.mli b/src/naive_node_list.mli index e1fde9c..010acd8 100644 --- a/src/naive_node_list.mli +++ b/src/naive_node_list.mli @@ -14,4 +14,4 @@ (***********************************************************************) -include Node_list.S with type node = Naive_tree.node +include Deque.S with type elem = Naive_tree.node diff --git a/src/run.ml b/src/run.ml index 0ae25f9..887eb35 100644 --- a/src/run.ml +++ b/src/run.ml @@ -23,9 +23,9 @@ open Bigarray 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; } @@ -120,15 +120,15 @@ let get_form run tag (q : State.t) = 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 = @@ -191,17 +191,17 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo = 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 = @@ -222,9 +222,9 @@ struct 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 = []; } } diff --git a/src/run.mli b/src/run.mli index c942277..705b44f 100644 --- a/src/run.mli +++ b/src/run.mli @@ -17,13 +17,13 @@ type stats = private { 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; } -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) : sig val eval : Ata.t -> T.t -> L.t -> L.t val full_eval : Ata.t -> T.t -> L.t -> (State.t * L.t) list diff --git a/src/tatoo.ml b/src/tatoo.ml index e0f29ee..20bc903 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -124,10 +124,10 @@ let main () = let s = Naive.stats () in Run.( Logger.msg `STATS - "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache hit ratio: %f@\ntransition eval cache hit ratio: %f@\nNumber of visited nodes per pass: %a@]" + "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache miss ratio: %f@\ntransition eval cache miss ratio: %f@\nNumber of visited nodes per pass: %a@]" s.tree_size s.pass - (float s.fetch_trans_cache_hit /. float s.fetch_trans_cache_access) - (float s.eval_trans_cache_hit /. float s.eval_trans_cache_access) + (float s.fetch_trans_cache_miss /. float s.fetch_trans_cache_access) + (float s.eval_trans_cache_miss /. float s.eval_trans_cache_access) (let i = ref 0 in Pretty.print_list ~sep:"," (fun fmt n -> Format.fprintf fmt "%i: %i" !i n;incr i)) s.nodes_per_run); -- 2.17.1