summaryrefslogtreecommitdiff
path: root/src/api/java/jni/cvc5JavaApi.h
blob: 7b550ef28c040a1fe972858c394d393c9291a1b0 (plain)
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
/******************************************************************************
 * 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 <jni.h>

#ifndef CVC5__JAVA_API_H
#define CVC5__JAVA_API_H

#define CVC5_JAVA_API_TRY_CATCH_BEGIN \
  try                                 \
  {
#define CVC5_JAVA_API_TRY_CATCH_END(env)                             \
  }                                                                  \
  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;
#endif  // CVC5__JAVA_API_H

/**
 * 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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback