Z3
Statistics.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class Statistics extends Z3Object
24 {
29  public class Entry
30  {
34  public String Key;
35 
39  public int getUIntValue()
40  {
41  return m_int;
42  }
43 
47  public double getDoubleValue()
48  {
49  return m_double;
50  }
51 
55  public boolean isUInt()
56  {
57  return m_is_int;
58  }
59 
63  public boolean isDouble()
64  {
65  return m_is_double;
66  }
67 
73  public String getValueString() throws Z3Exception
74  {
75  if (isUInt())
76  return Integer.toString(m_int);
77  else if (isDouble())
78  return Double.toString(m_double);
79  else
80  throw new Z3Exception("Unknown statistical entry type");
81  }
82 
86  public String toString()
87  {
88  try
89  {
90  return Key + ": " + getValueString();
91  } catch (Z3Exception e)
92  {
93  return new String("Z3Exception: " + e.getMessage());
94  }
95  }
96 
97  private boolean m_is_int = false;
98  private boolean m_is_double = false;
99  private int m_int = 0;
100  private double m_double = 0.0;
101 
102  Entry(String k, int v)
103  {
104  Key = k;
105  m_is_int = true;
106  m_int = v;
107  }
108 
109  Entry(String k, double v)
110  {
111  Key = k;
112  m_is_double = true;
113  m_double = v;
114  }
115  }
116 
120  public String toString()
121  {
122  try
123  {
124  return Native.statsToString(getContext().nCtx(), getNativeObject());
125  } catch (Z3Exception e)
126  {
127  return "Z3Exception: " + e.getMessage();
128  }
129  }
130 
134  public int size() throws Z3Exception
135  {
136  return Native.statsSize(getContext().nCtx(), getNativeObject());
137  }
138 
144  public Entry[] getEntries() throws Z3Exception
145  {
146 
147  int n = size();
148  Entry[] res = new Entry[n];
149  for (int i = 0; i < n; i++)
150  {
151  Entry e;
152  String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
153  if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i))
154  e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
155  getNativeObject(), i));
156  else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i))
157  e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
158  getNativeObject(), i));
159  else
160  throw new Z3Exception("Unknown data entry value");
161  res[i] = e;
162  }
163  return res;
164  }
165 
169  public String[] getKeys() throws Z3Exception
170  {
171  int n = size();
172  String[] res = new String[n];
173  for (int i = 0; i < n; i++)
174  res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
175  return res;
176  }
177 
184  public Entry get(String key) throws Z3Exception
185  {
186  int n = size();
187  Entry[] es = getEntries();
188  for (int i = 0; i < n; i++)
189  if (es[i].Key == key)
190  return es[i];
191  return null;
192  }
193 
194  Statistics(Context ctx, long obj) throws Z3Exception
195  {
196  super(ctx, obj);
197  }
198 
199  void incRef(long o) throws Z3Exception
200  {
201  getContext().statistics_DRQ().incAndClear(getContext(), o);
202  super.incRef(o);
203  }
204 
205  void decRef(long o) throws Z3Exception
206  {
207  getContext().statistics_DRQ().add(o);
208  super.decRef(o);
209  }
210 }
static int statsSize(long a0, long a1)
Definition: Native.java:4380
String Key
Definition: Statistics.java:34
static String statsGetKey(long a0, long a1, int a2)
Definition: Native.java:4389
Definition: Statistics.java:29
int getUIntValue()
Definition: Statistics.java:39
static boolean statsIsUint(long a0, long a1, int a2)
Definition: Native.java:4398
static int statsGetUintValue(long a0, long a1, int a2)
Definition: Native.java:4416
static double statsGetDoubleValue(long a0, long a1, int a2)
Definition: Native.java:4425
String getValueString()
Definition: Statistics.java:73
static boolean statsIsDouble(long a0, long a1, int a2)
Definition: Native.java:4407
static String statsToString(long a0, long a1)
Definition: Native.java:4355
String toString()
Definition: Statistics.java:86
double getDoubleValue()
Definition: Statistics.java:47
boolean isUInt()
Definition: Statistics.java:55
boolean isDouble()
Definition: Statistics.java:63