Commits

Anonymous committed 64ad855

New implementation with the module Cache.

  • Participants
  • Parent commits b45b584

Comments (0)

Files changed (2)

     val log_file : string option  (** Optional filename for printing a log of internal messages. *)
   end
 
+(** The second input signature of the functor {!Logdag.Make} specifying the logic. *)
 module type LOG =
   sig
-    type t
-    val top : unit -> t
-    val entails : t -> t -> bool
-    val gen : t -> t -> t list -> t list
-    val parse : Syntax.t_stream -> t
-    val print : t -> Syntax.t_list
+    type t  (** Abstract type of formulas. *)
+    val top : unit -> t  (** Most general formula. *)
+    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
+    val gen : t -> t -> t list -> t list  (** Dichotomic operator for generating new features. *)
+    val parse : Syntax.t_stream -> t  (** Parsing of formulas from token streams. *)
+    val print : t -> Syntax.t_list  (** Printing of formulas to token lists. *)
   end
 
 (** The signature of implementations of logical diagrams. *)
     val log_fmt : Format.formatter
     (** The formatter associated to the log file when it exists. *)
 
+    val db : Dbm.t
+    (** The database used for persistency and swapping. *)
+
     type nid = int
     (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)
 
     (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
         @raise Not_found when the node [nid] does not exist in the diagram. *)
 
-    val forget : nid -> unit
-    (** [forget nid] removes the node identified by [nid] from the memory, after saving it in the database. *)
-
-    val sync : unit -> unit
-    (** [sync ()] synchronizes the database with the memory contents. *)
-
     val insert : Log.t -> bool -> nid * bool
     (** [insert f obj] returns the node id whose formula label is
 	logically equivalent to [f]. If such a node does not yet exist in the
     let some_log = match Param.log_file with None -> false | Some _ -> true
     let log_fmt = match Param.log_file with None -> Format.err_formatter | Some name -> formatter_of_out_channel (open_out name)
 
+
     type nid = int
 
     module Ext =
         let fold_right f (_,l) e = List.fold_right f l e
       end
 
+    module Nval =
+      struct
+        type t = float
+        let init () = Common.utime ()
+        let update v = Common.utime ()
+        let better v1 v2 = v1 >= v2
+      end
+
     type node = {
 	mutable feat : Log.t;  (* formula describing the node, and description of local object if some *)
 	mutable ext : Ext.t;  (* object idents of the extent *)
 	mutable sup : nid LSet.t;  (* list of parent nodes *)
 	mutable inf : nid LSet.t;  (* list of child nodes *)
+        mutable v : Nval.t  (* value w.r.t. swapping *)
       }
 
     let nil = 0
         feat = Log.top ();
         ext = Ext.empty;
         inf = LSet.empty ();
-        sup = LSet.empty ()
+        sup = LSet.empty ();
+        v = Nval.init ()
       }
 
     let top = 1
 
-    module Ndb =
-      struct
-        let db = Dbm.opendbm Param.dbname [Dbm.Dbm_create; Dbm.Dbm_rdwr] 0o664
-        let get_cpt () : int = try Marshal.from_string (Dbm.find db "cpt") 0 with Not_found -> top+1
-        let replace_cpt cpt = Dbm.replace db "cpt" (Marshal.to_string cpt [])
-        let get nid : node = Marshal.from_string (Dbm.find db ("nid" ^ string_of_int nid)) 0
-        let replace nid node = Dbm.replace db ("nid" ^ string_of_int nid) (Marshal.to_string node [])
-        let remove nid = try Dbm.remove db ("nid" ^ string_of_int nid) with _ -> ()
-        let close () = Dbm.close db
-      end
+    let db = Dbm.opendbm Param.dbname [Dbm.Dbm_create; Dbm.Dbm_rdwr] 0o664
+    let _ = at_exit (fun () -> Dbm.close db)
 
-    let cpt = ref (Ndb.get_cpt ())
+    let db_mod : Dbm.t Cache.db_mod = {
+        Cache.find = Dbm.find;
+        Cache.replace = Dbm.replace;
+        Cache.remove = Dbm.remove
+      }
 
-    module Nval =
-      struct
-        type t = float
-        let eval (nid,node) = (Unix.times ()).Unix.tms_utime
-        let ge v1 v2 = v1 >= v2
-      end
+    let cache_cpt = Cache.create db_mod db "cpt" 1
+    let _ =
+      if not (Cache.mem cache_cpt 0)
+      then Cache.add cache_cpt 0 (ref (top+1))
+
+    let cpt () = Cache.get cache_cpt 0
 
