18package com.microsoft.z3;
25@SuppressWarnings(
"unchecked")
32 public static class Entry<R
extends Sort> extends
Z3Object {
43 Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
50 public int getNumArgs()
52 return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
65 for (
int i = 0; i < n; i++)
66 res[i] =
Expr.create(getContext(), Native.funcEntryGetArg(
67 getContext().nCtx(), getNativeObject(), i));
80 for (
int i = 0; i < n; i++)
81 res += args[i] +
", ";
82 return res + getValue() +
"]";
91 Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
95 void addToReferenceQueue() {
96 getContext().getFuncEntryDRQ().storeReference(getContext(),
this);
107 return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
118 int n = getNumEntries();
119 Entry<R>[] res =
new Entry[n];
120 for (
int i = 0; i < n; i++)
121 res[i] =
new Entry<>(getContext(), Native.funcInterpGetEntry(getContext()
122 .nCtx(), getNativeObject(), i));
136 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
146 return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
156 for (Entry<R> e : getEntries())
158 int n = e.getNumArgs();
162 for (
int i = 0; i < n; i++)
170 res +=
" -> " + e.getValue() +
", ";
172 res +=
"else -> " + getElse();
184 Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
188 void addToReferenceQueue() {
189 getContext().getFuncInterpDRQ().storeReference(getContext(),
this);
Entry< R >[] getEntries()
def String(name, ctx=None)