Various minor docs improvements (#7626)

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

diff --git a/docs/api/api.rst b/docs/api/api.rst
index a3acdda1749fa4b52e1c09c90d1511ff7f636370..4a1fb72022086f7354ae3753bf4f22d1e8770e6e 100644 (file)
--- 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 (file)
index b441106..0000000
--- 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 edcbbd87dd3e75ecc7cb7bacb66b1949d3ec66a3..96177e7d8c71c7e9e8c53e0f4ce38c94a2186bbb 100644 (file)
--- 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 6df794435d71dda5de8daefb738d40f3d198fe24..8a728407fd6ec96a9f33942cd816f941f50711bd 100644 (file)
--- 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 f6258af2d342f60c5fc6752a60debb31f7b22b8a..0cf78d0ce1b1634e8fd5fc89cb5089334fd4e7bc 100644 (file)
--- 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 91e2493e79c6df81c58648895d9406806f8c4dbf..44a177afb0d32f0d649632a10a1cdb78d951fbbc 100644 (file)
--- 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/binary/languages.rst b/docs/binary/languages.rst
new file mode 100644 (file)
index 0000000..34c5360
--- /dev/null
+++ b/docs/binary/languages.rst
@@ -0,0 +1,8 @@
+Input Languages
+===============
+
+cvc5 supports the following input languages:
+
+* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
+* `SyGuS-IF <https://sygus.org/language/>`_
+* `TPTP <http://www.tptp.org/>`_

diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index 67280ca450b2299736d333113be24b3476295ba7..f3c9c4ad870843f42c7084d7303a69f0b1a242d6 100644 (file)
--- 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 0b2651851c547e17bc876a5b6ea7608e79323c7e..accdd004fc1ce0a76f17a2f757049a89bb6c4055 100644 (file)
--- 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 5f0ede34f05e1eefadabc16b7509dd358757c823..27b7b728dfaee32696642a0e90c41b35b32c1ce2 100644 (file)
--- 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/docs/languages.rst b/docs/languages.rst
deleted file mode 100644 (file)
index 34c5360..0000000
--- a/docs/languages.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-Input Languages
-===============
-
-cvc5 supports the following input languages:
-
-* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
-* `SyGuS-IF <https://sygus.org/language/>`_
-* `TPTP <http://www.tptp.org/>`_

diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in
index a15472a1a4e1cdf957b694844f4ed41d4ae71878..d44ae3c0d76df6321a379c35ae88288927dfae6a 100644 (file)
--- 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": "",
     }