Does not modify the code to return a SynthResult yet, just adds the class.
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
solver
sort
statistics
+ synthresult
term
^^^^^^^^^^^^^^^
``namespace cvc5::api {``
-
+
* class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>`
* class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>`
* class :ref:`api/cpp/datatype:datatype`
* class :ref:`api/cpp/sort:sort`
* class :cpp:class:`Stat <cvc5::api::Stat>`
* class :cpp:class:`Statistics <cvc5::api::Statistics>`
+ * class :ref:`api/cpp/synthresult:synthresult`
* class :ref:`api/cpp/term:term`
* class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>`
-``}``
\ No newline at end of file
+``}``
--- /dev/null
+SynthResult
+===========
+
+.. doxygenclass:: cvc5::api::SynthResult
+ :project: cvc5
+ :members:
+ :undoc-members:
* class `Sort <io/github/cvc5/api/Sort.html>`_
* class `Stat <io/github/cvc5/api/Stat.html>`_
* class `Statistics <io/github/cvc5/api/Statistics.html>`_
+ * class `SynthResult <io/github/cvc5/api/SynthResult.html>`_
* class `Term <io/github/cvc5/api/Term.html>`_
* class `Triplet<A,B,C> <io/github/cvc5/api/Triplet.html>`_
* class `Utils <io/github/cvc5/api/Utils.html>`_
roundingmode
solver
sort
- term
+ synthresult
+ term
unknownexplanation
--- /dev/null
+SynthResult
+===========
+
+.. autoclass:: cvc5.SynthResult
+ :members:
+ :undoc-members:
#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"
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 */
/* -------------------------------------------------------------------------- */
class Random;
class Rational;
class Result;
+class SynthResult;
class StatisticsRegistry;
namespace main {
class Solver;
class Statistics;
struct APIStatistics;
+class Term;
/* -------------------------------------------------------------------------- */
/* Exception */
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.
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<cvc5::SynthResult> 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 */
/* -------------------------------------------------------------------------- */
friend class DatatypeSelector;
friend class Solver;
friend class Grammar;
+ friend class SynthResult;
friend struct std::hash<Term>;
public:
${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
jni/sort.cpp
jni/stat.cpp
jni/statistics.cpp
+ jni/synth_result.cpp
jni/term.cpp)
add_dependencies(cvc5jni generate-jni-headers)
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
*/
--- /dev/null
+/******************************************************************************
+ * 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);
+}
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<jlong>(ret);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: io_github_cvc5_api_Solver
* Method: getNullOp
--- /dev/null
+/******************************************************************************
+ * 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);
+}
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
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
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:
"""
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)
--- /dev/null
+/******************************************************************************
+ * 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
${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
)
--- /dev/null
+/******************************************************************************
+ * 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());
+ }
+}
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)
--- /dev/null
+###############################################################################
+# 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()
projects / cvc5.git / commitdiff