summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/java/cvc5/Result.java210
-rw-r--r--src/api/java/jni/cvc5_Result.cpp186
-rw-r--r--test/unit/api/java/cvc5/ResultTest.java126
3 files changed, 522 insertions, 0 deletions
diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java
new file mode 100644
index 000000000..bd142b985
--- /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
index 000000000..4bc5cec1b
--- /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
index 000000000..8ba50c00a
--- /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);
+ }
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback