Z3
src/api/java/Statistics.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines