Various minor docs improvements (#7626)

This PR does a number of minor improvements to the docs.

11 files changed, 65 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 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/<!-- Generated by javadoc [^>]* -->//' {} "\;"
     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 <quickstart>` gives a short introduction on how to use cvc5 via the SMT-LIBv2
+interface, but cvc5 also supports other :doc:`input languages <languages>`.
+The behavior of cvc5 can be changed with a number of :doc:`options <options>`, and :doc:`output tags <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
index 34c536017..34c536017 100644
--- a/docs/languages.rst
+++ b/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 <https://github.com/cvc5/cvc5/blob/master/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>": "Term[]",
         r"std::string": "String",
         r"&": "",
-        r"::": "."
+        r"::": ".",
+        r">": "&gt;",
+        r"<": "&lt;",
+        r"@f\[": "",
+        r"@f\]": "",
+        r"@note": "",
     }