From: mudathirmahgoub Date: Fri, 14 May 2021 01:15:21 +0000 (-0500) Subject: Add Result.java to the java API (#6385) X-Git-Tag: cvc5-1.0.0~1762 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce851ed5aea5ee4bd36ffbba9f86052025434126;p=cvc5.git 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 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 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); + } +}