-    module Ntbl =  (* table of nodes, initialized with the top node *)
-      struct
-        let nb = ref 0  (* number of nodes in the table *)
-        let v : (nid,Nval.t * node) Hashtbl.t = Hashtbl.create Param.node_chunk
-        let get nid = snd (Hashtbl.find v nid)
-        let add nid node = incr nb; Hashtbl.add v nid (Nval.eval (nid,node), node)
-        let remove nid = decr nb; Hashtbl.remove v nid
-        let get_smallests () =
-          let rec insert x =
-            function
-            | [] -> [x]
-            | y::ys ->
-                if Nval.ge x y
-                then x::y::ys
-                else y::insert x ys in
-          let _, smallests =
-            Hashtbl.fold
-              (fun nid (v,node) (n,l) ->
-                 let n', l' = n+1, insert (v,nid) l in
-                 if n' <= Param.node_chunk
-                 then n', l'
-                 else n, List.tl l')
-              v (0,[]) in
-          List.map snd smallests
-        let iter f = Hashtbl.iter f v
-        let fold f e = Hashtbl.fold f v e
-        let _ = add top (try Ndb.get top with Not_found -> node_nil)
-      end
 
-    let forget nid =
-      try
-        Ndb.replace nid (Ntbl.get nid);
-        Ntbl.remove nid
-      with Not_found -> ()
+    let cache_nid = Cache.create db_mod db "nid" Param.node_chunk
+    let _ =
+      if not (Cache.mem cache_nid top)
+      then Cache.add cache_nid top node_nil
 
-    let forget_smallests () =
-      if Common.heap_size () > Param.max_mem
+    let rec unget_chunk () =
+      if Random.int Param.node_chunk = 0 & Common.heap_size () > Param.max_mem
       then begin
         if some_log then pp_print_string log_fmt "Logdag: swapping nodes on disk\n";
-        List.iter forget (Ntbl.get_smallests ()) end
-
-    let forget_all () =
-      Ntbl.iter (fun nid node -> forget nid);
-      Ndb.replace_cpt !cpt
-
-    let sync () =
-      Ntbl.iter (fun nid node -> Ndb.replace nid node)
-
-    let get nid =
-      try Ntbl.get nid
-      with Not_found ->
-        if !Ntbl.nb mod Param.node_chunk = 0
-        then forget_smallests ();
-        let node =
-          try Ndb.get nid
-          with Not_found ->
-            pp_print_string log_fmt "Logdag: nid not found: "; pp_print_int log_fmt nid; pp_print_newline log_fmt ();
-            raise Not_found in
-        Ntbl.add nid node;
-        node
+        let keys = get_worst_chunk () in
+        List.iter (Cache.unget cache_nid) keys;
+        Gc.major () end
+    and get_worst_chunk () =
+      let rec insert x =
+        function
+        | [] -> [x]
+        | y::ys ->
+           if Nval.better x y
+           then x::y::ys
+           else y::insert x ys in
+      let _, worst_chunk =
+        Cache.fold
+          (fun nid node (n,l) ->
+             let n', l' = n+1, insert (node.v,nid) l in
+             if n' <= Param.node_chunk
+             then n', l'
+             else n, List.tl l')
+          cache_nid (0,[]) in
+      List.map snd worst_chunk
+
+    let get nid = Common.prof "Logdag.get" (fun () ->
+      unget_chunk ();
+      let node = Cache.get cache_nid nid in
+      node.v <- Nval.update node.v;
+      node)
 
     let create node =
-      if !Ntbl.nb mod Param.node_chunk = 0
-      then forget_smallests ();
+      unget_chunk ();
+      let cpt = cpt () in
       let nid = !cpt in
       incr cpt;
-      Ntbl.add nid node;
+      Cache.add cache_nid nid node;
       nid
 
-    let delete nid =
-      Ntbl.remove nid;
-      Ndb.remove nid
+    let delete nid = Cache.remove cache_nid nid
 
 
     let feat node = node.feat
 
     let rec fold : (nid * node -> 'a -> 'a * nid list) -> nid * node -> 'a -> 'a =
       fun f_next (nid,node) init ->
-        let m = Array.make !cpt `Unknown
+        let m = Array.make !(cpt ()) `Unknown
         in fold2 m f_next (nid,node) init
     and fold2 m f_next (nid,node) init =
       if m.(nid) = `Unknown
 
     let rec first : pred_next:(bool -> nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list =
       fun ~pred_next ~start ->
-	let m = Array.make !cpt `Unknown
+	let m = Array.make !(cpt ()) `Unknown
 	in List.map snd (
           List.fold_left
 	    (fun res nid -> first2 m pred_next (nid,get nid) true res)
 
     let rec last : pred_next:(nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list =
       fun ~pred_next ~start ->
-	let m = Array.make !cpt `Unknown in
+	let m = Array.make !(cpt ()) `Unknown in
 	snd (new_last m pred_next start [])
     and new_last m pred_next (nid,node) res =
 	let x, nids = pred_next (nid,node) in
 	| [] -> [(top,get top)]
 	| [nidnode] when pred nidnode -> [nidnode]
 	| nidnodes ->
-	    let m = Array.make !cpt 0 in
+	    let m = Array.make !(cpt ()) 0 in
 	    let lnodes = List.length nidnodes in
 	    List.iter
 	      (fun (nid,node) ->
     let rec lubs : pred:(nid * node -> int -> 'a option) -> suppmin:int -> (nid * node) list -> 'a list =
       fun ~pred ~suppmin -> function
 	| [] -> raise (Invalid_argument "LogDag.Make.lubs : the list is empty") 
-	| nidnodes ->
-	    let m = Array.make !cpt 0 in
+	| nidnodes -> Common.prof "Logdag.lubs" (fun () ->
+	    let m = Array.make !(cpt ()) 0 in
 	    let l = List.length nidnodes in
 	    let supp = min suppmin l in
 	    List.iter
                 let s = m.(nid) in
 		(if s >= smin then pred (nid,node) s else None),
 		node.sup)
-	      (if supp=l then (List.hd nidnodes) else (nil,{node_nil with sup = List.map fst nidnodes}))
+	      (if supp=l then (List.hd nidnodes) else (nil,{node_nil with sup = List.map fst nidnodes})))
 
 
     let locate : Log.t -> bool -> nid * node =
 		feat = feat;
 		ext = ext;
 		sup = LSet.of_list (List.map fst sup);
-		inf = LSet.of_list (List.map fst inf)} in
+		inf = LSet.of_list (List.map fst inf);
+                v = Nval.init ()} in
 	     0, new_node
 
     let connect : nid -> node -> bool -> unit =
 	    (nid,node)
 	    ()
 
-    let insert feat obj =
+    let insert feat obj = Common.prof "Logdag.insert" (fun () ->
       let nid, node = locate feat obj in
       if nid = nil
       then begin
         connect nid node obj;
         nid, true end
       else begin
-        nid, false end
+        nid, false end)
 
     let rec disconnect nid =
       let node = get nid in
 	  ();
       List.iter (fun n -> let nd = get n in nd.inf <- LSet.remove nid nd.inf) node.sup;
       List.iter (fun n -> let nd = get n in nd.sup <- LSet.remove nid nd.sup) node.inf;
-      let mup = Array.make !cpt false in
+      let mup = Array.make !(cpt ()) false in
       fold
         (fun (n,nd) () -> (mup.(n) <- true), nd.sup)
         (nil,{node_nil with sup = node.inf})
         ();
-      let mdown = Array.make !cpt false in
+      let mdown = Array.make !(cpt ()) false in
       let tbl = Hashtbl.create (2 * LSet.cardinal node.inf) in
       List.iter (fun n -> Hashtbl.add tbl n node.sup) node.inf;
       List.iter
         try disconnect nid with Not_found -> ();
         delete nid end
 
-    let _ = at_exit (fun () -> forget_all (); Ndb.close ())    
-
   end
     val log_fmt : Format.formatter
     (** The formatter associated to the log file when it exists. *)
 
+    val db : Dbm.t
+    (** The database used for persistency and swapping. *)
+
     type nid = int
     (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)
 
     (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
         @raise Not_found when the node [nid] does not exist in the diagram. *)
 
-    val forget : nid -> unit
-    (** [forget nid] removes the node identified by [nid] from the memory, after saving it in the database. *)
-
-    val sync : unit -> unit
-    (** [sync ()] synchronizes the database with the memory contents. *)
-
     val insert : Log.t -> bool -> nid * bool
     (** [insert f obj] returns the node id whose formula label is
 	logically equivalent to [f]. If such a node does not yet exist in the