Add Result.java to the java API (#6385)

This PR adds Result.java ResultTest.java and cvc5_Result.cpp to the java api.

diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java
new file mode 100644 (file)
index 0000000..bd142b9
--- /dev/null
+++ b/src/api/java/cvc5/Result.java
@@ -0,0 +1,210 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, 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.
+ */
+
+package cvc5;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class Result extends AbstractPointer
+{
+  // region construction and destruction
+  Result(Solver solver, long pointer)
+  {
+    super(solver, pointer);
+  }
+
+  protected static native void deletePointer(long pointer);
+
+  public long getPointer()
+  {
+    return pointer;
+  }
+
+  @Override
+  public void finalize()
+  {
+    deletePointer(pointer);
+  }
+
+  // endregion
+
+  public enum UnknownExplanation
+  {
+    REQUIRES_FULL_CHECK(0),
+    INCOMPLETE(1),
+    TIMEOUT(2),
+    RESOURCEOUT(3),
+    MEMOUT(4),
+    INTERRUPTED(5),
+    NO_STATUS(6),
+    UNSUPPORTED(7),
+    OTHER(8),
+    UNKNOWN_REASON(9);
+
+    /* the int value of the UnknownExplanation */
+    private int value;
+    private static Map<Integer, UnknownExplanation> explanationMap = new HashMap<>();
+    private UnknownExplanation(int value)
+    {
+      this.value = value;
+    }
+
+    static
+    {
+      for (UnknownExplanation explanation : UnknownExplanation.values())
+      {
+        explanationMap.put(explanation.getValue(), explanation);
+      }
+    }
+
+    public static UnknownExplanation fromInt(int value) throws CVC5ApiException
+    {
+      if (value < REQUIRES_FULL_CHECK.value || value > UNKNOWN_REASON.value)
+      {
+        throw new CVC5ApiException("UnknownExplanation value " + value
+            + " is outside the valid range [" + REQUIRES_FULL_CHECK.value + ","
+            + UNKNOWN_REASON.value + "]");
+      }
+      return explanationMap.get(value);
+    }
+
+    public int getValue()
+    {
+      return value;
+    }
+  }
+
+  /**
+   * Return true if Result is empty, i.e., a nullary Result, and not an actual
+   * result returned from a checkSat() (and friends) query.
+   */
+  public boolean isNull()
+  {
+    return isNull(pointer);
+  }
+
+  private native boolean isNull(long pointer);
+
+  /**
+   * Return true if query was a satisfiable checkSat() or checkSatAssuming()
+   * query.
+   */
+  public boolean isSat()
+  {
+    return isSat(pointer);
+  }
+
+  private native boolean isSat(long pointer);
+
+  /**
+   * Return true if query was an unsatisfiable checkSat() or
+   * checkSatAssuming() query.
+   */
+  public boolean isUnsat()
+  {
+    return isUnsat(pointer);
+  }
+
+  private native boolean isUnsat(long pointer);
+
+  /**
+   * Return true if query was a checkSat() or checkSatAssuming() query and
+   * CVC4 was not able to determine (un)satisfiability.
+   */
+  public boolean isSatUnknown()
+  {
+    return isSatUnknown(pointer);
+  }
+
+  private native boolean isSatUnknown(long pointer);
+
+  /**
+   * Return true if corresponding query was an entailed checkEntailed() query.
+   */
+  public boolean isEntailed()
+  {
+    return isEntailed(pointer);
+  }
+
+  private native boolean isEntailed(long pointer);
+
+  /**
+   * Return true if corresponding query was a checkEntailed() query that is
+   * not entailed.
+   */
+  public boolean isNotEntailed()
+  {
+    return isNotEntailed(pointer);
+  }
+
+  private native boolean isNotEntailed(long pointer);
+
+  /**
+   * Return true if query was a checkEntailed() () query and CVC4 was not able
+   * to determine if it is entailed.
+   */
+  public boolean isEntailmentUnknown()
+  {
+    return isEntailmentUnknown(pointer);
+  }
+
+  private native boolean isEntailmentUnknown(long pointer);
+
+  /**
+   * Operator overloading for equality of two results.
+   * @param r the result to compare to for equality
+   * @return true if the results are equal
+   */
+  @Override public boolean equals(Object r)
+  {
+    if (this == r)
+      return true;
+    if (r == null || getClass() != r.getClass())
+      return false;
+    Result result = (Result) r;
+    if (this.pointer == result.pointer)
+    {
+      return true;
+    }
+    return equals(pointer, result.getPointer());
+  }
+
+  private native boolean equals(long pointer1, long pointer2);
+
+  /**
+   * @return an explanation for an unknown query result.
+   */
+  public UnknownExplanation getUnknownExplanation()
+  {
+    try
+    {
+      int explanation = getUnknownExplanation(pointer);
+      return UnknownExplanation.fromInt(explanation);
+    }
+    catch (CVC5ApiException e)
+    {
+      e.printStackTrace();
+      throw new RuntimeException(e.getMessage());
+    }
+  }
+
+  private native int getUnknownExplanation(long pointer);
+
+  /**
+   * @return a string representation of this result.
+   */
+  protected native String toString(long pointer);
+}

diff --git a/src/api/java/jni/cvc5_Result.cpp b/src/api/java/jni/cvc5_Result.cpp
new file mode 100644 (file)
index 0000000..4bc5cec
--- /dev/null
+++ b/src/api/java/jni/cvc5_Result.cpp
@@ -0,0 +1,186 @@
+/******************************************************************************
+ * 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 "cvc5_Result.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Result
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Result_deletePointer(JNIEnv*,
+                                                      jclass,
+                                                      jlong pointer)
+{
+  delete ((Result*)pointer);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isNull
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNull(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isNull();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isSat
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSat(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isSat();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isUnsat
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isUnsat(JNIEnv* env,
+                                                    jobject,
+                                                    jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isUnsat();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isSatUnknown
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSatUnknown(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isSatUnknown();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isEntailed
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailed(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isEntailed();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isNotEntailed
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNotEntailed(JNIEnv* env,
+                                                          jobject,
+                                                          jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isNotEntailed();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    isEntailmentUnknown
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailmentUnknown(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jboolean)current->isEntailmentUnknown();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    equals
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_cvc5_Result_equals(JNIEnv* env,
+                                                   jobject,
+                                                   jlong pointer1,
+                                                   jlong pointer2)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* result1 = (Result*)pointer1;
+  Result* result2 = (Result*)pointer2;
+  // We compare the actual terms, not their pointers.
+  return (jboolean)(*result1 == *result2);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    getUnknownExplanation
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_cvc5_Result_getUnknownExplanation(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return (jint)current->getUnknownExplanation();
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Result
+ * Method:    toString
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_cvc5_Result_toString(JNIEnv* env,
+                                                    jobject,
+                                                    jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Result* current = (Result*)pointer;
+  return env->NewStringUTF(current->toString().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}

diff --git a/test/unit/api/java/cvc5/ResultTest.java b/test/unit/api/java/cvc5/ResultTest.java
new file mode 100644 (file)
index 0000000..8ba50c0
--- /dev/null
+++ b/test/unit/api/java/cvc5/ResultTest.java
@@ -0,0 +1,126 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Result class
+ */
+
+package cvc5;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class ResultTest
+{
+  private Solver d_solver;
+
+  @BeforeEach void setUp()
+  {
+    d_solver = new Solver();
+  }
+
+  @Test void isNull()
+  {
+    Result res_null = d_solver.getNullResult();
+    assertTrue(res_null.isNull());
+    assertFalse(res_null.isSat());
+    assertFalse(res_null.isUnsat());
+    assertFalse(res_null.isSatUnknown());
+    assertFalse(res_null.isEntailed());
+    assertFalse(res_null.isNotEntailed());
+    assertFalse(res_null.isEntailmentUnknown());
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res = d_solver.checkSat();
+    assertFalse(res.isNull());
+  }
+
+  @Test void eq()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res;
+    Result res2 = d_solver.checkSat();
+    Result res3 = d_solver.checkSat();
+    res = res2;
+    assertEquals(res, res2);
+    assertEquals(res3, res2);
+  }
+
+  @Test void isSat()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    Result res = d_solver.checkSat();
+    assertTrue(res.isSat());
+    assertFalse(res.isSatUnknown());
+  }
+
+  @Test void isUnsat()
+  {
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkVar(u_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkSat();
+    assertTrue(res.isUnsat());
+    assertFalse(res.isSatUnknown());
+  }
+
+  @Test void isSatUnknown() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_NIA");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("solve-int-as-bv", "32");
+    Sort int_sort = d_solver.getIntegerSort();
+    Term x = d_solver.mkVar(int_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkSat();
+    assertFalse(res.isSat());
+    assertTrue(res.isSatUnknown());
+  }
+
+  @Test void isEntailed()
+  {
+    d_solver.setOption("incremental", "true");
+    Sort u_sort = d_solver.mkUninterpretedSort("u");
+    Term x = d_solver.mkConst(u_sort, "x");
+    Term y = d_solver.mkConst(u_sort, "y");
+    Term a = x.eqTerm(y).notTerm();
+    Term b = x.eqTerm(y);
+    d_solver.assertFormula(a);
+    Result entailed = d_solver.checkEntailed(a);
+    assertTrue(entailed.isEntailed());
+    assertFalse(entailed.isEntailmentUnknown());
+    Result not_entailed = d_solver.checkEntailed(b);
+    assertTrue(not_entailed.isNotEntailed());
+    assertFalse(not_entailed.isEntailmentUnknown());
+  }
+
+  @Test void isEntailmentUnknown() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_NIA");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("solve-int-as-bv", "32");
+    Sort int_sort = d_solver.getIntegerSort();
+    Term x = d_solver.mkVar(int_sort, "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    Result res = d_solver.checkEntailed(x.eqTerm(x));
+    assertFalse(res.isEntailed());
+    assertTrue(res.isEntailmentUnknown());
+    assertEquals(res.getUnknownExplanation(), Result.UnknownExplanation.UNKNOWN_REASON);
+  }
+}