diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /docs | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'docs')
-rw-r--r-- | docs/cpp.rst | 72 | ||||
-rw-r--r-- | docs/cpp/Doxyfile.in | 2 | ||||
-rw-r--r-- | docs/cpp/exceptions.rst | 2 |
3 files changed, 74 insertions, 2 deletions
diff --git a/docs/cpp.rst b/docs/cpp.rst new file mode 100644 index 000000000..eeeae257e --- /dev/null +++ b/docs/cpp.rst @@ -0,0 +1,72 @@ +C++ API Documentation +===================== + +Class Hierarchy +--------------- + +* namespace ``cvc5`` + + * namespace ``api`` + + * class :cpp:class:`cvc5::api::CVC5ApiException` + + * class :cpp:class:`cvc5::api::CVC5ApiRecoverableException` + + * 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>` + + + +Full API Documentation +---------------------- + +.. toctree:: + :maxdepth: 2 + + cpp/datatype + cpp/datatypeconstructor + cpp/datatypeconstructordecl + cpp/datatypedecl + cpp/datatypeselector + cpp/exceptions + cpp/grammar + cpp/kind + cpp/op + cpp/result + cpp/roundingmode + cpp/solver + cpp/sort + cpp/term diff --git a/docs/cpp/Doxyfile.in b/docs/cpp/Doxyfile.in index 400b3dd0d..75a732ceb 100644 --- a/docs/cpp/Doxyfile.in +++ b/docs/cpp/Doxyfile.in @@ -2216,7 +2216,7 @@ INCLUDE_FILE_PATTERNS = # recursively expanded use the := operator instead of the = operator. # This tag requires that the tag ENABLE_PREPROCESSING is set to YES. -PREDEFINED = DOXYGEN_SKIP CVC4_EXPORT= +PREDEFINED = DOXYGEN_SKIP CVC5_EXPORT= # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this # tag can be used to specify a list of macro names that should be expanded. The diff --git a/docs/cpp/exceptions.rst b/docs/cpp/exceptions.rst index 414f27a78..5fa65e5e5 100644 --- a/docs/cpp/exceptions.rst +++ b/docs/cpp/exceptions.rst @@ -1,7 +1,7 @@ Exceptions ========== -The CVC5 API communicates certain errors using exceptions. We broadly +The cvc5 API communicates certain errors using exceptions. We broadly distinguish two types of exceptions: :cpp:class:`CVC5ApiException <cvc5::api::CVC5ApiException>` and :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>` (which is derived from |