let rec mk_sub n i j a =
  assert (0 <= i && j < n && n >= 0);
  if i = 0 && j = n-1 then 
    a 
  else if j < i then
    mk_eps
  else 
    match d_interp a with
      | Some(Const(b), []) -> 
          mk_const(Bitv.sub b i (j-i+1))
      | Some(Sub(m,k,l), [x]) ->
          mk_sub m (k+i) (k+j) x
      | Some(Conc(n,m), [x;y]) ->
          if j < n then
            mk_sub n i j x
          else if n <= i then
            mk_sub m (i-n) (j-n) y
          else 
            (assert(i < n && n <= j);
            let t = mk_sub n i (n-1) x in
            let u = mk_sub m 0 (j-n) y in
            mk_conc (n-i) (j-n+1) t u)
      | Some(Bitwise(n), [x;y;z]) ->
          mk_bitwise (j-i+1) (mk_sub n i j x) (mk_sub n i j y) (mk_sub n i j z) 
      | None ->
          Term.mk_app (Bv(Sub(n, i, j))) [a]
      | Some _ ->
          failwith "Bv.mk_sub: ill-formed expression"
        
and mk_conc n m a b =
  assert (0 <= n && 0 <= m);
  match n = 0, m = 0 with
    | true, true -> mk_eps
    | true, false -> b
    | false, true -> a
    | false, false ->
        (match merge n m a b with
           | None -> Term.mk_app (Bv(Conc(n,m))) [a;b]
           | Some(c) -> c)

and merge n m a b =
  match d_interp a, d_interp b with
    | _, Some(Conc(m1,m2), [b1;b2]) -> 
        Some(mk_conc (n + m1) m2 (mk_conc n m1 a b1) b2)
    | Some(Conc(m1, m2), [b1; App(Bv(Const(c)), [])]), Some(Const(d), []) ->
        let n = Bitv.length d in
        Some(mk_conc m1 (m2 + n) b1 (mk_const (Bitv.append c d)))
    | Some(Const(c),[]), Some(Const(d),[]) -> 
        Some(mk_const (Bitv.append c d))
    | Some(Sub(n,i,j),[x]), Some(Sub(m,j',k), [y])
        when j' = j + 1 && Term.eq x y ->
        assert(n = m);
          Some(mk_sub n i k x)
    | Some(Bitwise(n1),[x1;y1;z1]), Some(Bitwise(n2),[x2;y2;z2]) ->
        (match merge n1 n2 x1 x2 with
           | None -> None
           | Some(x) ->
               (match merge n1 n2 y1 y2 with
                  | None -> None
                  | Some(y) ->
                      (match merge n1 n2 z1 z2 with
                         | None -> None
                         | Some(z) -> Some(mk_bitwise (n1+n2) x y z))))
    | _ -> 
        None
 

and mk_conc3 n m k a b c =
  mk_conc n (m + k) a (mk_conc m k b c)

and mk_bitwise n a b c =
  assert (n >= 0);
  if n = 0 then 
    mk_eps
  else 
    match d_const a, d_const b, d_const c with
      | Some(c1), Some(c2), Some(c3) ->
          mk_const (Bitv.bw_or (Bitv.bw_and c1 c2) (Bitv.bw_and (Bitv.bw_not c1) c3))
      | _ ->
          (match d_conc a, d_conc b, d_conc c with
             | Some(n1,n2,a1,a2), _, _ ->
                 assert(n = n1 + n2);
                 let b1,b2 = cut n n1 b in
                 let c1,c2 = cut n n1 c in 
                 mk_conc n1 n2 (mk_bitwise n1 a1 b1 c1) (mk_bitwise n2 a2 b2 c2)
             | _, Some(n1,n2,b1,b2), _ ->
                 assert(n = n1 + n2);
                 let a1,a2 = cut n n1 a in
                 let c1,c2 = cut n n1 c in 
                 mk_conc n1 n2 (mk_bitwise n1 a1 b1 c1) (mk_bitwise n2 a2 b2 c2)
             | _, _, Some(n1,n2,c1,c2) ->
                 assert(n = n1 + n2);
                 let a1,a2 = cut n n1 a in
                 let b1,b2 = cut n n1 b in 
                 mk_conc n1 n2 (mk_bitwise n1 a1 b1 c1) (mk_bitwise n2 a2 b2 c2)
             | _ ->
                 drop (build n (lift n a, lift n b, lift n c)))

and lift n a =
  if is_bvbdd a then 
    a 
  else
    Term.mk_app (Bv(Bitwise(n))) [a;mk_one n;mk_zero n]

and drop a =
 match d_bitwise a with
   | Some(_,b1,b2,b3) when is_one b2 && is_zero b3 -> b1
   | _ -> a

and cut n i a =
  (mk_sub n 0 (i - 1) a, mk_sub n i (n - 1) a)