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);
102 checkContextMatch(pat);
103 checkContextMatch(p);
129 public int return_value = 0;
130 public String error = null;
145 Expr.arrayToNative(cnsts),
147 Expr.arrayToNative(interps),
150 Expr.arrayToNative(theory));
151 res.
error = n_err_str.value;
157 public int return_value = 0;
181 int num = n_num.value;
182 int num_theory = n_num_theory.value;
183 res.
error = n_err_str.value;
186 theory =
new Expr[num_theory];
187 for (
int i = 0; i < num; i++)
189 res.
cnsts[i] =
Expr.create(
this, n_cnsts.value[i]);
190 res.
parents[i] = n_parents.value[i];
192 for (
int i = 0; i < num_theory; i++)
193 res.
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)
BoolExpr[] ToBoolExprArray()
static long mkInterpolant(long a0, long a1)
ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
static int computeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
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()
void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, 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)