From 02f6d2b5e2aba3760ffacdb40b76ce9f5625066f Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 28 Sep 2021 22:28:36 -0500 Subject: [PATCH] Add Statistics and Stat to the Java API (#7243) This adds Statistics and Stat to the Java API --- src/api/java/cvc5/Stat.java | 166 ++++++++++++++++++++ src/api/java/cvc5/Statistics.java | 127 +++++++++++++++ src/api/java/jni/cvc5_Stat.cpp | 223 +++++++++++++++++++++++++++ src/api/java/jni/cvc5_Statistics.cpp | 180 +++++++++++++++++++++ 4 files changed, 696 insertions(+) create mode 100644 src/api/java/cvc5/Stat.java create mode 100644 src/api/java/cvc5/Statistics.java create mode 100644 src/api/java/jni/cvc5_Stat.cpp create mode 100644 src/api/java/jni/cvc5_Statistics.cpp 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`). + * 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 getHistogram() + { + return getHistogram(pointer); + } + + private native Map 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> +{ + // 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 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> + { + private long iteratorPointer = 0; + + public ConstIterator() + { + iteratorPointer = getIterator(pointer); + } + + @Override + public boolean hasNext() + { + return Statistics.this.hasNext(pointer, iteratorPointer); + } + + @Override + public Pair next() + { + try + { + Pair 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> 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(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(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(pointer); + return static_cast(current->isExpert()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isDefault()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isInt()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->getInt()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isDouble()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->getDouble()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + return static_cast(current->isString()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(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(pointer); + return static_cast(current->isHistogram()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + std::map histogram = current->getHistogram(); + // HashMap hashMap = new HashMap(); + jclass hashMapClass = env->FindClass("Ljava/util/HashMap;"); + jmethodID constructor = env->GetMethodID(hashMapClass, "", "()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, "", "(J)V"); + + for (const std::pair, uint64_t>& it : histogram) + { + // hashmap.put(key, value); + jstring key = env->NewStringUTF(it.first.c_str()); + jobject value = env->NewObject( + longClass, longConstructor, static_cast(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 + +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(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(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(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(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(pointer); + Statistics::iterator* it = + new Statistics::iterator(current->begin(true, true)); + return reinterpret_cast(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(pointer); + Statistics::iterator it = + *reinterpret_cast(iteratorPointer); + return static_cast(it != current->end()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(iteratorPointer); + std::string cName = it->first; + jstring jName = env->NewStringUTF(cName.c_str()); + Stat* stat = new Stat(it->second); + jlong statPointer = reinterpret_cast(stat); + + // Long longObject = new Long(statPointer) + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); + jobject longObject = env->NewObject(longClass, longConstructor, statPointer); + + // Pair pair = new Pair(jName, longObject) + jclass pairClass = env->FindClass("Lcvc5/Pair;"); + jmethodID pairConstructor = env->GetMethodID( + pairClass, "", "(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(pointer); + Statistics::iterator* itPointer = + reinterpret_cast(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(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(iteratorPointer); +} -- 2.30.2