18 package com.microsoft.z3;
21 import java.lang.String;
52 for (
Map.Entry<String, String> kv : settings.entrySet())
78 checkContextMatch(pf);
79 checkContextMatch(pat);
82 ASTVector seq =
new ASTVector(
this,
Native.
getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
85 for (
int i = 0; i < n; i++)
86 res[i] =
Expr.create(
this, seq.get(i).getNativeObject());
97 Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
throws Z3Exception
99 checkContextMatch(pat);
100 checkContextMatch(p);
102 Native.LongPtr n_i =
new Native.LongPtr();
103 Native.LongPtr n_m =
new Native.LongPtr();
104 int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
105 interp =
new ASTVector(
this, n_i.value);
106 model =
new Model(
this, n_m.value);
132 Expr.arrayToNative(cnsts),
134 Expr.arrayToNative(interps),
137 Expr.arrayToNative(theory));
138 error = n_err_str.value;
157 int num = n_num.value;
158 int num_theory = n_num_theory.value;
159 error = n_err_str.value;
160 cnsts =
new Expr[num];
161 parents =
new int[num];
162 theory =
new Expr[num_theory];
163 for (
int i = 0; i < num; i++)
165 cnsts[i] =
Expr.create(
this, n_cnsts.value[i]);
166 parents[i] = n_parents.value[i];
168 for (
int i = 0; i < num_theory; i++)
169 theory[i] =
Expr.create(
this, n_theory.value[i]);
static void delConfig(long a0)
static int readInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
static String interpolationProfile(long a0)
static long mkInterpolant(long a0, long a1)
Z3_lbool
Lifted Boolean type: false, undefined, true.
int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
Reads an interpolation problem from a file.
The InterpolationContext is suitable for generation of interpolants.
static void setParamValue(long a0, String a1, String a2)
static long mkInterpolationContext(long a0)
InterpolationContext(Map< String, String > settings)
static long getInterpolant(long a0, long a1, long a2, long a3)
BoolExpr MkInterpolant(BoolExpr a)
static void writeInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
String InterpolationProfile()
Return a string summarizing cumulative time used for interpolation.
int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
Checks the correctness of an interpolant.
void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
Writes an interpolation problem to a file.
static int checkInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)