Merge branch 'main' into python-api-mkbitvector

docs/api/cpp/Doxyfile.in

@@ -2186,7 +2186,7 @@ MACRO_EXPANSION        = YES
 # The default value is: NO.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-EXPAND_ONLY_PREDEF     = YES
+EXPAND_ONLY_PREDEF     = NO
 
 # If the SEARCH_INCLUDES tag is set to YES, the include files in the
 # INCLUDE_PATH will be searched if a #include is found.

docs/api/cpp/cpp.rst

@@ -27,6 +27,7 @@ For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
     roundingmode
     solver
     sort
+    sortkind
     statistics
     synthresult
     term
@@ -65,9 +66,18 @@ Class hierarchy
 
     * class :cpp:class:`const_iterator <cvc5::Term::const_iterator>`
 
-  * enum :ref:`api/cpp/kind:kind`
-  * enum :ref:`api/cpp/roundingmode:roundingmode`
-  * enum :ref:`api/cpp/unknownexplanation:unknownexplanation`
-  * modes enums :ref:`api/cpp/modes:modes`
+  * enum class :ref:`api/cpp/kind:kind`
+  * enum class :ref:`api/cpp/sortkind:sortkind`
+  * enum class :ref:`api/cpp/roundingmode:roundingmode`
+  * enum class :ref:`api/cpp/unknownexplanation:unknownexplanation`
+
+``namespace modes {``
+  * enum classes for :ref:`configuration modes<api/cpp/modes:modes>`
+
+    * enum class for :cpp:enum:`cvc5::modes::BlockModelsMode`
+    * enum class for :cpp:enum:`cvc5::modes::LearnedLitType`
+    * enum class for :cpp:enum:`cvc5::modes::ProofComponent`
+    * enum class for :cpp:enum:`cvc5::modes::FindSynthTarget`
+``}``
 
 ``}``

docs/api/cpp/datatype.rst

@@ -1,7 +1,23 @@
 Datatype
 ========
 
+This class represents a datatype. A :cpp:class:`cvc5::Datatype` is encapsulated
+by a datatype :cpp:class:`Sort <cvc5::Sort>` and can be retrieved from a
+datatype sort via :cpp:func:`cvc5::Sort::getDatatype()`.
+
+----
+
+- class :cpp:class:`cvc5::Datatype`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const Datatype& dt)`
+
+----
+
 .. doxygenclass:: cvc5::Datatype
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Datatype& dt)
+    :project: cvc5

docs/api/cpp/datatypeconstructor.rst

@@ -1,7 +1,24 @@
 DatatypeConstructor
 ===================
 
+This class represents a datatype constructor. Datatype constructors are
+specified via :cpp:class:`cvc5::DatatypeConstructorDecl` when constructing a
+datatype sort and can be retrieved from a :cpp:class:`cvc5::Datatype` via
+:cpp:func:`cvc5::Datatype::getConstructor()`.
+
+----
+
+- class :cpp:class:`cvc5::DatatypeConstructor`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeConstructor& cons)`
+
+----
+
 .. doxygenclass:: cvc5::DatatypeConstructor
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const DatatypeConstructor& cons)
+    :project: cvc5

docs/api/cpp/datatypeconstructordecl.rst

@@ -1,7 +1,31 @@
 DatatypeConstructorDecl
 =======================
 
+This class encapsulates a datatype constructor declaration. A datatype
+constructor declaration is constructed via
+:cpp:func:`cvc5::Solver::mkDatatypeConstructorDecl()`. This is not a
+datatype itself (see :doc:`datatype`), but the representation of the
+specification for creating a datatype constructor of a datatype
+:cpp:class:`Sort <cvc5::Sort>` (see :cpp:func:`cvc5::Solver::mkDatatypeSort()`
+and :cpp:func:`cvc5::Solver::mkDatatypeSorts()`).
+
+----
+
+- class :cpp:class:`cvc5::DatatypeConstructorDecl`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeConstructorDecl& decl)`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector)`
+
+----
+
 .. doxygenclass:: cvc5::DatatypeConstructorDecl
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const DatatypeConstructorDecl& decl)
+    :project: cvc5
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector)
+    :project: cvc5

docs/api/cpp/datatypedecl.rst

@@ -1,7 +1,27 @@
 DatatypeDecl
 ============
 
+This class encapsulates a datatype declaration. A datatype declaration is
+constructed via :cpp:func:`cvc5::Solver::mkDatatypeDecl()`. This is not a
+datatype itself (see :doc:`datatype`), but the representation of the
+specification for creating a datatype :cpp:class:`Sort <cvc5::Sort>` (see
+:cpp:func:`cvc5::Solver::mkDatatypeSort()` and
+:cpp:func:`cvc5::Solver::mkDatatypeSorts()`).
+
+
+----
+
+- class :cpp:class:`cvc5::DatatypeDecl`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeDecl& decl)`
+
+----
+
 .. doxygenclass:: cvc5::DatatypeDecl
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const DatatypeDecl& decl)
+    :project: cvc5

docs/api/cpp/datatypeselector.rst

@@ -1,7 +1,25 @@
 DatatypeSelector
 ================
 
+This class represents a datatype selector. Datatype selectors are
+specified via :cpp:func:`cvc5::DatatypeConstructorDecl::addSelector()` when
+constructing a datatype sort and can be retrieved from a
+:cpp:class:`cvc5::DatatypeConstructor` via
+:cpp:func:`cvc5::DatatypeConstructor::getSelector()`.
+
+----
+
+- class :cpp:class:`cvc5::DatatypeSelector`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeSelector& sel)`
+
+----
+
 .. doxygenclass:: cvc5::DatatypeSelector
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const DatatypeSelector& sel)
+    :project: cvc5

docs/api/cpp/grammar.rst

@@ -1,7 +1,24 @@
 Grammar
 =======
 
+This class encapsulates a SyGuS grammar. It is created via
+:cpp:func:`cvc5::Solver::mkGrammar()` and allows to define a context-free
+grammar of terms, according to the definition of grammars in the SyGuS IF 2.1
+standard.
+
+----
+
+- class :cpp:class:`cvc5::Grammar`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const Grammar& g)`
+
+----
+
 .. doxygenclass:: cvc5::Grammar
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Grammar& g)
+    :project: cvc5

docs/api/cpp/kind.rst

@@ -1,7 +1,8 @@
 Kind
 ====
 
-Every :cpp:class:`Term <cvc5::Term>` has an associated kind.
+Every :cpp:class:`Term <cvc5::Term>` has an associated kind, represented
+as enum class :cpp:enum:`cvc5::Kind`.
 This kind distinguishes if the Term is a value, constant, variable or operator,
 and what kind of each.
 For example, a bit-vector value has kind
@@ -12,9 +13,24 @@ an equality over terms of any sort has kind
 :cpp:enumerator:`EQUAL <cvc5::Kind::EQUAL>`, and a universally
 quantified formula has kind :cpp:enumerator:`FORALL <cvc5::Kind::FORALL>`.
 
+----
+
+- enum class :cpp:enum:`cvc5::Kind`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, Kind kind)`
+- :cpp:struct:`std::hash\<cvc5::Kind>`
+
+----
+
 .. doxygenenum:: cvc5::Kind
     :project: cvc5
 
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, Kind kind)
+    :project: cvc5
+
+----
+
 .. doxygenstruct:: std::hash< cvc5::Kind >
     :project: std
     :members:

docs/api/cpp/modes.rst

@@ -1,5 +1,52 @@
 Modes
 ======
 
-.. doxygennamespace:: cvc5::modes
+Some API functions require a configuration mode argument, e.g.,
+:cpp:func:`cvc5::Solver::blockModel()`.
+The following enum classes define such configuration modes.
+
+----
+
+- enum class :cpp:enum:`cvc5::modes::BlockModelsMode`
+- :cpp:func:`std::ostream& cvc5::modes::operator<< (std::ostream& out, BlockModelsMode mode)`
+
+- enum class :cpp:enum:`cvc5::modes::LearnedLitType`
+- :cpp:func:`std::ostream& cvc5::modes::operator<< (std::ostream& out, LearnedLitType type)`
+
+- enum class :cpp:enum:`cvc5::modes::ProofComponent`
+- :cpp:func:`std::ostream& cvc5::modes::operator<< (std::ostream& out, ProofComponent pc)`
+
+- enum class :cpp:enum:`cvc5::modes::FindSynthTarget`
+- :cpp:func:`std::ostream& cvc5::modes::operator<< (std::ostream& out, FindSynthTarget target)`
+
+----
+
+.. doxygenenum:: cvc5::modes::BlockModelsMode
+    :project: cvc5
+
+.. doxygenfunction:: cvc5::modes::operator<<(std::ostream& out, BlockModelsMode mode)
+    :project: cvc5
+
+----
+
+.. doxygenenum:: cvc5::modes::LearnedLitType
+    :project: cvc5
+
+.. doxygenfunction:: cvc5::modes::operator<<(std::ostream& out, LearnedLitType type)
+    :project: cvc5
+
+----
+
+.. doxygenenum:: cvc5::modes::ProofComponent
+    :project: cvc5
+
+.. doxygenfunction:: cvc5::modes::operator<<(std::ostream& out, ProofComponent pc)
+    :project: cvc5
+
+----
+
+.. doxygenenum:: cvc5::modes::FindSynthTarget
+    :project: cvc5
+
+.. doxygenfunction:: cvc5::modes::operator<<(std::ostream& out, FindSynthTarget target)
     :project: cvc5

docs/api/cpp/op.rst

@@ -1,10 +1,42 @@
 Op
 ==
 
+This class encapsulates a cvc5 operator. A :cpp:class:`cvc5::Op` is a term that
+represents an operator, instantiated with the parameters it requires (if any).
+
+A :cpp:class:`cvc5::Term` of operator kind that does not require additional
+parameters, e.g., :cpp:enumerator:`cvc5::Kind::ADD`, is usually constructed via
+:cpp:func:`cvc5::Solver::mkTerm(Kind kind, const std::vector\<Term>& children) <Term cvc5::Solver::mkTerm(Kind kind, const std::vector\<Term>& children) const>`.
+Alternatively, any :cpp:class:`cvc5::Term` can be constructed via first
+instantiating a corresponding :cpp:class:`cvc5::Op`, even if the operator does
+not require additional parameters.
+Terms with operators that require additional parameters, e.g.,
+:cpp:enumerator:`cvc5::Kind::BITVECTOR_EXTRACT`, must be created via
+:cpp:func:`cvc5::Solver::mkOp(Kind kind, const std::vector\<uint32_t> args) <cvc5::Solver::mkOp()>` and
+:cpp:func:`cvc5::Solver::mkTerm(const Op& op, const std::vector\<Term>& children) <Term cvc5::Solver::mkTerm(const Op& op, const std::vector\<Term>& children) const>`.
+
+
+
+
+----
+
+- class :cpp:class:`cvc5::Op`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const Op& op)`
+- :cpp:struct:`std::hash\<cvc5::Op>`
+
+----
+
 .. doxygenclass:: cvc5::Op
     :project: cvc5
     :members:
 
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Op& op)
+    :project: cvc5
+
+----
+
 .. doxygenstruct:: std::hash< cvc5::Op >
     :project: std
     :members:

docs/api/cpp/optioninfo.rst

@@ -1,6 +1,22 @@
 OptionInfo
 ==========
 
+This class encapsulates all the information associated with a configuration
+option. It can be retrieved via :cpp:func:`cvc5::Solver::getOptionInfo()`
+and allows to query any configuration information associated with an option.
+
+----
+
+- class :cpp:class:`cvc5::OptionInfo`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const OptionInfo& info)`
+
+----
+
 .. doxygenstruct:: cvc5::OptionInfo
     :project: cvc5
     :members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const OptionInfo& info)
+    :project: cvc5

docs/api/cpp/result.rst

@@ -1,7 +1,27 @@
 Result
 ======
 
+This class represents a :cpp:class:`cvc5::Solver` result.
+
+A :cpp:class:`cvc5::Result` encapsulates a 3-valued solver result (sat, unsat,
+unknown). Explanations for unknown results are represented as enum class
+:cpp:enum:`cvc5::UnknownExplanation` and can be queried via
+:cpp:func:`cvc5::Result::getUnknownExplanation()`.
+
+----
+
+- class :cpp:class:`cvc5::Result`
+- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const Result& r)`
+
+----
+
 .. doxygenclass:: cvc5::Result
     :project: cvc5
     :members:
     :undoc-members:
+
+----
+
+.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Result& r)
+    :project: cvc5
+

docs/api/cpp/roundingmode.rst

@@ -1,5 +1,15 @@
 RoundingMode
 ============
 
+This enum class represents a floating-point rounding mode.
+
+----
+
+- enum class :cpp:enum:`cvc5::RoundingMode`
+
+----
+
 .. doxygenenum:: cvc5::RoundingMode
     :project: cvc5
+
+