--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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) : S with type elem = E.t
(* *)
(***********************************************************************)
-
-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)
(***********************************************************************)
-include Node_list.S with type node = Naive_tree.node
+include Deque.S with type elem = Naive_tree.node
+++ /dev/null
-(***********************************************************************)
-(* *)
-(* 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 node
- 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 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 finished : iterator -> bool
- val copy : t -> t
- end
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;
}
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 =
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 = [];
}
}
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
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);
projects / tatoo.git / commitdiff