Data Structures | |
class | Entry |
Public Member Functions | |
String | toString () |
int | size () throws Z3Exception |
Entry[] | getEntries () throws Z3Exception |
String[] | getKeys () throws Z3Exception |
Entry | get (String key) throws Z3Exception |
Package Functions | |
Statistics (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
Objects of this class track statistical information about solvers.
Definition at line 23 of file Statistics.java.
Statistics | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 194 of file Statistics.java.
{ super(ctx, obj); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 205 of file Statistics.java.
{ getContext().statistics_DRQ().add(o); super.decRef(o); }
Entry get | ( | String | key | ) | throws Z3Exception [inline] |
The value of a particular statistical counter. Returns null if the key is unknown.
Z3Exception |
Definition at line 184 of file Statistics.java.
{ int n = size(); Entry[] es = getEntries(); for (int i = 0; i < n; i++) if (es[i].Key == key) return es[i]; return null; }
Entry [] getEntries | ( | ) | throws Z3Exception [inline] |
The data entries.
Z3Exception |
Definition at line 144 of file Statistics.java.
Referenced by Statistics.get().
{ int n = size(); Entry[] res = new Entry[n]; for (int i = 0; i < n; i++) { Entry e; String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i); if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(), getNativeObject(), i)); else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(), getNativeObject(), i)); else throw new Z3Exception("Unknown data entry value"); res[i] = e; } return res; }
String [] getKeys | ( | ) | throws Z3Exception [inline] |
The statistical counters.
Definition at line 169 of file Statistics.java.
{ int n = size(); String[] res = new String[n]; for (int i = 0; i < n; i++) res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i); return res; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 199 of file Statistics.java.
{ getContext().statistics_DRQ().incAndClear(getContext(), o); super.incRef(o); }
int size | ( | ) | throws Z3Exception [inline] |
The number of statistical data.
Definition at line 134 of file Statistics.java.
Referenced by Statistics.get(), Statistics.getEntries(), and Statistics.getKeys().
{ return Native.statsSize(getContext().nCtx(), getNativeObject()); }
String toString | ( | ) | [inline] |
A string representation of the statistical data.
Definition at line 120 of file Statistics.java.
{ try { return Native.statsToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }