2 using System.Collections.Generic;
5 using System.Diagnostics.Contracts;
6 using System.Runtime.InteropServices;
15 [ContractVerification(
true)]
36 Contract.Requires(a != null);
37 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
52 Contract.Requires(pf != null);
53 Contract.Requires(pat != null);
54 Contract.Requires(p != null);
55 Contract.Ensures(Contract.Result<
Expr>() != null);
57 CheckContextMatch(pf);
58 CheckContextMatch(pat);
64 for (uint i = 0; i < n; i++)
65 res[i] =
Expr.Create(
this, seq[i].NativeObject);
77 Contract.Requires(pat != null);
78 Contract.Requires(p != null);
79 Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
80 Contract.Ensures(Contract.ValueAtReturn(out model) != null);
82 CheckContextMatch(pat);
85 IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
88 model =
new Model(
this, m);
111 Contract.Requires(cnsts.Length == parents.Length);
112 Contract.Requires(cnsts.Length == interps.Length + 1);
116 Expr.ArrayToNative(cnsts),
118 Expr.ArrayToNative(interps),
121 Expr.ArrayToNative(theory));
122 error = Marshal.PtrToStringAnsi(n_err_str);
134 uint num = 0, num_theory = 0;
139 error = Marshal.PtrToStringAnsi(n_err_str);
140 cnsts =
new Expr[num];
141 parents =
new uint[num];
142 theory =
new Expr[num_theory];
143 for (
int i = 0; i < num; i++)
144 cnsts[i] =
Expr.Create(
this, n_cnsts[i]);
145 for (
int i = 0; i < num_theory; i++)
146 theory[i] =
Expr.Create(
this, n_theory[i]);
158 Contract.Requires(cnsts.Length == parents.Length);
static Z3_ast Z3_mk_interpolant(Z3_context a0, Z3_ast a1)
string InterpolationProfile()
Return a string summarizing cumulative time used for interpolation.
static int Z3_compute_interpolant(Z3_context a0, Z3_ast a1, Z3_params a2, [In, Out] ref Z3_ast_vector a3, [In, Out] ref Z3_model a4)
static int Z3_read_interpolation_problem(Z3_context a0, [In, Out] ref uint a1, [Out] out Z3_ast[] a2, [Out] out uint[] a3, string a4, out IntPtr a5, [In, Out] ref uint a6, [Out] out Z3_ast[] a7)
uint Size
The size of the vector
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
Computes an interpolant.
The InterpolationContext is suitable for generation of interpolants.
static int Z3_check_interpolant(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, [In] Z3_ast[] a4, out IntPtr a5, uint a6, [In] Z3_ast[] a7)
InterpolationContext()
Constructor.
int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
Reads an interpolation problem from a file.
A Params objects represents a configuration in the form of Symbol/value pairs.
A Model contains interpretations (assignments) of constants and functions.
int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
Checks the correctness of an interpolant.
static string Z3_interpolation_profile(Z3_context a0)
The main interaction with Z3 happens via the Context.
void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
Writes an interpolation problem to a file.
static void Z3_write_interpolation_problem(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In] uint[] a3, string a4, uint a5, [In] Z3_ast[] a6)
Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
Computes an interpolant.
static Z3_ast_vector Z3_get_interpolant(Z3_context a0, Z3_ast a1, Z3_ast a2, Z3_params a3)
InterpolationContext(Dictionary< string, string > settings)
Constructor.