18 package com.microsoft.z3;
37 getContext().checkContextMatch(a);
52 getContext().checkContextMatch(f);
55 "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
62 return Expr.create(getContext(), n);
75 getContext().checkContextMatch(f);
78 .nCtx(),
Native.
getRange(getContext().nCtx(), f.getNativeObject())));
83 getNativeObject(), f.getNativeObject());
100 "Constant functions do not have a function interpretation; use getConstInterp");
105 getNativeObject(), f.getNativeObject());
130 for (
int i = 0; i < n; i++)
132 .nCtx(), getNativeObject(), i));
153 for (
int i = 0; i < n; i++)
155 .nCtx(), getNativeObject(), i));
168 int n = nFuncs + nConsts;
170 for (
int i = 0; i < nConsts; i++)
172 .nCtx(), getNativeObject(), i));
173 for (
int i = 0; i < nFuncs; i++)
175 getContext().nCtx(), getNativeObject(), i));
183 @SuppressWarnings(
"serial")
212 t.getNativeObject(), (completion), v))
215 return Expr.create(getContext(), v.value);
225 return eval(t, completion);
253 for (
int i = 0; i < n; i++)
254 res[i] =
Sort.create(getContext(),
272 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
293 Native.modelIncRef(getContext().nCtx(), getNativeObject());
297 void addToReferenceQueue() {
Expr evaluate(Expr t, boolean completion)
Expr getConstInterp(Expr a)
static long modelGetSort(long a0, long a1, int a2)
Expr [] getSortUniverse(Sort s)
Expr getConstInterp(FuncDecl f)
static int modelGetNumSorts(long a0, long a1)
static int modelGetNumConsts(long a0, long a1)
static long getAsArrayFuncDecl(long a0, long a1)
static int getSortKind(long a0, long a1)
static final Z3_sort_kind fromInt(int v)
FuncDecl [] getFuncDecls()
Expr eval(Expr t, boolean completion)
ModelEvaluationFailedException()
IDecRefQueue< Model > getModelDRQ()
static boolean isAsArray(long a0, long a1)
void storeReference(Context ctx, T obj)
FuncDecl [] getConstDecls()
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
static long modelGetFuncDecl(long a0, long a1, int a2)
static long modelGetSortUniverse(long a0, long a1, long a2)
static long modelGetConstDecl(long a0, long a1, int a2)
static long modelGetConstInterp(long a0, long a1, long a2)
static int modelGetNumFuncs(long a0, long a1)
static String modelToString(long a0, long a1)
static long getRange(long a0, long a1)
static long modelGetFuncInterp(long a0, long a1, long a2)
def String(name, ctx=None)
FuncInterp getFuncInterp(FuncDecl f)