18 package com.microsoft.z3;
38 getContext().checkContextMatch(a);
53 getContext().checkContextMatch(f);
59 "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
66 return Expr.create(getContext(), n);
79 getContext().checkContextMatch(f);
82 .nCtx(),
Native.
getRange(getContext().nCtx(), f.getNativeObject())));
87 getNativeObject(), f.getNativeObject());
97 "Argument was not an array constant");
104 "Constant functions do not have a function interpretation; use ConstInterp");
109 getNativeObject(), f.getNativeObject());
134 for (
int i = 0; i < n; i++)
136 .nCtx(), getNativeObject(), i));
157 for (
int i = 0; i < n; i++)
159 .nCtx(), getNativeObject(), i));
172 int n = nFuncs + nConsts;
174 for (
int i = 0; i < nConsts; i++)
176 .nCtx(), getNativeObject(), i));
177 for (
int i = 0; i < nFuncs; i++)
179 getContext().nCtx(), getNativeObject(), i));
187 @SuppressWarnings(
"serial")
215 t.getNativeObject(), (completion) ?
true :
false, v) ^
true)
218 return Expr.create(getContext(), v.value);
228 return eval(t, completion);
256 for (
int i = 0; i < n; i++)
257 res[i] =
Sort.create(getContext(),
275 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
291 return "Z3Exception: " + e.getMessage();
Expr evaluate(Expr t, boolean completion)
Expr getConstInterp(Expr a)
static long modelGetSort(long a0, long a1, int a2)
Expr[] getSortUniverse(Sort s)
IDecRefQueue getModelDRQ()
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()
void incAndClear(Context ctx, long o)
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)