18 package com.microsoft.z3;
76 return Integer.toString(m_int);
78 return Double.toString(m_double);
80 throw new Z3Exception(
"Unknown statistical entry type");
93 return new String(
"Z3Exception: " + e.getMessage());
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;
102 Entry(String k,
int v)
109 Entry(String k,
double v)
127 return "Z3Exception: " + e.getMessage();
149 for (
int i = 0; i < n; i++)
155 getNativeObject(), i));
158 getNativeObject(), i));
172 String[] res =
new String[n];
173 for (
int i = 0; i < n; i++)
189 for (
int i = 0; i < n; i++)
190 if (es[i].
Key == key)
202 getContext().getStatisticsDRQ().incAndClear(getContext(), o);
208 getContext().getStatisticsDRQ().add(o);
static int statsSize(long a0, long a1)
static String statsGetKey(long a0, long a1, int a2)
static boolean statsIsUint(long a0, long a1, int a2)
static int statsGetUintValue(long a0, long a1, int a2)
static double statsGetDoubleValue(long a0, long a1, int a2)
static boolean statsIsDouble(long a0, long a1, int a2)
static String statsToString(long a0, long a1)