Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00023 public class Statistics extends Z3Object
00024 {
00029 public class Entry
00030 {
00034 public String Key;
00035
00039 public int getUIntValue()
00040 {
00041 return m_int;
00042 }
00043
00047 public double getDoubleValue()
00048 {
00049 return m_double;
00050 }
00051
00055 public boolean isUInt()
00056 {
00057 return m_is_int;
00058 }
00059
00063 public boolean isDouble()
00064 {
00065 return m_is_double;
00066 }
00067
00073 public String getValueString() throws Z3Exception
00074 {
00075 if (isUInt())
00076 return Integer.toString(m_int);
00077 else if (isDouble())
00078 return Double.toString(m_double);
00079 else
00080 throw new Z3Exception("Unknown statistical entry type");
00081 }
00082
00086 public String toString()
00087 {
00088 try
00089 {
00090 return Key + ": " + getValueString();
00091 } catch (Z3Exception e)
00092 {
00093 return new String("Z3Exception: " + e.getMessage());
00094 }
00095 }
00096
00097 private boolean m_is_int = false;
00098 private boolean m_is_double = false;
00099 private int m_int = 0;
00100 private double m_double = 0.0;
00101
00102 Entry(String k, int v)
00103 {
00104 Key = k;
00105 m_is_int = true;
00106 m_int = v;
00107 }
00108
00109 Entry(String k, double v)
00110 {
00111 Key = k;
00112 m_is_double = true;
00113 m_double = v;
00114 }
00115 }
00116
00120 public String toString()
00121 {
00122 try
00123 {
00124 return Native.statsToString(getContext().nCtx(), getNativeObject());
00125 } catch (Z3Exception e)
00126 {
00127 return "Z3Exception: " + e.getMessage();
00128 }
00129 }
00130
00134 public int size() throws Z3Exception
00135 {
00136 return Native.statsSize(getContext().nCtx(), getNativeObject());
00137 }
00138
00144 public Entry[] getEntries() throws Z3Exception
00145 {
00146
00147 int n = size();
00148 Entry[] res = new Entry[n];
00149 for (int i = 0; i < n; i++)
00150 {
00151 Entry e;
00152 String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
00153 if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i))
00154 e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
00155 getNativeObject(), i));
00156 else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i))
00157 e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
00158 getNativeObject(), i));
00159 else
00160 throw new Z3Exception("Unknown data entry value");
00161 res[i] = e;
00162 }
00163 return res;
00164 }
00165
00169 public String[] getKeys() throws Z3Exception
00170 {
00171 int n = size();
00172 String[] res = new String[n];
00173 for (int i = 0; i < n; i++)
00174 res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
00175 return res;
00176 }
00177
00184 public Entry get(String key) throws Z3Exception
00185 {
00186 int n = size();
00187 Entry[] es = getEntries();
00188 for (int i = 0; i < n; i++)
00189 if (es[i].Key == key)
00190 return es[i];
00191 return null;
00192 }
00193
00194 Statistics(Context ctx, long obj) throws Z3Exception
00195 {
00196 super(ctx, obj);
00197 }
00198
00199 void incRef(long o) throws Z3Exception
00200 {
00201 getContext().statistics_DRQ().incAndClear(getContext(), o);
00202 super.incRef(o);
00203 }
00204
00205 void decRef(long o) throws Z3Exception
00206 {
00207 getContext().statistics_DRQ().add(o);
00208 super.decRef(o);
00209 }
00210 }