18 package com.microsoft.z3;
37 getContext().checkContextMatch(a);
52 getContext().checkContextMatch(f);
57 throw new Z3Exception(
58 "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp.");
65 return Expr.create(getContext(), n);
78 getContext().checkContextMatch(f);
81 .nCtx(),
Native.
getRange(getContext().nCtx(), f.getNativeObject())));
86 getNativeObject(), f.getNativeObject());
102 throw new Z3Exception(
103 "Constant functions do not have a function interpretation; use getConstInterp");
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")
187 public class ModelEvaluationFailedException extends Z3Exception
192 public ModelEvaluationFailedException()
211 public Expr eval(Expr t,
boolean completion)
213 Native.LongPtr v =
new Native.LongPtr();
214 if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
215 t.getNativeObject(), (completion), v))
216 throw new ModelEvaluationFailedException();
218 return Expr.create(getContext(), v.value);
226 public Expr evaluate(Expr t,
boolean completion)
228 return eval(t, completion);
235 public int getNumSorts()
237 return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
251 public Sort[] getSorts()
254 int n = getNumSorts();
255 Sort[] res =
new Sort[n];
256 for (
int i = 0; i < n; i++)
257 res[i] = Sort.create(getContext(),
258 Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
271 public Expr[] getSortUniverse(Sort s)
274 ASTVector nUniv =
new ASTVector(getContext(), Native.modelGetSortUniverse(
275 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
276 return nUniv.ToExprArray();
285 public String toString() {
286 return Native.modelToString(getContext().nCtx(), getNativeObject());
289 Model(Context ctx,
long obj)
296 Native.modelIncRef(getContext().nCtx(), getNativeObject());
300 void addToReferenceQueue() {
301 getContext().
getModelDRQ().storeReference(getContext(),
this);
Expr getConstInterp(Expr a)
Expr getConstInterp(FuncDecl f)
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()
IDecRefQueue< Model > getModelDRQ()
static boolean isAsArray(long a0, long a1)
FuncDecl[] getConstDecls()
static long modelGetFuncDecl(long a0, long a1, int 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 long getRange(long a0, long a1)
static long modelGetFuncInterp(long a0, long a1, long a2)
FuncInterp getFuncInterp(FuncDecl f)