let rec solve e =
  fresh := [];
  solvel ([e], [])

and solvel (el, sl) =
  match el with
    | [] -> sl
    | (a, b) :: el1 -> solve1 (a, b) (el1, sl)

and solve1 (a, b) (el, sl) = 
  Trace.msg "l" "Solve" (a, b) Term.Equal.pp;
  if Term.eq a b then                        (* [Triv] *)
    solvel (el, sl)
  else if is_functional a || is_functional b then
    let d = mk_fresh () in                   (* [Ext] *)
    let e = (mk_apply a d, mk_apply b d) in
      solvel (e :: el, sl)
  else if is_fo_app a || is_fo_app b then
    let sl' = solve_fo (a, b) in
      solvel (List.fold_right install sl' (el, sl))
  else 
    let (f, al) = d_apply a
    and (g, bl) = d_apply b in               (* [Decompose] *)
      if Term.eq f g && 
        is_redex_atom f && 
        List.length al = List.length bl 
      then
        let el' = List.combine al bl in
          solvel (el' @ el, sl)
      else if is_pure a && is_pure b then
        raise Exc.Inconsistent
      else if not(Term.occurs f b) then
        solvel (install (imitate f al b) (el, sl))
      else if not(Term.occurs g a) then
        solvel (install (imitate g bl a) (el, sl))
      else 
        raise Exc.Incomplete

and solve_fo ((a, b) as e) = 
  let shostak_theory_of a =
    match Term.App.theory_of a with
      | Th.Shostak(i) -> i
      | _ -> raise Not_found
  in
    try
      let i = shostak_theory_of a in
        solve_interp i (a, b)
    with
        Not_found -> 
          let j = shostak_theory_of b in
            solve_interp j (a, b)
                
and solve_interp i e =
    match i with
      | Th.LA -> Arith.solve e
      | Th.BV -> Bitvector.solve e
      | Th.P -> Product.solve e
      | Th.COP -> Coproduct.solve e
      | Th.SET -> Propset.solve e
      | _ -> invalid_arg "no solving for CL terms"

and imitate x al b =
  assert(not(Term.occurs x b));
  match al with
    | [] -> (x, b)
    | [a] -> 
        let y = mk_fresh () in
        let zb = mk_bound () in
          (x, abstract (z()) (mk_cases zb a b (mk_apply y zb)))
    | _ -> 
        raise Exc.Incomplete

    
and install (x, a) (el, sl) =
  (substitute (x, a) el, compose (x, a) sl)

and compose (x, b) sl =
  Term.Subst.compose apply (x, b) sl

and substitute (x, b) el =
  let subst1 (a1, a2) =
    (apply (x, b) a1, apply (x, b) a2)
  in
    List.map subst1 el