src/api/java/jni/result.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_Result.h"
  19
  20 using namespace cvc5::api;
  21
  22 /*
  23  * Class:     io_github_cvc5_api_Result
  24  * Method:    deletePointer
  25  * Signature: (J)V
  26  */
  27 JNIEXPORT void JNICALL
  28 Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jobject, jlong pointer)
  29 {
  30   delete ((Result*)pointer);
  31 }
  32
  33 /*
  34  * Class:     io_github_cvc5_api_Result
  35  * Method:    isNull
  36  * Signature: (J)Z
  37  */
  38 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isNull(JNIEnv* env,
  39                                                                  jobject,
  40                                                                  jlong pointer)
  41 {
  42   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  43   Result* current = (Result*)pointer;
  44   return (jboolean)current->isNull();
  45   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  46 }
  47
  48 /*
  49  * Class:     io_github_cvc5_api_Result
  50  * Method:    isSat
  51  * Signature: (J)Z
  52  */
  53 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isSat(JNIEnv* env,
  54                                                                 jobject,
  55                                                                 jlong pointer)
  56 {
  57   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  58   Result* current = (Result*)pointer;
  59   return (jboolean)current->isSat();
  60   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  61 }
  62
  63 /*
  64  * Class:     io_github_cvc5_api_Result
  65  * Method:    isUnsat
  66  * Signature: (J)Z
  67  */
  68 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isUnsat(JNIEnv* env,
  69                                                                   jobject,
  70                                                                   jlong pointer)
  71 {
  72   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  73   Result* current = (Result*)pointer;
  74   return (jboolean)current->isUnsat();
  75   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  76 }
  77
  78 /*
  79  * Class:     io_github_cvc5_api_Result
  80  * Method:    isSatUnknown
  81  * Signature: (J)Z
  82  */
  83 JNIEXPORT jboolean JNICALL
  84 Java_io_github_cvc5_api_Result_isSatUnknown(JNIEnv* env, jobject, jlong pointer)
  85 {
  86   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  87   Result* current = (Result*)pointer;
  88   return (jboolean)current->isSatUnknown();
  89   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
  90 }
  91
  92 /*
  93  * Class:     io_github_cvc5_api_Result
  94  * Method:    isEntailed
  95  * Signature: (J)Z
  96  */
  97 JNIEXPORT jboolean JNICALL
  98 Java_io_github_cvc5_api_Result_isEntailed(JNIEnv* env, jobject, jlong pointer)
  99 {
 100   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 101   Result* current = (Result*)pointer;
 102   return (jboolean)current->isEntailed();
 103   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
 104 }
 105
 106 /*
 107  * Class:     io_github_cvc5_api_Result
 108  * Method:    isNotEntailed
 109  * Signature: (J)Z
 110  */
 111 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isNotEntailed(
 112     JNIEnv* env, jobject, jlong pointer)
 113 {
 114   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 115   Result* current = (Result*)pointer;
 116   return (jboolean)current->isNotEntailed();
 117   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
 118 }
 119
 120 /*
 121  * Class:     io_github_cvc5_api_Result
 122  * Method:    isEntailmentUnknown
 123  * Signature: (J)Z
 124  */
 125 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isEntailmentUnknown(
 126     JNIEnv* env, jobject, jlong pointer)
 127 {
 128   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 129   Result* current = (Result*)pointer;
 130   return (jboolean)current->isEntailmentUnknown();
 131   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
 132 }
 133
 134 /*
 135  * Class:     io_github_cvc5_api_Result
 136  * Method:    equals
 137  * Signature: (JJ)Z
 138  */
 139 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_equals(JNIEnv* env,
 140                                                                  jobject,
 141                                                                  jlong pointer1,
 142                                                                  jlong pointer2)
 143 {
 144   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 145   Result* result1 = (Result*)pointer1;
 146   Result* result2 = (Result*)pointer2;
 147   // We compare the actual terms, not their pointers.
 148   return (jboolean)(*result1 == *result2);
 149   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
 150 }
 151
 152 /*
 153  * Class:     io_github_cvc5_api_Result
 154  * Method:    getUnknownExplanation
 155  * Signature: (J)I
 156  */
 157 JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Result_getUnknownExplanation(
 158     JNIEnv* env, jobject, jlong pointer)
 159 {
 160   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 161   Result* current = (Result*)pointer;
 162   return (jint)current->getUnknownExplanation();
 163   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 164 }
 165
 166 /*
 167  * Class:     io_github_cvc5_api_Result
 168  * Method:    toString
 169  * Signature: (J)Ljava/lang/String;
 170  */
 171 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Result_toString(JNIEnv* env,
 172                                                                   jobject,
 173                                                                   jlong pointer)
 174 {
 175   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 176   Result* current = (Result*)pointer;
 177   return env->NewStringUTF(current->toString().c_str());
 178   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 179 }