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

diff --git a/docs/conf.py b/docs/conf.py
index 8489f39d7940bdbe4a565b86f7dfa3861361a335..5713d3fa305548a90b855a6c8e8a42a2f659fffc 100644 (file)
--- 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 (file)
index 0000000..b9bc5f0
--- /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 (file)
index 0000000..7c5325e
--- /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 (file)
index 0000000..90b48e8
--- /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 (file)
index 0000000..7cb5b6a
--- /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 (file)
index 0000000..d3927b8
--- /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 (file)
index 0000000..22ac01a
--- /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 (file)
index 0000000..dc7291f
--- /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 (file)
index 0000000..2342190
--- /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 (file)
index 0000000..cee7a19
--- /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 (file)
index 0000000..9ba1aaa
--- /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 (file)
index 0000000..83e2e00
--- /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 (file)
index 0000000..17529f0
--- /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 (file)
index 0000000..64b631d
--- /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 (file)
index 0000000..c17d749
--- /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 645561f2bb4ce6388dada690d306d1f3a738d4e7..b6eb7edac97f25dcc82e55523db5a266001223d7 100644 (file)
--- 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

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index d3e0857ffdf58d23a2fd949a033ca0b7ee1f0ab2..d334da1092d6aeb05dc7ae55e7ba17e7920abeaa 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -30,9 +30,11 @@
 
 namespace cvc5 {
 
+#ifndef DOXYGEN_SKIP
 template <bool ref_count>
 class NodeTemplate;
 typedef NodeTemplate<true> Node;
+#endif
 
 class Command;
 class DType;
@@ -1800,7 +1802,7 @@ class CVC4_EXPORT DatatypeConstructor
   std::shared_ptr<cvc5::DTypeConstructor> d_ctor;
 };
 
-/*
+/**
  * A CVC4 datatype.
  */
 class CVC4_EXPORT Datatype
@@ -2259,7 +2261,7 @@ struct CVC4_EXPORT RoundingModeHashFunction
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
-/*
+/**
  * A CVC4 solver.
  */
 class CVC4_EXPORT Solver