let rec build n s3 =
  try
    H3.find ht s3
  with Not_found ->
    let b = build_fun n s3 in
    H3.add ht s3 b; b 

and build_fun n (s1,s2,s3) =
  if Term.eq s2 s3 then s2
  else if is_one s2 && is_zero s3 then s1
  else if is_one s1 then s2
  else if is_zero s1 then s3
  else match d_bitwise s1 with
    | Some(_,y,_,_) ->
        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 n (pos1,pos2,pos3) in
        let neg = build n (neg1,neg2,neg3) in
        if Term.eq pos neg then pos else Term.mk_app (Bv(Bitwise(n))) [x;pos;neg]
    | None ->
        Term.mk_app (Bv(Bitwise(n))) [s1;s2;s3]