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()
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()
135  {
136  return Native.statsSize(getContext().nCtx(), getNativeObject());
137  }
138 
144  public Entry[] getEntries()
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()
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 
185  public Entry get(String key)
186  {
187  int n = size();
188  Entry[] es = getEntries();
189  for (int i = 0; i < n; i++)
190  if (es[i].Key == key)
191  return es[i];
192  return null;
193  }
194 
195  Statistics(Context ctx, long obj)
196  {
197  super(ctx, obj);
198  }
199 
200  void incRef(long o)
201  {
202  getContext().getStatisticsDRQ().incAndClear(getContext(), o);
203  super.incRef(o);
204  }
205 
206  void decRef(long o)
207  {
208  getContext().getStatisticsDRQ().add(o);
209  super.decRef(o);
210  }
211 }
static int statsSize(long a0, long a1)
Definition: Native.java:4673
String Key
Definition: Statistics.java:34
static String statsGetKey(long a0, long a1, int a2)
Definition: Native.java:4682
Definition: Statistics.java:29
int getUIntValue()
Definition: Statistics.java:39
static boolean statsIsUint(long a0, long a1, int a2)
Definition: Native.java:4691
static int statsGetUintValue(long a0, long a1, int a2)
Definition: Native.java:4709
static double statsGetDoubleValue(long a0, long a1, int a2)
Definition: Native.java:4718
String getValueString()
Definition: Statistics.java:73
static boolean statsIsDouble(long a0, long a1, int a2)
Definition: Native.java:4700
static String statsToString(long a0, long a1)
Definition: Native.java:4648
String toString()
Definition: Statistics.java:86
double getDoubleValue()
Definition: Statistics.java:47
boolean isUInt()
Definition: Statistics.java:55
boolean isDouble()
Definition: Statistics.java:63