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.