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);
85 for (
int i = 0; i < n; i++)
86 res[i] =
Expr.create(
this, seq.
get(i).getNativeObject());
99 checkContextMatch(pat);
100 checkContextMatch(p);
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)
Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
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)
static int computeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
static void setParamValue(long a0, String a1, String a2)
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
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()
int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
static final Z3_lbool fromInt(int v)
static int checkInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)