bool.ml 24.3 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 23

  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) 
    -> 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 58 59 60 61 62 63 64 65 66 67 68 69
  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
70 71


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

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
  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) ->
137
	(*OPT: can avoid creating this list cell when pos or neg =False *)
138 139 140 141 142 143
	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
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 167 168
  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
169
	  and n = diff (aux n) (atom x) in
170 171 172 173 174 175
	  cup (cup p i) n
    in
    aux b
      
(* Invariant: correct hash value *)

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

  let empty = False
  let full = True
181 182

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

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

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

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

202 203 204 205 206 207 208 209
  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
210
    | [] -> 
211 212 213 214 215 216 217
	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
218 219
    | True -> assert false
    | Split (_,x2,p2,i2,n2) as b ->
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
	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

  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
235 236 237 238

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

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

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

279 280 281
  let rec neg = function
    | True -> False
    | False -> True
282
    | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
283
    | Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False 
284 285 286 287
    | Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n)  
(*    | Split (_,x, p, False, False) -> 
	split x False (neg p) True
    | Split (_,x, False, False, n) -> split x True (neg n) False *)
288 289 290
    | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
	      
  let rec ( // ) a b =  
291 292
(*    if equal a b then False  *)
    if a == b then False 
293 294 295 296 297 298 299
    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
300 301 302 303 304 305
	    if (i2 == False) && (n2 == False) 
	    then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
(*	    else if (i2 == False) && (p2 == False)
	    then split x1 (p1 ++ i1) (i1 // n2) (n1 // n2) *)
	    else 
	      split x1 ((p1++i1) // (p2 ++ i2)) False ((n1++i1) // (n2 ++ i2))
306
	  else if c < 0 then
307
	    split x1 (p1 // b) (i1 // b) (n1 // b) 
308 309 310 311 312 313 314 315 316
(*	    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 = ( // )

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

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

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

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

  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"
	dump x dump y dump d;  
    d
357
*)
358
end
359 360


361
(*
362 363 364 365 366 367
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) =
368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386
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 *)
387
  module W = Weak(*Myweak*).Make(
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
    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
  
451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
  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
*)
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 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
	  

  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 -> 
525
	Serialize.Put.bool t true; Serialize.Put.bool t (b == One)
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
    | 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 = ()
551 552 553 554 555 556 557

  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


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

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

569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
  let tset_equal = ref ()
  let tset_compare = ref ()

  module rec TSet : Hashset.SET with type elt = TSet.t s = 
    Hashset.MakeSet(
      struct
	type t = TSet.t s
	let compare t1 t2 = 
	  if (t1 == t2) then 0 
	  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
	    
	let equal t1 t2 = 
	  (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)
593
      
594 595 596
  let () = 
    tset_compare := Obj.magic TSet.compare;
    tset_equal := Obj.magic TSet.equal
597

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

601 602 603 604 605 606 607
  let compare t1 t2 = 
    if (t1 == t2) then 0 
    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
608

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

616
  let hash t = t.hash
617 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
  let any = make XSet.empty XSet.empty TSet.empty
  let empty = make XSet.empty XSet.empty (TSet.singleton any)
641

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

644 645 646 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 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
  let compl t =
    if t == any then empty else if t == empty then any 
    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 =
    if (t1 == any) || (equal t1 t2) || (triv_subset t2 t1) then t2 
    else if (t2 == any) || (triv_subset t1 t2) then t1
    else if (t1 == empty || t2 == empty) 
      || not (XSet.disjoint t1.pos t2.neg)
      || not (XSet.disjoint t1.neg t2.pos)
      || TSet.mem t1 t2.sub
      || TSet.mem t2 t1.sub then empty 
    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
		make XSet.empty XSet.empty 
		  (TSet.singleton
		     (make pos neg (TSet.add (make XSet.empty XSet.empty 
						t1t2) sub))) *)
	    | _ ->
		make XSet.empty XSet.empty (TSet.union t1.sub t2.sub)
      else
	make 
	  (XSet.union t1.pos t2.pos) 
	  (XSet.union t1.neg t2.neg)
	  (TSet.union t1.sub t2.sub)
708

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

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

714 715 716 717 718 719
  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'
720

721 722
  let cup t1 t2 = compl (cap (compl t1) (compl t2))
  let diff t1 t2 = cap t1 (compl t2)
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
  let rec simplify pos neg t =
    if not (XSet.disjoint t.pos neg) 
      || not (XSet.disjoint t.neg pos) then empty
    else
      let npos = XSet.diff t.pos pos
      and nneg = XSet.diff t.neg neg in
      let n = 
	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
      try 
	TSet.fold 
	  (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 ->
	  let pos0 = 
	    XSet.fold 
	      (fun x pos0' -> 
		 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
	    loop pos (XSet.elements p :: neg) pos0 tl; 
	  TSet.iter (fun s ->loop 
		       (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
      (TSet.elements t.sub)  
773

774 775 776 777
  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)
778

779 780 781 782 783 784
  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
785

786
  let full = any
787

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

  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
822

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
  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''
854
*)
855 856
end

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