18package com.microsoft.z3;
20import com.microsoft.z3.enumerations.Z3_sort_kind;
25@SuppressWarnings(
"unchecked")
38 getContext().checkContextMatch(a);
53 getContext().checkContextMatch(f);
56 "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
58 long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
76 getContext().checkContextMatch(f);
79 .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
83 long n = Native.modelGetConstInterp(getContext().nCtx(),
84 getNativeObject(), f.getNativeObject());
92 if (Native.isAsArray(getContext().nCtx(), n)) {
93 long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
94 return getFuncInterp(
new FuncDecl<>(getContext(), fd));
101 "Constant functions do not have a function interpretation; use getConstInterp");
105 long n = Native.modelGetFuncInterp(getContext().nCtx(),
106 getNativeObject(), f.getNativeObject());
119 return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
129 int n = getNumConsts();
131 for (
int i = 0; i < n; i++)
132 res[i] =
new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
133 .nCtx(), getNativeObject(), i));
142 return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
152 int n = getNumFuncs();
154 for (
int i = 0; i < n; i++)
155 res[i] =
new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext()
156 .nCtx(), getNativeObject(), i));
167 int nFuncs = getNumFuncs();
168 int nConsts = getNumConsts();
169 int n = nFuncs + nConsts;
171 for (
int i = 0; i < nConsts; i++)
172 res[i] =
new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
173 .nCtx(), getNativeObject(), i));
174 for (
int i = 0; i < nFuncs; i++)
175 res[nConsts + i] =
new FuncDecl<>(getContext(), Native.modelGetFuncDecl(
176 getContext().nCtx(), getNativeObject(), i));
184 @SuppressWarnings(
"serial")
209 public <R extends Sort>
Expr<R> eval(
Expr<R> t,
boolean completion)
211 Native.LongPtr v =
new Native.LongPtr();
212 if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
213 t.getNativeObject(), (completion), v))
214 throw new ModelEvaluationFailedException();
216 return (
Expr<R>)
Expr.create(getContext(), v.value);
224 public <R extends Sort> Expr<R> evaluate(Expr<R> t,
boolean completion)
226 return eval(t, completion);
235 return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
252 int n = getNumSorts();
254 for (
int i = 0; i < n; i++)
255 res[i] =
Sort.create(getContext(),
256 Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
269 public <R extends Sort>
Expr<R>[] getSortUniverse(R s)
273 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
284 return Native.modelToString(getContext().nCtx(), getNativeObject());
294 Native.modelIncRef(getContext().nCtx(), getNativeObject());
298 void addToReferenceQueue() {
299 getContext().getModelDRQ().storeReference(getContext(),
this);
FuncDecl< R > getFuncDecl()
ModelEvaluationFailedException()
FuncDecl<?>[] getFuncDecls()
FuncDecl<?>[] getConstDecls()
def String(name, ctx=None)
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).