boolVar.ml 13.7 KB
Newer Older
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
let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=)


module type E =
sig
  (* module V : sig type t end *)
  type elem
  include Custom.T

  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t

end

module type S =
sig
  type elem
  include Custom.T

  val get: t -> (elem list * elem list) list
  val get': t -> (elem list * (elem list) list) list

  val empty : t
  val full  : t
  val cup   : t -> t -> t
  val cap   : t -> t -> t
  val diff  : t -> t -> t
  val atom  : elem -> t

  val iter: (elem-> unit) -> t -> unit

  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) 
    -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
    atom:(elem -> 'b) -> t -> 'b

  val is_empty : t -> bool

  val splitvars : t -> t * t

  val print: string -> t -> (Format.formatter -> unit) list

  val trivially_disjoint: t -> t -> bool
end

(* ternary BDD
 * where the nodes are Atm of X.t | Var of String.t
 * Variables are always before Values
 * All the leaves are then base types 
 *
 * we add a third case when two leaves of the bdd are of the same
 * kind, that's it Val of t1 , Val of t2
 *
 * This representation can be used for all kinds.
 * Intervals, Atoms and Chars can be always merged (for union and intersection)
 * Products can be merged for intersections
 * Arrows can be never merged
 *
 * extract_var : copy the orginal tree and on one copy put to zero all 
 * leaves that have an Atm on the other all leaves that have a Var
 *
 * *)

module type MAKE = functor (T : E) -> S with type elem = T.t Custom.pairvar

module Make(T : E) =
struct
  (* ternary decision trees . cf section 11.3.3 Frish PhD *)
  (* plus variables *)
  (* Custom.Atm are containers (Atoms, Chars, Intervals, Pairs ... )
   * Custom.Var are String
   *)
  module X = Custom.Var(T)
  type elem = T.t Custom.pairvar
  type t =
    | True
    | False
    | Split of int * elem * t * t * t

  let rec equal a b =
    (a == b) ||
    match (a,b) with
      | Split (h1,x1,p1,i1,n1), Split (h2,x2,p2,i2,n2) ->
	  (h1 == h2) &&
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
      | _ -> false

(* Idea: add a mutable "unique" identifier and set it to
   the minimum of the two when egality ... *)

  let rec compare a b =
    if (a == b) then 0 
    else match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
	  if h1 < h2 then -1 else if h1 > h2 then 1 
	  else let c = X.compare x1 x2 in if c <> 0 then c
	  else let c = compare p1 p2 in if c <> 0 then c
	  else let c = compare i1 i2 in if c <> 0 then c 
	  else compare n1 n2
      | True,_  -> -1
      | _, True -> 1
      | False,_ -> -1
      | _,False -> 1

  let rec hash = function
    | True -> 1
    | False -> 0
    | Split(h, _,_,_,_) -> h

  let compute_hash x p i n = 
	(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)

  let rec check = function
    | True | False -> ()
    | Split (h,x,p,i,n) ->
	assert (h = compute_hash x p i n);
	(match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match i with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	(match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ());
	X.check x; check p; check i; check n

  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
    Split (h, x,True,False,False)
 
  let neg_atom x =
    let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
    Split (h, x,False,False,True)

  let rec iter f = function
    | Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
    | _ -> ()

  let rec dump ppf = function
    | True -> Format.fprintf ppf "+"
    | False -> Format.fprintf ppf "-"
    | Split (_,x, p,i,n) -> 
	Format.fprintf ppf "%i(@[%a,%a,%a@])" 
	(* X.dump x *) (X.hash x) dump p dump i dump n

  let rec print f ppf = function
    | True -> Format.fprintf ppf "Any"
    | False -> Format.fprintf ppf "Empty"
    | Split (_, x, p,i, n) ->
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
	(match p with 
	   | True -> b(); Format.fprintf ppf "%a" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
	(match i with 
	   | True -> assert false;
	   | False -> ()
	   | _ -> b(); print f ppf i);
	(match n with 
	   | True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
	
  let print a = function
    | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | False -> []
    | c -> [ fun ppf -> print X.dump ppf c ]

  (* XXX : since every path contains 1 Atm, I should be able to
   * descend on the first path and get a sample from the leaf *)    
  let rec sample = function
    | Split (_,Custom.Var _, p,i,n) ->
        begin match sample p with
        |Some x -> Some x
        |None ->
            begin match sample i with
            |Some x -> Some x
            |None ->
                begin match sample n with
                |Some x -> Some x
                |None -> None
                end
            end
        end
    | Split (_,Custom.Atm x, _,_,_) -> Some x
    | _ -> None

  let rec contains y x =
    match x,y with
    |True,_ |False,_ -> false
    |Split (_,Custom.Var a, p,i,n),Custom.Var b ->
        (a == b) || (contains y p) || (contains y i) || (contains y n)
    |Split (_,Custom.Atm a, p,i,n),Custom.Atm b ->
        ((T.cap a b) == T.empty) || (contains y p) || (contains y i) || (contains y n)
    |Split (_,_, p,i,n),_ ->
        (contains y p) || (contains y i) || (contains y n)

  let rec get accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x, p,i,n) ->
	(*OPT: can avoid creating this list cell when pos or neg =False *)
	let accu = get accu (x::pos) neg p in
	let accu = get accu pos (x::neg) n in
	let accu = get accu pos neg i in
	accu
	  
  let get x = get [] [] [] x

  let rec get' accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x,p,i,n) ->
	let accu = get' accu (x::pos) neg p in
	let rec aux l = function
	  | Split (_,x,False,i,n') when equal n n' ->
	      aux (x :: l) i
	  | i ->
	      let accu = get' accu pos (l :: neg) n in
	      get' accu pos neg i
	in
	aux [x] i

  let get' x = get' [] [] [] x

  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | True -> full
      | False -> empty
      | Split(_,x, p,i,n) ->
	  let p = cap (atom x) (aux p)
	  and i = aux i
	  and n = diff (aux n) (atom x) in
	  cup (cup p i) n
    in
    aux b
      
(* Invariant: correct hash value *)

  let split0 x pos ign neg =
    Split (compute_hash x pos ign neg, x, pos, ign, neg)

  let empty = False
  let full = True

  let is_empty t = (t == empty)

(* Invariants:
     Split (x, pos,ign,neg) ==>  (ign <> True), (pos <> neg)
*)

  let rec has_true = function
    | [] -> false
    | True :: _ -> true
    | _ :: l -> has_true l

  let rec has_same a = function
    | [] -> false
    | b :: l -> (equal a b) || (has_same a l)

  let rec split x p i n =
    if X.equal x (Custom.Atm T.empty) then False
    else if i == True then True 
    else if equal p n then p ++ i
    else let p = simplify p [i] and n = simplify n [i] in
    if equal p n then p ++ i
    else split0 x p i n

  and simplify a l =
    match a with
      | False -> False
      | True -> if has_true l then False else True
      | Split (_,Custom.Atm x, True,False,False) -> split (Custom.Atm(T.diff T.full x)) True False False
      | Split (_,Custom.Atm x, False,False,True) -> split (Custom.Atm(T.diff T.full x)) True False False
      | Split (_,x,p,i,n) ->
	  if (has_true l) || (has_same a l) then False
	  else s_aux2 a x p i n [] [] [] l
  and s_aux2 a x p i n ap ai an = function
    | [] -> 
	let p = simplify p ap 
	and n = simplify n an
	and i = simplify i ai in
	if equal p n then p ++ i else split0 x p i n
    | b :: l -> s_aux3 a x p i n ap ai an l b 
  and s_aux3 a x p i n ap ai an l = function
    | False -> s_aux2 a x p i n ap ai an l
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
	if equal a b then False 
	else let c = X.compare x2 x in
	if c < 0 then s_aux3 a x p i n ap ai an l i2
	else if c > 0 then s_aux2 a x p i n (b :: ap) (b :: ai) (b :: an) l
	else s_aux2 a x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l

  (* Inv : all leafs are of type Val are always merged *)
  (* union *)
  and ( ++ ) a b = if a == b then a
  else match (a,b) with
    | True, _ | _, True -> True
    | False, a | a, False -> a
    
    | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, True,False,False) ->
        split (Custom.Atm (T.cup x1 x2)) True False False

    | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, False,False,True) ->
        split (Custom.Atm (T.cup (T.diff T.full x1) (T.diff T.full x2))) True False False

    | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, False,False,True) ->
        split (Custom.Atm (T.cup x1 (T.diff T.full x2))) True False False

    | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, True,False,False) ->
        split (Custom.Atm (T.cup (T.diff T.full x1) x2)) True False False

    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	let c = X.compare x1 x2 in
	if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
	else if c < 0 then split x1 p1 (i1 ++ b) n1
	else split x2 p2 (i2 ++ a) n2

