From: Aina Niemetz Date: Fri, 9 Apr 2021 22:28:18 +0000 (-0700) Subject: New C++ Api: Initial layout of Api documentation. (#6325) X-Git-Tag: cvc5-1.0.0~1930 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca7e206c239d8de0f25fb23544e4923641b85d11;p=cvc5.git New C++ Api: Initial layout of Api documentation. (#6325) --- 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` + + * class :ref:`CVC4ApiRecoverableException` + + * class :doc:`cpp/datatype` + + * class :ref:`Datatype::const_iterator` + + * class :doc:`cpp/datatypeconstructor` + + * class :ref:`DatatypeConstructor::const_iterator` + + * 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` + + * enum :doc:`cpp/kind` + + * enum :doc:`cpp/roundingmode` + + * struct :ref:`KindHashFunction` + + * struct :ref:`OpHashFunction` + + * struct :ref:`SortHashFunction` + + * struct :ref:`TermHashFunction` + + +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 diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index d3e0857ff..d334da109 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -30,9 +30,11 @@ namespace cvc5 { +#ifndef DOXYGEN_SKIP template class NodeTemplate; typedef NodeTemplate Node; +#endif class Command; class DType; @@ -1800,7 +1802,7 @@ class CVC4_EXPORT DatatypeConstructor std::shared_ptr 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