src/api/java/jni/op.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The cvc5 Java API.
  14  */
  15
  16 #include "api/cpp/cvc5.h"
  17 #include "api_utilities.h"
  18 #include "io_github_cvc5_api_Op.h"
  19
  20 using namespace cvc5::api;
  21
  22 /*
  23  * Class:     io_github_cvc5_api_Op
  24  * Method:    deletePointer
  25  * Signature: (J)V
  26  */
  27 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Op_deletePointer(JNIEnv*,
  28                                                                 jobject,
  29                                                                 jlong pointer)
  30 {
  31   delete reinterpret_cast<Op*>(pointer);
  32 }
  33
  34 /*
  35  * Class:     io_github_cvc5_api_Op
  36  * Method:    equals
  37  * Signature: (JJ)Z
  38  */
  39 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_equals(JNIEnv* env,
  40                                                              jobject,
  41                                                              jlong pointer1,
  42                                                              jlong pointer2)
  43 {
  44   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  45   Op* op1 = reinterpret_cast<Op*>(pointer1);
  46   Op* op2 = reinterpret_cast<Op*>(pointer2);
  47   // We compare the actual operators, not their pointers.
  48   return static_cast<jboolean>(*op1 == *op2);
  49   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  50 }
  51
  52 /*
  53  * Class:     io_github_cvc5_api_Op
  54  * Method:    getKind
  55  * Signature: (J)I
  56  */
  57 JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getKind(JNIEnv* env,
  58                                                           jobject,
  59                                                           jlong pointer)
  60 {
  61   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  62   Op* current = reinterpret_cast<Op*>(pointer);
  63   return static_cast<jboolean>(current->getKind());
  64   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  65 }
  66
  67 /*
  68  * Class:     io_github_cvc5_api_Op
  69  * Method:    isNull
  70  * Signature: (J)Z
  71  */
  72 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_isNull(JNIEnv* env,
  73                                                              jobject,
  74                                                              jlong pointer)
  75 {
  76   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  77   Op* current = reinterpret_cast<Op*>(pointer);
  78   return static_cast<jboolean>(current->isNull());
  79   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  80 }
  81
  82 /*
  83  * Class:     io_github_cvc5_api_Op
  84  * Method:    isIndexed
  85  * Signature: (J)Z
  86  */
  87 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_isIndexed(JNIEnv* env,
  88                                                                 jobject,
  89                                                                 jlong pointer)
  90 {
  91   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  92   Op* current = reinterpret_cast<Op*>(pointer);
  93   return static_cast<jboolean>(current->isIndexed());
  94   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, false);
  95 }
  96
  97 /*
  98  * Class:     io_github_cvc5_api_Op
  99  * Method:    getNumIndices
 100  * Signature: (J)I
 101  */
 102 JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getNumIndices(JNIEnv* env,
 103                                                                 jobject,
 104                                                                 jlong pointer)
 105 {
 106   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 107   Op* current = reinterpret_cast<Op*>(pointer);
 108   return static_cast<jint>(current->getNumIndices());
 109   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 110 }
 111
 112 /*
 113  * Class:     io_github_cvc5_api_Op
 114  * Method:    getIntegerIndices
 115  * Signature: (J)[I
 116  */
 117 JNIEXPORT jintArray JNICALL Java_io_github_cvc5_api_Op_getIntegerIndices(
 118     JNIEnv* env, jobject, jlong pointer)
 119 {
 120   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 121   Op* current = reinterpret_cast<Op*>(pointer);
 122   size_t size = current->getNumIndices();
 123   std::vector<jint> indices(size);
 124   if (size == 1)
 125   {
 126     uint32_t index = current->getIndices<uint32_t>();
 127     indices[0] = index;
 128   }
 129
 130   if (size == 2)
 131   {
 132     std::pair<uint32_t, uint32_t> pair =
 133         current->getIndices<std::pair<uint32_t, uint32_t>>();
 134     indices[0] = pair.first;
 135     indices[1] = pair.second;
 136   }
 137
 138   if (size > 2)
 139   {
 140     std::string message = "Unhandled case when number of indices > 2.";
 141     throw CVC5ApiException(message);
 142   }
 143
 144   jintArray ret = env->NewIntArray((jsize)size);
 145   env->SetIntArrayRegion(ret, 0, size, indices.data());
 146   return ret;
 147   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 148 }
 149
 150 /*
 151  * Class:     io_github_cvc5_api_Op
 152  * Method:    getStringIndices
 153  * Signature: (J)[Ljava/lang/String;
 154  */
 155 JNIEXPORT jobjectArray JNICALL
 156 Java_io_github_cvc5_api_Op_getStringIndices(JNIEnv* env, jobject, jlong pointer)
 157 {
 158   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 159   Op* current = reinterpret_cast<Op*>(pointer);
 160   size_t size = current->getNumIndices();
 161   std::vector<jstring> indices(size);
 162   if (size == 1)
 163   {
 164     std::string cIndex = current->getIndices<std::string>();
 165     jstring jIndex = env->NewStringUTF(cIndex.c_str());
 166     indices[0] = jIndex;
 167   }
 168
 169   if (size > 1)  // currently only one string is implemented in cvc5.cpp
 170   {
 171     std::string message = "Unhandled case when number of indices > 1.";
 172     throw CVC5ApiException(message);
 173   }
 174
 175   // construct a java array of String
 176   jclass stringClass = env->FindClass("Ljava/lang/String;");
 177   jobjectArray ret = env->NewObjectArray((jsize)size, stringClass, nullptr);
 178   for (size_t i = 0; i < size; i++)
 179   {
 180     env->SetObjectArrayElement(ret, i, indices[i]);
 181   }
 182   return ret;
 183   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 184 }
 185
 186 /*
 187  * Class:     io_github_cvc5_api_Op
 188  * Method:    toString
 189  * Signature: (J)Ljava/lang/String;
 190  */
 191 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Op_toString(JNIEnv* env,
 192                                                               jobject,
 193                                                               jlong pointer)
 194 {
 195   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 196   Op* current = reinterpret_cast<Op*>(pointer);
 197   return env->NewStringUTF(current->toString().c_str());
 198   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 199 }