diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-20 16:29:17 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-20 16:29:17 +0200 |
commit | 777b1a5f2bbfec6040e292cc182f5ec5f48d03e5 (patch) | |
tree | bc08bfed3cd7f642fc40efefd524920ebaac142f /docs | |
parent | f91f8f24d6ed98698373f5d51b17cf583adcd768 (diff) |
Minor improvements to the API (#6585)
This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term
Diffstat (limited to 'docs')
-rw-r--r-- | docs/cpp/term.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/docs/cpp/term.rst b/docs/cpp/term.rst index 022c570b5..1f112a58a 100644 --- a/docs/cpp/term.rst +++ b/docs/cpp/term.rst @@ -1,6 +1,13 @@ Term ==== +The :cpp:class:`Term <cvc5::api::Term>` class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the :cpp:enum:`Kind <cvc5::api::Kind>` enum. +The :cpp:class:`Term <cvc5::api::Term>` class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., :code:`is<Type>Value()` and :code:`get<Type>Value()`, which returns the constant values in the best type standard C++ offers). + +Additionally, a :cpp:class:`Term <cvc5::api::Term>` can be hashed (using :cpp:class:`std::hash\<cvc5::api::Term>`) and given to output streams, including terms within standard containers like :code:`std::map`, :code:`std::set`, or :code:`std::vector`. + +The :cpp:class:`Term <cvc5::api::Term>` only offers the default constructor to create a null term. Instead, the :cpp:class:`Solver <cvc5::api::Solver>` class provides factory functions for all other terms, e.g., :code:`Solver::mkTerm()` for generic terms and :code:`Solver::mk<Type>()` for constant values of a given type. + .. doxygenclass:: cvc5::api::Term :project: cvc5 :members: |