8 using System.Collections.Generic;
11 using System.Diagnostics.Contracts;
12 using System.Runtime.InteropServices;
21 [ContractVerification(
true)]
42 Contract.Requires(a != null);
43 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
58 Contract.Requires(pf != null);
59 Contract.Requires(pat != null);
60 Contract.Requires(p != null);
61 Contract.Ensures(Contract.Result<
Expr>() != null);
63 CheckContextMatch(pf);
64 CheckContextMatch(pat);
79 Contract.Requires(pat != null);
80 Contract.Requires(p != null);
81 Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
82 Contract.Ensures(Contract.ValueAtReturn(out model) != null);
84 CheckContextMatch(pat);
87 IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
90 model =
new Model(
this, m);
113 Contract.Requires(cnsts.Length == parents.Length);
114 Contract.Requires(cnsts.Length == interps.Length + 1);
118 Expr.ArrayToNative(cnsts),
120 Expr.ArrayToNative(interps),
123 Expr.ArrayToNative(theory));
124 error = Marshal.PtrToStringAnsi(n_err_str);
136 uint num = 0, num_theory = 0;
141 error = Marshal.PtrToStringAnsi(n_err_str);
142 cnsts =
new Expr[num];
143 parents =
new uint[num];
144 theory =
new Expr[num_theory];
145 for (
int i = 0; i < num; i++)
146 cnsts[i] =
Expr.Create(
this, n_cnsts[i]);
147 for (
int i = 0; i < num_theory; i++)
148 theory[i] =
Expr.Create(
this, n_theory[i]);
160 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)
Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
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.
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
A Params objects represents a configuration in the form of Symbol/value pairs.
A Model contains interpretations (assignments) of constants and functions.
static string Z3_interpolation_profile(Z3_context a0)
The main interaction with Z3 happens via the Context.
BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
Computes an interpolant.
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)
int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
Checks the correctness of 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.