Add Statistics and Stat to the Java API (#7243)

This adds Statistics and Stat to the Java API

4 files changed, 696 insertions, 0 deletions

diff --git a/src/api/java/cvc5/Stat.java b/src/api/java/cvc5/Stat.java
new file mode 100644
index 000000000..964f4025c
--- /dev/null
+++ b/src/api/java/cvc5/Stat.java
@@ -0,0 +1,166 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+import java.util.Map;
+
+/**
+ * Represents a snapshot of a single statistic value.
+ * A value can be of type `long`, `double`, `String` or a histogram
+ * (`Map<String, Long>`).
+ * The value type can be queried (using `isInt()`, `isDouble()`, etc.) and
+ * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
+ * It is possible to query whether this statistic is an expert statistic by
+ * `isExpert()` and whether its value is the default value by `isDefault()`.
+ */
+public class Stat extends AbstractPointer
+{
+   // region construction and destruction
+   Stat(Solver solver, long pointer)
+   {
+     super(solver, pointer);
+   }
+
+   protected static native void deletePointer(long pointer);
+
+   public long getPointer()
+   {
+     return pointer;
+   }
+
+   @Override
+   public void finalize()
+   {
+     deletePointer(pointer);
+   }
+
+   // endregion
+
+  /**
+   * @return a string representation of this Stat
+   */
+  protected native String toString(long pointer);
+
+  /**
+   * Is this value intended for experts only?
+   * @return Whether this is an expert statistic.
+   */
+  public boolean isExpert()
+  {
+    return isExpert(pointer);
+  }
+
+  private native boolean isExpert(long pointer);
+
+  /**
+   * Does this value hold the default value?
+   * @return Whether this is a defaulted statistic.
+   */
+  public boolean isDefault()
+  {
+    return isDefault(pointer);
+  }
+
+  private native boolean isDefault(long pointer);
+
+  /**
+   * Is this value an integer?
+   * @return Whether the value is an integer.
+   */
+  public boolean isInt()
+  {
+    return isInt(pointer);
+  }
+
+  private native boolean isInt(long pointer);
+
+  /**
+   * Return the integer value.
+   * @return The integer value.
+   */
+  public long getInt()
+  {
+    return getInt(pointer);
+  }
+
+  private native long getInt(long pointer);
+
+  /**
+   * Is this value a double?
+   * @return Whether the value is a double.
+   */
+  public boolean isDouble()
+  {
+    return isDouble(pointer);
+  }
+
+  private native boolean isDouble(long pointer);
+
+  /**
+   * Return the double value.
+   * @return The double value.
+   */
+  public double getDouble()
+  {
+    return getDouble(pointer);
+  }
+
+  private native double getDouble(long pointer);
+
+  /**
+   * Is this value a string?
+   * @return Whether the value is a string.
+   */
+  public boolean isString()
+  {
+    return isString(pointer);
+  }
+
+  private native boolean isString(long pointer);
+
+  /**
+   * Return the string value.
+   * @return The string value.
+   */
+  public String getString()
+  {
+    return getString(pointer);
+  }
+
+  private native String getString(long pointer);
+
+  /**
+   * Is this value a histogram?
+   * @return Whether the value is a histogram.
+   */
+  public boolean isHistogram()
+  {
+    return isHistogram(pointer);
+  }
+
+  private native boolean isHistogram(long pointer);
+
+  /**
+   * Return the histogram value.
+   * @return The histogram value.
+   */
+  public Map<String, Long> getHistogram()
+  {
+      return getHistogram(pointer);
+  }
+
+  private native Map<String, Long> getHistogram(long pointer);
+};
diff --git a/src/api/java/cvc5/Statistics.java b/src/api/java/cvc5/Statistics.java
new file mode 100644
index 000000000..ba4828284
--- /dev/null
+++ b/src/api/java/cvc5/Statistics.java
@@ -0,0 +1,127 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+import java.util.Iterator;
+import java.util.NoSuchElementException;
+
+public class Statistics extends AbstractPointer implements Iterable<Pair<String, Stat>>
+{
+   // region construction and destruction
+   Statistics(Solver solver, long pointer)
+   {
+     super(solver, pointer);
+   }
+
+   protected static native void deletePointer(long pointer);
+
+   public long getPointer()
+   {
+     return pointer;
+   }
+
+   @Override
+   public void finalize()
+   {
+     deletePointer(pointer);
+   }
+
+   // endregion
+
+  /**
+   * @return a string representation of this Statistics
+   */
+  protected native String toString(long pointer);
+
+
+  /**
+   * Retrieve the statistic with the given name.
+   * Asserts that a statistic with the given name actually exists and throws
+   * a `CVC5ApiRecoverableException` if it does not.
+   * @param name Name of the statistic.
+   * @return The statistic with the given name.
+   */
+  public Stat get(String name)
+  {
+    long statPointer = get(pointer, name);
+    return new Stat(solver, statPointer);
+  }
+
+  private native long get(long pointer, String name);
+
+  /**
+   * Begin iteration over the statistics values.
+   * By default, only entries that are public (non-expert) and have been set
+   * are visible while the others are skipped.
+   * @param expert If set to true, expert statistics are shown as well.
+   * @param defaulted If set to true, defaulted statistics are shown as well.
+   */
+
+
+   private native long getIterator(long pointer);
+
+   private native boolean hasNext(long pointer, long iteratorPointer);
+
+   private native Pair<String, Long> getNext(long pointer, long iteratorPointer) throws CVC5ApiException;
+
+   private native long increment(long pointer, long iteratorPointer) throws CVC5ApiException;
+
+   private native void deleteIteratorPointer(long iteratorPointer);
+
+   public class ConstIterator implements Iterator<Pair<String, Stat>>
+   {
+     private long iteratorPointer = 0;
+
+     public ConstIterator()
+     {
+       iteratorPointer = getIterator(pointer);
+     }
+
+     @Override
+     public boolean hasNext()
+     {
+       return Statistics.this.hasNext(pointer, iteratorPointer);
+     }
+
+     @Override
+     public Pair<String, Stat> next()
+     {
+       try
+       {
+         Pair<String, Long> pair = Statistics.this.getNext(pointer, iteratorPointer);
+         Stat stat = new Stat(solver, pair.second);
+         this.iteratorPointer = Statistics.this.increment(pointer, iteratorPointer);
+         return new Pair<>(pair.first, stat);
+       }
+       catch(CVC5ApiException e)
+       {
+         throw new NoSuchElementException(e.getMessage());
+       }
+     }
+
+     @Override
+     public void finalize()
+     {
+       deleteIteratorPointer(iteratorPointer);
+     }
+   }
+
+   @Override
+   public Iterator<Pair<String, Stat>> iterator()
+   {
+     return new ConstIterator();
+   }
+};
diff --git a/src/api/java/jni/cvc5_Stat.cpp b/src/api/java/jni/cvc5_Stat.cpp
new file mode 100644
index 000000000..9345729cb
--- /dev/null
+++ b/src/api/java/jni/cvc5_Stat.cpp
@@ -0,0 +1,223 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Stat.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Stat_deletePointer(JNIEnv*,
+                                                    jclass,
+                                                    jlong pointer)
+{
+  delete reinterpret_cast<Stat*>(pointer);
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Stat_toString(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  std::stringstream ss;
+  ss << *current;
+  return env->NewStringUTF(ss.str().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isExpert
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isExpert(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isExpert());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isDefault
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDefault(JNIEnv* env,
+                                                    jobject,
+                                                    jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isDefault());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isInt
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isInt(JNIEnv* env,
+                                                jobject,
+                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isInt());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    getInt
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Stat_getInt(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jlong>(current->getInt());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jlong>(0));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isDouble
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDouble(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isDouble());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    getDouble
+ * Signature: (J)D
+ */
+JNIEXPORT jdouble JNICALL Java_cvc5_Stat_getDouble(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jdouble>(current->getDouble());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jdouble>(0));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isString
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isString(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isString());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    getString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Stat_getString(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return env->NewStringUTF(current->getString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    isHistogram
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isHistogram(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  return static_cast<jboolean>(current->isHistogram());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Stat
+ * Method:    getHistogram
+ * Signature: (J)Ljava/util/Map;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_Stat_getHistogram(JNIEnv* env,
+                                                      jobject,
+                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Stat* current = reinterpret_cast<Stat*>(pointer);
+  std::map<std::string, uint64_t> histogram = current->getHistogram();
+  // HashMap hashMap = new HashMap();
+  jclass hashMapClass = env->FindClass("Ljava/util/HashMap;");
+  jmethodID constructor = env->GetMethodID(hashMapClass, "<init>", "()V");
+  jobject hashMap = env->NewObject(hashMapClass, constructor);
+  jmethodID putMethod = env->GetMethodID(
+      hashMapClass,
+      "put",
+      "(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;");
+
+  // Long longObject = new Long(statPointer)
+  jclass longClass = env->FindClass("Ljava/lang/Long;");
+  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+
+  for (const std::pair<const std::basic_string<char>, uint64_t>& it : histogram)
+  {
+    // hashmap.put(key, value);
+    jstring key = env->NewStringUTF(it.first.c_str());
+    jobject value = env->NewObject(
+        longClass, longConstructor, static_cast<jlong>(it.second));
+    env->CallObjectMethod(hashMap, putMethod, key, value);
+  }
+  return hashMap;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
diff --git a/src/api/java/jni/cvc5_Statistics.cpp b/src/api/java/jni/cvc5_Statistics.cpp
new file mode 100644
index 000000000..8db2e156a
--- /dev/null
+++ b/src/api/java/jni/cvc5_Statistics.cpp
@@ -0,0 +1,180 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Statistics.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+#include <sstream>
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Statistics_deletePointer(JNIEnv*,
+                                                          jclass,
+                                                          jlong pointer)
+{
+  delete reinterpret_cast<Statistics*>(pointer);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Statistics_toString(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+
+  Statistics* current = reinterpret_cast<Statistics*>(pointer);
+  std::stringstream ss;
+  ss << *current;
+  return env->NewStringUTF(ss.str().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    get
+ * Signature: (JLjava/lang/String;)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Statistics_get(JNIEnv* env,
+                                                 jobject,
+                                                 jlong pointer,
+                                                 jstring jName)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Statistics* current = reinterpret_cast<Statistics*>(pointer);
+  const char* s = env->GetStringUTFChars(jName, nullptr);
+  std::string cName(s);
+  Stat* retPointer = new Stat(current->get(cName));
+  env->ReleaseStringUTFChars(jName, s);
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    getIterator
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Statistics_getIterator(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Statistics* current = reinterpret_cast<Statistics*>(pointer);
+  Statistics::iterator* it =
+      new Statistics::iterator(current->begin(true, true));
+  return reinterpret_cast<jlong>(it);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    hasNext
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Statistics_hasNext(JNIEnv* env,
+                                                        jobject,
+                                                        jlong pointer,
+                                                        jlong iteratorPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Statistics* current = reinterpret_cast<Statistics*>(pointer);
+  Statistics::iterator it =
+      *reinterpret_cast<Statistics::iterator*>(iteratorPointer);
+  return static_cast<jboolean>(it != current->end());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    getNext
+ * Signature: (JJ)Lcvc5/Pair;
+ */
+JNIEXPORT jobject JNICALL Java_cvc5_Statistics_getNext(JNIEnv* env,
+                                                       jobject,
+                                                       jlong,
+                                                       jlong iteratorPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Statistics::iterator it =
+      *reinterpret_cast<Statistics::iterator*>(iteratorPointer);
+  std::string cName = it->first;
+  jstring jName = env->NewStringUTF(cName.c_str());
+  Stat* stat = new Stat(it->second);
+  jlong statPointer = reinterpret_cast<jlong>(stat);
+
+  // Long longObject = new Long(statPointer)
+  jclass longClass = env->FindClass("Ljava/lang/Long;");
+  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+  jobject longObject = env->NewObject(longClass, longConstructor, statPointer);
+
+  // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
+  jclass pairClass = env->FindClass("Lcvc5/Pair;");
+  jmethodID pairConstructor = env->GetMethodID(
+      pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
+  jobject pair = env->NewObject(pairClass, pairConstructor, jName, longObject);
+
+  it++;
+  return pair;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    increment
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Statistics_increment(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer,
+                                                       jlong iteratorPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Statistics* current = reinterpret_cast<Statistics*>(pointer);
+  Statistics::iterator* itPointer =
+      reinterpret_cast<Statistics::iterator*>(iteratorPointer);
+  Statistics::iterator it = *itPointer;
+  if (it == current->end())
+  {
+    delete itPointer;
+    std::string message = "Reached the end of Statistics::iterator";
+    throw CVC5ApiException(message);
+  }
+
+  Statistics::iterator* nextIt = new Statistics::iterator(it.operator++());
+  delete itPointer;
+  return reinterpret_cast<jlong>(nextIt);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Statistics
+ * Method:    deleteIteratorPointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Statistics_deleteIteratorPointer(
+    JNIEnv*, jobject, jlong iteratorPointer)
+{
+  delete reinterpret_cast<Statistics::iterator*>(iteratorPointer);
+}