From 5cfbb67e228daf76835b7fd0a95d214859be030e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 11 Nov 2021 18:27:53 -0800 Subject: [PATCH] Various minor docs improvements (#7626) This PR does a number of minor improvements to the docs. --- docs/api/api.rst | 5 ++++ docs/api/cpp/class_hierarchy.rst | 47 ------------------------------ docs/api/cpp/cpp.rst | 50 +++++++++++++++++++++++++++----- docs/api/java/CMakeLists.txt | 5 ++-- docs/api/python/python.rst | 2 -- docs/binary/binary.rst | 7 +++++ docs/{ => binary}/languages.rst | 0 docs/binary/quickstart.rst | 2 +- docs/examples/examples.rst | 2 +- docs/index.rst | 1 - src/api/java/genkinds.py.in | 7 ++++- 11 files changed, 65 insertions(+), 63 deletions(-) delete mode 100644 docs/api/cpp/class_hierarchy.rst rename docs/{ => binary}/languages.rst (100%) 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 ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`Python API ` 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 ` - * class :cpp:class:`CVC5ApiRecoverableException ` - - * class :ref:`api/cpp/datatype:datatype` - - * class :cpp:class:`const_iterator ` - - * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` - - * class :cpp:class:`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 ` - - * class :ref:`api/cpp/roundingmode:roundingmode` - - * class :ref:`api/cpp/solver:solver` - - * class :ref:`api/cpp/sort:sort` - - * class :cpp:class:`Stat ` - - * class :cpp:class:`Statistics ` - - * class :ref:`api/cpp/term:term` - - * class :cpp:class:`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 ` 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 ` 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 ` + * class :cpp:class:`CVC5ApiRecoverableException ` + * class :ref:`api/cpp/datatype:datatype` + + * class :cpp:class:`const_iterator ` + + * class :ref:`api/cpp/datatypeconstructor:datatypeconstructor` + + * class :cpp:class:`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 ` + + * class :ref:`api/cpp/roundingmode:roundingmode` + * class :ref:`api/cpp/solver:solver` + * class :ref:`api/cpp/sort:sort` + * class :cpp:class:`Stat ` + * class :cpp:class:`Statistics ` + * class :ref:`api/cpp/term:term` + + * class :cpp:class:`const_iterator ` + +``}`` \ No newline at end of file diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 6df794435..8a728407f 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -25,17 +25,16 @@ if(BUILD_BINDINGS_JAVA) get_target_property(CVC5_JAR_FILE cvc5jar JAR_FILE) add_custom_command( - OUTPUT "${JAVADOC_INDEX_FILE}" + OUTPUT ${JAVADOC_INDEX_FILE} COMMAND ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ - -Xdoclint:none -d ${JAVADOC_OUTPUT_DIR} -cp ${CVC5_JAR_FILE} -notimestamp COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's///' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete - DEPENDS cvc5jar + 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 ======================== diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index 91e2493e7..44a177afb 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -1,11 +1,18 @@ Binary Documentation ==================== +The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line. +The :doc:`quickstart guide ` gives a short introduction on how to use cvc5 via the SMT-LIBv2 +interface, but cvc5 also supports other :doc:`input languages `. +The behavior of cvc5 can be changed with a number of :doc:`options `, and :doc:`output tags ` allow to extract structured information about the solving process. + +Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages. .. toctree:: :maxdepth: 2 quickstart + languages options output-tags diff --git a/docs/languages.rst b/docs/binary/languages.rst similarity index 100% rename from docs/languages.rst rename to docs/binary/languages.rst diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst index 67280ca45..f3c9c4ad8 100644 --- a/docs/binary/quickstart.rst +++ b/docs/binary/quickstart.rst @@ -119,7 +119,7 @@ Example | The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. .. api-examples:: + ../../examples/api/smtlib/quickstart.smt2 ../../examples/api/cpp/quickstart.cpp ../../examples/api/java/QuickStart.java ../../examples/api/python/quickstart.py - ../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index 0b2651851..accdd004f 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,7 +1,7 @@ Examples =========== -The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) +The following examples show how the APIs (:doc:`../api/cpp/cpp`, :doc:`../api/java/index`, :doc:`../api/python/python`) and input languages can be used. For every example, the same problem is constructed and solved using different input mechanisms. diff --git a/docs/index.rst b/docs/index.rst index 5f0ede34f..27b7b728d 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -18,7 +18,6 @@ Table of Contents binary/binary api/api examples/examples - languages theory references genindex diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in index a15472a1a..d44ae3c0d 100644 --- a/src/api/java/genkinds.py.in +++ b/src/api/java/genkinds.py.in @@ -97,7 +97,12 @@ CPP_JAVA_MAPPING = \ r"std::vector": "Term[]", r"std::string": "String", r"&": "", - r"::": "." + r"::": ".", + r">": ">", + r"<": "<", + r"@f\[": "", + r"@f\]": "", + r"@note": "", } -- 2.30.2