Translation (astral.Astral_internal.SingleQuerySolver.Make.Translation)

val formula_footprint : ('a, 'b) Translation_context.t -> SL.t -> SMT.t

val translate_var : 
  (Encoding.Locations.t, Encoding.HeapEncoding.t) Translation_context.t ->
  SL.Variable.t ->
  SMT.Variable.t

val translate_term : 
  (Encoding.Locations.t, Encoding.HeapEncoding.t) Translation_context.t ->
  SL.Term.t ->
  SMT.t

val translate : Context.t -> SMT.t

val solve : Context.t -> Context.t