Module Z3.Interpolation

module Interpolation: sig .. end
Interpolation

val mk_interpolant : context -> Expr.expr -> Expr.expr
Create an AST node marking a formula position for interpolation. The expression must have Boolean sort.
val mk_interpolation_context : (string * string) list -> context
The interpolation context is suitable for generation of interpolants. For more information on interpolation please refer too the C/C++ API, which is well documented.
val get_interpolant : context ->
Expr.expr -> Expr.expr -> Params.params -> Expr.expr list
Gets an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented.
val compute_interpolant : context ->
Expr.expr ->
Params.params ->
Z3enums.lbool * Expr.expr list option * Model.model option
Computes an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented.
val get_interpolation_profile : context -> string
Retrieves an interpolation profile. For more information on interpolation please refer too the C/C++ API, which is well documented.
val read_interpolation_problem : context -> string -> Expr.expr list * int list * Expr.expr list
Read an interpolation problem from file. For more information on interpolation please refer too the C/C++ API, which is well documented.
val check_interpolant : context ->
int ->
Expr.expr list ->
int list -> Expr.expr list -> int -> Expr.expr list -> unit
Check the correctness of an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented.
val write_interpolation_problem : context ->
int ->
Expr.expr list -> int list -> string -> int -> Expr.expr list -> unit
Write an interpolation problem to file suitable for reading with Z3_read_interpolation_problem. For more information on interpolation please refer too the C/C++ API, which is well documented.