(* seems better not to make ++ and this split mutually recursive;
   is the invariant still inforced ? *)

  (* intersection *)
  let rec ( ** ) a b = if a == b then a else match (a,b) with
    | True, a | a, True -> a
    | False, _ | _, False -> False

    | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, True,False,False) ->
        split (Custom.Atm(T.cap x1 x2)) True False False

    | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, False,False,True) ->
        split (Custom.Atm(T.cap (T.diff T.full x1) (T.diff T.full x2))) True False False

    | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, False,False,True) ->
        split (Custom.Atm(T.cap x1 (T.diff T.full x2))) True False False

    | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, True,False,False) ->
        split (Custom.Atm(T.cap (T.diff T.full x1) x2)) True False False

    | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	let c = X.compare x1 x2 in
	if c = 0 then
	  split x1 
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))  
	else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else split x2 (p2 ** a) (i2 ** a) (n2 ** a)

  let rec trivially_disjoint a b =
    if a == b then a == False
    else match (a,b) with
      | True, a | a, True -> a == False
      | False, _ | _, False -> true
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
(* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
	    trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
	    trivially_disjoint (n1 ++ i1) (n2 ++ i2)
	  else if c < 0 then
	    trivially_disjoint p1 b &&
	    trivially_disjoint i1 b &&
	    trivially_disjoint n1 b
	  else
	    trivially_disjoint p2 a &&
	    trivially_disjoint i2 a &&
	    trivially_disjoint n2 a

  let rec neg = function
    | True -> False
    | False -> True
    | Split (_,Custom.Atm x, True,False,False) -> split (Custom.Atm(T.diff T.full x)) True False False
    | Split (_,Custom.Atm x, False,False,True) -> split (Custom.Atm(T.diff T.full x)) True False False
    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
    | Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False 
    | Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)  
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
	      
  let rec ( // ) a b =
    let negatm = T.diff T.full in
    if a == b then False 
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b

      | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, True,False,False) ->
          split (Custom.Atm(T.diff x1 x2)) True False False

      | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, False,False,True) ->
          split (Custom.Atm(T.diff (negatm x1) (negatm x2))) True False False

      | Split (_,Custom.Atm x1, True,False,False), Split (_,Custom.Atm x2, False,False,True) ->
          split (Custom.Atm(T.diff x1 (negatm x2))) True False False

      | Split (_,Custom.Atm x1, False,False,True), Split (_,Custom.Atm x2, True,False,False) ->
          split (Custom.Atm(T.diff (negatm x1) x2)) True False False

      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    if (i2 == False) && (n2 == False) 
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
	    else 
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
	  else if c < 0 then
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
	      
  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

  (* return a couple of trees (v,a), the second where all variables
   * v = only variables as leaves
   * a = only atoms as leaves
   *)
  let rec splitvars = function
    | True -> True,True
    | False -> False,False
    | Split (_,Custom.Var _, True,False,False) as x -> x, False
    | Split (_,Custom.Atm _, True,False,False) as x -> True, x
    | Split (_,x, p,i,n) ->
        let l,p' = splitvars p in
        let c,i' = splitvars i in
        let r,n' = splitvars n in 
        match split x l c r, split x p' i' n' with
        |t,Split (_,Custom.Var _, True,False,False) -> t,False
        |(_,_) as t -> t

  let splitvars t = splitvars t
  
end