let mk_ite a b c = 
  let cofactors x a =
    try
      let (y, pos, neg) = d_ite a in
        if Term.eq x y then (pos, neg) else (a, a)
    with
        Not_found -> (a, a)
  in
  let topvar x s2 s3 =
    let to_option f s = try Some(f s) with Not_found -> None in
    let max x y = if Term.(<<<) x y then x else y in
      match to_option d_ite s2, to_option d_ite s3 with
        | Some(y,_,_), Some(z,_,_) -> max x (max y z)
        | Some(y,_,_), None -> max x y
        | None, Some(z,_,_) -> max x z
        | None, None -> x
  in
  let rec build s3 =
    let module H3 = Hashtbl.Make(
      struct
        type t = Term.t * Term.t * Term.t
        let equal (a1, a2, a3) (b1, b2, b3) = 
          Term.eq a1 b1 && Term.eq a2 b2 && Term.eq a3 b3
        let hash = Hashtbl.hash
      end)
    in
    let ht =  H3.create 17 in
    let _ = Tools.add_at_reset (fun () -> H3.clear ht) in
      try
        H3.find ht s3
      with 
          Not_found ->
            let b = build_fun s3 in
              H3.add ht s3 b; b 
  and build_fun (s1, s2, s3) =
    if Term.eq s2 s3 then s2
    else if is_full s2 && is_empty s3 then s1
    else if is_full s1 then s2
    else if is_empty s1 then s3
    else 
      try
        let (y, _, _) = d_ite s1 in
        let x = topvar y s2 s3 in
        let (pos1, neg1) = cofactors x s1 in
        let (pos2, neg2) = cofactors x s2 in
        let (pos3, neg3) = cofactors x s3 in
        let pos = build (pos1, pos2, pos3) in
        let neg = build (neg1, neg2, neg3) in
          if Term.eq pos neg then pos else 
            Term.App.mk_app Sym.Propset.mk_ite [x; pos; neg]
      with
          Not_found -> 
            Term.App.mk_app Sym.Propset.mk_ite [s1; s2; s3]
  in
  let lift a =
    if is_interp a then a else
      Term.App.mk_app Sym.Propset.mk_ite [a; mk_full(); mk_empty()]
  in
  let  drop a =
    try
      let (b1, b2, b3) = d_ite a in
        if is_full b2 && is_empty b3 then b1
        else 
          a
    with
        Not_found -> a
  in        
    try
      drop (build (lift a, lift b, lift c))
    with
        Not_found -> invalid_arg "ite"