8 using System.Collections.Generic;
12 using System.Runtime.InteropServices;
42 Contract.Requires(a != null);
43 Contract.Ensures(Contract.Result<
BoolExpr>() != null);
46 return new BoolExpr(
this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
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);
67 ASTVector seq =
new ASTVector(
this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
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;
88 int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
90 model =
new Model(
this, m);
102 return Native.Z3_interpolation_profile(nCtx);
113 Contract.Requires(cnsts.Length == parents.Length);
114 Contract.Requires(cnsts.Length == interps.Length + 1);
116 int r = Native.Z3_check_interpolant(nCtx,
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;
140 int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
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);
161 Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length,
Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length,
Expr.ArrayToNative(theory));
string InterpolationProfile()
Return a string summarizing cumulative time used for interpolation.
Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
Computes an interpolant.
Z3_lbool
Lifted Boolean type: false, undefined, true.
The InterpolationContext is suitable for generation of interpolants.
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.
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.
int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
Checks the correctness of an interpolant.
InterpolationContext(Dictionary< string, string > settings)
Constructor.