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 
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 }
static int statsSize(long a0, long a1)
Definition: Native.java:4392
String Key
Definition: Statistics.java:33
static String statsGetKey(long a0, long a1, int a2)
Definition: Native.java:4401
Definition: Statistics.java:28
int getUIntValue()
Definition: Statistics.java:38
static boolean statsIsUint(long a0, long a1, int a2)
Definition: Native.java:4410
static int statsGetUintValue(long a0, long a1, int a2)
Definition: Native.java:4428
static double statsGetDoubleValue(long a0, long a1, int a2)
Definition: Native.java:4437
String getValueString()
Definition: Statistics.java:72
static void statsIncRef(long a0, long a1)
Definition: Native.java:4376
static boolean statsIsDouble(long a0, long a1, int a2)
Definition: Native.java:4419
static String statsToString(long a0, long a1)
Definition: Native.java:4367
String toString()
Definition: Statistics.java:87
double getDoubleValue()
Definition: Statistics.java:46
boolean isUInt()
Definition: Statistics.java:54
boolean isDouble()
Definition: Statistics.java:62
def String(name, ctx=None)
Definition: z3py.py:9443