
    let ks', s' =
      Map.fold s ~init:(ks, s) ~f:(fun ~key ~data (ks, s) ->
          let fv_key = Term.fv key in
          let fv_data = Term.fv data in
          if Set.disjoint ks (Set.union fv_key fv_data) then (ks, s)
          else
            let ks = Set.union ks (Set.inter bound fv_key) in
            let s = Map.remove s key in
            (ks, s) )
    in
    if s'!= s then trim ~bound ks' s' else s'
end

(** Theory Solver *)

(* orient equations s.t. Var < Memory < Extract < Concat < others, then
   using height of aggregate nesting, and then using Term.compare *)
let orient e f =
  let compare e f =
    let rank e =
      match (e : Term.t) with
      | Var _ -> 0
      | Ap2 (Memory, _, _) -> 1
      | Ap3 (Extract, _, _, _) -> 2
      | ApN (Concat, _) -> 3
      | _ -> 4
    in
    let rec height e =
      match (e : Term.t) with
      | Ap2 (Memory, _, x) -> 1 + height x
      | Ap3 (Extract, x, _, _) -> 1 + height x
      | ApN (Concat, xs) ->
          1 + Vector.fold ~init:0 ~f:(fun h x -> max h (height x)) xs
      | _ -> 0
    in
    let o = compare (rank e) (rank f) in
    if o <> 0 then o
    else
      let o = compare (height e) (height f) in
      if o <> 0 then o else Term.compare e f
  in
  match Ordering.of_int (compare e f) with
  | Less -> Some (e, f)
  | Equal -> None
  | Greater -> Some (f, e)

let norm (_, _, s) e = Subst.norm s e

let extend ~var ~rep (us, xs, s) =
  Some (us, xs, Subst.compose1 ~key:var ~data:rep s)

let fresh name (us, xs, s) =
  let x, us = Var.fresh name ~wrt:us in
  let xs = Set.add xs x in
  (Term.var x, (us, xs, s))

let solve_poly p q s =
  match Term.sub p q with
  | Integer {data} -> if Z.equal Z.zero data then Some s else None
  | Var _ as var -> extend ~var ~rep:Term.zero s
  | p_q -> (
    match Term.solve_zero_eq p_q with
    | Some (var, rep) -> extend ~var ~rep s
    | None -> extend ~var:p_q ~rep:Term.zero s )

(* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n
   = |α| and c fresh *)
let rec solve_extract a o l b s =
  let n = Term.agg_size_exn a in
  let c, s = fresh "c" s in
  let n_c = Term.memory ~siz:n ~arr:c in
  let o_l = Term.add o l in
  let n_o_l = Term.sub n o_l in
  let c0 = Term.extract ~agg:n_c ~off:Term.zero ~len:o in
  let c1 = Term.extract ~agg:n_c ~off:o_l ~len:n_o_l in
  let b, s =
    match Term.agg_size b with
    | None -> (Term.memory ~siz:l ~arr:b, Some s)
    | Some m -> (b, solve_ l m s)
  in
  s >>= solve_ a (Term.concat [|c0; b; c1|])

(* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ …
   where nₓ ≡ |αₓ| and m = |β| *)
and solve_concat a0V b m s =
  Vector.fold_until a0V ~init:(s, Term.zero)
    ~f:(fun (s, oI) aJ ->
      let nJ = Term.agg_size_exn aJ in
      let oJ = Term.add oI nJ in
      match solve_ aJ (Term.extract ~agg:b ~off:oI ~len:nJ) s with
      | Some s -> Continue (s, oJ)
      | None -> Stop None )
    ~finish:(fun (s, n0V) -> solve_ n0V m s)

and solve_ e f s =
  [%Trace.call fun {pf} ->
    pf "%a@[%a@ %a@ %a@]" Var.Set.pp_xs (snd3 s) Term.pp e Term.pp f
      Subst.pp (trd3 s)]
  ;
  ( match orient (norm s e) (norm s f) with
  (* e' = f' ==> true when e' ≡ f' *)
  | None -> Some s
  (* i = j ==> false when i ≠ j *)
  | Some (Integer _, Integer _) -> None
  (* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *)
  | Some (Ap2 (Memory, n, a), b) when Term.equal n Term.zero ->
      s |> solve_ a (Term.concat [||]) >>= solve_ b (Term.concat [||])
  | Some (b, Ap2 (Memory, n, a)) when Term.equal n Term.zero ->
      s |> solve_ a (Term.concat [||]) >>= solve_ b (Term.concat [||])
  (* v = ⟨n,a⟩ ==> v = a *)
  | Some ((Var _ as v), Ap2 (Memory, _, a)) -> s |> solve_ v a
  (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
  | Some (Ap2 (Memory, n, a), Ap2 (Memory, m, b)) ->
      s |> solve_ n m >>= solve_ a b
  (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *)
  | Some (Ap2 (Memory, n, a), b) ->
      (match Term.agg_size b with None -> Some s | Some m -> solve_ n m s)
      >>= solve_ a b
  | Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) ->
      if not (Set.mem (Term.fv e) (Var.of_ v)) then
        (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *)
        extend ~var:v ~rep:e s
      else
        (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
        extend ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s
  | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
      if not (Set.mem (Term.fv c) (Var.of_ v)) then
        (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
        extend ~var:v ~rep:c s
      else
        (* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^