1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/******************************************************************************
* 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.
*/
#ifndef CVC5__JAVA_API_H
#define CVC5__JAVA_API_H
#include <jni.h>
#include <string>
#include <vector>
#define CVC5_JAVA_API_TRY_CATCH_BEGIN \
try \
{
#define CVC5_JAVA_API_TRY_CATCH_END(env) \
} \
catch (const CVC5ApiOptionException& e) \
{ \
jclass exceptionClass = env->FindClass("cvc5/CVC5ApiOptionException"); \
env->ThrowNew(exceptionClass, e.what()); \
} \
catch (const CVC5ApiRecoverableException& e) \
{ \
jclass exceptionClass = \
env->FindClass("cvc5/CVC5ApiRecoverableException"); \
env->ThrowNew(exceptionClass, e.what()); \
} \
catch (const CVC5ApiException& e) \
{ \
jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \
env->ThrowNew(exceptionClass, e.what()); \
}
#define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \
CVC5_JAVA_API_TRY_CATCH_END(env) \
return returnValue;
/**
* Convert pointers coming from Java to cvc5 objects
* @tparam T cvc5 class (Term, Sort, Grammar, etc)
* @param env jni environment
* @param jPointers pointers coming from java
* @return a vector of cvc5 objects
*/
template <class T>
std::vector<T> getObjectsFromPointers(JNIEnv* env, jlongArray jPointers)
{
// get the size of pointers
jsize size = env->GetArrayLength(jPointers);
// allocate a buffer for c pointers
std::vector<jlong> cPointers(size);
// copy java array to the buffer
env->GetLongArrayRegion(jPointers, 0, size, cPointers.data());
// copy the terms into a vector
std::vector<T> objects;
for (jlong pointer : cPointers)
{
T* term = reinterpret_cast<T*>(pointer);
objects.push_back(*term);
}
return objects;
}
/**
* Convert cvc5 objects into pointers
* @tparam T cvc5 class (Term, Sort, Grammar, etc)
* @param env jni environment
* @param objects cvc5 objects
* @return jni array of pointers
*/
template <class T>
jlongArray getPointersFromObjects(JNIEnv* env, const std::vector<T>& objects)
{
std::vector<jlong> pointers(objects.size());
for (size_t i = 0; i < objects.size(); i++)
{
pointers[i] = reinterpret_cast<jlong>(new T(objects[i]));
}
jlongArray ret = env->NewLongArray(objects.size());
env->SetLongArrayRegion(ret, 0, objects.size(), pointers.data());
return ret;
}
/**
* Convert a cpp signed (unsigned) integer to an object of BigInteger class
* @tparam T cpp types (int64_t, uint64_t, int32_t, int32_t, etc)
* @param env jni environment
* @param value cpp integer value
* @return an object of java BigInteger
*/
template <class T>
jobject getBigIntegerObject(JNIEnv* env, T value)
{
std::string s = std::to_string(value);
jstring javaString = env->NewStringUTF(s.c_str());
jclass bigIntegerClass = env->FindClass("java/math/BigInteger");
jmethodID bigIntegerConstructor =
env->GetMethodID(bigIntegerClass, "<init>", "(Ljava/lang/String;)V");
jobject ret =
env->NewObject(bigIntegerClass, bigIntegerConstructor, javaString);
return ret;
}
/**
* Generate an array of java strings from a vector of cpp strings
* @param env jni environment
* @param cStrings a vector of strings
* @return an array of java strings
*/
jobjectArray getStringArrayFromStringVector(
JNIEnv* env, const std::vector<std::string>& cStrings);
/**
* Generate a Double object from cpp double value
* @param env jni environment
* @param value
* @return a Double object
*/
jobject getDoubleObject(JNIEnv* env, double value);
/**
* Generate a Boolean object from cpp bool value
* @param env jni environment
* @param value
* @return a Boolean object
*/
jobject getBooleanObject(JNIEnv* env, bool value);
#endif // CVC5__JAVA_API_H
|
