Source

ocaml-lib / logdag.ml

Full commit
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493

module type PARAM =
  sig
    val dbname : string
    val max_mem : float
    val node_chunk : int
  end

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
  end

(** The signature of implementations of logical diagrams. *)
module type T =
  sig
    module Log : LOG
    (** The logic module passed as a parameter. *)

    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. *)

    val nil : nid
    (** Nil id referencing no node. *)

    val top : nid
    (** Id of the most general node. *)

    (** Module for the representation of extents (sets of objects). *)
    module Ext :
      sig
        type t  (** Abstract type of extents. *)
        val empty : t  (** The empty extent. *)
        val is_empty : t -> bool  (** [is_empty ext] tests whether [ext] is empty. *)
        val cardinal : t -> int  (** [cardinal ext] returns the size of the extent [ext]. *)
        val mem : nid -> t -> bool  (** [mem o ext] tests whether [o] belongs to [ext]. *)
        val contains : t -> t -> bool  (** [contains ext1 ext2] tests whether [ext1] contains [ext2]. *)
        val add : nid -> t -> t  (** [add o ext] returns the addition of [o] to [ext]. *)
        val remove : nid -> t -> t  (** [remove o ext] returns the removal of [o] from [ext]. *)
        val union : t -> t -> t  (** [union ext1 ext2] returns the set union of [ext1] and [ext2]. *)
        val union_r : t list -> t  (** [union_r exts] returns the union of all extents in [exts]. *)
        val inter : t -> t -> t  (** [inter ext1 ext2] returns the set intersection of [ext1] and [ext2]. *)
        val inter_r : t list -> t  (** [inter_r exts] returns the intersection of all extents in [exts].
                                       @raise Invalid_argument if [exts] is the empty list. *)
        val subtract : t -> t -> t  (** [subtract ext1 ext2] returns the set subtraction of [ext1] and [ext2]. *)
        val inter_difsym : t -> t -> t * t * t
          (** [inter_difsym ext1 ext2] returns the extent triplet [(subtract ext1 ext2, inter ext1 ext2, subtract ext2 ext1)]. *)
        val iter : (nid -> unit) -> t -> unit
          (** Iteration on the objects of an extent (see [List.iter]). Objects visited from low ids to high ids. *)
        val fold_left : ('a -> nid -> 'a) -> 'a -> t -> 'a
          (** Folding on an extent from low ids to high ids (see List.fold_left). *)
        val fold_right : (nid -> 'a -> 'a) -> t -> 'a -> 'a
          (** Folding on an extent from high ids to low ids (see List.fold_right). *)
      end

    type node
    (** Abstract type of nodes.

       {e Warning}: values of this type are relevant at the time they are
	retrieved, but are not guarenteed to remain consistent after changes are
	made. *)

    val feat : node -> Log.t
    (** [feat node] gets the formula label of [node]. *)

    val ext : node -> Ext.t
    (** [ext node] gets the extent label of [node]. *)

    val inf : node -> nid LSet.t
    (** [inf node] gets the inferior (more specific) neighbours of [node]. *)

    val sup : node -> nid LSet.t
    (** [sup node] gets the superior (more general) neighbours of [node]. *)

    val is_obj : node -> bool
    (** [is_obj node] test whether [node] is labeled by an object. *)

    val get : nid -> 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
	diagram, it is inserted and the second result is [true]; otherwise the second result is [false]. 
        If [obj] is true, then a new object is
	associated to this node, and extents of existing nodes are updated
	accordingly. *)

    val remove : nid -> unit
    (** [remove nid] removes the node identified by [nid] from the diagram (both in memory and the database). *)

    val fold : (nid * node -> 'a -> 'a * nid list) -> nid * node -> 'a -> 'a
    (** [fold f_next (nid,node) e] computes a result through a traversal of
	the diagram. The starting node is specified by [(nid,node)], where
	[node] must be equal to [get nid]. The application [f_next (nid,node)
	res] to the current node [(nid,node)] and the current result [res]
	returns a pair [(res',next_nids)], where [res'] is the new result, and
	[next_nids] are the ids of the next nodes to be visited. The traversal
	order is not specified, but each node is ensured to be visited at most
	once. *)

    val first : pred_next:(bool -> nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list
    (** [first ~pred_next ~start:(nid,node)] looks for the first nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. The
	first parameter can be used for optimization as, when it is false,
	[None] can be returned in all cases. *)

    val last : pred_next:(nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list
    (** [last ~pred_next ~start:(nid,node)] looks for the last nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. *)

    val glbs : pred:(nid * node -> bool) -> (nid * node) list -> (nid * node) list
    (** [glbs ~pred nodes] returns the {e glbs} (greatest lower bounds) of the nodes [nodes] among the nodes satisfying [pred]. *)

    val lubs : pred:(nid * node -> int -> 'a option) -> suppmin:int -> (nid * node) list -> 'a list
    (** [lubs ~pred ~suppmin nodes] returns the [suppmin]-approximate {e lubs}
	(least upper bounds) of the nodes [nodes] among the nodes satisfying
	[pred]. A node is a [suppmin]-approximate lub if it has at least
	[suppmin] more specific nodes in [nodes]. The second argument of
	[pred] is the support of the node (number of more specific nodes in
	[nodes]). *)

  end

module Make (Param : PARAM) (Log : LOG) : T =
  struct
    module Log = Log

    type nid = int

    module Ext =
      struct
        type t = int * nid LSet.t
        let empty = 0, LSet.empty ()
        let is_empty (s,_) = s=0
        let cardinal (s,_) = s
        let mem nid (_,l) = LSet.mem nid l
        let contains (_,l1) (_,l2) = LSet.contains l1 l2
        let add nid (_,l) = let l' = LSet.add nid l in LSet.cardinal l', l'
        let remove nid (_,l) = let l' = LSet.remove nid l in LSet.cardinal l', l'
        let union (_,l1) (_,l2) = let l' = LSet.union l1 l2 in LSet.cardinal l', l'
        let union_r exts = let l' = LSet.union_r (List.map snd exts) in LSet.cardinal l', l'
        let inter (_,l1) (_,l2) = let l' = LSet.inter l1 l2 in LSet.cardinal l', l'
        let inter_r exts = let l' = LSet.inter_r (List.map snd exts) in LSet.cardinal l', l'
        let subtract (_,l1) (_,l2) = let l' = LSet.subtract l1 l2 in LSet.cardinal l', l'
        let inter_difsym (_,l1) (_,l2) =
          LSet.fold
            (fun ((s1,l1), (s2,l2), (s3,l3)) (w,x) ->
               match w with
               | LSet.Infst -> (s1+1,LSet.add x l1), (s2,l2), (s3,l3)
               | LSet.Inboth -> (s1,l1), (s2+1,LSet.add x l2), (s3,l3)
               | LSet.Insnd -> (s1,l1), (s2,l2), (s3+1,LSet.add x l3))
            ((0,LSet.empty ()) , (0,LSet.empty ()), (0,LSet.empty ()))
            l1 l2
        let iter f (_,l) = List.iter f l
        let fold_left f e (_,l) = List.fold_left f e l
        let fold_right f (_,l) e = List.fold_right f l e
      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 *)
      }

    let nil = 0
    let node_nil = {
        feat = Log.top ();
        ext = Ext.empty;
        inf = LSet.empty ();
        sup = LSet.empty ()
      }

    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 cpt = ref (Ndb.get_cpt ())

    module Nval =
      struct
        type t = float
        let eval (nid,node) = (Unix.times ()).Unix.tms_utime
        let ge v1 v2 = v1 >= v2
      end

    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 forget_smallests () =
      let heap_size = float_of_int (Gc.stat ()).Gc.heap_words *. float_of_int (Sys.word_size / 8) in (* in bytes *)
      if Param.max_mem < heap_size
      then List.iter forget (Ntbl.get_smallests ())

    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 -> print_string "\nNid not found: "; print_int nid; raise Not_found in
        Ntbl.add nid node;
        node

    let create node =
      if !Ntbl.nb mod Param.node_chunk = 0
      then forget_smallests ();
      let nid = !cpt in
      incr cpt;
      Ntbl.add nid node;
      nid

    let delete nid =
      Ntbl.remove nid;
      Ndb.remove nid


    let feat node = node.feat

    let ext node = node.ext

    let inf node = node.inf

    let sup node = node.sup

    let is_obj node = LSet.is_empty node.inf & node.ext <> Ext.empty

    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
        in fold2 m f_next (nid,node) init
    and fold2 m f_next (nid,node) init =
      if m.(nid) = `Unknown
      then begin
	m.(nid) <- `Good;
	let res0, nids = f_next (nid,node) init in
	List.fold_left
	  (fun res n -> fold2 m f_next (n,get n) res)
	  res0
	  nids end
      else init

    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
	in List.map snd (
          List.fold_left
	    (fun res nid -> first2 m pred_next (nid,get nid) true res)
	    [] (snd (pred_next false start)))
    and first2 m pred_next (nid,node) above res =
	if m.(nid) = `Unknown then
	  let x, nids = pred_next above (nid,node) in
	  let good = above & (x <> None) in
	  m.(nid) <- if good then `Good else `Bad;
	  List.fold_left
	    (fun res n -> first2 m pred_next (n,get n) (above & not good) res)
	    (match x with None -> res | Some v -> if good then ((nid, v)::res) else res)
	    nids
	else if m.(nid) = `Good & not above then begin
	  m.(nid) <- `Bad;
	  List.filter (fun (n,v) -> n != nid) res end 
	else 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
	snd (new_last m pred_next start [])
    and new_last m pred_next (nid,node) res =
	let x, nids = pred_next (nid,node) in
	let last, res1 = List.fold_left
	    (fun (last,res) n ->
	      if m.(n) = `Good then (false,res) (* node is not a last one *)
	      else if m.(n) = `Bad then (last,res) (* node may be a last one *)
	      else (* m.(n) = `Unknown *)
		let last',res' = new_last m pred_next (n,get n) res in
		last & last', res')
	    (true,res)
	    nids in
	if not last
	then begin m.(nid) <- `Good; (false,res1) end
	else match x with
	| None -> begin m.(nid) <- `Bad; (true,res1) end
	| Some v -> begin m.(nid) <- `Good; (false,v::res1) end

    let glbs : pred:(nid * node -> bool) -> (nid * node) list -> (nid * node) list =
      fun ~pred -> function
	| [] -> [(top,get top)]
	| [nidnode] when pred nidnode -> [nidnode]
	| nidnodes ->
	    let m = Array.make !cpt 0 in
	    let lnodes = List.length nidnodes in
	    List.iter
	      (fun (nid,node) ->
		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), nd.inf) (nid,node) ())
	      nidnodes;
	    first
	      (fun above (nid,node) ->
		(if above & m.(nid) >= lnodes & pred (nid,node) then Some (nid,node) else None), node.inf)
	      (nil, {node_nil with inf = List.map fst nidnodes})

    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
	    let l = List.length nidnodes in
	    let supp = min suppmin l in
	    List.iter
	      (fun (nid,node) ->
		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), nd.sup) (nid,node) ())
	      (if supp=l then List.tl nidnodes else nidnodes);
            let smin = if supp=l then supp-1 else supp in
	    first
	      (fun _ (nid,node) ->
                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}))


    let locate : Log.t -> bool -> nid * node =
      fun feat obj ->
	let sup =
	  last
	    ~pred_next:(fun (nid,node) ->
	       if not (is_obj node) & Log.entails feat node.feat
	       then Some (nid,node), node.inf
	       else None, [])
	    ~start:(top,get top) in
(* print_string "\nsup"; List.iter (fun (nid,_) -> print_string "-"; print_int nid) sup; *)
	match sup with
	| [(nid,node)] when not obj & Log.entails node.feat feat ->
	     node.feat <- feat;  (* the old formula is replaced by the new equivalent one *)
	     nid, node  (* the searched node already exists *)
	| nodes ->  (* the searched node must be inserted *)
	     let inf, ext =
	       if obj
               then LSet.empty (), Ext.empty
               else
                 let inf = glbs (fun (nid,node) -> Log.entails node.feat feat) nodes in
                 inf, List.fold_left Ext.union Ext.empty (List.map (fun (nid,node) -> node.ext) inf) in
(* print_string "\ninf"; List.iter (fun (nid,_) -> print_string "-"; print_int nid) inf; *)
	     let new_node = {
		feat = feat;
		ext = ext;
		sup = LSet.of_list (List.map fst sup);
		inf = LSet.of_list (List.map fst inf)} in
	     0, new_node

    let connect : nid -> node -> bool -> unit =
      fun nid node obj ->
	List.iter
	  (fun n ->
             let nd = get n in
             nd.inf <- LSet.add nid (LSet.subtract nd.inf node.inf))
	  node.sup;
	List.iter
	  (fun n ->
             let nd = get n in
             nd.sup <- LSet.add nid (LSet.subtract nd.sup node.sup))
	  node.inf;
        if obj
        then
	  fold
	    (fun (n,nd) () -> nd.ext <- Ext.add nid nd.ext; (), nd.sup)
	    (nid,node)
	    ()

    let insert feat obj =
      let nid, node = locate feat obj in
      if nid = nil
      then begin
        let nid = create node in
(* print_string "\nnid="; print_int nid; *)
        connect nid node obj;
        nid, true end
      else begin
(* print_string "\nnid="; print_int nid; *)
        nid, false end

    let rec disconnect nid =
      let node = get nid in
      if is_obj node
      then
	fold
	  (fun (n,nd) () -> nd.ext <- Ext.remove nid nd.ext; (), nd.sup)
	  (nid,node)
	  ();
      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
      fold
        (fun (n,nd) () -> (mup.(n) <- true), nd.sup)
        (nil,{node_nil with sup = node.inf})
        ();
      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
	(fun n ->
           let nd = get n in
           List.iter (fun n' -> mdown.(n') <- false) node.inf;
           fold
             (fun (n',nd') () -> (mdown.(n') <- true), if mup.(n') then nd'.inf else [])
             (n,get n)
             ();
           let inf_old, inf_new = List.partition (fun n' -> mdown.(n')) node.inf in
	   nd.inf <- LSet.union nd.inf inf_new;
           List.iter (fun n' -> Hashtbl.replace tbl n' (LSet.remove n (Hashtbl.find tbl n'))) inf_old)
        node.sup;
      List.iter
        (fun n ->
           let nd = get n in
           nd.sup <- LSet.union nd.sup (Hashtbl.find tbl n))
        node.inf

    let remove nid =
      if nid <> top
      then begin
        try disconnect nid with Not_found -> ();
        delete nid end

    let _ = at_exit (fun () -> forget_all (); Ndb.close ())    

  end