|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
The InterpolationContext is suitable for generation of interpolants. More...
Inheritance diagram for InterpolationContext: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));
}
1.7.6.1