bool.ml 38.9 KB
Newer Older
1
2
3
4
let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=)

5
6
module type S =
sig
7
8
  type elem
  include Custom.T
9

10
  val get: t -> (elem list * elem list) list
11

12
13
14
15
16
17
  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
18

19
  val iter: (elem-> unit) -> t -> unit
20
21
22

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

25
(*
26
  val print: string -> (Format.formatter -> elem -> unit) -> t ->
27
    (Format.formatter -> unit) list
28
*)
29

30
  val trivially_disjoint: t -> t -> bool
31
32
end

33
34
35
module type MAKE = functor (X : Custom.T) -> S with type elem = X.t

module Make(X : Custom.T) =
36
struct
37
38
  type elem = X.t
  type t =
39
40
    | True
    | False
41
    | Split of int * elem * t * t * t
42

43
44
45
46
47
  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) &&
48
49
	  (equal p1 p2) && (equal i1 i2) &&
	  (equal n1 n2) && (X.equal x1 x2)
50
51
      | _ -> false

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


56
57
58
59
60
61
62
63
64
65
66
67
68
  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
69
70


71
72
73
74
75
76
77
78
  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)

79
80
81
82
83
84
85
86

  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) | _ -> ());
87
	X.check x; check p; check i; check n
88

89
90
91
  let atom x =
    let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
    Split (h, x,True,False,False)
92
93
94
95
 
  let neg_atom x =
    let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *)
    Split (h, x,False,False,True)
96
97
98
99
100
101
102
103
104

  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) -> 
105
106
	Format.fprintf ppf "%i(@[%a,%a,%a@])" 
	(* X.dump x *) (X.hash x) dump p dump i dump n
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
  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 f = function
    | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | False -> []
    | c -> [ fun ppf -> print f ppf c ]
	
	
  let rec get accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x, p,i,n) ->
138
	(*OPT: can avoid creating this list cell when pos or neg =False *)
139
140
141
142
143
144
145
146
147
148
149
150
151
152
	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 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
153
	  and n = diff (aux n) (atom x) in
154
155
156
157
158
159
160
161
162
	  cup (cup p i) n
    in
    aux b
      
(* Invariant: correct hash value *)

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

163
164
165
166

    


167
168
  let empty = False
  let full = True
169
170
171
172
173
174

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

175
  let split x pos ign neg =
176
177
    if ign == True then True 
    else if (pos == False) && (neg == False) then ign
178
    else split x pos ign neg
179
180


181
182
(* Invariant:
   - no ``subsumption'
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
  let rec simplify a b =
    if equal a b then False 
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, _ -> True
      | Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    let p1' = simplify (simplify p1 i2) p2 
	    and i1' = simplify i1 i2
	    and n1' = simplify (simplify n1 i2) n2 in
	    if (p1 != p1') || (n1 != n1') || (i1 != i1') 
	    then split x1 p1' i1' n1'
	    else a
	  else if c > 0 then
	    simplify a i2
	  else
	    let p1' = simplify p1 b 
	    and i1' = simplify i1 b
	    and n1' = simplify n1 b in
	    if (p1 != p1') || (n1 != n1') || (i1 != i1') 
	    then split x1 p1' i1' n1'
	    else a
210
211
212
*)


213
  let rec simplify a l =
214
    if (a == False) then False else simpl_aux1 a [] l
215
  and simpl_aux1 a accu = function
216
    | [] -> 
217
	if accu == [] then a else
218
219
220
221
	  (match a with
	     | True -> True
	     | False -> assert false
	     | Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
222
223
224
    | False :: l -> simpl_aux1 a accu l
    | True :: l -> False
    | b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
225
226
227
228
229
230
231
232
  and simpl_aux2 x p i n ap ai an = function
    | [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
    | (Split (_,x2,p2,i2,n2) as b) :: l ->
	let c = X.compare x2 x in
	if c < 0 then 
	  simpl_aux3 x p i n ap ai an l i2
	else if c > 0 then 
	  simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
233
	else
234
235
236
237
238
239
240
241
242
243
244
	  simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
    | _ -> assert false
  and simpl_aux3 x p i n ap ai an l = function
    | False -> simpl_aux2 x p i n ap ai an l
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
	let c = X.compare x2 x in
	if c < 0 then 
	  simpl_aux3 x p i n ap ai an l i2
	else if c > 0 then 
	  simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
245
	else
246
	  simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
247
248
249

	  
    
250
  let split x p i n = 
251
252
    split x (simplify p [i]) i (simplify n [i])

253
254

  let rec ( ++ ) a b =
255
256
(*    if equal a b then a *)
    if a == b then a  
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
    else match (a,b) with
      | True, _ | _, True -> True
      | False, a | a, False -> a
      | 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

(* Pseudo-Invariant:
   - pos <> neg
*)

  let split x pos ign neg =
    if equal pos neg then (neg ++ ign) else split x pos ign neg

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

  let rec ( ** ) a b =
280
281
    (*    if equal a b then a *)
    if a == b then a
282
283
284
285
286
287
288
289
290
    else match (a,b) with
      | True, a | a, True -> a
      | False, _ | _, 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)
291
	      (n1 ** (n2 ++ i2) ++ (n2 ** i1))  *)
292
293
294
	    split x1 
	      ((p1 ++ i1) ** (p2 ++ i2))
	      False
295
	      ((n1 ++ i1) ** (n2 ++ i2)) 
296
297
298
299
300
	  else if c < 0 then
	    split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	  else
	    split x2 (p2 ** a) (i2 ** a) (n2 ** a)

301
  let rec trivially_disjoint a b =
302
    if a == b then a == False
303
    else match (a,b) with
304
      | True, a | a, True -> a == False
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
      | 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

321
322
323
324
325
326
327
328
329
  let rec neg = function
    | True -> False
    | False -> True
(*    | 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 =  
330
331
(*    if equal a b then False  *)
    if a == b then False 
332
333
334
335
336
337
338
339
340
341
342
343
    else match (a,b) with
      | False,_ | _, True -> False
      | a, False -> a
      | True, b -> neg b
      | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
	  let c = X.compare x1 x2 in
	  if c = 0 then
	    split x1
	      ((p1 ++ i1) // (p2 ++ i2))
	      False
	      ((n1 ++ i1) // (n2 ++ i2))
	  else if c < 0 then
344
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
345
346
347
348
349
350
351
352
353
(*	    split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b)  *)
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
	      

  let cup = ( ++ )
  let cap = ( ** )
  let diff = ( // )

354
355
 let rec serialize t = function
    | (True | False) as b -> 
356
	Serialize.Put.bool t true; Serialize.Put.bool t (b == True)
357
358
359
360
361
362
363
364
365
366
367
368
369
370
    | Split (_,x,p,i,n) ->
	Serialize.Put.bool t false;
	X.serialize t x;
	serialize t p;
	serialize t i;
	serialize t n

  let rec cap_atom x pos a = (* Assume that x does not appear in a *)
    match a with
      | False -> False
      | True -> if pos then atom x else neg_atom x
      | Split (_,y,p,i,n) ->
	  let c = X.compare x y in
	  assert (c <> 0);
371
	  if (c < 0) then 
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
	    if pos then split x a False False
	    else split x False False a
	  else split y (cap_atom x pos p) (cap_atom x pos i) (cap_atom x pos n)


    
  let rec deserialize t =
    if Serialize.Get.bool t then
      if Serialize.Get.bool t then True else False
    else
      let x = X.deserialize t in
      let p = deserialize t in
      let i = deserialize t in
      let n = deserialize t in
      (cap_atom x true p) ++ i ++ (cap_atom x false n)
      (* split x p i n is not ok, because order of keys might have changed! *)
  
389
(*
390
  let diff x y =
391
    let d = diff x y in
392
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
393
394
395
396
397
398
399
400
401
      dump x dump y dump d;  
    d

  let cap x y =
    let d = cap x y in
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
      dump x dump y dump d;  
    d
*)
402
end
403
404


405
406
407
408
409
410
module type S' = sig
  include S
  type bdd = False | True | Br of elem * t * t
  val br: t -> bdd
end
module MakeBdd(X : Custom.T) =
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
struct
  type elem = X.t
  type t =
    | Zero
    | One
    | Branch of elem * t * t * int * t
  type node = t

  let neg = function
    | Zero -> One | One -> Zero
    | Branch (_,_,_,_,neg) -> neg

  let id = function
    | Zero -> 0
    | One -> 1
    | Branch (_,_,_,id,_) -> id

(* Internalization + detection of useless branching *)
  let max_id = ref 2 (* Must be >= 2 *)
430
  module W = Weak(*Myweak*).Make(
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
    struct
      type t = node
	  
      let hash = function
	| Zero | One -> assert false
	| Branch (v,yes,no,_,_) -> 
	    1 + 17*X.hash v + 257*(id yes) + 65537*(id no)

      let equal x y = (x == y) || match x,y with
	| Branch (v1,yes1,no1,id1,_), Branch (v2,yes2,no2,id2,_) ->
	    (id1 == 0 || id2 == 0) && X.equal v1 v2 && 
	      (yes1 == yes2) && (no1 == no2)
	| _ -> assert false
    end)
  let table = W.create 16383
  type branch = 
      { v : X.t; yes : node; no : node; mutable id : int; neg : branch }
  let mk v yes no =
    if yes == no then yes
    else
      let rec pos = Branch (v,yes,no,0,Branch (v,neg yes,neg no,0,pos)) in
      let x = W.merge table pos in
      let pos : branch = Obj.magic x in
      if (pos.id == 0) 
      then (let n = !max_id in
	    max_id := succ n;
	    pos.id <- n;
	    pos.neg.id <- (-n));
      x

  let atom v = mk v One Zero

  let dummy = Obj.magic (ref 0)
  let memo_size = 16383
  let memo_keys = Array.make memo_size (Obj.magic dummy)
  let memo_vals = Array.make memo_size (Obj.magic dummy)
  let memo_occ = Array.make memo_size 0

  let eg2 (x1,y1) (x2,y2) = x1 == x2 && y1 == y2
  let rec cup x1 x2 = if (x1 == x2) then x1 else match x1,x2 with
    | One, x | x, One -> One
    | Zero, x | x, Zero -> x
    | Branch (v1,yes1,no1,id1,neg1), Branch (v2,yes2,no2,id2,neg2) ->
	if (x1 == neg2) then One
	else
	  let k,h = 
	    if id1<id2 then (x1,x2),id1+65537*id2 else (x2,x1),id2+65537*id1 in
	  let h = (h land max_int) mod memo_size in
	  let i = memo_occ.(h) in
	  let k' = memo_keys.(h) in
	  if (k' != dummy) && (eg2 k k') 
	  then (memo_occ.(h) <- succ i; memo_vals.(h))
	  else 
	    let r = 
              let c = X.compare v1 v2 in
	      if (c = 0) then mk v1 (cup yes1 yes2) (cup no1 no2)
	      else if (c < 0) then mk v1 (cup yes1 x2) (cup no1 x2)
	      else mk v2 (cup yes2 x1) (cup no2 x1) in
	    if (i = 0) then (memo_keys.(h) <- k; memo_vals.(h) <- r;
			     memo_occ.(h) <- 1)
	    else memo_occ.(h) <- pred i;
	    r
  
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
  let rec dump ppf = function
    | One -> Format.fprintf ppf "+"
    | Zero -> Format.fprintf ppf "-"
    | Branch (x,p,n,id,_) -> 
	Format.fprintf ppf "%i:%a(@[%a,%a@])" 
	  id
	  X.dump x dump p dump n

(*
  let cup x y =
    let d = cup x y in
    Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX+Z = %a@\n"
      dump x dump y dump d;  
    d
*)
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
	  

  let cap x1 x2 = neg (cup (neg x1) (neg x2))
  let diff x1 x2 = neg (cup (neg x1) x2)


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



  let rec print f ppf = function
    | One -> Format.fprintf ppf "Any"
    | Zero -> Format.fprintf ppf "Empty"
    | Branch (x,p,n,_,_) ->
	let flag = ref false in
	let b () = if !flag then Format.fprintf ppf " | " else flag := true in
	(match p with 
	   | One -> b(); Format.fprintf ppf "%a" f x
	   | Zero -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
	(match n with 
	   | One -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | Zero -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
	
  let print a f = function
    | One -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | Zero -> []
    | c -> [ fun ppf -> print f ppf c ]
	
  let rec get accu pos neg = function
    | One -> (pos,neg) :: accu
    | Zero -> accu
    | Branch (x,p,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
	accu
	  
  let get x = get [] [] [] x
		
  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | One -> full
      | Zero -> empty
      | Branch(x,p,n,_,_) ->
	  let p = cap (atom x) (aux p)
	  and n = diff (aux n) (atom x) in
	  cup p n
    in
    aux b
      
  let empty = Zero
  let full = One

  let rec serialize t = function
    | (Zero | One) as b -> 
568
	Serialize.Put.bool t true; Serialize.Put.bool t (b == One)
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
    | Branch (x,p,n,_,_) ->
	Serialize.Put.bool t false;
	X.serialize t x;
	serialize t p;
	serialize t n

  let rec deserialize t =
    if Serialize.Get.bool t then
      if Serialize.Get.bool t then One else Zero
    else
      let x = X.deserialize t in
      let p = deserialize t in
      let n = deserialize t in

      let x = atom x in
      cup (cap x p) (cap (neg x) n)

      (* mk x p n is not ok, because order of keys might have changed!
	 OPT TODO: detect when this is ok *)

  let trivially_disjoint x y = neg x == y  
  let compare x y = compare (id x) (id y)
  let equal x y = x == y
  let hash x = id x
  let check x = ()
594
595
596
597
598
599

  type bdd = False | True | Br of elem * t * t 
  let br = function
    | Zero -> False | One -> True | Branch (x,p,n,_,_) -> Br (x,p,n)
end

600
(*
601
module Simplify(X : Custom.T) = struct
602
603
  type elem = X.t

604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
  module V = SortedList.Make(X)

  type f = {
    pos: V.t;
    neg: V.t;
    subs: fset;
    mutable id: int  (* unique id for hash consing *)
  }
  and fset =
    | Empty
    | Leaf of f
    | Branch of int * int * fset * fset

  type t = PosF of f | NegF of f | PosV of X.t | NegV of X.t | Zero | One

  let id k = k.id

  module F = struct
    let empty = Empty
    let is_empty = function Empty -> true | _ -> false
    let singleton k = Leaf k
    let zero_bit k m = (k land m) == 0
    let rec mem k = function
      | Empty -> false
      | Leaf j -> k == j
      | Branch (_, m, l, r) -> mem k (if zero_bit (id k) m then l else r)
    let lowest_bit x = x land (-x)
    let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
    let mask p m = p land (m-1)
    let join (p0,t0,p1,t1) = 
      let m = branching_bit p0 p1 in
      if zero_bit p0 m then Branch (mask p0 m, m, t0, t1)
      else Branch (mask p0 m, m, t1, t0)
    let match_prefix k p m = (mask k m) == p
    let add k t =
      let rec ins = function
	| Empty -> Leaf k
	| Leaf j as t -> if j== k then t else join (id k, Leaf k, id j, t)
	| Branch (p,m,t0,t1) as t ->
            if match_prefix (id k) p m then
              if zero_bit (id k) m then Branch (p, m, ins t0, t1)
              else Branch (p, m, t0, ins t1)
            else join (id k, Leaf k, p, t)
      in
      ins t
649
	
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
    let rec union s t = match s,t with
      | Empty, t  -> t
      | t, Empty  -> t
      | Leaf k, t -> add k t
      | t, Leaf k -> add k t
      | (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
	  if m == n && match_prefix q p m then 
	    Branch (p, m, union s0 t0, union s1 t1)
	  else if m < n && match_prefix q p m then
            if zero_bit q m then Branch (p, m, union s0 t, s1)
            else Branch (p, m, s0, union s1 t)
	  else if m > n && match_prefix p q n then
            if zero_bit p n then Branch (q, n, union s t0, t1)
            else Branch (q, n, t0, union s t1)
	  else join (p, s, q, t)
	    
    let rec subset s1 s2 = match s1,s2 with
      | Empty, _ -> true
      | _, Empty -> false
      | Leaf k1, _ -> mem k1 s2
      | Branch _, Leaf _ -> false
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
	  if m1 == m2 && p1 == p2 then subset l1 l2 && subset r1 r2
	  else if m1 > m2 && match_prefix p1 p2 m2 then
            if zero_bit p1 m2 then subset l1 l2 && subset r1 l2
            else subset l1 r2 && subset r1 r2
	  else
            false
	      
    let branch = function
      | (_,_,Empty,t) -> t
      | (_,_,t,Empty) -> t
      | (p,m,t0,t1)   -> Branch (p,m,t0,t1)
	  
    let rec remove k = function
      | Empty -> Empty
      | Leaf j as t -> if k == j then Empty else t
      | Branch (p,m,t0,t1) as t ->
          if match_prefix (id k) p m then 
	    if zero_bit (id k) m then branch (p, m, remove k t0, t1)
            else branch (p, m, t0, remove k t1)
          else t
	    
    let rec inter s1 s2 = match s1,s2 with
      | Empty, _ -> Empty
      | _, Empty -> Empty
      | Leaf k1, _ -> if mem k1 s2 then s1 else Empty
      | _, Leaf k2 -> if mem k2 s1 then s2 else Empty
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
	  if m1 == m2 && p1 == p2 then union (inter l1 l2) (inter r1 r2)
	  else if m1 < m2 && match_prefix p2 p1 m1 then
            inter (if zero_bit p2 m1 then l1 else r1) s2
	  else if m1 > m2 && match_prefix p1 p2 m2 then
            inter s1 (if zero_bit p1 m2 then l2 else r2)
	  else Empty
	    
    let rec split s1 s2 = match s1,s2 with
      | Empty, _ -> Empty,Empty,s2
      | _, Empty -> s1,Empty,Empty
      | Leaf k1, _ -> if mem k1 s2 then Empty,s1,(remove k1 s2) else s1,Empty,s2
      | _, Leaf k2 -> if mem k2 s1 then (remove k2 s1),s2,Empty else s1,Empty,s2
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
	  if m1 == m2 && p1 == p2 then 
	    let x1,x12,x2 = split l1 l2
	    and y1,y12,y2 = split r1 r2 in
	    union x1 y1, union x12 y12, union x2 y2
	  else if m1 < m2 && match_prefix p2 p1 m1 then
	    if zero_bit p2 m1 
	    then let x1,x12,x2 = split l1 s2 in union x1 r1, x12, x2
	    else let x1,x12,x2 = split r1 s2 in union l1 x1, x12, x2
	  else if m2 < m1 && match_prefix p1 p2 m1 then
	    if zero_bit p1 m2 
	    then let x1,x12,x2 = split l2 s1 in x1, x12, union x2 r2
	    else let x1,x12,x2 = split r1 s2 in x1, x12, union l2 x2
	  else (s1,Empty,s2)

    let rec diff s1 s2 = match s1,s2 with
      | Empty, _ -> Empty
      | _, Empty -> s1
      | Leaf k1, _ -> if mem k1 s2 then Empty else s1
      | _, Leaf k2 -> remove k2 s1
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
	  if m1 == m2 && p1 == p2 then union (diff l1 l2) (diff r1 r2)
	  else if m1 < m2 && match_prefix p2 p1 m1 then
            if zero_bit p2 m1 then union (diff l1 s2) r1
            else union l1 (diff r1 s2)
	  else if m1 > m2 && match_prefix p1 p2 m2 then
            if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
	  else s1

    let rec intersect s1 s2 = match s1,s2 with
      | Empty, _ -> false
      | _, Empty -> false
      | Leaf k1, _ -> mem k1 s2
      | _, Leaf k2 -> mem k2 s1
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
	  if m1 == m2 && p1 == p2 then intersect l1 l2 || intersect r1 r2
	  else if m1 < m2 && match_prefix p2 p1 m1 then
            intersect (if zero_bit p2 m1 then l1 else r1) s2
	  else if m1 > m2 && match_prefix p1 p2 m2 then
            intersect s1 (if zero_bit p1 m2 then l2 else r2)
	  else false

    let disjoint s1 s2 = not (intersect s1 s2)

    let rec equal x y = x == y || match x,y with
      | Leaf k1, Leaf k2 -> k1 == k2
      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
          p1 == p2 && m1 == m2 && (equal l1 l2) && (equal r1 r2)
      | _ -> false

    let rec hash = function
      | Empty -> 0
      | Leaf k -> 1 + 3 * (id k)
      | Branch (p,m,l,r) -> 
	  2 + 3 * p + 257 * m + 16387 * (hash l) + 1048577 * (hash r)

    let rec iter f = function
      | Empty -> ()
      | Leaf k -> f k
      | Branch (_,_,t0,t1) -> iter f t0; iter f t1

    let rec fold f s accu = match s with
      | Empty -> accu
      | Leaf k -> f k accu
      | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)

    let rec card f s accu = match s with
      | Empty -> accu
      | Leaf k -> f k accu
      | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)

    let rec cardinal = function
      | Empty -> 0
      | Leaf _ -> 1
      | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1

    let rec allvars = function
      | Empty -> V.empty
      | Leaf f -> f.allvars
      | Branch (_,_,t0,t1) -> V.cup (allvars t0) (allvars t1)
  end



  let print_f px =
796
797
798
    let rec aux ppf f =
      let first = ref true in
      let sep () = if !first then first := false else Format.fprintf ppf "|" in
799
800
801
      V.iter (fun x -> sep (); Format.fprintf ppf "%a" px x) f.pos;
      V.iter (fun x -> sep (); Format.fprintf ppf "~%a" px x) f.neg;
      F.iter (fun f -> sep (); Format.fprintf ppf "~(@[%a@])" aux f) f.subs;
802
803
804
805
      if !first then Format.fprintf ppf "."
    in
    fun ppf f -> (*allvars ppf f; *) aux ppf f

806
807
808
809
810
811
812
813
814
  let print_t px ppf = function
    | PosV f -> Format.fprintf ppf "%a" px f
    | NegV f -> Format.fprintf ppf "~%a" px f
    | PosF f -> Format.fprintf ppf "%a" (print_f px) f
    | NegF f -> Format.fprintf ppf "~(%a)" (print_f px) f
    | Zero -> Format.fprintf ppf "0"
    | One -> Format.fprintf ppf "1"

  let dump = print_f
815
816
    (fun ppf i -> Format.fprintf ppf "%i" (X.hash i))

817
818
819
820
821
822
823
824
825
826
  let dump_vars ppf v =
    let first = ref true in
    let sep () = if !first then first := false else Format.fprintf ppf "|" in
    V.iter (fun x -> sep (); Format.fprintf ppf "%i" (X.hash x)) v
    
  let dump_subs ppf v =
    let first = ref true in
    let sep () = if !first then first := false else Format.fprintf ppf "|" in
    F.iter (fun f -> sep (); Format.fprintf ppf "#%i:%a" f.id dump f) v
    
827
828

(*
829
830
831
832
833
834
835
836
837
  let rec form f =
    let rec aux1 accu = function
      | x::l -> aux1 (B.cup accu (B.atom x)) l
      | [] -> accu in
    let rec aux2 accu = function
      | x::l -> aux2 (B.cup accu (B.diff B.full (B.atom x))) l
      | [] -> accu in
    let accu = aux2 (aux1 B.empty f.pos) f.neg in
    F.fold (fun f accu -> B.cup accu (B.diff B.full (form f))) f.subs accu
838
      
839
840
841
842
843
  let get f = match f.get with Some x -> x | None ->
    let r = B.get (form f) in
    f.get <- Some r;
    r
*)
844

845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
  (* Hash-consing *)
  module W = Weak.Make(
    struct
      type t = f
      let hash f = 
	(V.hash f.pos) 
	+ 257 * (V.hash f.neg) 
	+ 65537 * (F.hash f.subs)

      let equal f1 f2 =
	V.equal f1.pos f2.pos 
	&& V.equal f1.neg f2.neg 
	&& F.equal f1.subs f2.subs
    end
  )

  let tmpl = { pos = V.empty; neg = V.empty; subs = F.empty; id = 0 }

  let mk_f = let id = ref 0 and tbl = W.create 16387 in
  fun pos neg subs ->
    assert (V.length pos + V.length neg + F.cardinal >= 2);
    let f = W.merge tbl { pos = pos; neg = neg; subs = subs; id = 0 } in
    if f.id = 0 then f.id <- (incr id; !id);
    f
869
870

  let neg = function
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
    | PosF x -> NegF x
    | NegF x -> PosF x
    | PosV x -> NegV x
    | NegV x -> PosV x
    | Zero -> One
    | One -> Zero

  let only_vars pos neg = match pos,neg with
    | [x],[] -> PosV x
    | [],[x] -> NegV x
    | [], [] -> Zero
    | _ -> PosF (mk_f pos neg Empty)

  let mk pos neg subs = match pos,neg,subs with
    | [],[],Empty  -> Zero
    | [x],[],Empty -> PosV x
    | [],[x],Empty -> NegV x
    | [],[],Leaf f -> NegF f
    | _ -> PosF (mk_f pos neg subs)

  let cap t1 t2 = match t1,t2 with 
    | Zero, t | t, Zero -> Zero
    | One, t | t, One -> t
    | PosV x, PosV y -> 
	let c = X.compare x y in
	if c = 0 then t1 
	else PosF (mk_f (if c <0 then [x;y] else [y;x]) [] Empty)
    | NegV x, NegV y ->
	let c = X.compare x y in
	if c = 0 then t1 
	else PosF (mk_f [] (if c <0 then [x;y] else [y;x]) Empty)
    | PosV x, NegV y 
    | NegV y, PosV x -> if X.equal x y then Zero else PosF (mk_f [x] [y] Empty)
    | PosF f, PosF g -> cap_f f g
    | PosF f, NegF g
    | NegF g, PosF f -> diff_f f g
    | NegF f, NegF g -> nor_f f g
    | (PosF f as t), PosV x
    | PosV x, (PosF f as t) -> 
	if V.mem x f.pos then t
	else if V.mem x f.neg then Zero
	else PosF (mk_f 

	  PosF { tmpl with pos = [x]; neg = [y]; 
		   allvars = if c <0 then [x;y] else [y;x] }
    | PosV x, (PosF f as t)| (PosF f as t), PosV x ->
	if V.mem f.pos x then t 
	else if V.mem f.neg x then One
	else if V.mem f.allvars x
	then zero_var_mk x (V.add x f.pos) f.neg f.subs
	else
	  PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
	      allvars = V.add x f.allvars; subs = f.subs }
    | PosV x, NegF f | NegF f, PosV x ->
	if V.mem f.neg x then One
	else if V.mem f.allvars x 
	then match zero_var_mk x f.pos f.neg f.subs with
	  | NegF f -> PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
			       allvars = V.add x f.allvars; subs = f.subs }
	  | PosF f -> PosF { tmpl with pos = [x];
			       allvars = V.add x f.allvars; subs = Leaf f }
	  | One -> PosV x
	  | Zero -> One
	  | PosV y -> 
	      PosF { tmpl with pos = [x]; neg = [y];
		       allvars = if X.compare x y <0 then [x;y] else [y;x] }
	  | NegV y -> 
	      let vs = if X.compare x y < 0 then [x;y] else [y;x] in
	      PosF { tmpl with pos = vs; allvars = vs }
	else PosF { tmpl with pos = V.add x f.pos; neg = f.neg;
		      allvars = V.add x f.allvars; subs = f.subs }
    | NegF x, _ -> assert false
    | PosF x, _ -> assert false
	
(*
946

947
948
  (* Memoization *)
  type memo = { key1 : int array; key2 : int array; res  : f array }
949

950
951
  let new_memo n = { key1 = Array.create n (-1); key2 = Array.create n (-1);
		     res = Array.create n tmpl }
952
953
954
955
956
957
958
959

  let memo_cup = new_memo 16383

  let memo_bin tbl g f1 f2 =
    let h = ((f1.id + 1027 * f2.id) land max_int) mod (Array.length tbl.res) in
    if (tbl.key1.(h) == f1.id) && (tbl.key2.(h) == f2.id) then
      tbl.res.(h)
    else
960
      let r = g f1 f2 in
961
962
963
964
965
966
      tbl.key1.(h) <- f1.id;
      tbl.key2.(h) <- f2.id;
      tbl.res.(h) <- r;
      r


967
968
  let empty = mk V.empty V.empty F.empty
  let full = mk V.empty V.empty (F.singleton empty)
969

970
971
972
973
974
975
976
977
978
979
980
981
  let rec check f =
    F.iter 
      (fun g -> 
	 let n1 = V.length g.pos and n2 = V.length g.neg and n3 =
	   F.fold (fun _ x -> succ x) g.subs 0 in
	 if (n1 + n2 + n3 < 2) && f != full then
	   (Format.fprintf Format.std_formatter "BUG f=%a g=%a pos=%i neg=%i subs=%i@." dump f dump g n1 n2 n3; 
	    assert false);
	 check g;
	 assert(V.disjoint f.pos g.allvars);
	 assert(V.disjoint f.neg g.allvars)) f.subs;
    assert (V.disjoint f.pos f.neg)
982

983
984
  let posvar x = mk (V.singleton x) V.empty F.empty
  let negvar x = mk V.empty (V.singleton x) F.empty
985

986
987
988
989
990
  let neg = function
    | { pos = [x]; neg = []; subs = Empty } -> negvar x
    | { pos = []; neg = [x]; subs = Empty } -> posvar x
    | { pos = []; neg = []; subs = Leaf f } -> f
    | f -> mk V.empty V.empty (F.singleton f)
991

992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
(*
  let neg f =
    let r = neg f in
    Format.fprintf Format.std_formatter
      "NEG %a ===>%a@." dump f dump r; 
    check f; check r;
    r 
*)

  let trivially_disjoint f1 f2 =
    f1 == empty || f2 == empty || 
      match f1,f2 with
	| { pos=[x]; neg=[]; subs=Empty }, { pos=[]; neg=[y]; subs=Empty }
	| { pos=[]; neg=[x]; subs=Empty }, { pos=[y]; neg=[]; subs=Empty } ->
	    X.equal x y
	| { pos=[]; neg=[]; subs=Leaf f }, _ when f == f2 -> true
	| _, { pos=[]; neg=[]; subs=Leaf f } when f == f1 -> true
	| _ -> false
	    

  let rec mk_subs pos neg vpos vneg (spos:fset) (sneg:fset) subs =
    (* pos and neg cannot appears in subs *)
    (* invariant: pos <= vneg, neg <= vpos *)

    let loop = ref true and subs = ref subs and pos = ref pos and neg = ref neg and
	vpos = ref vpos and vneg = ref vneg and spos = ref spos and sneg = ref sneg
1018
1019
    in

1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
    (* let check_inv () = 
       Format.fprintf Format.std_formatter
	"mk_subs pos=%a neg=%a vpos=%a vneg=%a spos=%a sneg=%a subs=%a:@."
	dump_vars !pos dump_vars !neg dump_vars !vpos dump_vars !vneg
	dump_subs !spos	dump_subs !sneg	dump_subs !subs;
      assert(V.disjoint !pos !neg); assert(V.subset !pos !vneg);
      assert(V.subset !neg !vpos); assert(V.disjoint !vpos !vneg);
      assert(F.disjoint !spos !sneg); assert(F.disjoint !spos !subs);
      assert(F.disjoint !sneg !subs) in check_inv (); *)

    (* OPT TODO: maintain (union subs spos) ? *)
    let aux f = 
      if F.mem f !sneg then raise Exit 
      else if F.mem f !spos then ()
      else let f' = filter_sub !vpos !vneg (F.union !subs !spos) !sneg f in
      if f == f' then ()
      else let () = subs := F.remove f !subs; spos := F.add f !spos in 
      if f' == empty then raise Exit
      else if f' == full then ()
      else loop := true; match f' with
	| { pos = []; neg = [v]; subs = Empty } -> 
	    pos := V.add v !pos; vneg := V.add v !vneg
	| { pos = [v]; neg = []; subs = Empty } -> 
	    neg := V.add v !neg; vpos := V.add v !vpos
	| { pos = []; neg = []; subs = Leaf f'' } ->
(*	    assert(F.disjoint f''.subs !spos); *)
	    subs := F.union f''.subs !subs;
	    pos := V.cup !pos f''.pos;
	    vneg := V.cup !vneg f''.pos;
	    neg := V.cup !neg f''.neg;
	    vpos := V.cup !vpos f''.neg;
	    sneg := F.add f'' !sneg;
	| _ ->
(*	    assert (not (F.mem f' !spos)); *)
	    subs := F.add f' !subs
1055
    in
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
    if (try while !loop do loop := false; F.iter aux !subs done; false 
	with Exit -> true) then full
    else let f = mk !pos !neg !subs in
    if F.mem f !sneg then empty
    else if F.mem f !spos then full
    else f

      
  and filter_sub vpos vneg spos sneg f =
    if V.disjoint f.allvars vpos && V.disjoint f.allvars vneg &&
      F.disjoint f.allsubs spos && F.disjoint f.allsubs sneg
    then f
    else if not (V.disjoint vpos f.pos) || not (V.disjoint vneg f.neg)
      || F.intersect sneg f.subs then full
1070
    else
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
      let pos = V.diff f.pos vneg in
      let neg = V.diff f.neg vpos in
      mk_subs pos neg (V.cup neg vpos) (V.cup pos vneg) spos sneg 
	(F.diff f.subs spos)

  let real_cup f1 f2 =
    let pos = V.cup f1.pos f2.pos in
    let neg = V.cup f1.neg f2.neg in
    let subs = F.union f1.subs f2.subs in
    mk_subs pos neg neg pos F.empty F.empty subs

  let trivially_subset f1 f2 =
    V.subset f1.pos f2.pos && V.subset f1.neg f2.neg && F.subset f1.subs f2.subs

  let trivially_cover f1 f2 =
    F.mem f1 f2.subs || F.mem f2 f2.subs 
    || not (V.disjoint f1.pos f2.neg)
    || not (V.disjoint f1.neg f2.pos)

  let no_overlap f1 f2 =
    V.disjoint f1.pos f2.pos && V.disjoint f1.neg f2.neg 
    && F.disjoint f1.subs f2.subs

  let remove_overlap f1 f2 = 
    let pos1 = V.diff f1.pos f2.pos in
    let neg1 = V.diff f1.neg f2.neg in
    let subs1 = F.diff f1.subs f2.subs in
    mk pos1 neg1 subs1

  let split_overlap f1 f2 =
    let pos1,pos,pos2 = V.split f1.pos f2.pos in
    let neg1,ne,neg2 = V.split f1.neg f2.neg in
    let sub1,sub,sub2 = F.split f1.subs f2.subs in
    let f1 = mk pos1 neg1 sub1 in
    let f2 = mk pos2 neg2 sub2 in
    let f  = mk pos  ne  sub in
    f1,f,f2

  let rec cup f1 f2 = 
    if (f1 == f2) then f1 else if (f1 == full) || (f2 == full)
    then full else if (f1 == empty) then f2 else if (f2 == empty) then f1 
    else match f1,f2 with
      | { pos=[];neg=[];subs=Leaf f1' }, { pos=[];neg=[];subs=Leaf f2' } -> 
	  if trivially_subset f1' f2' then f1
	  else if trivially_subset f2' f1' then f2
	  else if no_overlap f1' f2' 
	  then mk [] [] (F.union (F.singleton f1') (F.singleton f2'))
	  else 
	    let f1,f,f2 = split_overlap f1' f2' in
	    neg (cup f (cap f1 f2))
(* TODO: special cases with variables *)
      |  f1, ({ pos=[];neg=[];subs=Leaf f2 } as f0)
      | ({ pos=[];neg=[];subs=Leaf f2 } as f0), f1 ->
	  if f1 == f2 then full else
	    if trivially_cover f1 f2 then f1
	    else if trivially_subset f2 f1 then full
	    else if no_overlap f1 f2 then 
	      mk_subs f1.pos f1.neg f1.neg f1.pos F.empty F.empty (F.add f2 f1.subs)
	    else cup f1 (neg (remove_overlap f2 f1)) 
      | f1,f2 ->
	  if trivially_subset f1 f2 then f2
	  else if trivially_subset f2 f1 then f1
	  else if trivially_cover f1 f2 then full
	  else if f1.id < f2.id then memo_bin memo_cup real_cup f1 f2
	  else memo_bin memo_cup real_cup f2 f1

  and cap f1 f2 = neg (cup (neg f1) (neg f2))
(*
    if (f1 == f2) then f1 else if (f1 == empty) || (f2 == empty)
    then empty else if (f1 == full) then f2 else if (f2 == full) then f1 
    else match f1,f2 with
      | { pos=[x]; neg=[]; subs=Empty }, { pos=[y]; neg=[]; subs=Empty } ->
	  mk [] [] (Leaf (mk (if X.compare x y < 0 then [x;y] else [y;x]) [] Empty))
      | { pos=[x]; neg=[]; subs=Empty }, { pos=[]; neg=[y]; subs=Empty }
      | { pos=[]; neg=[y]; subs=Empty }, { pos=[x]; neg=[]; subs=Empty } ->
	  if X.equal x y then empty
	  else mk [] [] (Leaf (mk [x] [y] Empty))
      | ({ pos=[x]; neg=[]; subs=Empty } as fx), f
      | f, ({ pos=[x]; neg=[]; subs=Empty } as fx) ->
	  Format.fprintf Format.std_formatter
	    "%!!! %a AND %a ===> %b,%b,%b,%a@." dump f1 dump f2
	    (V.mem f.allvars x) (V.mem f.pos x ) (V.mem f.neg x)
	    dump (neg (mk_subs [x] [] [] [x] F.empty F.empty (Leaf f)));
	  if V.mem f.allvars x then
	    if V.mem f.pos x then fx
	    else if V.mem f.neg x then cap fx (mk f.pos (V.remove x f.neg) f.subs)
	    else neg (mk_subs [] [x] [x] [] F.empty F.empty (Leaf f))
	  else mk [] [] (Leaf (mk [] [x] (Leaf f)))
      | ({ pos=[]; neg=[x]; subs=Empty } as fx), f
      | f, ({ pos=[]; neg=[x]; subs=Empty } as fx) ->
	  if V.mem f.allvars x then
	    if V.mem f.neg x then fx
	    else if V.mem f.pos x then cap fx (mk (V.remove x f.pos) f.neg f.subs)
	    else neg (mk_subs [x] [] [] [x] F.empty F.empty (Leaf f))
	  else mk [] [] (Leaf (mk [x] [] (Leaf f)))

      | { pos=[];neg=[];subs=Leaf f1' }, { pos=[];neg=[];subs=Leaf f2' } -> 
	  if trivially_subset f1' f2' then f2
	  else if trivially_subset f2' f1' then f1
	  else if trivially_cover f1' f2' then empty
	  else if f1'.id < f2'.id then neg (memo_bin memo_cup real_cup f1' f2')
	  else neg (memo_bin memo_cup real_cup f2' f1')
      |  f1, ({ pos=[];neg=[];subs=Leaf f2 } as f0)
      | ({ pos=[];neg=[];subs=Leaf f2 } as f0), f1 ->
	  if f1 == f2 then empty else
	    if trivially_cover f1 f2 then f0
	    else if trivially_subset f1 f2 then empty
	    else if no_overlap f1 f2 then 
	      neg (mk_subs f2.pos f2.neg f2.neg f2.pos F.empty F.empty 
		     (F.add f1 f2.subs))
	    else cap (remove_overlap f1 f2) f0
      | f1,f2 ->
	  if trivially_subset f1 f2 then f1
	  else if trivially_subset f2 f1 then f2
	  else if no_overlap f1 f2
	  then mk [] [] (F.singleton 
			   (mk [] [] (F.union (F.singleton f1) (F.singleton f2))))
	  else 
	    let f1,f,f2 = split_overlap f1 f2 in
	    cup f (cap f1 f2)
*)
1192

1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
(*
  let cap f1 f2 =
    let r = cap f1 f2 in
    if (f1 != full) && (f2 != full) && ((f1.subs != Empty) || (f2.subs != Empty)) then
      Format.fprintf Format.std_formatter
	"%a AND %a ===>%a@." dump f1 dump f2 dump r;
    check r;
    r
*)	 
(*   
  let cup f1 f2 =
    let r = cup f1 f2 in
    if (f1 != empty) && (f1 != full) && (f2 != empty) && (f2 != full)
    then Format.fprintf Format.std_formatter
      "%a \\/ %a ===>%a@." dump f1 dump f2 dump r;
    check f1; check f2; check r;
    r 
*)
(*  let cap f1 f2 = 
    if (f1 == empty) || (f2 == empty) then empty
    else if f1 == f2 then f1
    else if trivially_subset f1 f2 then f1
    else if trivially_subset f2 f1 then f2
    else 
    neg (cup (neg f1) (neg f2)) *)

  let diff f1 f2 = neg (cup (neg f1) f2)
    
1221

1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
    
(*
  let cap f1 f2 =
    let r = cap f1 f2 in
    Format.fprintf Format.std_formatter
      "%a /\\ %a ===>%a@." dump f1 dump f2 dump r;
    check f1; check f2; check r;
    r
  let diff f1 f2 =
    let r = diff f1 f2 in
    Format.fprintf Format.std_formatter
      "%a \\  %a ===>%a@." dump f1 dump f2 dump r;
    check f1; check f2; check r;
    r
*)
1237

1238
(*
1239
  let simplify f =
1240
1241
1242
1243
1244
    let g =
      if (n = 0) then
	cup (elim [x,false] f) (cap (posvar x) (elim [x,true] f))
      else if (p = 0) then
	cup (elim [x,true] f) (cap (negvar x) (elim [x,false] f))
1245
      else
1246
1247
1248
1249
1250
1251
	cup (cap (negvar x) (elim [x,false] f)) 
	  (cap (posvar x) (elim [x,true] f))
    in
    Format.fprintf Format.std_formatter
      "Simplify %a ==> %a@." dump f dump g;
    g
1252
    with Not_found -> f
1253
*)
1254
1255
1256
1257

  let hash f = f.id (* B.hash (form f) *)
  let equal f1 f2 = (f1 == f2) (* || B.equal (form f1) (form f2) *)
  let compare f1 f2 = f1.id - f2.id (* B.compare (form f1) (form f2) *)
1258
1259

(*
1260
1261
1262
1263
1264
  let hash f = B.hash (form f)
  let equal f1 f2 = (f1 == f2) || B.equal (form f1) (form f2)
  let compare f1 f2 = B.compare (form f1) (form f2)
*)

1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
  let rec iter g =
    let rec aux f =
      V.iter g f.pos;
      V.iter g f.neg;
      F.iter aux f.subs
    in
    aux

  let compute ~empty ~full ~cup ~cap ~diff ~atom =
    let rec aux f =
      let rec aux1 accu = function
	| x::l -> aux1 (cup accu (atom x)) l
	| [] -> accu in
      let rec aux2 accu = function
	| x::l -> aux2 (cup accu (diff full (atom x))) l
	| [] -> accu in
      let accu = aux2 (aux1 empty f.pos) f.neg in
      F.fold (fun f accu -> cup accu (diff full (aux f))) f.subs accu
    in aux
  (*    B.compute ~empty ~full ~cup ~cap ~diff ~atom (form f) *)
1285
1286

  let rec serialize s f =
1287
1288
1289
    V.serialize s f.pos;
    V.serialize s f.neg;
    Serialize.Put.list serialize s (F.fold (fun x accu -> x::accu) f.subs [])
1290
1291

  let rec deserialize s =
1292
1293
    let pos = V.deserialize s in
    let neg = V.deserialize s in
1294
    let subs = Serialize.Get.list deserialize s in
1295
1296
1297
1298
1299
1300
1301
1302
    let f = mk pos neg (List.fold_left (fun accu x -> F.add x accu) F.empty subs) in
(*    check f; *)
    f

  let atom = posvar

  type t = f
*)
1303
end
1304
*)
1305