Z3 |

Statistics.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public 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
72 public String getValueString()
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
115 public String toString()
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}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.getStatisticsDRQ
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4130
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Statistics.Entry
Definition: Statistics.java:29
com.microsoft.z3.Statistics.Entry.Key
String Key
Definition: Statistics.java:33
com.microsoft.z3.Statistics.Entry.getDoubleValue
double getDoubleValue()
Definition: Statistics.java:46
com.microsoft.z3.Statistics.Entry.isDouble
boolean isDouble()
Definition: Statistics.java:62
com.microsoft.z3.Statistics.Entry.isUInt
boolean isUInt()
Definition: Statistics.java:54
com.microsoft.z3.Statistics.Entry.getUIntValue
int getUIntValue()
Definition: Statistics.java:38
com.microsoft.z3.Statistics.Entry.toString
String toString()
Definition: Statistics.java:87
com.microsoft.z3.Statistics.Entry.getValueString
String getValueString()
Definition: Statistics.java:72
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Statistics.getEntries
Entry[] getEntries()
Definition: Statistics.java:133
com.microsoft.z3.Statistics.getKeys
String[] getKeys()
Definition: Statistics.java:159
com.microsoft.z3.Statistics.toString
String toString()
Definition: Statistics.java:115
com.microsoft.z3.Statistics.size
int size()
Definition: Statistics.java:123
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693