let (<) : int -> int -> bool = (<) let (>) : int -> int -> bool = (>) let (=) : int -> int -> bool = (=) module type S = sig type elem include Custom.T val get: t -> (elem list * elem list) list val get': t -> (elem list * (elem list) list) list val empty : t val full : t val cup : t -> t -> t val cap : t -> t -> t val diff : t -> t -> t val atom : elem -> t val iter: (elem-> unit) -> t -> unit val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b) -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) -> atom:(elem -> 'b) -> t -> 'b (* val print: string -> (Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list *) val trivially_disjoint: t -> t -> bool end module type MAKE = functor (X : Custom.T) -> S with type elem = X.t module Make(X : Custom.T) = struct type elem = X.t type t = | True | False | Split of int * elem * t * t * t let rec equal a b = (a == b) || match (a,b) with | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) -> (h1 == h2) && (equal p1 p2) && (equal i1 i2) && (equal n1 n2) && (X.equal x1 x2) | _ -> false (* Idea: add a mutable "unique" identifier and set it to the minimum of the two when egality ... *) let rec compare a b = if (a == b) then 0 else match (a,b) with | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) -> if h1 < h2 then -1 else if h1 > h2 then 1 else let c = X.compare x1 x2 in if c <> 0 then c else let c = compare p1 p2 in if c <> 0 then c else let c = compare i1 i2 in if c <> 0 then c else compare n1 n2 | True,_ -> -1 | _, True -> 1 | False,_ -> -1 | _,False -> 1 let rec hash = function | True -> 1 | False -> 0 | Split(h, _,_,_,_) -> h let compute_hash x p i n = (X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n) let rec check = function | True | False -> () | Split (h,x,p,i,n) -> assert (h = compute_hash x p i n); (match p with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ()); (match i with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ()); (match n with Split (_,y,_,_,_) -> assert (X.compare x y < 0) | _ -> ()); X.check x; check p; check i; check n let atom x = let h = X.hash x + 17 in (* partial evaluation of compute_hash... *) Split (h, x,True,False,False) let neg_atom x = let h = X.hash x + 16637 in (* partial evaluation of compute_hash... *) Split (h, x,False,False,True) let rec iter f = function | Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n | _ -> () let rec dump ppf = function | True -> Format.fprintf ppf "⊤" | False -> Format.fprintf ppf "⊥" | Split (_,x, p,i,n) -> Format.fprintf ppf "@[@[%a@][@[%a,@\n%a,@\n%a@]]@]" X.dump x dump p dump i dump n let rec print f ppf = function | True -> Format.fprintf ppf "Any" | False -> Format.fprintf ppf "Empty" | Split (_, x, p,i, n) -> let flag = ref false in let b () = if !flag then Format.fprintf ppf " | " else flag := true in (match p with | True -> b(); Format.fprintf ppf "%a" f x | False -> () | _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p ); (match i with | True -> assert false; | False -> () | _ -> b(); print f ppf i); (match n with | True -> b (); Format.fprintf ppf "@[~%a@]" f x | False -> () | _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n) let print a 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) -> (*OPT: can avoid creating this list cell when pos or neg =False *) let accu = get accu (x::pos) neg p in let accu = get accu pos (x::neg) n in let accu = get accu pos neg i in accu let get x = get [] [] [] x let rec get' accu pos neg = function | True -> (pos,neg) :: accu | False -> accu | Split (_,x,p,i,n) -> let accu = get' accu (x::pos) neg p in let rec aux l = function | Split (_,x,False,i,n') when equal n n' -> aux (x :: l) i | i -> (* 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 let compute ~empty ~full ~cup ~cap ~diff ~atom b = let rec aux = function | True -> full | False -> empty | Split(_,x, p,i,n) -> 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 in aux b (* Invariant: correct hash value *) let split0 x pos ign neg = Split (compute_hash x pos ign neg, x, pos, ign, neg) let empty = False let full = True (* Invariants: Split (x, pos,ign,neg) ==> (ign <> True), (pos <> neg) *) let rec has_true = function | [] -> false | True :: _ -> true | _ :: l -> has_true l let rec has_same a = function | [] -> false | b :: l -> (equal a b) || (has_same a l) let rec split x p i n = if i == True then True else if equal p n then p ++ i else let p = simplify p [i] and n = simplify n [i] in if equal p n then p ++ i else split0 x p i n and simplify a l = match a with | False -> False | True -> if has_true l then False else True | Split (_,x,p,i,n) -> if (has_true l) || (has_same a l) then False else s_aux2 a x p i n [] [] [] l and s_aux2 a x p i n ap ai an = function | [] -> let p = simplify p ap and n = simplify n an and i = simplify i ai in if equal p n then p ++ i else split0 x p i n | b :: l -> s_aux3 a x p i n ap ai an l b and s_aux3 a x p i n ap ai an l = function | False -> s_aux2 a x p i n ap ai an l | True -> assert false | Split (_,x2,p2,i2,n2) as b -> if equal a b then False else let c = X.compare x2 x in if c < 0 then s_aux3 a x p i n ap ai an l i2 else if c > 0 then s_aux2 a x p i n (b :: ap) (b :: ai) (b :: an) l else s_aux2 a x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l 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 (* seems better not to make ++ and this split mutually recursive; is the invariant still inforced ? *) 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) let rec trivially_disjoint a b = if a == b then a == False else match (a,b) with | True, a | a, True -> a == False | False, _ | _, False -> true | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) -> let c = X.compare x1 x2 in if c = 0 then (* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *) trivially_disjoint (p1 ++ i1) (p2 ++ i2) && trivially_disjoint (n1 ++ i1) (n2 ++ i2) else if c < 0 then trivially_disjoint p1 b && trivially_disjoint i1 b && trivially_disjoint n1 b else trivially_disjoint p2 a && trivially_disjoint i2 a && trivially_disjoint n2 a let rec neg = function | True -> False | False -> True | Split (_,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, False, False) -> split x False (neg p) True | Split (_,x, False, False, n) -> split x True (neg n) False *) | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n)) let rec ( // ) a b = (* if equal a b then False *) if a == b then False 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 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)) else if c < 0 then split x1 (p1 // b) (i1 // b) (n1 // b) (* 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 = ( // ) (* 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); if (c < 0) then 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 not_triv = function | True | False -> false | _ -> true let diff x y = let d = diff 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 let cap x y = let d = cap 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 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 *) end (* 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) = 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 *) module W = Weak(*Myweak*).Make( 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 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 *) 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 -> Serialize.Put.bool t true; Serialize.Put.bool t (b == One) | 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 = () 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 module Make2(X : Custom.T) = struct module XSet = Hashset.MakeSet(X) type 'a s = { pos : XSet.t; neg : XSet.t; sub : 'a; (* vars : XSet.t; *) hash : int; } 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) let () = tset_compare := Obj.magic TSet.compare; tset_equal := Obj.magic TSet.equal type elem = X.t 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 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 && TSet.equal t1.sub t2.sub) let hash t = t.hash 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 } let any = make XSet.empty XSet.empty TSet.empty let empty = make XSet.empty XSet.empty (TSet.singleton any) let atom x = make (XSet.singleton x) XSet.empty TSet.empty 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) let dump ppf t = print (fun ppf x -> Format.fprintf ppf "%i" (X.hash x)) ppf t let not_triv t = t != empty && t != any 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' let cup t1 t2 = compl (cap (compl t1) (compl t2)) let diff t1 t2 = cap t1 (compl t2) 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) 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) 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 let full = any let get t = let l = ref [] in let rec aux pos neg = function | [] -> l := (pos,neg) :: !l | x::tl -> List.iter (fun a -> aux pos (a::neg) tl) x in 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 (* 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'' *) end module type S'' = sig include S val dnf: (elem list -> (elem list) list -> unit) -> t -> unit end *)