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() {