let rec solve e =
  fresh := [];                      (* reinitialize [is_fresh]. *)
  let e0, sl0, rho = pre e in
  let sl1 = solvel ([e0], sl0)in
  let sl2 = post rho sl1 in
    sl2



(** Preprocess the input equality e to replace each term of the form car(x) by k1 with the solution x = cons(k1, k2) added to sl, and similarly,cdr(x) can be replaced with k2, for fresh k2. This completely eliminates car and cdr from the input equality. Thus, pre (a, b) returns a triple consisting of an equality a' = b' such that a' and b' are built up from conses only, and none of the variables in a', b' is in the domain of the initial solution set, and an initial solution set with equalities x = cons(k1, k2) for each entry *)


and pre (a, b) =
  let (a', rho) = Symtab.abstract (a, Symtab.empty) in (* Abstract [car(x)] and [cdr(x)]. *)
  let (b', rho') = Symtab.abstract (b, rho) in         (* [a'] and [b'] do not contain [car], [cdr]. *)
  let sl0 =                                            (* Add [x = cons(k1, k2) for each *)
    Symtab.fold                                        (* renaming pair. *)
      (fun (x, k1, k2) acc -> 
         (x, mk_cons k1 k2) :: acc)
      rho' []
  in      
  let e0 = apply_to_eq sl0 (a', b') in                (* Apply these bindings. *)
    (e0, sl0, rho')
        
    



(** Repetitively apply the rules (symmetrically). Triv: a = a, el; sl ==> el; sl Ext: cons(a', a'') = cons(b', b''), el; sl ==> a' = b', a'' = b'', el; sl Bot: x = a, el; sl ==> bot if x is a proper subterm of a Subst: x = a, el; sl ==> sigma(el[a/x]); s o {x = a} if x occurs in el but not in a. Either a variable in el or a rhs in sl is eliminated (by Subst), or the size of el decreases, so the corresponding lexicographic measure yields termination. *)


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

and solve1 (a, b) (el, sl) =
  if Term.eq a b then                      (* Triv *)
    solvel (el, sl) 
  else                      
    try          
      let (a', a'') = d_cons a             (* Ext *)
      and (b', b'') = d_cons b in
        solvel (((a', b') :: (a'', b'') :: el), sl)
    with
        Not_found ->       
          assert(not(Term.eq a b)); 
          let (x, a) = if is_cons a then (b, a) else (a, b) in
            assert(not(is_interp x));
            if Term.subterm x a then       (* Bot *) 
              raise Exc.Inconsistent
            else                           (* Subst *)
              let (x, a) = orient (x, a) in
              let el' = apply_to_eqs [(x, a)] el in
              let sl' = compose (x, a) sl in
                solvel (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 apply_to_trm rho =
  let lookup x =
    try Term.Subst.lookup rho x with Not_found -> x
  in
    map lookup 
  
and apply_to_eq rho (a1, a2) =
  (apply_to_trm rho a1, apply_to_trm rho a2)
  
and apply_to_eqs rho a =
  List.map (apply_to_eq rho) a
       
and compose (x, a) sl =
  assert(not(is_interp x));
  Term.Subst.compose apply (x, a) sl



(** Postprocessing is needed to ensure that the solution does not contain new variables. We can then discard any equations of the form k = a in sl for newly introduced k. The result does not necessarily use a minimal number of fresh variables. *)


and post rho sl =
  List.filter (fun (x, _) -> not (is_fresh x)) sl