Make (astral.Astral_internal.Translation.Make)

Parameters

module Encoding : Translation_sig.ENCODING

module Solver : Backend_sig.BACKEND

val formula_footprint : (_, _) 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