--- /dev/null
+/******************************************************************************
+ * 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);
+};
--- /dev/null
+/******************************************************************************
+ * 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();
+ }
+};
--- /dev/null
+/******************************************************************************
+ * 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);
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+}
projects / cvc5.git / commitdiff