Z3
Statistics.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class Statistics extends Z3Object {
28 public class Entry
29 {
33 public String Key;
34
38 public int getUIntValue()
39 {
40 return m_int;
41 }
42
46 public double getDoubleValue()
47 {
48 return m_double;
49 }
50
54 public boolean isUInt()
55 {
56 return m_is_int;
57 }
58
62 public boolean isDouble()
63 {
64 return m_is_double;
65 }
66
73 {
74 if (isUInt()) {
75 return Integer.toString(m_int);
76 } else if (isDouble()) {
77 return Double.toString(m_double);
78 } else {
79 throw new Z3Exception("Unknown statistical entry type");
80 }
81 }
82
86 @Override
87 public String toString() {
88 return Key + ": " + getValueString();
89 }
90
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;
95
96 Entry(String k, int v)
97 {
98 Key = k;
99 m_is_int = true;
100 m_int = v;
101 }
102
103 Entry(String k, double v)
104 {
105 Key = k;
106 m_is_double = true;
107 m_double = v;
108 }
109 }
110
114 @Override
116 {
117 return Native.statsToString(getContext().nCtx(), getNativeObject());
118 }
119
123 public int size()
124 {
125 return Native.statsSize(getContext().nCtx(), getNativeObject());
126 }
127
133 public Entry[] getEntries()
134 {
135
136 int n = size();
137 Entry[] res = new Entry[n];
138 for (int i = 0; i < n; i++)
139 {
140 Entry e;
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));
148 } else {
149 throw new Z3Exception("Unknown data entry value");
150 }
151 res[i] = e;
152 }
153 return res;
154 }
155
159 public String[] getKeys()
160 {
161 int n = size();
162 String[] res = new String[n];
163 for (int i = 0; i < n; i++)
164 res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
165 return res;
166 }
167
175 public Entry get(String key)
176 {
177 int n = size();
178 Entry[] es = getEntries();
179 for (int i = 0; i < n; i++) {
180 if (es[i].Key.equals(key)) {
181 return es[i];
182 }
183 }
184 return null;
185 }
186
187 Statistics(Context ctx, long obj)
188 {
189 super(ctx, obj);
190 }
191
192 @Override
193 void incRef() {
194 getContext().getStatisticsDRQ().storeReference(getContext(), this);
195 }
196
197 @Override
198 void addToReferenceQueue() {
199 Native.statsIncRef(getContext().nCtx(), getNativeObject());
200 }
201}
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4130
void storeReference(Context ctx, T obj)
Definition: Statistics.java:29
String Key
Definition: Statistics.java:33
double getDoubleValue()
Definition: Statistics.java:46
boolean isDouble()
Definition: Statistics.java:62
boolean isUInt()
Definition: Statistics.java:54
int getUIntValue()
Definition: Statistics.java:38
String toString()
Definition: Statistics.java:87
String getValueString()
Definition: Statistics.java:72
def String(name, ctx=None)
Definition: z3py.py:10693