diff options
Diffstat (limited to 'docs/api')
-rw-r--r-- | docs/api/api.rst | 5 | ||||
-rw-r--r-- | docs/api/cpp/class_hierarchy.rst | 47 | ||||
-rw-r--r-- | docs/api/cpp/cpp.rst | 50 | ||||
-rw-r--r-- | docs/api/java/CMakeLists.txt | 13 | ||||
-rw-r--r-- | docs/api/python/python.rst | 2 |
5 files changed, 54 insertions, 63 deletions
diff --git a/docs/api/api.rst b/docs/api/api.rst index a3acdda17..4a1fb7202 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -1,6 +1,11 @@ API Documentation ================= +In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs +for several different programming languages. +While the :doc:`C++ API <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/index>` and the :doc:`Python API <python/python>` implement a thin wrapper around it. +Additionally, a more pythonic Python API is availble at https://github.com/cvc5/cvc5_z3py_compat. + .. toctree:: :maxdepth: 1 diff --git a/docs/api/cpp/class_hierarchy.rst b/docs/api/cpp/class_hierarchy.rst deleted file mode 100644 index b441106ff..000000000 --- a/docs/api/cpp/class_hierarchy.rst +++ /dev/null @@ -1,47 +0,0 @@ -C++ API Class Hierarchy -======================= - -``namespace cvc5::api {`` - - * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` - * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` - - * class :ref:`api/cpp/datatype:datatype` - - * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` - - * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` - - * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` - - * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl` - * class :ref:`api/cpp/datatypedecl:datatypedecl` - * class :ref:`api/cpp/datatypeselector:datatypeselector` - - * class :ref:`api/cpp/grammar:grammar` - - * class :ref:`api/cpp/kind:kind` - - * class :ref:`api/cpp/op:op` - - * class :ref:`api/cpp/optioninfo:optioninfo` - - * class :ref:`api/cpp/result:result` - - * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` - - * class :ref:`api/cpp/roundingmode:roundingmode` - - * class :ref:`api/cpp/solver:solver` - - * class :ref:`api/cpp/sort:sort` - - * class :cpp:class:`Stat <cvc5::api::Stat>` - - * class :cpp:class:`Statistics <cvc5::api::Statistics>` - - * class :ref:`api/cpp/term:term` - - * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` - -``}`` diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index edcbbd87d..96177e7d8 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -1,25 +1,23 @@ -.. _cpp-api: - C++ API Documentation ===================== -.. toctree:: - :maxdepth: 1 +The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5. +The :doc:`quickstart guide <quickstart>` gives a short introduction, while the following class hierarchy of the ``cvc5::api`` namespace provides more details on the individual classes. +For most applications, the :cpp:class:`Solver <cvc5::api::Solver>` class is the main entry point to cvc5. - quickstart - class_hierarchy .. container:: hide-toctree .. toctree:: :maxdepth: 0 + quickstart + exceptions datatype datatypeconstructor datatypeconstructordecl datatypedecl datatypeselector - exceptions grammar kind op @@ -30,3 +28,41 @@ C++ API Documentation sort statistics term + + +Class hierarchy +^^^^^^^^^^^^^^^ + +``namespace cvc5::api {`` + + * class :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` + * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` + * class :ref:`api/cpp/datatype:datatype` + + * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` + + * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>` + + * class :ref:`api/cpp/datatypeconstructordecl:datatypeconstructordecl` + * class :ref:`api/cpp/datatypedecl:datatypedecl` + * class :ref:`api/cpp/datatypeselector:datatypeselector` + * class :ref:`api/cpp/grammar:grammar` + * class :ref:`api/cpp/kind:kind` + * class :ref:`api/cpp/op:op` + * class :ref:`api/cpp/optioninfo:optioninfo` + * class :ref:`api/cpp/result:result` + + * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>` + + * class :ref:`api/cpp/roundingmode:roundingmode` + * class :ref:`api/cpp/solver:solver` + * class :ref:`api/cpp/sort:sort` + * class :cpp:class:`Stat <cvc5::api::Stat>` + * class :cpp:class:`Statistics <cvc5::api::Statistics>` + * class :ref:`api/cpp/term:term` + + * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>` + +``}``
\ No newline at end of file diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 7c897a354..8a728407f 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -23,19 +23,18 @@ if(BUILD_BINDINGS_JAVA) # used to trigger the rebuild set(JAVADOC_INDEX_FILE ${JAVADOC_OUTPUT_DIR}/index.html) - get_target_property(SOURCES cvc5jar SOURCES) - + get_target_property(CVC5_JAR_FILE cvc5jar JAR_FILE) add_custom_command( - OUTPUT "${JAVADOC_INDEX_FILE}" - COMMAND + OUTPUT ${JAVADOC_INDEX_FILE} + COMMAND ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api - -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/ + -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} - -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar + -cp ${CVC5_JAR_FILE} -notimestamp COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's/<!-- Generated by javadoc [^>]* -->//' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete - DEPENDS cvc5jar ${SOURCES} + DEPENDS cvc5jar ${CVC5_JAR_FILE} COMMENT "Generating javadocs" ) diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index f6258af2d..0cf78d0ce 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -1,5 +1,3 @@ -.. _python-api: - Python API Documentation ======================== |