From ba24986fe2d56e6664dc9aa72bb35e73b0a469fe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Mar 2022 16:56:33 -0500 Subject: [PATCH] Add SynthResult to the API (#8370) Does not modify the code to return a SynthResult yet, just adds the class. Co-authored-by: Aina Niemetz --- docs/api/cpp/cpp.rst | 6 +- docs/api/cpp/synthresult.rst | 7 ++ docs/api/java/java.rst | 1 + docs/api/python/base/python.rst | 3 +- docs/api/python/base/synthresult.rst | 6 ++ src/api/cpp/cvc5.cpp | 40 +++++++ src/api/cpp/cvc5.h | 79 +++++++++++++- src/api/java/CMakeLists.txt | 2 + src/api/java/io/github/cvc5/api/Solver.java | 11 ++ .../java/io/github/cvc5/api/SynthResult.java | 84 +++++++++++++++ src/api/java/jni/solver.cpp | 14 +++ src/api/java/jni/synth_result.cpp | 101 ++++++++++++++++++ src/api/python/cvc5.pxd | 7 ++ src/api/python/cvc5.pxi | 45 ++++++++ test/unit/api/cpp/CMakeLists.txt | 1 + test/unit/api/cpp/synth_result_black.cpp | 38 +++++++ test/unit/api/java/CMakeLists.txt | 1 + test/unit/api/java/SynthResultTest.java | 47 ++++++++ test/unit/api/python/CMakeLists.txt | 1 + test/unit/api/python/test_synth_result.py | 33 ++++++ 20 files changed, 523 insertions(+), 4 deletions(-) create mode 100644 docs/api/cpp/synthresult.rst create mode 100644 docs/api/python/base/synthresult.rst create mode 100644 src/api/java/io/github/cvc5/api/SynthResult.java create mode 100644 src/api/java/jni/synth_result.cpp create mode 100644 test/unit/api/cpp/synth_result_black.cpp create mode 100644 test/unit/api/java/SynthResultTest.java create mode 100644 test/unit/api/python/test_synth_result.py diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index 49548222a..67f2c8053 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -26,6 +26,7 @@ For most applications, the :cpp:class:`Solver ` class is the solver sort statistics + synthresult term @@ -33,7 +34,7 @@ Class hierarchy ^^^^^^^^^^^^^^^ ``namespace cvc5::api {`` - + * class :cpp:class:`CVC5ApiException ` * class :cpp:class:`CVC5ApiRecoverableException ` * class :ref:`api/cpp/datatype:datatype` @@ -60,8 +61,9 @@ Class hierarchy * class :ref:`api/cpp/sort:sort` * class :cpp:class:`Stat ` * class :cpp:class:`Statistics ` + * class :ref:`api/cpp/synthresult:synthresult` * class :ref:`api/cpp/term:term` * class :cpp:class:`const_iterator ` -``}`` \ No newline at end of file +``}`` diff --git a/docs/api/cpp/synthresult.rst b/docs/api/cpp/synthresult.rst new file mode 100644 index 000000000..1765f48c6 --- /dev/null +++ b/docs/api/cpp/synthresult.rst @@ -0,0 +1,7 @@ +SynthResult +=========== + +.. doxygenclass:: cvc5::api::SynthResult + :project: cvc5 + :members: + :undoc-members: diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst index 71a70023b..dad64be05 100644 --- a/docs/api/java/java.rst +++ b/docs/api/java/java.rst @@ -72,6 +72,7 @@ Building cvc5 Java API * class `Sort `_ * class `Stat `_ * class `Statistics `_ + * class `SynthResult `_ * class `Term `_ * class `Triplet `_ * class `Utils `_ diff --git a/docs/api/python/base/python.rst b/docs/api/python/base/python.rst index 5036fa081..cf2122b12 100644 --- a/docs/api/python/base/python.rst +++ b/docs/api/python/base/python.rst @@ -28,5 +28,6 @@ See the :doc:`pythonic API <../pythonic/pythonic>` for a higher-level programmin roundingmode solver sort - term + synthresult + term unknownexplanation diff --git a/docs/api/python/base/synthresult.rst b/docs/api/python/base/synthresult.rst new file mode 100644 index 000000000..e89ef80c1 --- /dev/null +++ b/docs/api/python/base/synthresult.rst @@ -0,0 +1,6 @@ +SynthResult +=========== + +.. autoclass:: cvc5.SynthResult + :members: + :undoc-members: diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 95d3815d6..0eba91ee2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -83,6 +83,7 @@ #include "util/statistics_stats.h" #include "util/statistics_value.h" #include "util/string.h" +#include "util/synth_result.h" #include "util/uninterpreted_sort_value.h" #include "util/utility.h" @@ -988,6 +989,45 @@ std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) return out; } +/* -------------------------------------------------------------------------- */ +/* SynthResult */ +/* -------------------------------------------------------------------------- */ + +SynthResult::SynthResult(const cvc5::SynthResult& r) + : d_result(new cvc5::SynthResult(r)) +{ +} + +SynthResult::SynthResult() : d_result(new cvc5::SynthResult()) {} + +bool SynthResult::isNull() const +{ + return d_result->getStatus() == cvc5::SynthResult::NONE; +} + +bool SynthResult::hasSolution(void) const +{ + return d_result->getStatus() == cvc5::SynthResult::SOLUTION; +} + +bool SynthResult::hasNoSolution() const +{ + return d_result->getStatus() == cvc5::SynthResult::NO_SOLUTION; +} + +bool SynthResult::isUnknown() const +{ + return d_result->getStatus() == cvc5::SynthResult::UNKNOWN; +} + +std::string SynthResult::toString(void) const { return d_result->toString(); } + +std::ostream& operator<<(std::ostream& out, const SynthResult& sr) +{ + out << sr.toString(); + return out; +} + /* -------------------------------------------------------------------------- */ /* Sort */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 9adae1337..6d7f0417c 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -50,6 +50,7 @@ class Options; class Random; class Rational; class Result; +class SynthResult; class StatisticsRegistry; namespace main { @@ -61,6 +62,7 @@ namespace api { class Solver; class Statistics; struct APIStatistics; +class Term; /* -------------------------------------------------------------------------- */ /* Exception */ @@ -257,7 +259,7 @@ class CVC5_EXPORT Result Result(const cvc5::Result& r); /** - * The interal result wrapped by this result. + * The internal result wrapped by this result. * * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` * since ``cvc5::Result`` is not ref counted. @@ -282,6 +284,80 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC5_EXPORT; +/* -------------------------------------------------------------------------- */ +/* Result */ +/* -------------------------------------------------------------------------- */ + +/** + * Encapsulation of a solver synth result. + * + * This is the return value of the API methods: + * - Solver::checkSynth() + * - Solver::checkSynthNext() + * + * which we call synthesis queries. This class indicates whether the + * synthesis query has a solution, has no solution, or is unknown. + */ +class CVC5_EXPORT SynthResult +{ + friend class Solver; + + public: + /** Constructor. */ + SynthResult(); + + /** + * @return true if SynthResult is null, i.e., not a SynthResult returned + * from a synthesis query. + */ + bool isNull() const; + + /** + * @return true if the synthesis query has a solution. + */ + bool hasSolution() const; + + /** + * @return true if the synthesis query has no solution. In this case, it + * was determined that there was no solution. + */ + bool hasNoSolution() const; + + /** + * @return true if the result of the synthesis query could not be determined. + */ + bool isUnknown() const; + + /** + * @return a string representation of this synthesis result. + */ + std::string toString() const; + + private: + /** + * Constructor. + * @param r the internal synth result that is to be wrapped by this synth + * result + * @return the SynthResult + */ + SynthResult(const cvc5::SynthResult& r); + /** + * The internal result wrapped by this result. + * + * @note This is a `std::shared_ptr` rather than a `std::unique_ptr` + * since `cvc5::SynthResult` is not ref counted. + */ + std::shared_ptr d_result; +}; + +/** + * Serialize a SynthResult to given stream. + * @param out the output stream + * @param r the result to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const SynthResult& r) CVC5_EXPORT; + /* -------------------------------------------------------------------------- */ /* Sort */ /* -------------------------------------------------------------------------- */ @@ -987,6 +1063,7 @@ class CVC5_EXPORT Term friend class DatatypeSelector; friend class Solver; friend class Grammar; + friend class SynthResult; friend struct std::hash; public: diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 95c1ae4a4..342a37394 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -67,6 +67,7 @@ set(JAVA_FILES ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Sort.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Stat.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Statistics.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/SynthResult.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Term.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Triplet.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Utils.java @@ -121,6 +122,7 @@ add_library(cvc5jni jni/sort.cpp jni/stat.cpp jni/statistics.cpp + jni/synth_result.cpp jni/term.cpp) add_dependencies(cvc5jni generate-jni-headers) diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index d0cc01232..f1f2b91f6 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2699,6 +2699,17 @@ public class Solver implements IPointer, AutoCloseable private native long getNullResult(long pointer); + /** + * @return null synth result + */ + public SynthResult getNullSynthResult() + { + long resultPointer = getNullSynthResult(pointer); + return new SynthResult(this, resultPointer); + } + + private native long getNullSynthResult(long pointer); + /** * @return null op */ diff --git a/src/api/java/io/github/cvc5/api/SynthResult.java b/src/api/java/io/github/cvc5/api/SynthResult.java new file mode 100644 index 000000000..7d9b5b6dd --- /dev/null +++ b/src/api/java/io/github/cvc5/api/SynthResult.java @@ -0,0 +1,84 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 io.github.cvc5.api; + +import java.util.HashMap; +import java.util.Map; + +public class SynthResult extends AbstractPointer +{ + // region construction and destruction + SynthResult(Solver solver, long pointer) + { + super(solver, pointer); + } + + protected native void deletePointer(long pointer); + + public long getPointer() + { + return pointer; + } + + // endregion + + /** + * Return true if SynthResult is empty, i.e., a nullary SynthResult, and not + * an actual result returned from a synthesis query. + */ + public boolean isNull() + { + return isNull(pointer); + } + + private native boolean isNull(long pointer); + + /** + * Return true if the synthesis query has a solution. + */ + public boolean hasSolution() + { + return hasSolution(pointer); + } + + private native boolean hasSolution(long pointer); + + /** + * Return true if the synthesis query has no solution. In this case, it was + * determined there was no solution. + */ + public boolean hasNoSolution() + { + return hasNoSolution(pointer); + } + + private native boolean hasNoSolution(long pointer); + + /** + * Return true if the result of the synthesis query could not be determined. + */ + public boolean isUnknown() + { + return isUnknown(pointer); + } + + private native boolean isUnknown(long pointer); + + /** + * @return a string representation of this result. + */ + protected native String toString(long pointer); +} diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index fae1b44eb..f440c1646 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2705,6 +2705,20 @@ Java_io_github_cvc5_api_Solver_getNullResult(JNIEnv* env, jobject, jlong) CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_api_Solver + * Method: getNullSynthResult + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getNullSynthResult(JNIEnv* env, jobject, jlong) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* ret = new SynthResult(); + return reinterpret_cast(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: getNullOp diff --git a/src/api/java/jni/synth_result.cpp b/src/api/java/jni/synth_result.cpp new file mode 100644 index 000000000..6d0ab38d7 --- /dev/null +++ b/src/api/java/jni/synth_result.cpp @@ -0,0 +1,101 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 "api/cpp/cvc5.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_SynthResult.h" + +using namespace cvc5::api; + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_io_github_cvc5_api_SynthResult_deletePointer( + JNIEnv*, jobject, jlong pointer) +{ + delete ((SynthResult*)pointer); +} + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: isNull + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_SynthResult_isNull(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* current = (SynthResult*)pointer; + return (jboolean)current->isNull(); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: hasSolution + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_SynthResult_hasSolution( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* current = (SynthResult*)pointer; + return (jboolean)current->hasSolution(); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: hasNoSolution + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_SynthResult_hasNoSolution( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* current = (SynthResult*)pointer; + return (jboolean)current->hasNoSolution(); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: isUnknown + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_SynthResult_isUnknown( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* current = (SynthResult*)pointer; + return (jboolean)current->isUnknown(); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, (jboolean) false); +} + +/* + * Class: io_github_cvc5_api_SynthResult + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_SynthResult_toString( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + SynthResult* current = (SynthResult*)pointer; + return env->NewStringUTF(current->toString().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 5f7b61cb5..c057e20f1 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -193,6 +193,13 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": UnknownExplanation getUnknownExplanation() except + string toString() except + + cdef cppclass SynthResult: + SynthResult() except+ + bint isNull() except + + bint hasSolution() except + + bint hasNoSolution() except + + bint isUnknown() except + + string toString() except + cdef cppclass RoundingMode: pass diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 9ef53b86b..3305352d3 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -21,6 +21,7 @@ from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl from cvc5 cimport DatatypeDecl as c_DatatypeDecl from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result +from cvc5 cimport SynthResult as c_SynthResult from cvc5 cimport RoundingMode as c_RoundingMode from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op @@ -615,6 +616,50 @@ cdef class Result: def __repr__(self): return self.cr.toString().decode() +cdef class SynthResult: + """ + Encapsulation of a solver synth result. This is the return value of the + API methods: + - :py:meth:`Solver.checkSynth()` + - :py:meth:`Solver.checkSynthNext()` + which we call synthesis queries. This class indicates whether the + synthesis query has a solution, has no solution, or is unknown. + """ + cdef c_SynthResult cr + def __cinit__(self): + # gets populated by solver + self.cr = c_SynthResult() + + def isNull(self): + """ + :return: True if SynthResult is null, i.e. not a SynthResult returned from a synthesis query. + """ + return self.cr.isNull() + + def hasSolution(self): + """ + :return: True if the synthesis query has a solution. + """ + return self.cr.hasSolution() + + def hasNoSolution(self): + """ + :return: True if the synthesis query has no solution. + In this case, then it was determined there was no solution. + """ + return self.cr.hasNoSolution() + + def isUnknown(self): + """ + :return: True if the result of the synthesis query could not be determined. + """ + return self.cr.isUnknown() + + def __str__(self): + return self.cr.toString().decode() + + def __repr__(self): + return self.cr.toString().decode() cdef class RoundingMode: """ diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt index d356236be..cf6816981 100644 --- a/test/unit/api/cpp/CMakeLists.txt +++ b/test/unit/api/cpp/CMakeLists.txt @@ -25,4 +25,5 @@ cvc5_add_unit_test_black(theory_arith_nl_black api/cpp) cvc5_add_unit_test_black(theory_uf_ho_black api/cpp) cvc5_add_unit_test_white(op_white api/cpp) cvc5_add_unit_test_white(solver_white api/cpp) +cvc5_add_unit_test_black(synth_result_black api/cpp) cvc5_add_unit_test_white(term_white api/cpp) diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp new file mode 100644 index 000000000..d2aebdbc4 --- /dev/null +++ b/test/unit/api/cpp/synth_result_black.cpp @@ -0,0 +1,38 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 SynthResult class + */ + +#include "test_api.h" + +namespace cvc5 { + +using namespace api; + +namespace test { + +class TestApiBlackSynthResult : public TestApi +{ +}; + +TEST_F(TestApiBlackSynthResult, isNull) +{ + cvc5::api::SynthResult res_null; + ASSERT_TRUE(res_null.isNull()); + ASSERT_FALSE(res_null.hasSolution()); + ASSERT_FALSE(res_null.hasNoSolution()); + ASSERT_FALSE(res_null.isUnknown()); +} + +} // namespace test +} // namespace cvc5 diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt index 5f573a117..697dff605 100644 --- a/test/unit/api/java/CMakeLists.txt +++ b/test/unit/api/java/CMakeLists.txt @@ -28,6 +28,7 @@ set(java_test_src_files ${CMAKE_CURRENT_SOURCE_DIR}/ResultTest.java ${CMAKE_CURRENT_SOURCE_DIR}/SolverTest.java ${CMAKE_CURRENT_SOURCE_DIR}/SortTest.java + ${CMAKE_CURRENT_SOURCE_DIR}/SynthResultTest.java ${CMAKE_CURRENT_SOURCE_DIR}/TermTest.java ) diff --git a/test/unit/api/java/SynthResultTest.java b/test/unit/api/java/SynthResultTest.java new file mode 100644 index 000000000..058decd0b --- /dev/null +++ b/test/unit/api/java/SynthResultTest.java @@ -0,0 +1,47 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 SynthResult class + */ + +package tests; + +import static org.junit.jupiter.api.Assertions.*; + +import io.github.cvc5.api.*; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class SynthResultTest +{ + private Solver d_solver; + + @BeforeEach void setUp() + { + d_solver = new Solver(); + } + + @AfterEach void tearDown() + { + d_solver.close(); + } + + @Test void isNull() + { + SynthResult res_null = d_solver.getNullSynthResult(); + assertTrue(res_null.isNull()); + assertFalse(res_null.hasSolution()); + assertFalse(res_null.hasNoSolution()); + assertFalse(res_null.isUnknown()); + } +} diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt index a322bbcc2..fe68f1eea 100644 --- a/test/unit/api/python/CMakeLists.txt +++ b/test/unit/api/python/CMakeLists.txt @@ -38,3 +38,4 @@ cvc5_add_python_api_unit_test(test_grammar test_grammar.py) cvc5_add_python_api_unit_test(test_to_python_obj test_to_python_obj.py) cvc5_add_python_api_unit_test(test_op test_op.py) cvc5_add_python_api_unit_test(test_result test_result.py) +cvc5_add_python_api_unit_test(test_synth_result test_synth_result.py) diff --git a/test/unit/api/python/test_synth_result.py b/test/unit/api/python/test_synth_result.py new file mode 100644 index 000000000..a07b635de --- /dev/null +++ b/test/unit/api/python/test_synth_result.py @@ -0,0 +1,33 @@ +############################################################################### +# Top contributors (to current version): +# Andrew Reynolds +# +# 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. +# ############################################################################# +# +# Unit tests for synth result API. +# +# Obtained by translating test/unit/api/synth_result_black.cpp +## + +import pytest +import cvc5 +from cvc5 import SynthResult + + +@pytest.fixture +def solver(): + return cvc5.Solver() + + +def test_is_null(solver): + res_null = SynthResult(solver) + assert res_null.isNull() + assert not res_null.hasSolution() + assert not res_null.hasNoSolution() + assert not res_null.isUnknown() -- 2.30.2