diff options
Diffstat (limited to 'src/bindings/compat/java/include/cvc3/JniUtils.h')
-rw-r--r-- | src/bindings/compat/java/include/cvc3/JniUtils.h | 292 |
1 files changed, 0 insertions, 292 deletions
diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h deleted file mode 100644 index 404774c62..000000000 --- a/src/bindings/compat/java/include/cvc3/JniUtils.h +++ /dev/null @@ -1,292 +0,0 @@ -#ifndef _java__cvc3__jni_utils_h_ -#define _java__cvc3__jni_utils_h_ - -#include <cassert> -#include <string> -#include <jni.h> -#include <typeinfo> -#include "compat/cvc3_compat.h" -//#include "vcl.h" -//#include "hash_map.h" -//#include "exception.h" - -#define DebugAssert(cond, str) assert(cond) - -namespace Java_cvc3_JniUtils { - - /// Embedding of c++ objects in java objects - - // generic delete function for any type T - template <class T> class DeleteEmbedded { - public: - static void deleteEmbedded(void* cobj) { - delete (T*) cobj; - } - }; - - typedef void (*TDeleteEmbedded)(void*); - - - // Encapsulates a c++ object so that: - // - (un)embedding casting is type safe - // - deallocation is automatic (if needed) - // This has probably quit a bit of overhead, because now for each - // wrapper object (even if only a temporary reference) an instance - // of Embedded is created. - // But considering the above two benefits it should be worth it - // because it should simplify maintenance quite a bit, - // as changes in the cvc API should lead to assertion failures - // instead of strange bugs. - class Embedded { - private: - // the actual embedded c++ object, - // as void* to make Embedded independent of its type - void* d_cobj; - - // the type info of d_cobj, - // to make sure that later unembeddings are type safe - // actually only needed in debugging, so might be guarded with IF_DEBUG - const std::type_info& d_typeInfo; - - // the type correct delete function for d_cobj, - // or NULL if this embedding is merely a reference - // and not responsible for its deallocation - TDeleteEmbedded d_delete; - - public: - Embedded(void* cobj, const std::type_info& ti, TDeleteEmbedded del) : - d_cobj(cobj), d_typeInfo(ti), d_delete(del) { - assert(d_cobj != NULL); - } - - ~Embedded() { - assert(d_cobj != NULL); - if (d_delete != NULL) d_delete(d_cobj); - } - - const void* getCObj() const { - return d_cobj; - } - - const std::type_info& getType() const { - return d_typeInfo; - } - }; - - - - // embed functions - - // embeds a c++ object of type T into a jobject - // by first wrapping it into an Embedded object. - template <class T> jobject embed(JNIEnv* env, T* cobj, const std::type_info& ti, - TDeleteEmbedded del) { - DebugAssert(cobj != NULL, "JniUtils::embed: null object given"); - Embedded* embedded = new Embedded((void*)cobj, ti, del); - return (jobject)env->NewDirectByteBuffer(embedded, sizeof(Embedded)); - } - - // embeds a constant reference to a c++ object into a jobject - template <class T> jobject embed_const_ref(JNIEnv* env, const T* cobj) { - DebugAssert(cobj != NULL, "JniUtils::embed_const: null object given"); - return embed<T>(env, (T*) cobj, typeid(cobj), NULL); - } - - // embeds a mutable reference to a c++ object into a jobject - template <class T> jobject embed_mut_ref(JNIEnv* env, T* cobj) { - DebugAssert(cobj != NULL, "JniUtils::embed_mut_ref: null object given"); - return embed<T>(env, (T*) cobj, typeid(cobj), NULL); - } - - // embeds a fresh copy of a (probably temporary) c++ object into a jobject - template <class T> jobject embed_copy(JNIEnv* env, const T& cobj) { - DebugAssert(&cobj != NULL, "JniUtils::embed_copy: null object given"); - T* copy = new T(cobj); - assert(copy != NULL); - return embed<T>(env, copy, typeid(copy), &DeleteEmbedded<T>::deleteEmbedded); - } - - // embeds a c++ object into a jobject, - // and takes over the responsibility to deallocate it - template <class T> jobject embed_own(JNIEnv* env, T* cobj) { - DebugAssert(cobj != NULL, "JniUtils::embed_own: null object given"); - return embed<T>(env, cobj, typeid(cobj), &DeleteEmbedded<T>::deleteEmbedded); - } - - - // unembed functions - - // extract Embedded* from a jobject - Embedded* unembed(JNIEnv* env, jobject jobj); - - // extract a constant c++ object of type T from a jobject - template <class T> const T* unembed_const(JNIEnv* env, jobject jobj) { - Embedded* embedded = unembed(env, jobj); - return (const T*) embedded->getCObj(); - } - - // extract a mutable c++ object of type T from a jobject - template <class T> T* unembed_mut(JNIEnv* env, jobject jobj) { - Embedded* embedded = unembed(env, jobj); - // check that the wrapped object is not const - DebugAssert(embedded->getType() == typeid(T*), - "JniUtils::unembed_mut: type mismatch"); - return (T*) embedded->getCObj(); - } - - - // delete embedded - - // delete the Embedded object contained in a jobject, - // and also destruct the wrapped c++ object if necessary. - void deleteEmbedded(JNIEnv* env, jobject jobj); - - - - - /// Conversions between c++ and java - - // bool - bool toCpp(jboolean j); - - // string - jstring toJava(JNIEnv* env, const std::string& cstring); - jstring toJava(JNIEnv* env, const char* cstring); - std::string toCpp(JNIEnv* env, const jstring& string); - - // enums - jstring toJava(JNIEnv* env, CVC3::QueryResult result); - jstring toJava(JNIEnv* env, CVC3::FormulaValue result); - jstring toJava(JNIEnv* env, CVC3::InputLanguage result); - CVC3::InputLanguage toCppInputLanguage(JNIEnv* env, const std::string& lang); - - // exceptions - void toJava(JNIEnv* env, const CVC3::Exception& e); - - // vectors - template <class T> jobjectArray toJavaVCopy(JNIEnv* env, const std::vector<T>& v) { - jobjectArray jarray = (jobjectArray) - env->NewObjectArray( - v.size(), - env->FindClass("java/lang/Object"), - NULL); - - for (size_t i = 0; i < v.size(); ++i) { - env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i])); - } - - return jarray; - } - - template <class T> jobjectArray toJavaVConstRef(JNIEnv* env, const std::vector<T>& v) { - jobjectArray jarray = (jobjectArray) - env->NewObjectArray( - v.size(), - env->FindClass("java/lang/Object"), - NULL); - - for (size_t i = 0; i < v.size(); ++i) { - env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i])); - } - - return jarray; - } - - template<class T> - jobjectArray - toJavaVVConstRef(JNIEnv* env, const std::vector<std::vector<T> >& v) - { - jobjectArray jarray = (jobjectArray) env->NewObjectArray(v.size(), - env->FindClass("[Ljava/lang/Object;"), NULL); - for (size_t i = 0; i < v.size(); ++i) - { - env->SetObjectArrayElement(jarray, i, toJavaVConstRef(env, v[i])); - } - return jarray; - } - - template <class T> std::vector<T> toCppV(JNIEnv* env, const jobjectArray& jarray) { - std::vector<T> v; - int length = env->GetArrayLength(jarray); - for (int i = 0; i < length; ++i) { - v.push_back(*unembed_const<T>(env, env->GetObjectArrayElement(jarray, i))); - } - return v; - } - - template <class T> std::vector<std::vector<T> > toCppVV(JNIEnv* env, const jobjectArray& jarray) { - std::vector<std::vector<T> > v; - int length = env->GetArrayLength(jarray); - for (int i = 0; i < length; ++i) { - jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i)); - v.push_back(toCppV<T>(env, jsub)); - } - return v; - } - - template <class T> std::vector<std::vector<std::vector<T> > > - toCppVVV(JNIEnv* env, const jobjectArray& jarray) { - std::vector<std::vector<std::vector<T> > > v; - int length = env->GetArrayLength(jarray); - for (int i = 0; i < length; ++i) { - jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i)); - v.push_back(toCppVV<T>(env, jsub)); - } - return v; - } - - // string vectors - std::vector<std::string> toCppV(JNIEnv* env, const jobjectArray& jarray); - std::vector<std::vector<std::string> > toCppVV(JNIEnv* env, const jobjectArray& jarray); - std::vector<std::vector<std::vector<std::string> > > toCppVVV(JNIEnv* env, const jobjectArray& jarray); - jobjectArray toJavaV(JNIEnv* env, const std::vector<std::string>& v); - - // primitive vectors - std::vector<bool> toCppV(JNIEnv* env, const jbooleanArray& jarray); - - - // hash map - /*template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) { - jobjectArray jarray = (jobjectArray) - env->NewObjectArray( - hm.size() * 2, - env->FindClass("java/lang/Object"), - NULL); - - int i = 0; - typename Hash::hash_map<K, V>::const_iterator it; - for (it = hm.begin(); it != hm.end(); ++it) { - assert(i < env->GetArrayLength(jarray)); - env->SetObjectArrayElement(jarray, i, embed_copy<K>(env, it->first)); - ++i; - assert(i < env->GetArrayLength(jarray)); - env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second)); - ++i; - } - return jarray; - }*/ - - template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) { - jobjectArray jarray = (jobjectArray) - env->NewObjectArray( - hm.size() * 2, - env->FindClass("java/lang/Object"), - NULL); - - int i = 0; - typename CVC3::ExprMap<V>::const_iterator it; - for (it = hm.begin(); it != hm.end(); ++it) { - assert(i < env->GetArrayLength(jarray)); - env->SetObjectArrayElement(jarray, i, embed_copy<CVC3::Expr>(env, it->first)); - ++i; - assert(i < env->GetArrayLength(jarray)); - env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second)); - ++i; - } - return jarray; - } - -} - - -#endif |