summaryrefslogtreecommitdiff
path: root/docs/api
diff options
context:
space:
mode:
Diffstat (limited to 'docs/api')
-rw-r--r--docs/api/api.rst5
-rw-r--r--docs/api/cpp/class_hierarchy.rst47
-rw-r--r--docs/api/cpp/cpp.rst50
-rw-r--r--docs/api/java/CMakeLists.txt13
-rw-r--r--docs/api/python/python.rst2
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
========================
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback