bool.ml 24.2 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
  val get': t -> (elem list * (elem list) list) list
12

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

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

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

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

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

33 34
end

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

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

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

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

57
  let rec compare a b =
58
    if (a == b) then 0
59 60
    else match (a,b) with
      | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
61
	  if h1 < h2 then -1 else if h1 > h2 then 1
62 63
	  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
64
	  else let c = compare i1 i2 in if c <> 0 then c
65 66 67 68 69
	  else compare n1 n2
      | True,_  -> -1
      | _, True -> 1
      | False,_ -> -1
      | _,False -> 1
70 71


72 73 74 75 76
  let rec hash = function
    | True -> 1
    | False -> 0
    | Split(h, _,_,_,_) -> h

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

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

  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
102 103 104 105 106
    | True -> Format.fprintf ppf "⊤"
    | False -> Format.fprintf ppf "⊥"
    | Split (_,x, p,i,n) ->
      Format.fprintf ppf "@[@[%a@][@[<hov>%a,@\n%a,@\n%a@]]@]"
	X.dump x dump p dump i dump n
107

108 109 110 111 112 113
  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
114
	(match p with
115 116 117
	   | True -> b(); Format.fprintf ppf "%a" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
118
	(match i with
119 120 121
	   | True -> assert false;
	   | False -> ()
	   | _ -> b(); print f ppf i);
122
	(match n with
123 124 125
	   | True -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | False -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
126

127 128 129 130
  let print a f = function
    | True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | False -> []
    | c -> [ fun ppf -> print f ppf c ]
131 132


133 134 135 136
  let rec get accu pos neg = function
    | True -> (pos,neg) :: accu
    | False -> accu
    | Split (_,x, p,i,n) ->
137
	(*OPT: can avoid creating this list cell when pos or neg =False *)
138 139 140 141
	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
142

143
  let get x = get [] [] [] x
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161

  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 ->
(*	      if (List.length l > 1) then (print_int (List.length l); flush stdout); *)
	      let accu = get' accu pos (l :: neg) n in
	      get' accu pos neg i
	in
	aux [x] i

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

162 163 164 165 166
  let compute ~empty ~full ~cup ~cap ~diff ~atom b =
    let rec aux = function
      | True -> full
      | False -> empty
      | Split(_,x, p,i,n) ->
167 168 169 170 171
          let x1 = atom x in
          let p = cap x1 (aux p)
          and i = aux i
          and n = diff (aux n) x1 in
          cup (cup p i) n
172 173
    in
    aux b
174

175 176
(* Invariant: correct hash value *)

177
  let split0 x pos ign neg =
178 179 180 181
    Split (compute_hash x pos ign neg, x, pos, ign, neg)

  let empty = False
  let full = True
182 183

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

187 188 189 190
  let rec has_true = function
    | [] -> false
    | True :: _ -> true
    | _ :: l -> has_true l
191

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

196
  let rec split x p i n =
197
    if i == True then True
198 199 200 201
    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
202

203 204 205 206 207 208 209 210
  and simplify a l =
    match a with
      | False -> False
      | True -> if has_true l then False else True
      | 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
211 212
    | [] ->
	let p = simplify p ap
213 214 215
	and n = simplify n an
	and i = simplify i ai in
	if equal p n then p ++ i else split0 x p i n
216
    | b :: l -> s_aux3 a x p i n ap ai an l b
217 218
  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
219 220
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
221
	if equal a b then False
222 223 224 225 226 227 228 229 230 231 232 233 234 235
	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

  and ( ++ ) a b = if a == b then a
  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
236 237 238 239

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

240 241 242 243 244 245
  let rec ( ** ) a b = if a == b then a 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
246
	  split x1
247 248
	    (p1 ** (p2 ++ i2) ++ (p2 ** i1))
	    (i1 ** i2)
249 250
	    (n1 ** (n2 ++ i2) ++ (n2 ** i1))
(*	  if (p2 == True) && (n2 == False)
251 252 253
	  then split x1 (p1 ++ i1) (i1 ** i2) (n1 ** i2)
	  else if (p2 == False) && (n2 == True)
	  then split x1 (p1 ** i2) (i1 ** i2) (n1 ++ i1)
254 255
	  else
	    split x1 ((p1++i1) ** (p2 ++ i2)) False ((n1 ++ i1) ** (n2 ++ i2))
256 257 258
*)
	else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
	else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
259

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

280 281 282
  let rec neg = function
    | True -> False
    | False -> True
283
    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
284 285 286
    | 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, False, False) ->
287 288
	split x False (neg p) True
    | Split (_,x, False, False, n) -> split x True (neg n) False *)
289
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
290 291

  let rec ( // ) a b =
292
(*    if equal a b then False  *)
293
    if a == b then False
294 295 296 297 298 299 300
    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
301
	    if (i2 == False) && (n2 == False)
302 303 304
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
(*	    else if (i2 == False) && (p2 == False)
	    then split x1 (p1 ++ i1) (i1 // n2) (n1 // n2) *)
305
	    else
306
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
307
	  else if c < 0 then
308
	    split x1 (p1 // b) (i1 // b) (n1 // b)
309 310 311
(*	    split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b)  *)
	  else
	    split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2))
312

313 314 315 316 317

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

318
(*
319 320 321 322 323 324 325
  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);
326
	  if (c < 0) then
327 328 329
	    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)
330
*)
331

332

333
(*
334 335 336 337
  let not_triv = function
    | True | False -> false
    | _ -> true

338
  let diff x y =
339
    let d = diff x y in
340 341
    if (not_triv x) && (not_triv y) then
      Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
342
	dump x dump y dump d;
343 344 345 346
    d

  let cap x y =
    let d = cap x y in
347 348
    if (not_triv x) && (not_triv y) then
      Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
349
	dump x dump y dump d;
350
    d
351 352 353 354 355

  let cup x y =
    let d = cup x y in
    if (not_triv x) && (not_triv y) then
      Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX++Z = %a@\n"
356
	dump x dump y dump d;
357
    d
358
*)
359
end
360 361


362
(*
363 364 365 366 367 368
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) =
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387
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 *)
388
  module W = Weak(*Myweak*).Make(
389 390
    struct
      type t = node
391

392 393
      let hash = function
	| Zero | One -> assert false
394
	| Branch (v,yes,no,_,_) ->
395 396 397 398
	    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,_) ->
399
	    (id1 == 0 || id2 == 0) && X.equal v1 v2 &&
400 401 402 403
	      (yes1 == yes2) && (no1 == no2)
	| _ -> assert false
    end)
  let table = W.create 16383
404
  type branch =
405 406 407 408 409 410 411
      { 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
412
      if (pos.id == 0)
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
      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
434
	  let k,h =
435 436 437 438
	    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
439
	  if (k' != dummy) && (eg2 k k')
440
	  then (memo_occ.(h) <- succ i; memo_vals.(h))
441 442
	  else
	    let r =
443 444 445 446 447 448 449 450
              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
451

452 453 454
  let rec dump ppf = function
    | One -> Format.fprintf ppf "+"
    | Zero -> Format.fprintf ppf "-"
455 456
    | Branch (x,p,n,id,_) ->
	Format.fprintf ppf "%i:%a(@[%a,%a@])"
457 458 459 460 461 462 463
	  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"
464
      dump x dump y dump d;
465 466
    d
*)
467

468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484

  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
485
	(match p with
486 487 488
	   | One -> b(); Format.fprintf ppf "%a" f x
	   | Zero -> ()
	   | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
489
	(match n with
490 491 492
	   | One -> b (); Format.fprintf ppf "@[~%a@]" f x
	   | Zero -> ()
	   | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
493

494 495 496 497
  let print a f = function
    | One -> [ fun ppf -> Format.fprintf ppf "%s" a ]
    | Zero -> []
    | c -> [ fun ppf -> print f ppf c ]
498

499 500 501 502 503 504 505 506
  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
507

508
  let get x = get [] [] [] x
509

510 511 512 513 514 515 516 517 518 519
  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
520

521 522 523 524
  let empty = Zero
  let full = One

  let rec serialize t = function
525
    | (Zero | One) as b ->
526
	Serialize.Put.bool t true; Serialize.Put.bool t (b == One)
527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546
    | 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 *)

547
  let trivially_disjoint x y = neg x == y
548 549 550 551
  let compare x y = compare (id x) (id y)
  let equal x y = x == y
  let hash x = id x
  let check x = ()
552

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


559 560
module Make2(X : Custom.T) = struct
  module XSet = Hashset.MakeSet(X)
561

562 563 564 565 566 567
  type 'a s = {
    pos : XSet.t;
    neg : XSet.t;
    sub : 'a;
(*    vars : XSet.t; *)
    hash : int;
568 569
  }

570 571 572
  let tset_equal = ref ()
  let tset_compare = ref ()

573
  module rec TSet : Hashset.SET with type elt = TSet.t s =
574 575 576
    Hashset.MakeSet(
      struct
	type t = TSet.t s
577 578
	let compare t1 t2 =
	  if (t1 == t2) then 0
579 580 581 582 583
	  else let x = t1.hash and y = t2.hash in
	  if x < y then (-1) else if x > y then 1
	  else let c = XSet.compare t1.pos t2.pos in if c <> 0 then c
	  else let c = XSet.compare t1.neg t2.neg in if c <> 0 then c
	  else (Obj.magic !tset_compare) t1.sub t2.sub
584 585

	let equal t1 t2 =
586 587 588 589 590 591 592 593
	  (t1 == t2) ||
	    (t1.hash == t2.hash &&
	       XSet.equal t1.pos t2.pos &&
	       XSet.equal t1.neg t2.neg &&
	       (Obj.magic !tset_equal) t1.sub t2.sub)

	let hash t = t.hash
      end)
594 595

  let () =
596 597
    tset_compare := Obj.magic TSet.compare;
    tset_equal := Obj.magic TSet.equal
598

599 600
  type elem = X.t
  type t = TSet.t s
601

602 603
  let compare t1 t2 =
    if (t1 == t2) then 0
604 605 606 607 608
    else let x = t1.hash and y = t2.hash in
    if x < y then (-1) else if x > y then 1
    else let c = XSet.compare t1.pos t2.pos in if c <> 0 then c
    else let c = XSet.compare t1.neg t2.neg in if c <> 0 then c
    else TSet.compare t1.sub t2.sub
609

610
  let equal t1 t2 =
611 612 613 614 615
    (t1 == t2) ||
      (t1.hash == t2.hash &&
	 XSet.equal t1.pos t2.pos &&
	 XSet.equal t1.neg t2.neg &&
	 TSet.equal t1.sub t2.sub)
616

617
  let hash t = t.hash
618 619


620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
  let rec print f ppf t =
    Format.fprintf ppf "(";
    let first = ref true in
    let sep () = if !first then first := false else Format.fprintf ppf "&" in
    XSet.iter (fun x -> sep (); f ppf x) t.pos;
    XSet.iter (fun x -> sep (); Format.fprintf ppf "~"; f ppf x) t.neg;
    TSet.iter (fun t -> sep (); Format.fprintf ppf "~"; print f ppf t) t.sub;
    Format.fprintf ppf ")"

  let make pos neg sub =
(*    let vars =
      TSet.fold (fun t accu -> XSet.union t.vars accu) sub (XSet.union pos neg)
    in *)
    { pos = pos;
      neg = neg;
      sub = sub;
(*       vars = vars; *)
      hash = XSet.hash pos + 17 * XSet.hash neg + 257 * TSet.hash sub }
638

639

640 641
  let any = make XSet.empty XSet.empty TSet.empty
  let empty = make XSet.empty XSet.empty (TSet.singleton any)
642

643
  let atom x = make (XSet.singleton x) XSet.empty TSet.empty
644

645
  let compl t =
646
    if t == any then empty else if t == empty then any
647 648 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
    else
    match XSet.is_empty t.pos, XSet.is_empty t.neg, TSet.is_empty t.sub with
      | true,true,false ->
	  (match TSet.is_singleton t.sub with
	     | Some t -> t
	     | None -> make XSet.empty XSet.empty (TSet.singleton t))
      | false,true,true ->
	  (match XSet.is_singleton t.pos with
	     | Some _ -> make XSet.empty t.pos TSet.empty
	     | None -> make XSet.empty XSet.empty (TSet.singleton t))
      | true,false,true ->
	  (match XSet.is_singleton t.neg with
	     | Some _ -> make t.neg XSet.empty TSet.empty
	     | None -> make XSet.empty XSet.empty (TSet.singleton t))
      | _ -> make XSet.empty XSet.empty (TSet.singleton t)

  let triv_subset t1 t2 =
    XSet.subset t2.pos t1.pos &&
      XSet.subset t2.neg t1.neg &&
      TSet.subset t2.sub t1.sub

  let can_factor t1 t2 =
    not (XSet.disjoint t1.pos t2.pos &&
      XSet.disjoint t1.neg t2.neg &&
      TSet.disjoint t1.sub t2.sub)


  let cap t1 t2 =
675
    if (t1 == any) || (equal t1 t2) || (triv_subset t2 t1) then t2
676
    else if (t2 == any) || (triv_subset t1 t2) then t1
677
    else if (t1 == empty || t2 == empty)
678 679 680
      || not (XSet.disjoint t1.pos t2.neg)
      || not (XSet.disjoint t1.neg t2.pos)
      || TSet.mem t1 t2.sub
681
      || TSet.mem t2 t1.sub then empty
682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
    else
      if XSet.is_empty t1.pos && XSet.is_empty t2.pos &&
	XSet.is_empty t1.neg && XSet.is_empty t2.neg then
	  match TSet.is_singleton t1.sub,TSet.is_singleton t2.sub with
	    | Some n1, Some n2 when triv_subset n1 n2 -> t2
	    | Some n1, Some n2 when triv_subset n2 n1 -> t1
(*	    | Some n1, Some n2 when can_factor n1 n2 ->
		Format.fprintf Format.std_formatter "XXX@.";
		let pos = XSet.inter n1.pos n2.pos
		and neg = XSet.inter n1.neg n2.neg
		and sub = TSet.inter n1.sub n2.sub in
		let t1 = make (XSet.diff n1.pos pos) (XSet.diff n1.neg neg)
		  (TSet.diff n1.sub sub)
		and t2 = make (XSet.diff n2.pos pos) (XSet.diff n2.neg neg)
		  (TSet.diff n2.sub sub) in
		let t1t2 = TSet.add t2 (TSet.singleton t1) in
698
		make XSet.empty XSet.empty
699
		  (TSet.singleton
700
		     (make pos neg (TSet.add (make XSet.empty XSet.empty
701 702 703 704
						t1t2) sub))) *)
	    | _ ->
		make XSet.empty XSet.empty (TSet.union t1.sub t2.sub)
      else
705 706
	make
	  (XSet.union t1.pos t2.pos)
707 708
	  (XSet.union t1.neg t2.neg)
	  (TSet.union t1.sub t2.sub)
709

710 711
  let dump ppf t =
    print (fun ppf x -> Format.fprintf ppf "%i" (X.hash x)) ppf t
712

713
  let not_triv t = t != empty && t != any
714

715 716 717 718 719 720
  let cap t1 t2 =
    let ppf = Format.std_formatter in
    let t' = cap t1 t2 in
    if (not_triv t1) && (not_triv t2) then
      Format.fprintf ppf "%a &&& %a === %a@." dump t1 dump t2 dump t';
    t'
721

722 723
  let cup t1 t2 = compl (cap (compl t1) (compl t2))
  let diff t1 t2 = cap t1 (compl t2)
724 725


726
  let rec simplify pos neg t =
727
    if not (XSet.disjoint t.pos neg)
728 729 730 731
      || not (XSet.disjoint t.neg pos) then empty
    else
      let npos = XSet.diff t.pos pos
      and nneg = XSet.diff t.neg neg in
732
      let n =
733 734 735 736
	if XSet.is_empty npos && XSet.is_empty nneg then any
	else make npos nneg TSet.empty in
      let pos' = XSet.union pos npos
      and neg' = XSet.union neg nneg in
737 738
      try
	TSet.fold
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755
	  (fun t accu ->
	     let t = simplify pos' neg' t in
	     if t == any then raise Exit;
	     if t == empty then accu else diff accu t)
	  t.sub n
      with Exit -> empty
