let rec solve ((a, b) as e) =
  match width a, width b with
    | Some(n), Some(m) when n <> m -> 
        raise Exc.Inconsistent
    | _ -> 
        fresh := [];         (* initialize fresh variables. *)
        solvel ([e], [])
  
and solvel (el, sl) =
  Trace.msg "bv'" "Solve" (el, sl) (Pretty.pair Term.Subst.pp Term.Subst.pp);
  match el with
    | [] -> sl
    | (a, b) :: el when Term.eq a b ->
        solvel (el,sl)
    | (a, b) :: el ->
        (match to_option d_interp a, to_option d_interp b  with   
           | None, Some _ when not(occurs a b) ->      (* Check if solved. *)
               solvel (add a b (el, sl))
           | Some _, None  when not(occurs b a) ->
               solvel (add b a (el, sl))
           | Some(Sym.Conc _, _), _                    (* Decomposition of [conc] *)
           | _, Some(Sym.Conc _, _) ->
               solvel (decompose (a, b) @ el, sl)
           | Some(Sym.Const(c), []), Some(Sym.Const(d), []) ->
               if Pervasives.compare c d = 0 then 
                 solvel (el,sl)
               else 
                 raise Exc.Inconsistent
           | Some(Sym.Sub(n,i,j),[x]), Some(Sym.Sub(m,k,l),[y]) when Term.eq x y ->
               assert(n = m);
               let (x, b) = solve_sub_sub x n i j k l in
                 solvel (add x b (el,sl))
           | Some(Sym.Sub(n,i,j),[x]),  Some(Sym.Const _, []) ->
               assert(n-j-1 >= 0);
               assert(i >= 0);
               let b' = 
                 mk_conc3 i (j-i+1) (n-j-1) 
                   (mk_fresh i) b (mk_fresh (n-j-1)) 
               in
                 solvel (add x b' (el,sl))
           | Some(Sym.Const _, []), Some(Sym.Sub(n,i,j), [x]) -> 
               assert(n-j-1 >= 0); 
               assert(i >= 0);
               let a' = mk_conc3 i (j-i+1) (n-j-1) (mk_fresh i) 
                          a (mk_fresh (n-j-1)) in
               solvel (add x a' (el,sl))
           | _ ->
               assert(not(is_interp a));
               assert(not(is_interp b));
               let a, b = Term.orient(a, b) in
                 solvel (add a b (el,sl)))

(* Solving [xn[i:j] = xn[k:l]] *)
and solve_sub_sub x n i j k l =  
  Trace.msg "bv'" "Solve(sub)" (mk_sub n i j x, mk_sub n k l x) (Pretty.pair Term.pp Term.pp);
  assert (n >= 0 && i < k && j-i = l-k);
  let lhs = 
    mk_sub n i l x 
  in
  let rhs =
    if (l-i+1) mod (k-i) = 0 then
      let a = mk_fresh (k-i) in
      mk_iterate (k-i) a ((l-i+1)/(k-i))
    else
      let h = (l-i+1) mod (k-i) in
      let h' = k-i-h in
      let a = mk_fresh h in
      let b = mk_fresh h' in
      let nc = (l-i-h+1)/(k-i) in
      let c = mk_iterate (h + h') (mk_conc h' h b a) nc in
      mk_conc h (nc * (h' + h)) a c
  in
    Trace.msg "bv'" "Solve(sub)" (lhs, rhs) (Pretty.pair Term.pp Term.pp);
    (lhs, rhs)


and occurs x a =
  assert(not(is_interp x));
  try
    let (_, bl) = d_interp a in
      List.exists (occurs x) bl
  with
      Not_found -> Term.eq x a




(** Adding a solved pair a |-> b to the list of solved forms sl, and propagating this new binding to the unsolved equalities el and the rhs of sl. It also makes sure that fresh variables a are never added to sl but only propagated. *)


and add x b (el, sl) =
  assert(not(is_interp x));
  if Term.eq x b then 
    (el, sl)
  else if inconsistent x b then
    raise Exc.Inconsistent
  else 
    let (x, b) = orient (x, b) in
    let el' = subst el (x, b) 
    and sl' = compose sl (x, b) in
      (el', sl')
                


(** Ensure y = x with y fresh and x not fresh can not happen. *)


and orient (a, b) =
  if Term.is_var a && Term.is_var b then
    if is_fresh a && not(is_fresh b) then
      (b, a)
    else 
      Term.orient (a, b)
  else
    (a, b)
     
and subst el (x, a) = 
  let apply_to_eq (b1, b2) =
    (apply (x, a) b1, apply (x, a) b2)
  in
    List.map apply_to_eq el

and compose sl (x, a) =
  if is_fresh x && is_fresh a then   (* equality between fresh variables *)
    Term.Subst.fuse apply (x, a) sl  (* can be dropped. *)
  else 
    Term.Subst.compose apply (x, a) sl

and inconsistent a b =
  match width a, width b with
    | Some(n), Some(m) -> n <> m
    | _ -> false