New C++ Api: Initial layout of Api documentation. (#6325)

16 files changed, 217 insertions, 12 deletions

diff --git a/docs/conf.py b/docs/conf.py
index 8489f39d7..5713d3fa3 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -28,7 +28,8 @@ author = 'The Authors of cvc5'
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
-        "breathe"
+        'breathe',
+        'sphinx.ext.autosectionlabel'
 ]
 
 # Add any paths that contain templates here, relative to this directory.
@@ -46,11 +47,14 @@ exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
 # a list of builtin themes.
 #
 html_theme = 'sphinx_rtd_theme'
+html_theme_options = {
+}
 
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['_static']
+html_static_path = []
 
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
+breathe_domain_by_extension = {"h" : "cpp"}
diff --git a/docs/cpp.rst b/docs/cpp.rst
new file mode 100644
index 000000000..b9bc5f077
--- /dev/null
+++ b/docs/cpp.rst
@@ -0,0 +1,95 @@
+C++ API Documentation
+=====================
+
+Class Hierarchy
+---------------
+
+* namespace ``cvc5``
+
+  * namespace ``api``
+
+    * class :ref:`CVC4ApiException<exceptions>`
+
+    * class :ref:`CVC4ApiRecoverableException<exceptions>`
+
+    * class :doc:`cpp/datatype`
+
+      * class :ref:`Datatype::const_iterator<datatype>`
+
+    * class :doc:`cpp/datatypeconstructor`
+
+      * class :ref:`DatatypeConstructor::const_iterator<datatypeconstructor>`
+
+    * class :doc:`cpp/datatypeconstructordecl`
+
+    * class :doc:`cpp/datatypedecl`
+
+    * class :doc:`cpp/datatypeselector`
+
+    * class :doc:`cpp/grammar`
+
+    * class :doc:`cpp/op`
+
+    * class :doc:`cpp/result`
+
+    * class :doc:`cpp/solver`
+
+    * class :doc:`cpp/term`
+
+      * class :ref:`Term::const_iterator<term>`
+
+    * enum :doc:`cpp/kind`
+
+    * enum :doc:`cpp/roundingmode`
+
+    * struct :ref:`KindHashFunction<kind>`
+
+    * struct :ref:`OpHashFunction<op>`
+
+    * struct :ref:`SortHashFunction<sort>`
+
+    * struct :ref:`TermHashFunction<term>`
+
+
+Full API Documentation
+----------------------
+
+Exceptions
+^^^^^^^^^^
+.. doxygenclass:: cvc5::api::CVC4ApiException
+    :project: cvc5
+    :members:
+
+.. doxygenclass:: cvc5::api::CVC4ApiRecoverableException
+    :project: cvc5
+    :members:
+
+
+Enums
+^^^^^
+
+.. toctree::
+   :maxdepth: 2
+
+   cpp/kind
+   cpp/roundingmode
+
+
+Classes
+^^^^^^^
+
+.. toctree::
+   :maxdepth: 2
+
+   cpp/datatype
+   cpp/datatypeconstructor
+   cpp/datatypeconstructordecl
+   cpp/datatypedecl
+   cpp/datatypeselector
+   cpp/grammar
+   cpp/op
+   cpp/result
+   cpp/solver
+   cpp/sort
+   cpp/term
+
diff --git a/docs/cpp/datatype.rst b/docs/cpp/datatype.rst
new file mode 100644
index 000000000..7c5325ec1
--- /dev/null
+++ b/docs/cpp/datatype.rst
@@ -0,0 +1,7 @@
+Datatype
+========
+
+.. doxygenclass:: cvc5::api::Datatype
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/datatypeconstructor.rst b/docs/cpp/datatypeconstructor.rst
new file mode 100644
index 000000000..90b48e8e1
--- /dev/null
+++ b/docs/cpp/datatypeconstructor.rst
@@ -0,0 +1,7 @@
+DatatypeConstructor
+===================
+
+.. doxygenclass:: cvc5::api::DatatypeConstructor
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/datatypeconstructordecl.rst b/docs/cpp/datatypeconstructordecl.rst
new file mode 100644
index 000000000..7cb5b6a8c
--- /dev/null
+++ b/docs/cpp/datatypeconstructordecl.rst
@@ -0,0 +1,7 @@
+DatatypeConstructorDecl
+=======================
+
+.. doxygenclass:: cvc5::api::DatatypeConstructorDecl
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/datatypedecl.rst b/docs/cpp/datatypedecl.rst
new file mode 100644
index 000000000..d3927b805
--- /dev/null
+++ b/docs/cpp/datatypedecl.rst
@@ -0,0 +1,7 @@
+DatatypeDecl
+============
+
+.. doxygenclass:: cvc5::api::DatatypeDecl
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/datatypeselector.rst b/docs/cpp/datatypeselector.rst
new file mode 100644
index 000000000..22ac01aa4
--- /dev/null
+++ b/docs/cpp/datatypeselector.rst
@@ -0,0 +1,7 @@
+DatatypeSelector
+================
+
+.. doxygenclass:: cvc5::api::DatatypeSelector
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/grammar.rst b/docs/cpp/grammar.rst
new file mode 100644
index 000000000..dc7291f67
--- /dev/null
+++ b/docs/cpp/grammar.rst
@@ -0,0 +1,7 @@
+Grammar
+=======
+
+.. doxygenclass:: cvc5::api::Grammar
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/kind.rst b/docs/cpp/kind.rst
new file mode 100644
index 000000000..23421905e
--- /dev/null
+++ b/docs/cpp/kind.rst
@@ -0,0 +1,10 @@
+Kind
+====
+
+.. doxygenstruct:: cvc5::api::KindHashFunction
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenenum:: cvc5::api::Kind
+    :project: cvc5
diff --git a/docs/cpp/op.rst b/docs/cpp/op.rst
new file mode 100644
index 000000000..cee7a1920
--- /dev/null
+++ b/docs/cpp/op.rst
@@ -0,0 +1,11 @@
+Op
+==
+
+.. doxygenstruct:: cvc5::api::OpHashFunction
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenclass:: cvc5::api::Op
+    :project: cvc5
+    :members:
diff --git a/docs/cpp/result.rst b/docs/cpp/result.rst
new file mode 100644
index 000000000..9ba1aaaaf
--- /dev/null
+++ b/docs/cpp/result.rst
@@ -0,0 +1,7 @@
+Result
+======
+
+.. doxygenclass:: cvc5::api::Result
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/roundingmode.rst b/docs/cpp/roundingmode.rst
new file mode 100644
index 000000000..83e2e003a
--- /dev/null
+++ b/docs/cpp/roundingmode.rst
@@ -0,0 +1,10 @@
+RoundingMode
+============
+
+.. doxygenstruct:: cvc5::api::RoundingModeHashFunction
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenenum:: cvc5::api::RoundingMode
+    :project: cvc5
diff --git a/docs/cpp/solver.rst b/docs/cpp/solver.rst
new file mode 100644
index 000000000..17529f09b
--- /dev/null
+++ b/docs/cpp/solver.rst
@@ -0,0 +1,7 @@
+Solver
+======
+
+.. doxygenclass:: cvc5::api::Solver
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/sort.rst b/docs/cpp/sort.rst
new file mode 100644
index 000000000..64b631d63
--- /dev/null
+++ b/docs/cpp/sort.rst
@@ -0,0 +1,12 @@
+Sort
+====
+
+.. doxygenstruct:: cvc5::api::SortHashFunction
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenclass:: cvc5::api::Sort
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/cpp/term.rst b/docs/cpp/term.rst
new file mode 100644
index 000000000..c17d74945
--- /dev/null
+++ b/docs/cpp/term.rst
@@ -0,0 +1,12 @@
+Term
+====
+
+.. doxygenstruct:: cvc5::api::TermHashFunction
+    :project: cvc5
+    :members:
+    :undoc-members:
+
+.. doxygenclass:: cvc5::api::Term
+    :project: cvc5
+    :members:
+    :undoc-members:
diff --git a/docs/index.rst b/docs/index.rst
index 645561f2b..b6eb7edac 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -6,18 +6,13 @@
 cvc5 API Documentation
 ======================
 
-.. toctree::
-   :maxdepth: 2
-   :caption: Contents:
-
-
----------------
 
 * :ref:`genindex`
-* :ref:`search`
 
 
-C++ API Documentation
----------------------
+---------------
+
+.. toctree::
+   :maxdepth: 2
 
-.. doxygenfile:: cvc5.h
+   cpp