(*  and simplify pos neg t =
    let ppf = Format.std_formatter in
    let t' = simplify' pos neg t in
    Format.fprintf ppf "Simplify %a ==> %a@." dump t dump t';
    t' *)

  let dnf f (t : t) =
    let rec loop pos neg pos0 = function
      | [] -> f (XSet.elements pos) neg
      | t::tl when not (XSet.disjoint t.neg pos) -> loop pos neg pos0 tl
      | t::tl ->
756 757 758
	  let pos0 =
	    XSet.fold
	      (fun x pos0' ->
759 760 761 762 763 764
		 loop (XSet.add x pos) neg pos0' tl;
		 XSet.add x pos0'
	      ) (XSet.diff t.neg pos0) pos0 in

	  let p = XSet.diff t.pos pos in
	  if not (XSet.is_empty p) then
765 766
	    loop pos (XSet.elements p :: neg) pos0 tl;
	  TSet.iter (fun s ->loop
767 768 769 770 771 772
		       (XSet.union s.pos pos)
		       (XSet.fold (fun x accu -> [x]::accu) s.neg neg)
		       pos0
		       (TSet.fold (fun t tl -> t::tl) s.sub tl)) t.sub
    in
    loop t.pos (List.map (fun x -> [x]) (XSet.elements t.neg))  XSet.empty
773
      (TSet.elements t.sub)
774

775 776 777 778
  let trivially_disjoint t1 t2 =
    TSet.mem t1 t2.sub || TSet.mem t2 t1.sub ||
      not (XSet.disjoint t1.pos t2.neg) ||
      not (XSet.disjoint t1.neg t2.pos)
779

780 781 782 783 784 785
  let iter f t =
    let rec aux t =
      XSet.iter f t.pos;
      XSet.iter f t.neg;
      TSet.iter aux t.sub in
    aux t
786

787
  let full = any
788

789 790
  let get t =
    let l = ref [] in
791
    let rec aux pos neg = function
792 793
      | [] -> l := (pos,neg) :: !l
      | x::tl -> List.iter (fun a -> aux pos (a::neg) tl) x
794
    in
795 796
    dnf (fun pos neg -> aux pos [] neg) t;
    !l
797

798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822

  let rec serialize s t =
    Serialize.Put.list X.serialize s (XSet.elements t.pos);
    Serialize.Put.list X.serialize s (XSet.elements t.neg);
    Serialize.Put.list serialize s (TSet.elements t.sub)

  let rec deserialize s =
    let pos = XSet.of_list (Serialize.Get.list X.deserialize s) in
    let neg = XSet.of_list (Serialize.Get.list X.deserialize s) in
    let sub = TSet.of_list (Serialize.Get.list deserialize s) in
    let t = make pos neg sub in
    if equal t empty then empty
    else if equal t any then any
    else t

  let check t = ()

  let compute ~empty ~full ~cup ~cap ~diff ~atom t =
    let rec aux t =
      let accu = XSet.fold (fun x accu -> cap (atom x) accu) t.pos empty in
      let accu = XSet.fold (fun x accu -> diff accu (atom x)) t.neg accu in
      let accu = TSet.fold (fun t accu -> diff accu (aux t)) t.sub accu in
      accu
    in
    aux t
823

824

825
(*
826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854
  let cap t1 t2 =
    let ppf = Format.std_formatter in
    let t' = cap t1 t2 in
    if (not_triv t1) && (not_triv t2) then
      Format.fprintf ppf "%a &&& %a === %a@." dump t1 dump t2 dump t';
    let t'' = simplify XSet.empty XSet.empty t' in
    if not (equal t' t'') then
      Format.fprintf ppf "SIMPLIF %a@." dump t'';
    t''

  let cup t1 t2 =
    let ppf = Format.std_formatter in
    let t' = cup t1 t2 in
    if (not_triv t1) && (not_triv t2) then
      Format.fprintf ppf "%a ||| %a === %a@." dump t1 dump t2 dump t';
    let t'' = simplify XSet.empty XSet.empty t' in
    if not (equal t' t'') then
      Format.fprintf ppf "SIMPLIF %a@." dump t'';
    t''

  let diff t1 t2 =
    let ppf = Format.std_formatter in
    let t' = diff t1 t2 in
    if (not_triv t1) && (not_triv t2) then
      Format.fprintf ppf "%a --- %a === %a@." dump t1 dump t2 dump t';
    let t'' = simplify XSet.empty XSet.empty t' in
    if not (equal t' t'') then
      Format.fprintf ppf "SIMPLIF %a@." dump t'';
    t''
855
*)
856 857
end

858 859
module type S'' = sig
  include S
860
  val dnf: (elem list -> (elem list) list -> unit) -> t -> unit
861
end
862
*)