18 package com.microsoft.z3;
37 getContext().checkContextMatch(a);
51 getContext().checkContextMatch(f);
57 "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
64 return Expr.create(getContext(), n);
78 getContext().checkContextMatch(f);
81 .nCtx(),
Native.
getRange(getContext().nCtx(), f.getNativeObject())));
83 if (f.getArity() == 0)
86 getNativeObject(), f.getNativeObject());
96 "Argument was not an array constant");
103 "Constant functions do not have a function interpretation; use ConstInterp");
108 getNativeObject(), f.getNativeObject());
133 for (
int i = 0; i < n; i++)
135 .nCtx(), getNativeObject(), i));
156 for (
int i = 0; i < n; i++)
158 .nCtx(), getNativeObject(), i));
171 int n = nFuncs + nConsts;
173 for (
int i = 0; i < nConsts; i++)
175 .nCtx(), getNativeObject(), i));
176 for (
int i = 0; i < nFuncs; i++)
178 getContext().nCtx(), getNativeObject(), i));
186 @SuppressWarnings(
"serial")
215 t.getNativeObject(), (completion) ?
true :
false, v) ^
true)
218 return Expr.create(getContext(), v.value);
228 return eval(t, completion);
254 for (
int i = 0; i < n; i++)
255 res[i] =
Sort.create(getContext(),
273 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
274 int n = nUniv.size();
276 for (
int i = 0; i < n; i++)
277 res[i] =
Expr.create(getContext(), nUniv.get(i).getNativeObject());
293 return "Z3Exception: " + e.getMessage();
302 void incRef(
long o)
throws Z3Exception
304 getContext().model_DRQ().incAndClear(getContext(), o);
308 void decRef(
long o)
throws Z3Exception
310 getContext().model_DRQ().add(o);
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()
static boolean isAsArray(long a0, long a1)
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)
FuncInterp getFuncInterp(FuncDecl f)