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]