sig
val mk_interpolant : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
val mk_interpolation_context : (string * string) list -> Z3.context
val get_interpolant :
Z3.context ->
Z3.Expr.expr -> Z3.Expr.expr -> Z3.Params.params -> Z3.Expr.expr list
val compute_interpolant :
Z3.context ->
Z3.Expr.expr ->
Z3.Params.params ->
Z3enums.lbool * Z3.Expr.expr list option * Z3.Model.model option
val get_interpolation_profile : Z3.context -> string
val read_interpolation_problem :
Z3.context -> string -> Z3.Expr.expr list * int list * Z3.Expr.expr list
val check_interpolant :
Z3.context ->
int ->
Z3.Expr.expr list ->
int list -> Z3.Expr.expr list -> int -> Z3.Expr.expr list -> unit
val write_interpolation_problem :
Z3.context ->
int ->
Z3.Expr.expr list ->
int list -> string -> int -> Z3.Expr.expr list -> unit
end