The InterpolationContext is suitable for generation of interpolants. More...
Public Member Functions | |
InterpolationContext () throws Z3Exception | |
InterpolationContext (Map< String, String > settings) throws Z3Exception | |
BoolExpr | MkInterpolant (BoolExpr a) throws Z3Exception |
String | InterpolationProfile () throws Z3Exception |
Return a string summarizing cumulative time used for interpolation. | |
int | CheckInterpolant (Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception |
Checks the correctness of an interpolant. | |
int | ReadInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception |
Reads an interpolation problem from a file. | |
void | WriteInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception |
Writes an interpolation problem to a file. | |
Package Functions | |
Expr[] | GetInterpolant (Expr pf, Expr pat, Params p) throws Z3Exception |
Z3_lbool | ComputeInterpolant (Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception |
The InterpolationContext is suitable for generation of interpolants.
For more information on interpolation please refer too the C/C++ API, which is well documented.
Definition at line 33 of file InterpolationContext.java.
InterpolationContext | ( | ) | throws Z3Exception [inline] |
Definition at line 38 of file InterpolationContext.java.
{ m_ctx = Native.mkInterpolationContext(0); initContext(); }
InterpolationContext | ( | Map< String, String > | settings | ) | throws Z3Exception [inline] |
Definition at line 49 of file InterpolationContext.java.
{ long cfg = Native.mkConfig(); for (Map.Entry<String, String> kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkInterpolationContext(cfg); Native.delConfig(cfg); initContext(); }
int CheckInterpolant | ( | Expr[] | cnsts, |
int[] | parents, | ||
Expr[] | interps, | ||
String | error, | ||
Expr[] | theory | ||
) | throws Z3Exception [inline] |
Checks the correctness of an interpolant.
For more information on interpolation please refer too the function Z3_check_interpolant in the C/C++ API, which is well documented.
Definition at line 127 of file InterpolationContext.java.
{ Native.StringPtr n_err_str = new Native.StringPtr(); int r = Native.checkInterpolant(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, Expr.arrayToNative(interps), n_err_str, theory.length, Expr.arrayToNative(theory)); error = n_err_str.value; return r; }
Z3_lbool ComputeInterpolant | ( | Expr | pat, |
Params | p, | ||
ASTVector | interp, | ||
Model | model | ||
) | throws Z3Exception [inline, package] |
Computes an interpolant. For more information on interpolation please refer too the function Z3_compute_interpolant in the C/C++ API, which is well documented.
Z3Exception |
Definition at line 97 of file InterpolationContext.java.
{ checkContextMatch(pat); checkContextMatch(p); Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m); interp = new ASTVector(this, n_i.value); model = new Model(this, n_m.value); return Z3_lbool.fromInt(r); }
Expr [] GetInterpolant | ( | Expr | pf, |
Expr | pat, | ||
Params | p | ||
) | throws Z3Exception [inline, package] |
Computes an interpolant. For more information on interpolation please refer too the function Z3_get_interpolant in the C/C++ API, which is well documented.
Z3Exception |
Definition at line 76 of file InterpolationContext.java.
{ checkContextMatch(pf); checkContextMatch(pat); checkContextMatch(p); ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); int n = seq.size(); Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(this, seq.get(i).getNativeObject()); return res; }
String InterpolationProfile | ( | ) | throws Z3Exception [inline] |
Return a string summarizing cumulative time used for interpolation.
For more information on interpolation please refer too the function Z3_interpolation_profile in the C/C++ API, which is well documented.
Definition at line 116 of file InterpolationContext.java.
{ return Native.interpolationProfile(nCtx()); }
BoolExpr MkInterpolant | ( | BoolExpr | a | ) | throws Z3Exception [inline] |
Create an expression that marks a formula position for interpolation.
Z3Exception |
Definition at line 63 of file InterpolationContext.java.
{ checkContextMatch(a); return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); }
int ReadInterpolationProblem | ( | String | filename, |
Expr[] | cnsts, | ||
int[] | parents, | ||
String | error, | ||
Expr[] | theory | ||
) | throws Z3Exception [inline] |
Reads an interpolation problem from a file.
For more information on interpolation please refer too the function Z3_read_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 148 of file InterpolationContext.java.
{ Native.IntPtr n_num = new Native.IntPtr(); Native.IntPtr n_num_theory = new Native.IntPtr(); Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr(); Native.StringPtr n_err_str = new Native.StringPtr(); int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory); int num = n_num.value; int num_theory = n_num_theory.value; error = n_err_str.value; cnsts = new Expr[num]; parents = new int[num]; theory = new Expr[num_theory]; for (int i = 0; i < num; i++) { cnsts[i] = Expr.create(this, n_cnsts.value[i]); parents[i] = n_parents.value[i]; } for (int i = 0; i < num_theory; i++) theory[i] = Expr.create(this, n_theory.value[i]); return r; }
void WriteInterpolationProblem | ( | String | filename, |
Expr[] | cnsts, | ||
int[] | parents, | ||
String | error, | ||
Expr[] | theory | ||
) | throws Z3Exception [inline] |
Writes an interpolation problem to a file.
For more information on interpolation please refer too the function Z3_write_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 179 of file InterpolationContext.java.
{ Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); }