Retrieves the interpretation (the assignment) of a non-constant f in the model. @param f A function declaration of non-zero arity @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise. @throws Z3Exception
(FuncDecl<R> f)
| 74 | * @throws Z3Exception |
| 75 | **/ |
| 76 | public <R extends Sort> FuncInterp<R> getFuncInterp(FuncDecl<R> f) |
| 77 | { |
| 78 | getContext().checkContextMatch(f); |
| 79 | |
| 80 | Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext() |
| 81 | .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject()))); |
| 82 | |
| 83 | if (f.getArity() == 0) |
| 84 | { |
| 85 | long n = Native.modelGetConstInterp(getContext().nCtx(), |
| 86 | getNativeObject(), f.getNativeObject()); |
| 87 | |
| 88 | if (sk == Z3_sort_kind.Z3_ARRAY_SORT) |
| 89 | { |
| 90 | if (n == 0) |
| 91 | return null; |
| 92 | else |
| 93 | { |
| 94 | if (Native.isAsArray(getContext().nCtx(), n)) { |
| 95 | long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); |
| 96 | return getFuncInterp(new FuncDecl<>(getContext(), fd)); |
| 97 | } |
| 98 | return null; |
| 99 | } |
| 100 | } else |
| 101 | { |
| 102 | throw new Z3Exception( |
| 103 | "Constant functions do not have a function interpretation; use getConstInterp"); |
| 104 | } |
| 105 | } else |
| 106 | { |
| 107 | long n = Native.modelGetFuncInterp(getContext().nCtx(), |
| 108 | getNativeObject(), f.getNativeObject()); |
| 109 | if (n == 0) |
| 110 | return null; |
| 111 | else |
| 112 | return new FuncInterp<>(getContext(), n); |
| 113 | } |
| 114 | } |
| 115 | |
| 116 | /** |
| 117 | * The number of constants that have an interpretation in the model. |
no test coverage detected