18package com.microsoft.z3;
75 return Integer.toString(m_int);
77 return Double.toString(m_double);
79 throw new Z3Exception(
"Unknown statistical entry type");
91 private boolean m_is_int =
false;
92 private boolean m_is_double =
false;
93 private int m_int = 0;
94 private double m_double = 0.0;
117 return Native.statsToString(getContext().nCtx(), getNativeObject());
125 return Native.statsSize(getContext().nCtx(), getNativeObject());
138 for (
int i = 0; i < n; i++)
141 String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
142 if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) {
143 e =
new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
144 getNativeObject(), i));
145 }
else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
146 e =
new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
147 getNativeObject(), i));
163 for (
int i = 0; i < n; i++)
164 res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
179 for (
int i = 0; i < n; i++) {
180 if (es[i].Key.equals(key)) {
198 void addToReferenceQueue() {
199 Native.statsIncRef(getContext().nCtx(), getNativeObject());
IDecRefQueue< Statistics > getStatisticsDRQ()
void storeReference(Context ctx, T obj)
def String(name, ctx=None)