api: Refactor kinds documentation. (#8384)

diff --git a/docs/api/cpp/kind.rst b/docs/api/cpp/kind.rst
index 4c07804a48cfd2767ecdcf58d54fa822aebc07ba..996691524cd93627e7206c2da2c90767e85c1bae 100644 (file)
--- a/docs/api/cpp/kind.rst
+++ b/docs/api/cpp/kind.rst
@@ -1,11 +1,16 @@
 Kind
 ====
 
-Every :cpp:class:`Term <cvc5::api::Term>` has a kind which represents its type,
-for example whether it is an equality (:cpp:enumerator:`EQUAL
-<cvc5::api::Kind::EQUAL>`), a conjunction (:cpp:enumerator:`AND
-<cvc5::api::Kind::AND>`), or a bit-vector addition
-(:cpp:enumerator:`BITVECTOR_ADD <cvc5::api::Kind::BITVECTOR_ADD>`).
+Every :cpp:class:`Term <cvc5::api::Term>` has an associated 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
+:cpp:enumerator:`CONST_BITVECTOR <cvc5::api::Kind::CONST_BITVECTOR>`,
+a free constant symbol has kind
+:cpp:enumerator:`CONSTANT <cvc5::api::Kind::CONSTANT>`,
+an equality over terms of any sort has kind
+:cpp:enumerator:`EQUAL <cvc5::api::Kind::EQUAL>`, and a universally
+quantified formula has kind :cpp:enumerator:`FORALL <cvc5::api::Kind::FORALL>`.
 
 .. doxygenenum:: cvc5::api::Kind
     :project: cvc5

diff --git a/docs/api/cpp/sort.rst b/docs/api/cpp/sort.rst
index b19b82942a9267d467baeb2bddc93a9e47f7fd1c..7cbf46271e66cc3d3d98a16b1bf50d54d5a7a6b0 100644 (file)
--- a/docs/api/cpp/sort.rst
+++ b/docs/api/cpp/sort.rst
@@ -1,12 +1,51 @@
 Sort
 ====
 
+The :cpp:class:`Sort <cvc5::api::Sort>` class represents the sort of a
+:cpp:class:`Term <cvc5::api::Term>`.
+
+A :cpp:class:`Sort <cvc5::api::Sort>` can be hashed (using
+:cpp:class:`std::hash\<cvc5::api::Sort>`) and serialized to an output stream
+(using :cpp:func:`cvc5::api::operator<<()`).
+
+Class :cpp:class:`Sort <cvc5::api::Sort>` offers the default constructor
+only to create a null Sort. Instead, the :cpp:class:`Solver <cvc5::api::Solver>`
+class provides factory functions for all other sorts, e.g.,
+:cpp:func:`cvc5::api::Solver::getBooleanSort()` for Sort Bool and
+:cpp:func:`cvc5::api::Solver::mkBitVectorSort()` for bit-vector
+sorts.
+
+Sorts are defined as standardized in the SMT-LIB standard for standardized
+theories. Additionally, we introduce the following sorts for non-standardized
+theories:
+
+- *Bag* (Multiset)
+
+  - Created with :cpp:func:`cvc5::api::Solver::mkBagSort()`
+
+- *Set* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
+
+  - Created with :cpp:func:`cvc5::api::Solver::mkSetSort()`
+
+- *Relation* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
+
+  - Created with :cpp:func:`cvc5::api::Solver::mkSetSort()` as a set of tuple
+    sorts
+
+- *Table*
+
+  - Created with :cpp:func:`cvc5::api::Solver::mkBagSort()` as a bag of tuple
+    sorts
+
 .. doxygenclass:: cvc5::api::Sort
     :project: cvc5
     :members:
     :undoc-members:
 
+.. doxygenfunction:: cvc5::api::operator<<(std::ostream& out, const Sort& s)
+
 .. doxygenstruct:: std::hash< cvc5::api::Sort >
     :project: std
     :members:
     :undoc-members:
+

diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index 132b029f97ca6a4dfe60f5da73acb7415820407a..cc0792aab1391a5b068e8f6de328da4170a01f33 100644 (file)
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -19,10 +19,10 @@ class SmtLibLexer(RegexLexer):
         'assert', 'block-model', 'block-model-values', 'check-sat',
         'check-sat-assuming', 'declare-const', 'declare-datatype',
         'declare-datatypes', 'declare-codatatypes', 'declare-fun',
-        'declare-sort', 'define-fun', 'define-fun-rec', 'define-funs-rec',
-        'define-sort', 'echo', 'exit', 'get-abduct', 'get-assertions',
-        'get-assignment', 'get-info', 'get-interpol', 'get-model',
-        'get-option', 'get-proof', 'get-qe', 'get-qe-disjunct',
+        'declare-sort', 'define-const', 'define-fun', 'define-fun-rec',
+        'define-funs-rec', 'define-sort', 'echo', 'exit', 'get-abduct',
+        'get-assertions', 'get-assignment', 'get-info', 'get-interpol',
+        'get-model', 'get-option', 'get-proof', 'get-qe', 'get-qe-disjunct',
         'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push',
         'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option',
         # SyGuS v2
@@ -30,8 +30,9 @@ class SmtLibLexer(RegexLexer):
         'synth-fun', 'synth-inv', 'declare-pool',
     ]
     SORTS = [
-        'Array', 'BitVec', 'Bool', 'FloatingPoint', 'Float[0-9]+', 'Int',
-        'Real', 'RegLan', 'RoundingMode', 'Set', 'String', 'Tuple',
+        'Array', 'BitVec', 'Bag', 'Bool', 'FloatingPoint', 'Float[0-9]+',
+        'Int', 'Real', 'RegLan', 'RoundingMode', 'Set', 'Seq', 'String',
+        'Tuple',
     ]
     OPERATORS = [
         # array
@@ -47,7 +48,7 @@ class SmtLibLexer(RegexLexer):
         '=>', '=', 'true', 'false', 'not', 'and', 'or', 'xor', 'distinct',
         'ite',
         # datatypes
-        'tuple', 'tuple_select',
+        'tuple', 'tuple_project', 'tuple_select',
         # fp
         'RNE', 'RNA', 'RTP', 'RTN', 'RTZ', 'fp', 'NaN', 'fp\.abs', 'fp\.neg',
         'fp\.add', 'fp\.sub', 'fp\.mul', 'fp\.div', 'fp\.fma', 'fp\.sqrt',
@@ -59,7 +60,7 @@ class SmtLibLexer(RegexLexer):
         '-zero',
         # int / real
         '<', '>', '<=', '>=', '!=', '\+', '-', '\*', '/', 'div', 'mod', 'abs',
-        'divisible', 'to_real', 'to_int', 'is_int',
+        'divisible', 'to_real', 'to_int', 'is_int', 'iand', 'int2bv',
         # separation logic
         'emp', 'pto', 'sep', 'wand', 'nil',
         # sets / relations
@@ -75,6 +76,13 @@ class SmtLibLexer(RegexLexer):
         'str\.replace_re_all', 're\.comp', 're\.diff', 're\.\+', 're\.opt',
         're\.range', 're\.^', 're\.loop', 'str\.is_digit', 'str\.to_code',
         'str\.from_code', 'str\.to_int', 'str\.from_int',
+        # sequences
+        'seq\.\+\+', 'seq\.len', 'seq\.extract', 'seq\.update', 'seq\.at',
+        'seq\.contains', 'seq\.indexof', 'seq\.replace', 'seq\.prefixof',
+        'seq\.suffixof', 'seq\.rev', 'seq\.replace_all', 'seq\.unit',
+        'seq\.nth', 'seq\.empty',
+        # others
+        'witness',
     ]
 
     tokens = {

diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 212ffa3d0dee48e593b5b59d1d5a0472e47930a6..4a6501653908bc0059d39c02a2c45611342326aa 100644 (file)
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -1,3 +1,5 @@
+.. _theory_reference_sets:
+
 Theory Reference: Sets and Relations
 ====================================
 

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 6d9b39df1219c4828117121ed9e66039df03a279..a7ed927df3925e9603c498bb4c1da76c7ccbcb2a 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2037,10 +2037,10 @@ class CVC5_EXPORT DatatypeConstructor
    *
    * This method is equivalent of applying the above, where this
    * DatatypeConstructor is the one corresponding to nil, and retSort is
-   * ``(List Int)``.
+   * `(List Int)`.
    *
-   * @note the returned constructor term ``t`` is an operator, while
-   *       ``Solver::mkTerm(APPLY_CONSTRUCTOR, t)`` is used to construct the
+   * @note the returned constructor term `t` is an operator, while
+   *       `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the
    *       above (nullary) application of nil.
    *
    * @param retSort the desired return sort of the constructor
@@ -2279,6 +2279,8 @@ class CVC5_EXPORT Datatype
    * This is a linear search through the constructors, so in case of multiple,
    * similarly-named constructors, the
    * first is returned.
+   * @param name the name of the datatype constructor
+   * @return a Term representing the datatype constructor with the given name
    */
   Term getConstructorTerm(const std::string& name) const;
 
@@ -4791,23 +4793,26 @@ class CVC5_EXPORT Solver
   std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
 
   /**
-   * Returns a snapshot of the current state of the statistic values of this
+   * Get a snapshot of the current state of the statistic values of this
    * solver. The returned object is completely decoupled from the solver and
    * will not change when the solver is used again.
+   * @return A snapshot of the current state of the statistic values
    */
   Statistics getStatistics() const;
 
   /**
-   * Whether the output stream for the given tag is enabled. Tags can be enabled
-   * with the `output` option (and `-o <tag>` on the command line). Raises an
-   * exception when an invalid tag is given.
+   * Determione the output stream for the given tag is enabled. Tags can be
+   * enabled with the `output` option (and `-o <tag>` on the command line).
+   * Raises an exception when an invalid tag is given.
+   * @return True if the given tag is enabled
    */
   bool isOutputOn(const std::string& tag) const;
 
   /**
-   * Returns an output stream for the given tag. Tags can be enabled with the
+   * Get an output stream for the given tag. Tags can be enabled with the
    * `output` option (and `-o <tag>` on the command line). Raises an exception
    * when an invalid tag is given.
+   * @return The output stream
    */
   std::ostream& getOutput(const std::string& tag) const;
 

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index ff170e567f4549cd036c955b9daf8f36c9c0b2e1..88da1fb760b0caa90c9e51c5f5cbd39b68eae0dd 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -27,11 +27,9 @@ namespace api {
 /* Kind                                                                       */
 /* -------------------------------------------------------------------------- */
 
-// TODO(Gereon): Fix links that involve std::vector. See
-// https://github.com/doxygen/doxygen/issues/8503
 // clang-format off
 /**
- * The kind of a cvc5 term.
+ * The kind of a cvc5 Term.
  *
  * \internal
  *
@@ -47,17 +45,23 @@ enum Kind : int32_t
 {
   /**
    * Internal kind.
-   * Should never be exposed or created via the API.
+   *
+   * @note Should never be created via the API.
    */
   INTERNAL_KIND = -2,
   /**
    * Undefined kind.
-   * Should never be exposed or created via the API.
+   *
+   * @note Should never be exposed or created via the API.
    */
   UNDEFINED_KIND = -1,
   /**
-   * Null kind (kind of null term `Term::Term()`).
-   * Do not explicitly create via API functions other than `Term::Term()`.
+   * Null kind.
+   *
+   * The kind of a null term (Term::Term()).
+   *
+   * @note May not be explicitly created via API functions other than
+   *       Term::Term().
    */
   NULL_EXPR,
 
@@ -67,8 +71,8 @@ enum Kind : int32_t
    * The value of an uninterpreted constant.
    *
    * @note May be returned as the result of an API call, but terms of this kind
-   *       may not be created explicitly via the API. Terms of this kind may
-   *       further not appear in assertions.
+   *       may not be created explicitly via the API and may not appear in
+   *       assertions.
    */
   UNINTERPRETED_SORT_VALUE,
 #if 0
@@ -78,50 +82,48 @@ enum Kind : int32_t
   /**
    * Equality, chainable.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms with same sorts
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of the same Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   EQUAL,
   /**
    * Disequality.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms with same sorts
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of the same Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   DISTINCT,
   /**
-   * First-order constant.
+   * Free constant symbol.
    *
-   * Not permitted in bindings (forall, exists, ...).
+   * @note Not permitted in bindings (e.g., #FORALL, #EXISTS).
    *
-   * Parameters:
-   *   - See @ref cvc5::api::Solver::mkConst() "mkConst()".
-   *
-   * Create with:
-   *   - `Solver::mkConst(const Sort& sort, const std::string& symbol) const`
-   *   - `Solver::mkConst(const Sort& sort) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkConst(const Sort&, const std::string&) const
+   *   - Solver::mkConst(const Sort&) const
    */
   CONSTANT,
   /**
    * (Bound) variable.
    *
-   * Permitted in bindings and in the lambda and quantifier bodies only.
-   *
-   * Parameters:
-   *   - See @ref cvc5::api::Solver::mkVar() "mkVar()".
+   * @note Only permitted in bindings and in lambda and quantifier bodies.
    *
-   * Create with:
-   *   - `Solver::mkVar(const Sort& sort, const std::string& symbol) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkVar(const Sort&, const std::string&) const
    */
   VARIABLE,
 #if 0
@@ -131,68 +133,89 @@ enum Kind : int32_t
   /**
    * Symbolic expression.
    *
-   * Parameters: n > 0
-   *   - 1..n: terms
+   * - Arity: `n > 0`
+   *   - `1..n:` Terms with same sorts
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SEXPR,
   /**
    * Lambda expression.
    *
-   * Parameters:
-   *   - 1: VARIABLE_LIST
-   *   - 2: Lambda body
+   * - Arity: `2`
+   *   - `1:` Term of kind #VARIABLE_LIST
+   *   - `2:` Term of any Sort (the body of the lambda)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   LAMBDA,
   /**
+   * Witness.
+   *
    * The syntax of a witness term is similar to a quantified formula except that
    * only one variable is allowed.
-   * The term `(witness ((x T)) F)` returns an element `x` of type `T`
-   * and asserts `F`.
+   * For example, the term
+   * \rst
+   * .. code:: smtlib
+   *
+   *     (witness ((x S)) F)
+   * \endrst
+   * returns an element @f$x@f$ of Sort @f$S@f$ and asserts formula @f$F@f$.
    *
    * The witness operator behaves like the description operator
-   * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x
-   * that satisfies F. But if such x exists, the witness operator does not
-   * enforce the axiom that ensures uniqueness up to logical equivalence:
+   * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is
+   * no @f$x@f$ that satisfies @f$F@f$. But if such @f$x@f$ exists, the witness
+   * operator does not enforce the following axiom which ensures uniqueness up
+   * to logical equivalence:
    *
    * @f[
    *   \forall x. F \equiv G \Rightarrow witness~x. F =  witness~x. G
    * @f]
    *
-   * For example if there are 2 elements of type T that satisfy F, then the
-   * following formula is satisfiable:
+   * For example, if there are two elements of Sort @f$S@f$ that satisfy
+   * formula @f$F@f$, then the following formula is satisfiable:
+   *
+   * \rst
+   * .. code:: smtlib
    *
    *     (distinct
    *        (witness ((x Int)) F)
    *        (witness ((x Int)) F))
+   * \endrst
    *
-   * This kind is primarily used internally, but may be returned in models
-   * (e.g. for arithmetic terms in non-linear queries). However, it is not
-   * supported by the parser. Moreover, the user of the API should be cautious
-   * when using this operator. In general, all witness terms
-   * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a
-   * valid formula. If this is not the case, then the semantics in formulas that
-   * use witness terms may be unintuitive. For example, the following formula is
-   * unsatisfiable:
-   * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))`
-   * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
-   *
-   * Parameters:
-   *   - 1: VARIABLE_LIST
-   *   - 2: Witness body
-   *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * @note This kind is primarily used internally, but may be returned in
+   *       models (e.g., for arithmetic terms in non-linear queries). However,
+   *       it is not supported by the parser. Moreover, the user of the API
+   *       should be cautious when using this operator. In general, all witness
+   *       terms `(witness ((x Int)) F)` should be such that `(exists ((x Int))
+   *       F)` is a valid formula. If this is not the case, then the semantics
+   *       in formulas that use witness terms may be unintuitive. For example,
+   *       the following formula is unsatisfiable:
+   *       `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int))
+   *       false) 0))`, whereas notice that `(or (= z 0) (not (= z 0)))` is
+   *       true for any @f$z@f$.
+   *
+   * - Arity: `3`
+   *   - `1:` Term of kind #VARIABLE_LIST
+   *   - `2:` Term of Sort Bool (the body of the witness)
+   *   - `3:` (optional) Term of kind #INST_PATTERN_LIST
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   WITNESS,
 
@@ -201,86 +224,96 @@ enum Kind : int32_t
   /**
    * Boolean constant.
    *
-   * Parameters:
-   *   - 1: Boolean value of the constant
-   *
-   * Create with:
+   * - Create Term of this Kind with:
    *   - `Solver::mkTrue() const`
    *   - `Solver::mkFalse() const`
-   *   - `Solver::mkBoolean(bool val) const`
+   *   - `Solver::mkBoolean(bool) const`
    */
   CONST_BOOLEAN,
   /**
    * Logical negation.
    *
-   * Parameters:
-   *   - 1: Boolean Term to negate
+   * - Arity: `1`
+   *   - `1:` Term of Sort Bool
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   NOT,
   /**
    * Logical conjunction.
    *
-   * Parameters: n > 1
-   *   - 1..n: Boolean Term of the conjunction
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Bool
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   AND,
   /**
    * Logical implication.
    *
-   * Parameters: n > 1
-   *   - 1..n: Boolean Terms, right associative
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Bool
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   IMPLIES,
   /**
    * Logical disjunction.
    *
-   * Parameters: n > 1
-   *   - 1..n: Boolean Term of the disjunction
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Bool
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   OR,
   /**
    * Logical exclusive disjunction, left associative.
    *
-   * Parameters: n > 1
-   *   - 1..n: Boolean Terms, `[1] xor ... xor [n]`
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Bool
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   XOR,
   /**
    * If-then-else.
    *
-   * Parameters:
-   *   - 1: is a Boolean condition Term
-   *   - 2: the 'then' Term
-   *   - 3: the 'else' Term
+   * - Arity: `3`
+   *   - `1:` Term of Sort Bool
+   *   - `2:` The 'then' term, Term of any Sort
+   *   - `3:` The 'else' term, Term of the same sort as second argument
    *
-   * 'then' and 'else' term must have same base sort.
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ITE,
 
@@ -289,14 +322,16 @@ enum Kind : int32_t
   /**
    * Application of an uninterpreted function.
    *
-   * Parameters: n > 1
-   *   - 1: Function Term
-   *   - 2..n: Function argument instantiation Terms
+   * - Arity: `n > 1`
+   *   - `1:` Function Term
+   *   - `2..n:` Function argument instantiation Terms of any first-class Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   APPLY_UF,
 #if 0
@@ -304,31 +339,39 @@ enum Kind : int32_t
   BOOLEAN_TERM_VARIABLE,
 #endif
   /**
-   * Cardinality constraint on uninterpreted sort S.
-   * Interpreted as a predicate that is true when the cardinality of S
-   * is less than or equal to the value of the second argument.
+   * Cardinality constraint on uninterpreted sort.
    *
-   * Parameters:
-   *   - 1: Term of sort S
-   *   - 2: Positive integer constant that bounds the cardinality of sort S
+   * Interpreted as a predicate that is true when the cardinality of
+   * uinterpreted Sort @f$S@f$ is less than or equal to the value of
+   * the second argument.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort @f$S@f$
+   *   - `2:` Term of Sort Int (positive integer value that bounds the
+   *          cardinality of @f$S@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   CARDINALITY_CONSTRAINT,
   /**
    * Higher-order applicative encoding of function application, left
    * associative.
    *
-   * Parameters: n > 1
-   *   - 1: Function to apply
-   *   - 2..n: Arguments of the function
+   * - Arity: `n = 2`
+   *   - `1:` Function Term
+   *   - `2:` Argument Term of the domain Sort of the function
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   HO_APPLY,
 
@@ -337,68 +380,78 @@ enum Kind : int32_t
   /**
    * Arithmetic addition.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ADD,
   /**
    * Arithmetic multiplication.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   MULT,
   /**
-   * Operator for bit-wise AND over integers, parameterized by a (positive)
-   * bitwidth k.
+   * Integer and.
    *
-   * ((_ iand k) i1 i2) is equivalent to:
-   * (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
-   * for all integers i1, i2.
+   * Operator for bit-wise `AND` over integers, parameterized by a (positive)
+   * bit-width @f$k@f$.
    *
-   * Parameters:
-   *   - 1: Size of the bit-vector that determines the semantics of the IAND
+   * \rst
+   * .. code:: smtlib
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
+   *     ((_ iand k) i_1 i_2)
+   * \endrst
+   * is equivalent to
+   * \rst
+   * .. code:: smtlib
    *
-   * Apply integer and.
+   *     ((_ iand k) i_1 i_2)
+   *     (bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2)))
+   * \endrst
+   * for all integers `i_1`, `i_2`.
    *
-   * Parameters:
-   *   - 1: Op of kind IAND
-   *   - 2: Integer term
-   *   - 3: Integer term
+   * - Arity: `2`
+   *   - `1..2:` Terms of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Indices: `1`
+   *   - `1:` Bit-width @f$k@f$
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   IAND,
   /**
-   * Operator for raising 2 to a non-negative integer power.
+   * Power of two.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind) const`
+   * Operator for raising `2` to a non-negative integer power.
    *
-   * Parameters:
-   *   - 1: Op of kind IAND
-   *   - 2: Integer term
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Apply 2 to the power operator.
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   POW2,
 #if 0
@@ -408,343 +461,431 @@ enum Kind : int32_t
   /**
    * Arithmetic subtraction, left associative.
    *
-   * Parameters:
-   *   - 1..n: Terms of sort Integer, Real (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SUB,
   /**
    * Arithmetic negation.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int or Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   NEG,
   /**
    * Real division, division by 0 undefined, left associative.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   DIVISION,
   /**
    * Integer division, division by 0 undefined, left associative.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   INTS_DIVISION,
   /**
-   * Integer modulus, division by 0 undefined.
+   * Integer modulus, modulus by `0` undefined.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer
-   *   - 2: Term of sort Integer
+   * - Arity: `2`
+   *   - `1:` Term of Sort Int
+   *   - `2:` Term of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   INTS_MODULUS,
   /**
    * Absolute value.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int or Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ABS,
   /**
    * Arithmetic power.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
-   *   - 2: Term of sort Integer, Real
+   * - Arity: `2`
+   *   - `1..2:` Term of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   POW,
   /**
    * Exponential function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   EXPONENTIAL,
   /**
    * Sine function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SINE,
   /**
    * Cosine function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   COSINE,
   /**
    * Tangent function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   TANGENT,
   /**
    * Cosecant function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   COSECANT,
   /**
    * Secant function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SECANT,
   /**
    * Cotangent function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   COTANGENT,
   /**
    * Arc sine function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCSINE,
   /**
    * Arc cosine function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCCOSINE,
   /**
    * Arc tangent function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCTANGENT,
   /**
    * Arc cosecant function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCCOSECANT,
   /**
    * Arc secant function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCSECANT,
   /**
    * Arc cotangent function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   ARCCOTANGENT,
   /**
    * Square root.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SQRT,
   /**
-   * Operator for the divisibility-by-k predicate.
-   *
-   * Parameter:
-   *   - 1: The k to divide by (sort Integer)
+   * Operator for the divisibility-by-@f$k@f$ predicate.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Apply divisibility-by-k predicate.
+   * - Indices: `1`
+   *   - `1:` The integer @f$k@f$ to divide by.
    *
-   * Parameters:
-   *   - 1: Op of kind DIVISIBLE
-   *   - 2: Integer Term
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   DIVISIBLE,
   /**
    * Multiple-precision rational constant.
    *
-   * Parameters:
-   *   See @ref cvc5::api::Solver::mkInteger() "mkInteger()", @ref cvc5::api::Solver::mkReal() "mkReal()".
-   *
-   * Create with:
-   *   - `Solver::mkInteger(const std::string& s) const`
-   *   - `Solver::mkInteger(int64_t val) const`
-   *   - `Solver::mkReal(const std::string& s) const`
-   *   - `Solver::mkReal(int64_t val) const`
-   *   - `Solver::mkReal(int64_t num, int64_t den) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkInteger(const std::string&) const
+   *   - Solver::mkInteger(int64_t) const
+   *   - Solver::mkReal(const std::string&) const
+   *   - Solver::mkReal(int64_t) const
+   *   - Solver::mkReal(int64_t, int64_t) const
    */
   CONST_RATIONAL,
   /**
    * Less than, chainable.
    *
-   * Parameters: n
-   *   - 1..n: Terms of sort Integer, Real; [1] < ... < [n]
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   LT,
   /**
    * Less than or equal, chainable.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real; [1] <= ... <= [n]
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   LEQ,
   /**
    * Greater than, chainable.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real, [1] > ... > [n]
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   GT,
   /**
    * Greater than or equal, chainable.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of sort Integer, Real; [1] >= ... >= [n]
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort Int or Real (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   GEQ,
   /**
    * Is-integer predicate.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int or Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   IS_INTEGER,
   /**
-   * Convert Term to Integer by the floor function.
+   * Convert Term of sort Int or Real to Int via the floor function.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer, Real
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int or Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   TO_INTEGER,
   /**
-   * Convert Term to Real.
+   * Convert Term of Sort Int or Real to Real.
    *
-   * Parameters:
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int or Real
    *
-   *   - 1: Term of sort Integer, Real
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * This is a no-op in cvc5, as Integer is a subtype of Real.
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   TO_REAL,
   /**
    * Pi constant.
    *
-   * Note that PI is considered a special symbol of sort Real, but is not
-   * a real value, i.e., `Term::isRealValue() const` will return false.
+   * @note #PI is considered a special symbol of Sort Real, but is not
+   * a Real value, i.e., Term::isRealValue() will return `false`.
    *
-   * Create with:
-   *   - `Solver::mkPi() const`
-   *   - `Solver::mkTerm(Kind kind) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkPi() const
    */
   PI,
 
@@ -753,411 +894,503 @@ enum Kind : int32_t
   /**
    * Fixed-size bit-vector constant.
    *
-   * Parameters:
-   *   See @ref cvc5::api::Solver::mkBitVector() "mkBitVector()".
-   *
-   * Create with:
-   *   - `Solver::mkBitVector(uint32_t size, uint64_t val) const`
-   *   - `Solver::mkBitVector(const std::string& s, uint32_t base) const`
-   *   - `Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const`
+   * - Create Term of this Kind with:
+   *   - `Solver::mkBitVector(uint32_t, uint64_t) const`
+   *   - `Solver::mkBitVector(uint32_t, const std::string&, uint32_t) const`
    */
   CONST_BITVECTOR,
   /**
    * Concatenation of two or more bit-vectors.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_CONCAT,
   /**
    * Bit-wise and.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_AND,
   /**
    * Bit-wise or.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_OR,
   /**
    * Bit-wise xor.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_XOR,
   /**
    * Bit-wise negation.
    *
-   * Parameters:
-   *   - 1: Term of bit-vector sort
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_NOT,
   /**
    * Bit-wise nand.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_NAND,
   /**
    * Bit-wise nor.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_NOR,
   /**
    * Bit-wise xnor, left associative.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_XNOR,
   /**
-   * Equality comparison (returns bit-vector of size 1).
+   * Equality comparison (returns bit-vector of size `1`).
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_COMP,
   /**
    * Multiplication of two or more bit-vectors.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_MULT,
   /**
    * Addition of two or more bit-vectors.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ADD,
   /**
    * Subtraction of two bit-vectors.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SUB,
   /**
    * Negation of a bit-vector (two's complement).
    *
-   * Parameters:
-   *   - 1: Term of bit-vector sort
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_NEG,
   /**
-   * Unsigned division of two bit-vectors, truncating towards 0. If the divisor
-   * is zero, the result is all ones.
+   * Unsigned bit-vector division.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * Truncates towards `0`. If the divisor is zero, the result is all ones.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_UDIV,
   /**
-   * Unsigned remainder from truncating division of two bit-vectors. If the
-   * modulus is zero, the result is the dividend.
+   * Unsigned bit-vector remainder.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * Remainder from unsigned bit-vector division. If the modulus is zero, the
+   * result is the dividend.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_UREM,
   /**
+   * Signed bit-vector division.
+   *
    * Two's complement signed division of two bit-vectors. If the divisor is
    * zero and the dividend is positive, the result is all ones. If the divisor
    * is zero and the dividend is negative, the result is one.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SDIV,
   /**
-   * Two's complement signed remainder of two bit-vectors (sign follows
-   * dividend). If the modulus is zero, the result is the dividend.
+   * Signed bit-vector remainder (sign follows dividend).
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * Two's complement signed remainder of two bit-vectors where the sign
+   * follows the dividend. If the modulus is zero, the result is the dividend.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SREM,
   /**
-   * Two's complement signed remainder (sign follows divisor). If the modulus
-   * is zero, the result is the dividend.
+   * Signed bit-vector remainder (sign follows divisor).
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * Two's complement signed remainder where the sign follows the divisor. If
+   * the modulus is zero, the result is the dividend.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SMOD,
   /**
    * Bit-vector shift left.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SHL,
   /**
    * Bit-vector logical shift right.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_LSHR,
   /**
    * Bit-vector arithmetic shift right.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ASHR,
   /**
    * Bit-vector unsigned less than.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ULT,
   /**
    * Bit-vector unsigned less than or equal.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ULE,
   /**
    * Bit-vector unsigned greater than.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_UGT,
   /**
    * Bit-vector unsigned greater than or equal.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_UGE,
   /**
    * Bit-vector signed less than.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SLT,
   /**
    * Bit-vector signed less than or equal.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SLE,
   /**
    * Bit-vector signed greater than.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SGT,
   /**
    * Bit-vector signed greater than or equal.
-   * The two bit-vector parameters must have same width.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SGE,
   /**
-   * Bit-vector unsigned less than, returns bit-vector of size 1.
+   * Bit-vector unsigned less than returning a bit-vector of size 1.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ULTBV,
   /**
-   * Bit-vector signed less than. returns bit-vector of size 1.
+   * Bit-vector signed less than returning a bit-vector of size `1`.
    *
-   * Parameters:
-   *   - 1..2: Terms of bit-vector sort (sorts must match)
+   * - Arity: `2`
+   *   - `1..2:` Terms of bit-vector Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_SLTBV,
   /**
-   * Same semantics as regular ITE, but condition is bit-vector of size 1.
+   * Bit-vector if-then-else.
    *
-   * Parameters:
-   *   - 1: Term of bit-vector sort of size 1, representing the condition
-   *   - 2: Term reprsenting the 'then' branch
-   *   - 3: Term representing the 'else' branch
+   * Same semantics as regular ITE, but condition is bit-vector of size `1`.
    *
-   * 'then' and 'else' term must have same base sort.
+   * - Arity: `3`
+   *   - `1:` Term of bit-vector Sort of size `1`
+   *   - `1..3:` Terms of bit-vector sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_ITE,
   /**
    * Bit-vector redor.
    *
-   * Parameters:
-   *   - 1: Term of bit-vector sort
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_REDOR,
   /**
    * Bit-vector redand.
    *
-   * Parameters:
-   *   - 1: Term of bit-vector sort
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_REDAND,
 #if 0
@@ -1172,124 +1405,101 @@ enum Kind : int32_t
   BITVECTOR_ACKERMANIZE_UREM,
 #endif
   /**
-   * Operator for bit-vector extract (from index 'high' to 'low').
+   * Bit-vector extract.
    *
-   * Parameters:
-   *   - 1: The 'high' index
-   *   - 2: The 'low' index
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector extract.
+   * - Indices: `2`
+   *   - `1:` The upper bit index.
+   *   - `2:` The lower bit index.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_EXTRACT
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   BITVECTOR_EXTRACT,
   /**
-   * Operator for bit-vector repeat.
-   *
-   * Parameter:
-   *   - 1: Number of times to repeat a given bit-vector
+   * Bit-vector repeat.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector repeat.
+   * - Indices: `1`
+   *   - `1:` The number of times to repeat the given term.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_REPEAT
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   BITVECTOR_REPEAT,
   /**
-   * Operator for bit-vector zero-extend.
-   *
-   * Parameter:
-   *   - 1: Number of bits by which a given bit-vector is to be extended
+   * Bit-vector zero extension.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector zero-extend.
+   * - Indices: `1`
+   *   - `1:` The number of zeroes to extend the given term with.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_ZERO_EXTEND
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   BITVECTOR_ZERO_EXTEND,
   /**
-   * Operator for bit-vector sign-extend.
-   *
-   * Parameter:
-   *   - 1: Number of bits by which a given bit-vector is to be extended
+   * Bit-vector sign extension.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector sign-extend.
+   * - Indices: `1`
+   *   - `1:` The number of bits (of the value of the sign bit) to extend
+   *          the given term with.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_SIGN_EXTEND
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   BITVECTOR_SIGN_EXTEND,
   /**
-   * Operator for bit-vector rotate left.
-   *
-   * Parameter:
-   *   - 1: Number of bits by which a given bit-vector is to be rotated
+   * Bit-vector rotate left.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector rotate left.
+   * - Indices: `1`
+   *   - `1:` The number of bits to rotate the given term left.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_ROTATE_LEFT
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   BITVECTOR_ROTATE_LEFT,
   /**
-   * Operator for bit-vector rotate right.
-   *
-   * Parameter:
-   *   - 1: Number of bits by which a given bit-vector is to be rotated
+   * Bit-vector rotate right.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Apply bit-vector rotate right.
+   * - Indices: `1`
+   *   - `1:` The number of bits to rotate the given term right.
    *
-   * Parameters:
-   *   - 1: Op of kind BITVECTOR_ROTATE_RIGHT
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   BITVECTOR_ROTATE_RIGHT,
 #if 0
@@ -1297,493 +1507,545 @@ enum Kind : int32_t
   BITVECTOR_BITOF,
 #endif
   /**
-   * Operator for the conversion from Integer to bit-vector.
-   *
-   * Parameter:
-   *   - 1: Size of the bit-vector to convert to
+   * Conversion from Int to bit-vector.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`.
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Apply integer conversion to bit-vector.
+   * - Indices: `1`
+   *   - `1:` The size of the bit-vector to convert to.
    *
-   * Parameters:
-   *   - 1: Op of kind INT_TO_BITVECTOR
-   *   - 2: Integer term
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   INT_TO_BITVECTOR,
   /**
-   * Bit-vector conversion to (nonnegative) integer.
+   * Bit-vector conversion to (non-negative) integer.
    *
-   * Parameter:
-   *   - 1: Term of bit-vector sort
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BITVECTOR_TO_NAT,
 
   /* FP -------------------------------------------------------------------- */
 
   /**
-   * Floating-point constant, constructed from a double or string.
-   *
-   * Parameters:
-   *   - 1: Size of the exponent
-   *   - 2: Size of the significand
-   *   - 3: Value of the floating-point constant as a bit-vector term
+   * Floating-point constant, created from IEEE-754 bit-vector representation
+   * of the floating-point value.
    *
-   * Create with:
-   *   - `Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const`
+   * - Create Term of this Kind with:
+   *   - Term mkFloatingPoint(uint32_t, uint32_t, Term) const;
    */
   CONST_FLOATINGPOINT,
   /**
-   * Floating-point rounding mode term.
+   * RoundingMode constant.
    *
-   * Create with:
+   * - Create Term of this Kind with:
    *   - `Solver::mkRoundingMode(RoundingMode rm) const`
    */
   CONST_ROUNDINGMODE,
   /**
    * Create floating-point literal from bit-vector triple.
    *
-   * Parameters:
-   *   - 1: Sign bit as a bit-vector term
-   *   - 2: Exponent bits as a bit-vector term
-   *   - 3: Significand bits as a bit-vector term (without hidden bit)
+   * - Arity: `3`
+   *   - `1:` Term of bit-vector Sort of size `1` (sign bit)
+   *   - `2:` Term of bit-vector Sort of exponent size (exponent)
+   *   - `3:` Term of bit-vector Sort of significand size - 1
+   *          (significand without hidden bit)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_FP,
   /**
    * Floating-point equality.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_EQ,
   /**
    * Floating-point absolute value.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_ABS,
   /**
    * Floating-point negation.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_NEG,
   /**
    * Floating-point addition.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
-   *   - 3: Term of floating-point sort
+   * - Arity: `3`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2..3:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_ADD,
   /**
    * Floating-point sutraction.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
-   *   - 3: Term of floating-point sort
+   * - Arity: `3`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2..3:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_SUB,
   /**
    * Floating-point multiply.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
-   *   - 3: Term of floating-point sort
+   * - Arity: `3`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2..3:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_MULT,
   /**
    * Floating-point division.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
-   *   - 3: Term of floating-point sort
+   * - Arity: `3`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2..3:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_DIV,
   /**
    * Floating-point fused multiply and add.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
-   *   - 3: Term of floating-point sort
-   *   - 4: Term of floating-point sort
+   * - Arity: `4`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2..4:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_FMA,
   /**
    * Floating-point square root.
    *
-   * Parameters:
-   *   - 1: CONST_ROUNDINGMODE
-   *   - 2: Term of floating-point sort
+   * - Arity: `2`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_SQRT,
   /**
    * Floating-point remainder.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_REM,
   /**
    * Floating-point round to integral.
    *
-   * Parameters:
-   *   -1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_RTI,
   /**
    * Floating-point minimum.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_MIN,
   /**
    * Floating-point maximum.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_MAX,
   /**
    * Floating-point less than or equal.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_LEQ,
   /**
    * Floating-point less than.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_LT,
   /**
    * Floating-point greater than or equal.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_GEQ,
   /**
    * Floating-point greater than.
    *
-   * Parameters:
-   *   - 1..2: Terms of floating-point sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of floating-point Sort (sorts must match)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_GT,
   /**
-   * Floating-point is normal.
+   * Floating-point is normal tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_NORMAL,
   /**
-   * Floating-point is sub-normal.
+   * Floating-point is sub-normal tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_SUBNORMAL,
   /**
-   * Floating-point is zero.
+   * Floating-point is zero tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_ZERO,
   /**
-   * Floating-point is infinite.
+   * Floating-point is infinite tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_INF,
   /**
-   * Floating-point is NaN.
+   * Floating-point is NaN tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_NAN,
   /**
-   * Floating-point is negative.
+   * Floating-point is negative tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_NEG,
   /**
-   * Floating-point is positive.
+   * Floating-point is positive tester.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_IS_POS,
   /**
-   * Operator for to_fp from bit-vector.
+   * Conversion to floating-point from IEEE-754 bit-vector.
    *
-   * Parameters:
-   *   - 1: Exponent size
-   *   - 2: Significand size
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
+   * - Arity: `1`
+   *   - `1:` Term of bit-vector Sort
    *
-   * Conversion from an IEEE-754 bit-vector to floating-point.
+   * - Indices: `2`
+   *   - `1:` The exponent size
+   *   - `2:` The significand size
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_IEEE_BV
-   *   - 2: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
   /**
-   * Operator for to_fp from floating-point.
+   * Conversion to floating-point from floating-point.
    *
-   * Parameters:
-   *   - 1: Exponent size
-   *   - 2: Significand size
+   * - Arity: `2`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2:` Term of floating-point Sort
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
+   * - Indices: `2`
+   *   - `1:` The exponent size
+   *   - `2:` The significand size
    *
-   * Conversion between floating-point sorts.
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_FP
-   *   - 2: Term of sort RoundingMode
-   *   - 3: Term of floating-point sort
-   *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FLOATINGPOINT_TO_FP_FROM_FP,
   /**
-   * Operator for to_fp from real.
-   *
-   * Parameters:
-   *   - 1: Exponent size
-   *   - 2: Significand size
+   * Conversion to floating-point from Real.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2:` Term of Sort Real
    *
-   * Conversion from a real to floating-point.
+   * - Indices: `2`
+   *   - `1:` The exponent size
+   *   - `2:` The significand size
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_REAL
-   *   - 2: Term of sort RoundingMode
-   *   - 3: Term of sort Real
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FLOATINGPOINT_TO_FP_FROM_REAL,
   /**
-   * Operator for to_fp from signed bit-vector
-   *
-   * Parameters:
-   *   - 1: Exponent size
-   *   - 2: Significand size
+   * Conversion to floating-point from signed bit-vector.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2:` Term of bit-vector Sort
    *
-   * Conversion from a signed bit-vector to floating-point.
+   * - Indices: `2`
+   *   - `1:` The exponent size
+   *   - `2:` The significand size
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_SBV
-   *   - 2: Term of sort RoundingMode
-   *   - 3: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FLOATINGPOINT_TO_FP_FROM_SBV,
   /**
-   * Operator for to_fp from unsigned bit-vector.
+   * Conversion to floating-point from unsigned bit-vector.
    *
-   * Parameters:
-   *   - 1: Exponent size
-   *   - 2: Significand size
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort RoundingMode
+   *   - `2:` Term of bit-vector Sort
    *
-   * Converting an unsigned bit-vector to floating-point.
+   * - Indices: `2`
+   *   - `1:` The exponent size
+   *   - `2:` The significand size
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_UBV
-   *   - 2: Term of sort RoundingMode
-   *   - 3: Term of bit-vector sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FLOATINGPOINT_TO_FP_FROM_UBV,
   /**
-   * Operator for to_ubv.
-   *
-   * Parameters:
-   *   - 1: Size of the bit-vector to convert to
+   * Conversion to unsigned bit-vector from floating-point.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Conversion from a floating-point value to an unsigned bit-vector.
+   * - Indices: `1`
+   *   - `1:` The size of the bit-vector to convert to.
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_TO_UBV
-   *   - 2: Term of floating-point sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   FLOATINGPOINT_TO_UBV,
   /**
-   * Operator for to_sbv.
-   *
-   * Parameters:
-   *   - 1: Size of the bit-vector to convert to
+   * Conversion to signed bit-vector from floating-point.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of floating-point Sort
    *
-   * Conversion from a floating-point value to a signed bit-vector.
+   * - Indices: `1`
+   *   - `1:` The size of the bit-vector to convert to.
    *
-   * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_TO_SBV
-   *   - 2: Term of floating-point sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   FLOATINGPOINT_TO_SBV,
   /**
-   * Floating-point to real.
+   * Conversion to Real from floating-point.
    *
-   * Parameters:
-   *   - 1: Term of floating-point sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort Real
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   FLOATINGPOINT_TO_REAL,
 
@@ -1792,63 +2054,75 @@ enum Kind : int32_t
   /**
    * Array select.
    *
-   * Parameters:
-   *   - 1: Term of array sort
-   *   - 2: Selection index
+   * - Arity: `2`
+   *   - `1:` Term of array Sort
+   *   - `2:` Term of array index Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SELECT,
   /**
    * Array store.
    *
-   * Parameters:
-   *   - 1: Term of array sort
-   *   - 2: Store index
-   *   - 3: Term to store at the index
+   * - Arity: `3`
+   *   - `1:` Term of array Sort
+   *   - `2:` Term of array index Sort
+   *   - `3:` Term of array element Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STORE,
   /**
    * Constant array.
    *
-   * Parameters:
-   *   - 1: Array sort
-   *   - 2: Term representing a constant
+   * - Arity: `2`
+   *   - `1:` Term of array Sort
+   *   - `2:` Term of array element Sort (value)
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * @note We currently support the creation of constant arrays, but under some
-   * conditions when there is a chain of equalities connecting two constant
-   * arrays, the solver doesn't know what to do and aborts (Issue <a
-   * href="https://github.com/cvc5/cvc5/issues/1667">#1667</a>).
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   CONST_ARRAY,
   /**
-   * Equality over arrays a and b over a given range [i,j], i.e.,
+   * Equality over arrays @f$a@f$ and @f$b@f$ over a given range @f$[i,j]@f$,
+   * i.e.,
    * @f[
    *   \forall k . i \leq k \leq j \Rightarrow a[k] = b[k]
    * @f]
    *
-   * Parameters:
-   *   - 1: First array
-   *   - 2: Second array
-   *   - 3: Lower bound of range (inclusive)
-   *   - 4: Uppper bound of range (inclusive)
+   * @note We currently support the creation of array equalities over index
+   *       Sorts bit-vector, floating-point, Int and Real.
+   *       \verbatim embed:rst:leading-asterisk
+   *       Requires to enable option :ref:`arrays-exp<lbl-option-arrays-exp>`.
+   *       \endverbatim
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Arity: `4`
+   *   - `1:` Term of array Sort (first array)
+   *   - `2:` Term of array Sort (second array)
+   *   - `3:` Term of array index Sort (lower bound of range, inclusive)
+   *   - `4:` Term of array index Sort (upper bound of range, inclusive)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    *
-   * Note: We currently support the creation of array equalities over index
-   * types bit-vector, floating-point, integer and real. Option --arrays-exp is
-   * required to support this operator.
    */
   EQ_RANGE,
 #if 0
@@ -1865,60 +2139,83 @@ enum Kind : int32_t
   /* Datatypes ------------------------------------------------------------- */
 
   /**
-   * Constructor application.
+   * Datatype constructor application.
    *
-   * Paramters: n > 0
-   *   - 1: Constructor (operator)
-   *   - 2..n: Parameters to the constructor
+   * - Arity: `n > 0`
+   *   - `1:` DatatypeConstructor Term
+   *          (see DatatypeConstructor::getConstructorTerm() const,
+   *          Datatype::getConstructorTerm(const std::string&) const)
+   *   - `2..n:` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op) const`
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   APPLY_CONSTRUCTOR,
   /**
-   * Datatype selector application, which is undefined if misapplied.
+   * Datatype selector application.
    *
-   * Parameters:
-   *   - 1: Selector (operator)
-   *   - 2: Datatype term
+   * @note Undefined if misapplied.
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
+   * - Arity: `2`
+   *   - `1:` DatatypeSelector Term
+   *          (see DatatypeSelector::getSelectorTerm() const,
+   *          DatatypeConstructor::getSelectorTerm(const std::string&) const)
+   *   - `2:` Term of the codomain Sort of the selector
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   APPLY_SELECTOR,
   /**
    * Datatype tester application.
    *
-   * Parameters:
-   *   - 1: Tester term
-   *   - 2: Datatype term
+   * - Arity: `2`
+   *   - `1:` Datatype tester Term
+   *          (see DatatypeConstructor::getTesterTerm() const)
+   *   - `2:` Term of Datatype Sort (DatatypeConstructor must belong to this
+   *          Datatype Sort)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   APPLY_TESTER,
   /**
-   * Datatype update application, which does not change the argument if
-   * misapplied.
+   * Datatype update application.
    *
-   * Parameters:
-   *   - 1: Updater (operator)
-   *   - 2: Datatype term
-   *   - 3: Value to update a field of the datatype term with
+   * @note Does not change the datatype argument if misapplied.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Datatype updater Term
+   *          (see DatatypeSelector::getUpdaterTerm() const)
+   *   - `2:` Term of Datatype Sort (DatatypeSelector of the updater must
+   *          belong to a constructor of this Datatype Sort)
+   *   - `3:` Term of the codomain Sort of the selector (the Term to update
+   *          the field of the datatype term with)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   APPLY_UPDATER,
   /**
-   * Match expressions.
-   * For example, the smt2 syntax match term
+   * Match expression.
+   *
+   * For example, the SMT-LIBv2 syntax for the following match term
    * \rst
    * .. code:: smtlib
    *
@@ -1928,81 +2225,120 @@ enum Kind : int32_t
    *
    * \rst
    * .. code:: lisp
-   * 
+   *
    *     (MATCH l
    *         (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h)
    *         (MATCH_CASE nil 0))
    * \endrst
    *
-   * The type of the last argument of each case term could be equal.
+   * Terms of kind #MATCH_CASE are constant case expressions, which are used
+   * for nullary constructors. Kind #MATCH_BIND_CASE is used for constructors
+   * with selectors and variable match patterns. If not all constructors are
+   * covered, at least one catch-all variable pattern must be included.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of kind MATCH_CASE or MATCH_BIND_CASE
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of kind #MATCH_CASE and #MATCH_BIND_CASE
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   MATCH,
   /**
-   * Match case
+   * Match case for nullary constructors.
+   *
    * A (constant) case expression to be used within a match expression.
    *
-   * Parameters:
-   *   - 1: Term denoting the pattern expression
-   *   - 2: Term denoting the return value
+   * - Arity: `2`
+   *   - `1:` Term of kind #APPLY_CONSTRUCTOR (the pattern to match against)
+   *   - `2:` Term of any Sort (the term the pattern evaluates to)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   MATCH_CASE,
   /**
-   * Match bind case
-   * A (non-constant) case expression to be used within a match expression.
+   * Match case with binders, for constructors with selectors and variable
+   * patterns.
    *
-   * Parameters:
-   *   - 1: a VARIABLE_LIST Term containing the free variables of the case
-   *   - 2: Term denoting the pattern expression
-   *   - 3: Term denoting the return value
+   * A (non-constant) case expression to be used within a match expression.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - For variable patterns:
+   *     - `1:` Term of kind #VARIABLE_LIST (containing the free variable of
+   *            the case)
+   *     - `2:` Term of kind #VARIABLE (the pattern expression, the free
+   *            variable of the case)
+   *     - `3:` Term of any Sort (the term the pattern evaluates to)
+   *   - For constructors with selectors:
+   *     - `1:` Term of kind #VARIABLE_LIST (containing the free variable of
+   *            the case)
+   *     - `2:` Term of kind #APPLY_CONSTRUCTOR (the pattern expression,
+   *            applying the set of variables to the constructor)
+   *     - `3:` Term of any Sort (the term the pattern evaluates to)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   MATCH_BIND_CASE,
   /**
-   * Datatypes size
-   * An operator mapping datatypes to an integer denoting the number of
-   * non-nullary applications of constructors they contain.
+   * Datatypes size operator.
    *
-   * Parameters:
-   *   - 1: Datatype term
+   * An operator mapping a datatype term to an integer denoting the number of
+   * non-nullary applications of constructors it contains.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `1`
+   *   - `1:` Term of datatype Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   DT_SIZE,
   /**
-   * Operator for tuple projection indices
+   * Tuple projection.
    *
-   * Parameters:
-   *   - 1: A vector of tuple projection indices.
+   * This operator takes a tuple as an argument and returns a tuple obtained by
+   * concatenating components of its argument at the provided indices.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) const`
+   * For example,
+   * \rst
+   * .. code:: smtlib
+   *
+   *     ((_ tuple_project 1 2 2 3 1) (tuple 10 20 30 40))
+   * \endrst
+   * yields
+   * \rst
+   * .. code:: smtlib
    *
-   * Constructs a new tuple from an existing one using the elements at the
-   * given indices
+   *     (tuple 20 30 30 40 20)
+   * \endrst
    *
-   * Parameters:
-   *   - 1: a term of tuple sort
+   * - Arity: `1`
+   *   - `1:` Term of tuple Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Indices: `n`
+   *   - `1..n:` The tuple indices to project
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   TUPLE_PROJECT,
 #if 0
@@ -2021,56 +2357,64 @@ enum Kind : int32_t
   /* Separation Logic ------------------------------------------------------ */
 
   /**
-   * Separation logic nil term.
+   * Separation logic nil.
    *
-   * Parameters: none
-   *
-   * Create with:
-   *   - `Solver::mkSepNil(const Sort& sort) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkSepNil(const Sort&) const
    */
   SEP_NIL,
   /**
-   * Separation logic empty heap constraint
+   * Separation logic empty heap.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkSepEmp() const
    */
   SEP_EMP,
   /**
    * Separation logic points-to relation.
    *
-   * Parameters:
-   *   - 1: Location of the points-to constraint
-   *   - 2: Data of the points-to constraint
+   * - Arity: `2`
+   *   - `1:` Term denoting the location of the points-to constraint
+   *   - `2:` Term denoting the data of the points-to constraint
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SEP_PTO,
   /**
    * Separation logic star.
    *
-   * Parameters: n > 1
-   *   - 1..n: Child constraints that hold in disjoint (separated) heaps
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of sort Bool (the child constraints that hold in
+   *             disjoint (separated) heaps)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SEP_STAR,
   /**
    * Separation logic magic wand.
    *
-   * Parameters:
-   *   - 1: Antecendant of the magic wand constraint
-   *   - 2: Conclusion of the magic wand constraint, which is asserted to
-   *         hold in all heaps that are disjoint extensions of the antecedent.
+   * - Arity: `2`
+   *   - `1:` Terms of Sort Bool (the antecendant of the magic wand constraint)
+   *   - `2:` Terms of Sort Bool (conclusion of the magic wand constraint,
+   *          which is asserted to hold in all heaps that are disjoint
+   *          extensions of the antecedent)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SEP_WAND,
 #if 0
@@ -2081,338 +2425,433 @@ enum Kind : int32_t
   /* Sets ------------------------------------------------------------------ */
 
   /**
-   * Empty set constant.
-   *
-   * Parameters:
-   *   - 1: Sort of the set elements
+   * Empty set.
    *
-   * Create with:
-   *   - `Solver::mkEmptySet(const Sort& sort) const`
+   * - Create Term of this Kind with:
+   *   - `Solver::mkEmptySet(const Sort&) const`
    */
   SET_EMPTY,
   /**
    * Set union.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_UNION,
   /**
    * Set intersection.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_INTER,
   /**
    * Set subtraction.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_MINUS,
   /**
    * Subset predicate.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort, [1] a subset of set [2]?
+   * Determines if the first set is a subset of the second set.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of set Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_SUBSET,
   /**
    * Set membership predicate.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort, [1] a member of set [2]?
+   * Determines if the given set element is a member of the second set.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of any Sort (must match the element Sort of the
+   *          given set Term)
+   *   - `2:` Term of set Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_MEMBER,
   /**
+   * Singleton set.
+   *
    * Construct a singleton set from an element given as a parameter.
-   * The returned set has same type of the element.
+   * The returned set has the same Sort as the element.
    *
-   * Parameters:
-   *   - 1: Single element
+   * - Arity: `1`
+   *   - `1:` Term of any Sort (the set element)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_SINGLETON,
   /**
    * The set obtained by inserting elements;
    *
-   * Parameters: n > 0
-   *   - 1..n-1: Elements inserted into set [n]
-   *   - n: Set Term
+   * - Arity: `n > 0`
+   *   - `1..n-1:` Terms of any Sort (must match the element sort of the
+   *               given set Term)
+   *   - `n:` Term of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_INSERT,
   /**
    * Set cardinality.
    *
-   * Parameters:
-   *   - 1: Set to determine the cardinality of
+   * - Arity: `1`
+   *   - `1:` Term of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_CARD,
   /**
    * Set complement with respect to finite universe.
    *
-   * Parameters:
-   *   - 1: Set to complement
+   * - Arity: `1`
+   *   - `1:` Term of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_COMPLEMENT,
   /**
    * Finite universe set.
+   *
    * All set variables must be interpreted as subsets of it.
    *
-   * Note that SET_UNIVERSE is considered a special symbol of the theory of
-   * sets and is not considered as a set value,
-   * i.e., `Term::isSetValue() const` will return false.
+   * @note #SET_UNIVERSE is considered a special symbol of the theory of
+   *       sets and is not considered as a set value, i.e.,
+   *       Term::isSetValue() will return `false`.
    *
-   * Create with:
-   *   - `Solver::mkUniverseSet(const Sort& sort) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkUniverseSet(const Sort&) const
    */
   SET_UNIVERSE,
   /**
    * Set comprehension
-   * A set comprehension is specified by a variable list x1 ... xn,
-   * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
-   * above form has members given by the following semantics:
+   *
+   * A set comprehension is specified by a variable list @f$x_1 ... x_n@f$,
+   * a predicate @f$P[x_1...x_n]@f$, and a term @f$t[x_1...x_n]@f$. A
+   * comprehension @f$C@f$ with the above form has members given by the
+   * following semantics:
    * @f[
    *  \forall y. ( \exists x_1...x_n. P[x_1...x_n] \wedge t[x_1...x_n] = y )
    * \Leftrightarrow (set.member \; y \; C)
    * @f]
-   * where y ranges over the element type of the (set) type of the
-   * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
-   * y in the above formula.
+   * where @f$y@f$ ranges over the element Sort of the (set) Sort of the
+   * comprehension. If @f$t[x_1..x_n]@f$ is not provided, it is equivalent
+   * to @f$y@f$ in the above formula.
    *
-   * Parameters:
-   *   - 1: Term VARIABLE_LIST
-   *   - 2: Term denoting the predicate of the comprehension
-   *   - 3: (optional) a Term denoting the generator for the comprehension
+   * - Arity: `3`
+   *   - `1:` Term of Kind #VARIABLE_LIST
+   *   - `2:` Term of sort Bool (the predicate of the comprehension)
+   *   - `3:` (optional) Term denoting the generator for the comprehension
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_COMPREHENSION,
   /**
-   * Returns an element from a given set.
-   * If a set A = {x}, then the term (set.choose A) is equivalent to the term x.
-   * If the set is empty, then (set.choose A) is an arbitrary value.
-   * If the set has cardinality > 1, then (set.choose A) will deterministically
-   * return an element in A.
+   * Set choose.
    *
-   * Parameters:
-   *   - 1: Term of set sort
+   * Select an element from a given set. For a set @f$A = \{x\}@f$, the term
+   * `(set.choose A)` is equivalent to the term @f$x@f$. For an empty set,
+   * it is an arbitrary value. For a set with cardinality > 1, it will
+   * deterministically return an element in @f$A@f$.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Arity: `1`
+   *   - `1:` Term of set Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_CHOOSE,
   /**
-   * Set is_singleton predicate.
+   * Set is singleton tester.
    *
-   * Parameters:
-   *   - 1: Term of set sort, is [1] a singleton set?
+   * - Arity: `1`
+   *   - `1:` Term of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   SET_IS_SINGLETON,
   /**
-   * set.map operator applies the first argument, a function of type (-> T1 T2),
-   * to every element of the second argument, a set of type (Set T1),
-   * and returns a set of type (Set T2).
+   * Set map.
    *
-   * Parameters:
-   *   - 1: a function of type (-> T1 T2)
-   *   - 2: a set of type (Set T1)
+   * This operator applies the first argument, a function of
+   * Sort @f$(\rightarrow S_1 \; S_2)@f$, to every element of the second
+   * argument, a set of Sort (Set @f$S_1@f$), and returns a set of Sort
+   * (Set @f$S_2@f$).
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$
+   *   - `2:` Term of set Sort (Set @f$S_1@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
    SET_MAP,
 
   /* Relations ------------------------------------------------------------- */
 
   /**
-   * Set join.
+   * Relation join.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_JOIN,
   /**
-   * Set cartesian product.
+   * Relation cartesian product.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_PRODUCT,
   /**
-   * Set transpose.
+   * Relation transpose.
    *
-   * Parameters:
-   *   - 1: Term of set sort
+   * - Arity: `1`
+   *   - `1:` Term of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_TRANSPOSE,
   /**
-   * Set transitive closure.
+   * Relation transitive closure.
    *
-   * Parameters:
-   *   - 1: Term of set sort
+   * - Arity: `1`
+   *   - `1:` Term of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_TCLOSURE,
   /**
-   * Set join image.
+   * Relation join image.
    *
-   * Parameters:
-   *   - 1..2: Terms of set sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_JOIN_IMAGE,
   /**
-   * Set identity.
+   * Relation identity.
    *
-   * Parameters:
-   *   - 1: Term of set sort
+   * - Arity: `1`
+   *   - `1:` Term of relation Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   RELATION_IDEN,
 
   /* Bags ------------------------------------------------------------------ */
 
   /**
-   * Empty bag constant.
+   * Empty bag.
    *
-   * Parameters:
-   *   - 1: Sort of the bag elements
-   *
-   * Create with:
-   *   mkEmptyBag(const Sort& sort)
+   * - Create Term of this Kind with:
+   *   - Solver::mkEmptyBag(const Sort&) const
    */
   BAG_EMPTY,
   /**
    * Bag max union.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_UNION_MAX,
   /**
    * Bag disjoint union (sum).
    *
-   * Parameters:
-   *   -1..2: Terms of bag sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_UNION_DISJOINT,
   /**
    * Bag intersection (min).
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_INTER_MIN,
   /**
-   * Bag difference subtract (subtracts multiplicities of the second from the
-   * first).
+   * Bag difference subtract.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * Subtracts multiplicities of the second from the first.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_DIFFERENCE_SUBTRACT,
   /**
-   * Bag difference 2 (removes shared elements in the two bags).
+   * Bag difference remove.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * Removes shared elements in the two bags.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_DIFFERENCE_REMOVE,
   /**
-   * Inclusion predicate for bags
-   * (multiplicities of the first bag <= multiplicities of the second bag).
+   * Bag inclusion predicate.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * Determine if multiplicities of the first bag are less than or equal to
+   * multiplicities of the second bag.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1..2:` Terms of bag Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_SUBBAG,
   /**
-   * Element multiplicity in a bag
+   * Bag element multiplicity.
    *
    * Parameters:
    *   - 1..2: Terms of bag sort (Bag E), [1] an element of sort E
@@ -2425,147 +2864,204 @@ enum Kind : int32_t
   /**
    * Bag membership predicate.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort (Bag E), is [1] of type E an element of [2]
+   * - Arity: `2`
+   *   - `1:` Term of any Sort (must match the element Sort of the
+   *          given bag Term)
+   *   - `2:` Terms of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_MEMBER,
   /**
+   * Bag duplicate removal.
+   *
    * Eliminate duplicates in a given bag. The returned bag contains exactly the
    * same elements in the given bag, but with multiplicity one.
    *
-   * Parameters:
-   *   - 1: a term of bag sort
+   * - Arity: `1`
+   *   - `1:` Term of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_DUPLICATE_REMOVAL,
   /**
+   * Bag make.
+   *
    * Construct a bag with the given element and given multiplicity.
    *
-   * Parameters:
-   *   - 1: The element
-   *   - 2: The multiplicity of the element. 
+   * - Arity: `2`
+   *   - `1:` Term of any Sort (the bag element)
+   *   - `2:` Term of Sort Int (the multiplicity of the element)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child, const Term& child) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_MAKE,
   /**
    * Bag cardinality.
    *
-   * Parameters:
-   *   - 1: Bag to determine the cardinality of
+   * - Arity: `1`
+   *   - `1:` Term of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_CARD,
   /**
-   * Returns an element from a given bag.
-   * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A)
-   * is equivalent to the term x.
-   * If the bag is empty, then (choose A) is an arbitrary value.
-   * If the bag contains distinct elements, then (choose A) will
-   * deterministically return an element in A.
+   * Bag choose.
    *
-   * Parameters:
-   *   - 1: Term of bag sort
+   * Select an element from a given bag.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * For a bag @f$A = \{(x,n)\}@f$ where @f$n@f$ is the multiplicity, then the
+   * term `(choose A)` is equivalent to the term @f$x@f$. For an empty bag,
+   * then it is an arbitrary value. For a bag that contains distinct elements,
+   * it will deterministically return an element in @f$A@f$.
+   *
+   * - Arity: `1`
+   *   - `1:` Term of bag Sort
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_CHOOSE,
   /**
-   * Bag is_singleton predicate (single element with multiplicity exactly one).
+   * Bag is singleton tester.
    *
-   * Parameters:
-   *   - 1: Term of bag sort, is [1] a singleton bag?
+   * - Arity: `1`
+   *   - `1:` Term of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_IS_SINGLETON,
   /**
-   * Bag.from_set converts a set to a bag.
+   * Conversion from set to bag.
    *
-   * Parameters:
-   *   - 1: Term of set sort
+   * - Arity: `1`
+   *   - `1:` Term of set Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_FROM_SET,
   /**
-   * Bag.to_set converts a bag to a set.
+   * Conversion from bag to set.
    *
-   * Parameters:
-   *   - 1: Term of bag sort
+   * - Arity: `1`
+   *   - `1:` Term of bag Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_TO_SET,
   /**
-   * bag.map operator applies the first argument, a function of type (-> T1 T2),
-   * to every element of the second argument, a bag of type (Bag T1),
-   * and returns a bag of type (Bag T2).
+   * Bag map.
    *
-   * Parameters:
-   *   - 1: a function of type (-> T1 T2)
-   *   - 2: a bag of type (Bag T1)
+   * This operator applies the first argument, a function of
+   * Sort @f$(\rightarrow S_1 \; S_2)@f$, to every element of the second
+   * argument, a set of Sort (Bag @f$S_1@f$), and returns a set of Sort
+   * (Bag @f$S_2@f$).
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$
+   *   - `2:` Term of bag Sort (Bag @f$S_1@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_MAP,
   /**
-    * bag.filter operator filters the elements of a bag.
-    * (bag.filter p B) takes a predicate p of type (-> T Bool) as a first
-    * argument, and a bag B of type (Bag T) as a second argument, and returns a
-    * subbag of type (Bag T) that includes all elements of B that satisfy p
-    * with the same multiplicity.
-    *
-    * Parameters:
-    *   - 1: a function of type (-> T Bool)
-    *   - 2: a bag of type (Bag T)
-    *
-    * Create with:
-    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
-    */
+   * Bag filter.
+   *
+   * This operator filters the elements of a bag.
+   * `(bag.filter p B)` takes a predicate @f$p@f$ of
+   * Sort @f$(\rightarrow S_1 \; S_2)@f$ as a first argument, and a bag @f$@f$
+   * of Sort (Bag @f$S@f$) as a second argument, and returns a subbag of Sort
+   * (Bag @f$T@f$) that includes all elements of @f$B@f$ that satisfy @f$p@f$
+   * with the same multiplicity.
+   *
+   * - Arity: `2`
+   *   - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$
+   *   - `2:` Term of bag Sort (Bag @f$S_1@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
+   */
    BAG_FILTER,
   /**
-   * bag.fold operator combines elements of a bag into a single value.
-   * (bag.fold f t B) folds the elements of bag B starting with term t and using
-   * the combining function f.
+   * Bag fold.
    *
-   * Parameters:
-   *   - 1: a binary operation of type (-> T1 T2 T2)
-   *   - 2: an initial value of type T2
-   *   - 2: a bag of type (Bag T1)
+   * This operator combines elements of a bag into a single value.
+   * `(bag.fold f t B)` folds the elements of bag @f$B@f$ starting with
+   * Term @f$t@f$ and using the combining function @f$f@f$.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2 \; S_2)@f$
+   *   - `2:` Term of Sort `S_2)` (the initial value)
+   *   - `3:` Term of bag Sort (Bag @f$S_1@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   BAG_FOLD,
   /**
    * Table cross product.
    *
-   * Parameters:
-   *   - 1..2: Terms of bag sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of table Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   TABLE_PRODUCT,
 
@@ -2574,737 +3070,919 @@ enum Kind : int32_t
   /**
    * String concat.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of String sort
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_CONCAT,
   /**
    * String membership.
    *
-   * Parameters:
-   *   - 1: Term of String sort
-   *   - 2: Term of RegExp sort
+   * - Arity: `2`
+   *   - `1:` Term of Sort String
+   *   - `2:` Term of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_IN_REGEXP,
   /**
    * String length.
    *
-   * Parameters:
-   *   - 1: Term of String sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_LENGTH,
   /**
    * String substring.
-   * Extracts a substring, starting at index i and of length l, from a string
-   * s.  If the start index is negative, the start index is greater than the
-   * length of the string, or the length is negative, the result is the empty
-   * string.
    *
-   * Parameters:
-   *   - 1: Term of sort String
-   *   - 2: Term of sort Integer (index i)
-   *   - 3: Term of sort Integer (length l)
+   * Extracts a substring, starting at index @f$i@f$ and of length @f$l@f$,
+   * from a string @f$s@f$.  If the start index is negative, the start index is
+   * greater than the length of the string, or the length is negative, the
+   * result is the empty string.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *   - `3:` Term of Sort Int (length @f$l@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_SUBSTR,
   /**
    * String update.
-   * Updates a string s by replacing its context starting at an index with t.
-   * If the start index is negative, the start index is greater than the
-   * length of the string, the result is s. Otherwise, the length of the
-   * original string is preserved.
    *
-   * Parameters:
-   *   - 1: Term of sort String
-   *   - 2: Term of sort Integer (index i)
-   *   - 3: Term of sort String (replacement string t)
+   * Updates a string @f$s@f$ by replacing its context starting at an index
+   * with string @f$t@f$. If the start index is negative, the start index is
+   * greater than the length of the string, the result is @f$s@f$. Otherwise,
+   * the length of the original string is preserved.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *   - `3:` Term of Sort Strong (replacement string @f$t@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_UPDATE,
   /**
    * String character at.
-   * Returns the character at index i from a string s. If the index is negative
-   * or the index is greater than the length of the string, the result is the
-   * empty string. Otherwise the result is a string of length 1.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s)
-   *   - 2: Term of sort Integer (index i)
+   * Returns the character at index @f$i@f$ from a string @f$s@f$. If the index is
+   * negative or the index is greater than the length of the string, the result
+   * is the empty string. Otherwise the result is a string of length @f$1@f$.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (string @f$s@f$)
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_CHARAT,
   /**
    * String contains.
-   * Checks whether a string s1 contains another string s2. If s2 is empty, the
-   * result is always true.
    *
-   * Parameters:
-   *   - 1: Term of sort String (the string s1)
-   *   - 2: Term of sort String (the string s2)
+   * Determines whether a string @f$s_1@f$ contains another string @f$s_2@f$.
+   * If @f$s_2@f$ is empty, the result is always `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (the string @f$s_1@f$)
+   *   - `2:` Term of Sort String (the string @f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_CONTAINS,
   /**
    * String index-of.
-   * Returns the index of a substring s2 in a string s1 starting at index i. If
-   * the index is negative or greater than the length of string s1 or the
-   * substring s2 does not appear in string s1 after index i, the result is -1.
    *
-   * Parameters:
-   *   - 1: Term of sort String (substring s1)
-   *   - 2: Term of sort String (substring s2)
-   *   - 3: Term of sort Integer (index i)
+   * Returns the index of a substring @f$s_2@f$ in a string @f$s_1@f$ starting
+   * at index @f$i@f$. If the index is negative or greater than the length of
+   * string @f$s_1@f$ or the substring @f$s_2@f$ does not appear in
+   * string @f$s_1@f$ after index @f$i@f$, the result is `-1`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (substring @f$s_1@f$)
+   *   - `2:` Term of Sort String (substring @f$s_2@f$)
+   *   - `3:` Term of Sort Int (index @f$i@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_INDEXOF,
   /**
    * String index-of regular expression match.
-   * Returns the first match of a regular expression r in a string s. If the
-   * index is negative or greater than the length of string s1, or r does not
-   * match a substring in s after index i, the result is -1.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s)
-   *   - 2: Term of sort RegLan (regular expression r)
-   *   - 3: Term of sort Integer (index i)
+   * Returns the first match of a regular expression @f$r@f$ in a
+   * string @f$s@f$. If the index is negative or greater than the length of
+   * string @f$s_1@f$, or @f$r@f$ does not match a substring in @f$s@f$ after
+   * index @f$i@f$, the result is `-1`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String (string @f$s@f$)
+   *   - `2:` Term of Sort RegLan (regular expression @f$r@f$)
+   *   - `3:` Term of Sort Int (index @f$i@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_INDEXOF_RE,
   /**
    * String replace.
-   * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
-   * in s1, s1 is returned unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort String (string s2)
-   *   - 3: Term of sort String (string s3)
+   * Replaces a string @f$s_2@f$ in a string @f$s_1@f$ with string @f$s_3@f$.
+   * If @f$s_2@f$ does not appear in @f$s_1@f$, @f$s_1@f$ is returned
+   * unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String (string @f$s_1@f$)
+   *   - `2:` Term of Sort String (string @f$s_2@f$)
+   *   - `3:` Term of Sort String (string @f$s_3@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_REPLACE,
   /**
    * String replace all.
-   * Replaces all occurrences of a string s2 in a string s1 with string s3.
-   * If s2 does not appear in s1, s1 is returned unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort String (string s2)
-   *   - 3: Term of sort String (string s3)
+   * Replaces all occurrences of a string @f$s_2@f$ in a string @f$s_1@f$ with
+   * string @f$s_3@f$. If @f$s_2@f$ does not appear in @f$s_1@f$, @f$s_1@f$ is
+   * returned unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort String (@f$s_2@f$)
+   *   - `3:` Term of Sort String (@f$s_3@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_REPLACE_ALL,
   /**
    * String replace regular expression match.
-   * Replaces the first match of a regular expression r in string s1 with
-   * string s2. If r does not match a substring of s1, s1 is returned
-   * unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort Regexp (regexp r)
-   *   - 3: Term of sort String (string s2)
+   * Replaces the first match of a regular expression @f$r@f$ in
+   * string @f$s_1@f$ with string @f$s_2@f$. If @f$r@f$ does not match a
+   * substring of @f$s_1@f$, @f$s_1@f$ is returned unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort RegLan
+   *   - `3:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_REPLACE_RE,
   /**
    * String replace all regular expression matches.
-   * Replaces all matches of a regular expression r in string s1 with string
-   * s2. If r does not match a substring of s1, s1 is returned unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort Regexp (regexp r)
-   *   - 3: Term of sort String (string s2)
+   * Replaces all matches of a regular expression @f$r@f$ in string @f$s_1@f$
+   * with string @f$s_2@f$. If @f$r@f$ does not match a substring of @f$s_1@f$,
+   * string @f$s_1@f$ is returned unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort RegLan
+   *   - `3:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_REPLACE_RE_ALL,
   /**
    * String to lower case.
    *
-   * Parameters:
-   *   - 1: Term of String sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_TOLOWER,
   /**
    * String to upper case.
    *
-   * Parameters:
-   *   - 1: Term of String sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_TOUPPER,
   /**
    * String reverse.
    *
-   * Parameters:
-   *   - 1: Term of String sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_REV,
   /**
    * String to code.
-   * Returns the code point of a string if it has length one, or returns -1
+   *
+   * Returns the code point of a string if it has length one, or returns `-1`
    * otherwise.
    *
-   * Parameters:
-   *   - 1: Term of String sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_TO_CODE,
   /**
    * String from code.
+   *
    * Returns a string containing a single character whose code point matches
    * the argument to this function, or the empty string if the argument is
    * out-of-bounds.
    *
-   * Parameters:
-   *   - 1: Term of Integer sort
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_FROM_CODE,
   /**
    * String less than.
-   * Returns true if string s1 is (strictly) less than s2 based on a
-   * lexiographic ordering over code points.
    *
-   * Parameters:
-   *   - 1: Term of sort String (the string s1)
-   *   - 2: Term of sort String (the string s2)
+   * Returns true if string @f$s_1@f$ is (strictly) less than @f$s_2@f$ based
+   * on a lexiographic ordering over code points.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_LT,
   /**
    * String less than or equal.
-   * Returns true if string s1 is less than or equal to s2 based on a
-   * lexiographic ordering over code points.
    *
-   * Parameters:
-   *   - 1: Term of sort String (the string s1)
-   *   - 2: Term of sort String (the string s2)
+   * Returns true if string @f$s_1@f$ is less than or equal to @f$s_2@f$ based
+   * on a lexiographic ordering over code points.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_LEQ,
   /**
    * String prefix-of.
-   * Checks whether a string s1 is a prefix of string s2. If string s1 is
-   * empty, this operator returns true.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort String (string s2)
+   * Determines whether a string @f$s_1@f$ is a prefix of string @f$s_2@f$.
+   * If string s1 is empty, this operator returns `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_PREFIX,
   /**
    * String suffix-of.
-   * Checks whether a string s1 is a suffix of string 2. If string s1 is empty,
-   * this operator returns true.
    *
-   * Parameters:
-   *   - 1: Term of sort String (string s1)
-   *   - 2: Term of sort String (string s2)
+   * Determines whether a string @f$s_1@f$ is a suffix of the second string.
+   * If string @f$s_1@f$ is empty, this operator returns `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (@f$s_1@f$)
+   *   - `2:` Term of Sort String (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_SUFFIX,
   /**
    * String is-digit.
-   * Returns true if string s is digit (it is one of "0", ..., "9").
    *
-   * Parameters:
-   *   - 1: Term of sort String
+   * Returns true if given string is a digit (it is one of `"0"`, ..., `"9"`).
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_IS_DIGIT,
   /**
-   * Integer to string.
+   * Conversion from Int to String.
+   *
    * If the integer is negative this operator returns the empty string.
    *
-   * Parameters:
-   *   - 1: Term of sort Integer
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_FROM_INT,
   /**
    * String to integer (total function).
+   *
    * If the string does not contain an integer or the integer is negative, the
-   * operator returns -1.
+   * operator returns `-1`.
    *
-   * Parameters:
-   *   - 1: Term of sort String
+   * - Arity: `1`
+   *   - `1:` Term of Sort Int
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_TO_INT,
   /**
    * Constant string.
    *
-   * Parameters:
-   *   - See @ref cvc5::api::Solver::mkString() "mkString()".
-   *
-   * Create with:
-   *   - `Solver::mkString(const std::string& s, bool useEscSequences) const`
-   *   - `Solver::mkString(const unsigned char c) const`
-   *   - `Solver::mkString(const std::vector<uint32_t>& s) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkString(const std::string&, bool) const
+   *   - Solver::mkString(const std::wstring&) const
    */
   CONST_STRING,
   /**
    * Conversion from string to regexp.
    *
-   * Parameters:
-   *   - 1: Term of sort String
+   * - Arity: `1`
+   *   - `1:` Term of Sort String
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   STRING_TO_REGEXP,
   /**
-   * Regexp Concatenation.
+   * Regular expression concatenation.
    *
-   * Parameters:
-   *   - 1..2: Terms of Regexp sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_CONCAT,
   /**
-   * Regexp union.
+   * Regular expression union.
    *
-   * Parameters:
-   *   - 1..2: Terms of Regexp sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_UNION,
   /**
-   * Regexp intersection.
+   * Regular expression intersection.
    *
-   * Parameters:
-   *   - 1..2: Terms of Regexp sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_INTER,
   /**
-   * Regexp difference.
+   * Regular expression difference.
    *
-   * Parameters:
-   *   - 1..2: Terms of Regexp sort
+   * - Arity: `2`
+   *   - `1..2:` Terms of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_DIFF,
   /**
-   * Regexp \*.
+   * Regular expression \*.
    *
-   * Parameters:
-   *   - 1: Term of sort Regexp
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_STAR,
   /**
-   * Regexp +.
+   * Regular expression +.
    *
-   * Parameters:
-   *   - 1: Term of sort Regexp
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_PLUS,
   /**
-   * Regexp ?.
+   * Regular expression ?.
    *
-   * Parameters:
-   *   - 1: Term of sort Regexp
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_OPT,
   /**
-   * Regexp range.
+   * Regular expression range.
    *
-   * Parameters:
-   *   - 1: Lower bound character for the range
-   *   - 2: Upper bound character for the range
+   * - Arity: `2`
+   *   - `1:` Term of Sort String (lower bound character for the range)
+   *   - `2:` Term of Sort String (upper bound character for the range)
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind) const
    */
   REGEXP_RANGE,
   /**
    * Operator for regular expression repeat.
    *
-   * Parameters:
-   *   - 1: The number of repetitions
-   *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Apply regular expression loop.
+   * - Indices: `1`
+   *   - `1:` The number of repetitions
    *
-   * Parameters:
-   *   - 1: Op of kind REGEXP_REPEAT
-   *   - 2: Term of regular expression sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t) const
    */
   REGEXP_REPEAT,
   /**
-   * Operator for regular expression loop, from lower bound to upper bound
-   * number of repetitions.
+   * Regular expression loop.
    *
-   * Parameters:
-   *   - 1: The lower bound
-   *   - 2: The upper bound
+   * Regular expression loop from lower bound to upper bound number of
+   * repetitions.
    *
-   * Create with:
-   *   - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Apply regular expression loop.
+   * - Indices: `1`
+   *   - `1:` The lower bound
+   *   - `2:` The upper bound
    *
-   * Parameters:
-   *   - 1: Op of kind REGEXP_LOOP
-   *   - 2: Term of regular expression sort
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
-   * Create with:
-   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
-   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   REGEXP_LOOP,
   /**
-   * Regexp none.
-   *
-   * Parameters: none
+   * Regular expression none.
    *
-   * Create with:
-   *   - `Solver::mkRegexpNone() const`
-   *   - `Solver::mkTerm(Kind kind) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkRegexpNone() const
    */
   REGEXP_NONE,
   /**
-   * Regexp all.
-   *
-   * Parameters: none
+   * Regular expression all.
    *
-   * Create with:
-   *   - `Solver::mkRegexpAll() const`
-   *   - `Solver::mkTerm(Kind kind) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkRegexpAll() const
    */
   REGEXP_ALL,
   /**
-   * Regexp all characters.
-   *
-   * Parameters: none
+   * Regular expression all characters.
    *
-   * Create with:
-   *   - `Solver::mkRegexpAllchar() const`
-   *   - `Solver::mkTerm(Kind kind) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkRegexpAllchar() const
    */
   REGEXP_ALLCHAR,
   /**
-   * Regexp complement.
+   * Regular expression complement.
    *
-   * Parameters:
-   *   - 1: Term of sort RegExp
+   * - Arity: `1`
+   *   - `1:` Term of Sort RegLan
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   REGEXP_COMPLEMENT,
 
   /**
    * Sequence concat.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of Sequence sort
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of sequence Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_CONCAT,
   /**
    * Sequence length.
    *
-   * Parameters:
-   *   - 1: Term of Sequence sort
+   * - Arity: `1`
+   *   - `1:` Term of sequence Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_LENGTH,
   /**
    * Sequence extract.
-   * Extracts a subsequence, starting at index i and of length l, from a
-   * sequence s.  If the start index is negative, the start index is greater
-   * than the length of the sequence, or the length is negative, the result is
-   * the empty sequence.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence
-   *   - 2: Term of sort Integer (index i)
-   *   - 3: Term of sort Integer (length l)
+   * Extracts a subsequence, starting at index @f$i@f$ and of length @f$l@f$,
+   * from a sequence @f$s@f$.  If the start index is negative, the start index
+   * is greater than the length of the sequence, or the length is negative, the
+   * result is the empty sequence.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of sequence Sort
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *   - `3:` Term of Sort Int (length @f$l@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_EXTRACT,
   /**
    * Sequence update.
-   * Updates a sequence s by replacing its context starting at an index with t.
-   * If the start index is negative, the start index is greater than the
-   * length of the sequence, the result is s. Otherwise, the length of the
-   * original sequence is preserved.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence
-   *   - 2: Term of sort Integer (index i)
-   *   - 3: Term of sort Sequence (replacement sequence t)
+   * Updates a sequence @f$s@f$ by replacing its context starting at an index
+   * with string @f$t@f$. If the start index is negative, the start index is
+   * greater than the length of the sequence, the result is @f$s@f$. Otherwise,
+   * the length of the original sequence is preserved.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of sequence Sort
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *   - `3:` Term of sequence Sort (replacement sequence @f$t@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_UPDATE,
   /**
    * Sequence element at.
-   * Returns the element at index i from a sequence s. If the index is negative
-   * or the index is greater or equal to the length of the sequence, the result
-   * is the empty sequence. Otherwise the result is a sequence of length 1.
    *
-   * Parameters:
-   *   - 1: Term of sequence sort (string s)
-   *   - 2: Term of sort Integer (index i)
+   * Returns the element at index @f$i@f$ from a sequence @f$s@f$. If the index
+   * is negative or the index is greater or equal to the length of the
+   * sequence, the result is the empty sequence. Otherwise the result is a
+   * sequence of length `1`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of sequence Sort
+   *   - `2:` Term of Sort Int (index @f$i@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_AT,
   /**
    * Sequence contains.
-   * Checks whether a sequence s1 contains another sequence s2. If s2 is empty,
-   * the result is always true.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (the sequence s1)
-   *   - 2: Term of sort Sequence (the sequence s2)
+   * Checks whether a sequence @f$s_1@f$ contains another sequence @f$s_2@f$.
+   * If @f$s_2@f$ is empty, the result is always `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `2`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_CONTAINS,
   /**
    * Sequence index-of.
-   * Returns the index of a subsequence s2 in a sequence s1 starting at index i.
-   * If the index is negative or greater than the length of sequence s1 or the
-   * subsequence s2 does not appear in sequence s1 after index i, the result is
-   * -1.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (subsequence s1)
-   *   - 2: Term of sort Sequence (subsequence s2)
-   *   - 3: Term of sort Integer (index i)
+   * Returns the index of a subsequence @f$s_2@f$ in a sequence @f$s_1@f$
+   * starting at index @f$i@f$. If the index is negative or greater than the
+   * length of sequence @f$s_1@f$ or the subsequence @f$s_2@f$ does not appear
+   * in sequence @f$s_1@f$ after index @f$i@f$, the result is `-1`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *   - `3:` Term of Sort Int (@f$i@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_INDEXOF,
   /**
    * Sequence replace.
-   * Replaces the first occurrence of a sequence s2 in a sequence s1 with
-   * sequence s3. If s2 does not appear in s1, s1 is returned unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (sequence s1)
-   *   - 2: Term of sort Sequence (sequence s2)
-   *   - 3: Term of sort Sequence (sequence s3)
+   * Replaces the first occurrence of a sequence @f$s_2@f$ in a
+   * sequence @f$s_1@f$ with sequence @f$s_3@f$. If @f$s_2@f$ does not
+   * appear in @f$s_1@f$, @f$s_1@f$ is returned unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *   - `3:` Term of sequence Sort (@f$s_3@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_REPLACE,
   /**
    * Sequence replace all.
-   * Replaces all occurrences of a sequence s2 in a sequence s1 with sequence
-   * s3. If s2 does not appear in s1, s1 is returned unmodified.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (sequence s1)
-   *   - 2: Term of sort Sequence (sequence s2)
-   *   - 3: Term of sort Sequence (sequence s3)
+   * Replaces all occurrences of a sequence @f$s_2@f$ in a sequence @f$s_1@f$
+   * with sequence @f$s_3@f$. If @f$s_2@f$ does not appear in @f$s_1@f$,
+   * sequence @f$s_1@f$ is returned unmodified.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `3`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *   - `3:` Term of sequence Sort (@f$s_3@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_REPLACE_ALL,
   /**
    * Sequence reverse.
    *
-   * Parameters:
-   *   - 1: Term of Sequence sort
+   * - Arity: `1`
+   *   - `1:` Term of sequence Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_REV,
   /**
    * Sequence prefix-of.
-   * Checks whether a sequence s1 is a prefix of sequence s2. If sequence s1 is
-   * empty, this operator returns true.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (sequence s1)
-   *   - 2: Term of sort Sequence (sequence s2)
+   * Checks whether a sequence @f$s_1@f$ is a prefix of sequence @f$s_2@f$. If
+   * sequence @f$s_1@f$ is empty, this operator returns `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `1`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_PREFIX,
   /**
    * Sequence suffix-of.
-   * Checks whether a sequence s1 is a suffix of sequence s2. If sequence s1 is
-   * empty, this operator returns true.
    *
-   * Parameters:
-   *   - 1: Term of sort Sequence (sequence s1)
-   *   - 2: Term of sort Sequence (sequence s2)
+   * Checks whether a sequence @f$s_1@f$ is a suffix of sequence @f$s_2@f$. If
+   * sequence @f$s_1@f$ is empty, this operator returns `true`.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Arity: `1`
+   *   - `1:` Term of sequence Sort (@f$s_1@f$)
+   *   - `2:` Term of sequence Sort (@f$s_2@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_SUFFIX,
   /**
    * Constant sequence.
    *
-   * Parameters:
-   *   - See @ref cvc5::api::Solver::mkEmptySequence() "mkEmptySequence()".
-   *
-   * Create with:
-   *   - `Solver::mkEmptySequence(const Sort& sort) const`
-   *
-   * Note that a constant sequence is a term that is equivalent to:
+   * A constant sequence is a term that is equivalent to:
+   * \rst
+   * .. code:: smtlib
    *
    *     (seq.++ (seq.unit c1) ... (seq.unit cn))
+   * \endrst
+   * where @f$n \leq 0@f$ and @f$c_1, ..., c_n@f$ are constants of some sort.
+   * The elements can be extracted with Term::getSequenceValue().
    *
-   * where n>=0 and c1, ..., cn are constants of some sort. The elements
-   * can be extracted by `Term::getSequenceValue()`.
+   * - Create Term of this Kind with:
+   *   - Solver::mkEmptySequence(const Sort&) const
    */
   CONST_SEQUENCE,
   /**
-   * Sequence unit, corresponding to a sequence of length one with the given
-   * term.
+   * Sequence unit.
    *
-   * Parameters:
-   *   - 1: Element term.
+   * Corresponds to a sequence of length one with the given term.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
+   * - Arity: `1`
+   *   - `1:` Term of any Sort (the element term)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_UNIT,
   /**
-   * Sequence nth, corresponding to the nth element of a sequence.
+   * Sequence nth.
    *
-   * Parameters:
-   *   - 1: Sequence term.
-   *   - 2: Integer term.
+   * Corresponds to the nth element of a sequence.
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+   * - Arity: `2`
+   *   - `1:` Term of sequence Sort
+   *   - `2:` Term of Sort Int (@f$n@f$)
+   *
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SEQ_NTH,
 
@@ -3313,129 +3991,161 @@ enum Kind : int32_t
   /**
    * Universally quantified formula.
    *
-   * Parameters:
-   *   - 1: VARIABLE_LIST Term
-   *   - 2: Quantifier body
-   *   - 3: (optional) INST_PATTERN_LIST Term
+   * - Arity: `3`
+   *   - `1:` Term of Kind #VARIABLE_LIST
+   *   - `2:` Term of Sort Bool (the quantifier body)
+   *   - `3:` (optional) Term of Kind #INST_PATTERN
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   FORALL,
   /**
    * Existentially quantified formula.
    *
-   * Parameters:
-   *   - 1: VARIABLE_LIST Term
-   *   - 2: Quantifier body
-   *   - 3: (optional) INST_PATTERN_LIST Term
+   * - Arity: `3`
+   *   - `1:` Term of Kind #VARIABLE_LIST
+   *   - `2:` Term of Sort Bool (the quantifier body)
+   *   - `3:` (optional) Term of Kind #INST_PATTERN
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   EXISTS,
   /**
+   * Variable list.
+   *
    * A list of variables (used to bind variables under a quantifier)
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms with kind VARIABLE
+   * - Arity: `n > 0`
+   *   - `1..n:` Terms of Kind #VARIABLE
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   VARIABLE_LIST,
   /**
-   * An instantiation pattern.
+   * Instantiation pattern.
+   *
    * Specifies a (list of) terms to be used as a pattern for quantifier
    * instantiation.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of any sort
+   * - Arity: `n > 0`
+   *   - `1..n:` Terms of any Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_PATTERN,
   /**
-   * An instantiation no-pattern.
+   * Instantiation no-pattern.
+   *
    * Specifies a (list of) terms that should not be used as a pattern for
    * quantifier instantiation.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms of any sort
+   * - Arity: `n > 0`
+   *   - `1..n:` Terms of any Sort
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_NO_PATTERN,
-  /*
-   * An instantiation pool.
+  /**
+   * Instantiation pool.
+   *
    * Specifies an annotation for pool based instantiation.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms that comprise the pools, which are one-to-one with the variables of the quantified formula to be instantiated.
+   * - Arity: `n > 0`
+   *   - `1..n:` Terms that comprise the pools, which are one-to-one with the
+   *             variables of the quantified formula to be instantiated
    *
-   * Create with:
-   *   - `mkTerm(Kind kind, Term child1, Term child2)`
-   *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)`
-   *   - `mkTerm(Kind kind, const std::vector<Term>& children)`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_POOL,
-  /*
+  /**
    * A instantantiation-add-to-pool annotation.
    *
-   * Parameters: n = 1
-   *   - 1: The pool to add to.
+   * - Arity: `1`
+   *   - `1:` The pool to add to.
    *
-   * Create with:
-   *   - `mkTerm(Kind kind, Term child)`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_ADD_TO_POOL,
-  /*
+  /**
    * A skolemization-add-to-pool annotation.
    *
-   * Parameters: n = 1
-   *   - 1: The pool to add to.
+   * - Arity: `1`
+   *   - `1:` The pool to add to.
    *
-   * Create with:
-   *   - `mkTerm(Kind kind, Term child)`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   SKOLEM_ADD_TO_POOL,
   /**
-   * An instantiation attribute
+   * Instantiation attribute.
+   *
    * Specifies a custom property for a quantified formula given by a
    * term that is ascribed a user attribute.
    *
-   * Parameters: n >= 1
-   *   - 1: The keyword of the attribute (a term with kind CONST_STRING).
-   *   - 2...n: The values of the attribute.
+   * - Arity: `n > 0`
+   *   - `1:` Term of Kind #CONST_STRING (the keyword of the attribute)
+   *   - `2...n:` Terms representing the values of the attribute
    *
-   * Create with:
-   *   - `mkTerm(Kind kind, Term child1, Term child2)`
-   *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)`
-   *   - `mkTerm(Kind kind, const std::vector<Term>& children)`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_ATTRIBUTE,
   /**
    * A list of instantiation patterns and/or attributes.
    *
-   * Parameters: n > 1
-   *   - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or INST_ATTRIBUTE.
+   * - Arity: `n > 1`
+   *   - `1..n:` Terms of Kind #INST_PATTERN, #INST_NO_PATTERN, or
+   *             #INST_ATTRIBUTE
    *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   * - Create Term of this Kind with:
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
    */
   INST_PATTERN_LIST,
 #if 0

diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java
index 47732b7ddb697d114fbd60d3d9010149207bd53c..f2e260eae56a9bc56d2938530de87fe423accfbd 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Datatype.java
+++ b/src/api/java/io/github/cvc5/api/Datatype.java
@@ -68,6 +68,8 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
    * This is a linear search through the constructors, so in case of multiple,
    * similarly-named constructors, the
    * first is returned.
+   * @param name the name of the datatype constructor
+   * @return a Term representing the datatype constructor with the given name
    */
   public Term getConstructorTerm(String name)
   {

diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
index 4a041dd992d3fc0d690b5189c9c213c85ca47449..f824ac121f23b2b43379bf7cb5b91559d1ccb94b 100644 (file)
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
@@ -107,7 +107,11 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
   }
   private native int getNumSelectors(long pointer);
 
-  /** @return the i^th DatatypeSelector. */
+  /**
+   * Get the DatatypeSelector at the given index
+   * @param index the given index i
+   * @return the i^th DatatypeSelector
+   */
   public DatatypeSelector getSelector(int index)
   {
     long selectorPointer = getSelector(pointer, index);

diff --git a/src/api/java/io/github/cvc5/api/DatatypeDecl.java b/src/api/java/io/github/cvc5/api/DatatypeDecl.java
index fb8da9abd1d2dde2aaf4d05375c8087607abaf0e..ddaca88df2dff2a07051547c217136cf2650e0b0 100644 (file)
--- a/src/api/java/io/github/cvc5/api/DatatypeDecl.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeDecl.java
@@ -50,7 +50,7 @@ public class DatatypeDecl extends AbstractPointer
 
   private native int getNumConstructors(long pointer);
 
-  /** Is this Datatype declaration parametric? */
+  /** @return true if this datatype is parametric */
   public boolean isParametric()
   {
     return isParametric(pointer);

diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java
index d222de78881eedea5d443e27a0a7f1bc62de5c51..7af2013fd40b6091dd4330a5008b347e038d4f07 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Result.java
+++ b/src/api/java/io/github/cvc5/api/Result.java
@@ -81,7 +81,7 @@ public class Result extends AbstractPointer
   }
 
   /**
-   * Return true if Result is empty, i.e., a nullary Result, and not an actual
+   * @return true if Result is empty, i.e., a nullary Result, and not an actual
    * result returned from a checkSat() (and friends) query.
    */
   public boolean isNull()
@@ -92,7 +92,7 @@ public class Result extends AbstractPointer
   private native boolean isNull(long pointer);
 
   /**
-   * Return true if query was a satisfiable checkSat() or checkSatAssuming()
+   * @return true if query was a satisfiable checkSat() or checkSatAssuming()
    * query.
    */
   public boolean isSat()
@@ -103,7 +103,7 @@ public class Result extends AbstractPointer
   private native boolean isSat(long pointer);
 
   /**
-   * Return true if query was an unsatisfiable checkSat() or
+   * @return true if query was an unsatisfiable checkSat() or
    * checkSatAssuming() query.
    */
   public boolean isUnsat()
@@ -114,7 +114,7 @@ public class Result extends AbstractPointer
   private native boolean isUnsat(long pointer);
 
   /**
-   * Return true if query was a checkSat() or checkSatAssuming() query and
+   * @return true if query was a checkSat() or checkSatAssuming() query and
    * cvc5 was not able to determine (un)satisfiability.
    */
   public boolean isUnknown() {

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 183d2de95fc7cccdec8b1ec8db9a6232f8dee66f..32b5c4adcd3618253a208f66b50fec6e7d9b4976 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -132,6 +132,7 @@ public class Solver implements IPointer, AutoCloseable
   private native long getRegExpSort(long pointer);
   /**
    * @return sort RoundingMode
+   * @throws CVC5ApiException
    */
   public Sort getRoundingModeSort() throws CVC5ApiException
   {
@@ -168,6 +169,7 @@ public class Solver implements IPointer, AutoCloseable
    * Create a bit-vector sort.
    * @param size the bit-width of the bit-vector sort
    * @return the bit-vector sort
+   * @throws CVC5ApiException
    */
   public Sort mkBitVectorSort(int size) throws CVC5ApiException
   {
@@ -182,6 +184,7 @@ public class Solver implements IPointer, AutoCloseable
    * Create a floating-point sort.
    * @param exp the bit-width of the exponent of the floating-point sort.
    * @param sig the bit-width of the significand of the floating-point sort.
+   * @throws CVC5ApiException
    */
   public Sort mkFloatingPointSort(int exp, int sig) throws CVC5ApiException
   {
@@ -198,6 +201,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param dtypedecl the datatype declaration from which the sort is
    *     created
    * @return the datatype sort
+   * @throws CVC5ApiException
    */
   public Sort mkDatatypeSort(DatatypeDecl dtypedecl) throws CVC5ApiException
   {
@@ -215,6 +219,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param dtypedecls the datatype declarations from which the sort is
    *     created
    * @return the datatype sorts
+   * @throws CVC5ApiException
    */
   public Sort[] mkDatatypeSorts(List<DatatypeDecl> dtypedecls) throws CVC5ApiException
   {
@@ -228,6 +233,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param dtypedecls the datatype declarations from which the sort is
    *     created
    * @return the datatype sorts
+   * @throws CVC5ApiException
    */
   public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls) throws CVC5ApiException
   {
@@ -260,6 +266,7 @@ public class Solver implements IPointer, AutoCloseable
    *     created
    * @param unresolvedSorts the set of unresolved sorts
    * @return the datatype sorts
+   * @throws CVC5ApiException
    */
   public List<Sort> mkDatatypeSorts(List<DatatypeDecl> dtypedecls, Set<Sort> unresolvedSorts)
       throws CVC5ApiException
@@ -429,6 +436,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param symbol the symbol of the sort
    * @param arity the number of sort parameters of the sort
    * @return the unresolved sort
+   * @throws CVC5ApiException
    */
   public Sort mkUnresolvedSort(String symbol, int arity) throws CVC5ApiException
   {
@@ -447,6 +455,7 @@ public class Solver implements IPointer, AutoCloseable
    *
    * @param symbol the symbol of the sort
    * @return the unresolved sort
+   * @throws CVC5ApiException
    */
   public Sort mkUnresolvedSort(String symbol) throws CVC5ApiException
   {
@@ -458,6 +467,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param symbol the symbol of the sort
    * @param arity the arity of the sort
    * @return the sort constructor sort
+   * @throws CVC5ApiException
    */
   public Sort mkSortConstructorSort(String symbol, int arity) throws CVC5ApiException
   {
@@ -719,6 +729,7 @@ public class Solver implements IPointer, AutoCloseable
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param arg the unsigned int argument to this operator
+   * @throws CVC5ApiException
    */
   public Op mkOp(Kind kind, int arg) throws CVC5ApiException
   {
@@ -741,6 +752,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param kind the kind of the operator
    * @param arg1 the first unsigned int argument to this operator
    * @param arg2 the second unsigned int argument to this operator
+   * @throws CVC5ApiException
    */
   public Op mkOp(Kind kind, int arg1, int arg2) throws CVC5ApiException
   {
@@ -758,6 +770,7 @@ public class Solver implements IPointer, AutoCloseable
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param args the arguments (indices) of the operator
+   * @throws CVC5ApiException
    */
   public Op mkOp(Kind kind, int[] args) throws CVC5ApiException
   {
@@ -822,6 +835,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123").
    * @return a constant of sort Integer assuming 's' represents an integer)
+   * @throws CVC5ApiException
    */
   public Term mkInteger(String s) throws CVC5ApiException
   {
@@ -849,6 +863,7 @@ public class Solver implements IPointer, AutoCloseable
    *          integer (e.g., "123") or real constant (e.g., "12.34" or
    * "12/34").
    * @return a constant of sort Real
+   * @throws CVC5ApiException
    */
   public Term mkReal(String s) throws CVC5ApiException
   {
@@ -1001,6 +1016,7 @@ public class Solver implements IPointer, AutoCloseable
    *     as
    * string
    * @return the String constant
+   * @throws CVC5ApiException
    */
   public Term mkString(int[] s) throws CVC5ApiException
   {
@@ -1055,6 +1071,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param size the bit-width of the bit-vector sort
    * @param val the value of the constant
    * @return the bit-vector constant
+   * @throws CVC5ApiException
    */
   public Term mkBitVector(int size, long val) throws CVC5ApiException
   {
@@ -1076,6 +1093,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param s the string representation of the constant
    * @param base the base of the string representation (2, 10, or 16)
    * @return the bit-vector constant
+   * @throws CVC5ApiException
    */
   public Term mkBitVector(int size, String s, int base) throws CVC5ApiException
   {
@@ -1107,6 +1125,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPointPosInf(int exp, int sig) throws CVC5ApiException
   {
@@ -1122,6 +1141,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPointNegInf(int exp, int sig) throws CVC5ApiException
   {
@@ -1137,6 +1157,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPointNaN(int exp, int sig) throws CVC5ApiException
   {
@@ -1153,6 +1174,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPointPosZero(int exp, int sig) throws CVC5ApiException
   {
@@ -1169,6 +1191,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPointNegZero(int exp, int sig) throws CVC5ApiException
   {
@@ -1197,6 +1220,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param exp Size of the exponent
    * @param sig Size of the significand
    * @param val Value of the floating-point constant as a bit-vector term
+   * @throws CVC5ApiException
    */
   public Term mkFloatingPoint(int exp, int sig, Term val) throws CVC5ApiException
   {
@@ -1213,6 +1237,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param sort the sort the cardinality constraint is for
    * @param upperBound the upper bound on the cardinality of the sort
    * @return the cardinality constraint
+   * @throws CVC5ApiException
    */
   public Term mkCardinalityConstraint(Sort sort, int upperBound) throws CVC5ApiException
   {
@@ -1533,6 +1558,7 @@ public class Solver implements IPointer, AutoCloseable
    * @param symbol the name of the sort
    * @param arity the arity of the sort
    * @return the sort
+   * @throws CVC5ApiException
    */
   public Sort declareSort(String symbol, int arity) throws CVC5ApiException
   {
@@ -2107,6 +2133,7 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    * ( pop <numeral> )
    * }
+   * @throws CVC5ApiException
    */
   public void pop() throws CVC5ApiException
   {
@@ -2120,6 +2147,7 @@ public class Solver implements IPointer, AutoCloseable
    * ( pop <numeral> )
    * }
    * @param nscopes the number of levels to pop
+   * @throws CVC5ApiException
    */
   public void pop(int nscopes) throws CVC5ApiException
   {
@@ -2315,6 +2343,7 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    * ( push <numeral> )
    * }
+   * @throws CVC5ApiException
    */
   public void push() throws CVC5ApiException
   {
@@ -2328,6 +2357,7 @@ public class Solver implements IPointer, AutoCloseable
    * ( push <numeral> )
    * }
    * @param nscopes the number of levels to push
+   * @throws CVC5ApiException
    */
   public void push(int nscopes) throws CVC5ApiException
   {
@@ -2359,6 +2389,7 @@ public class Solver implements IPointer, AutoCloseable
    * }
    * @param keyword the info flag
    * @param value the value of the info flag
+   * @throws CVC5ApiException
    */
   public void setInfo(String keyword, String value) throws CVC5ApiException
   {
@@ -2374,6 +2405,7 @@ public class Solver implements IPointer, AutoCloseable
    * ( set-logic <symbol> )
    * }
    * @param logic the logic to set
+   * @throws CVC5ApiException
    */
   public void setLogic(String logic) throws CVC5ApiException
   {

diff --git a/src/api/java/io/github/cvc5/api/SynthResult.java b/src/api/java/io/github/cvc5/api/SynthResult.java
index 7d9b5b6dd41e7c8b1f30790a9b19ca9f88ba22ff..fac196abfd7db51d845d4964926321a85bb7ddd2 100644 (file)
--- a/src/api/java/io/github/cvc5/api/SynthResult.java
+++ b/src/api/java/io/github/cvc5/api/SynthResult.java
@@ -36,7 +36,7 @@ public class SynthResult extends AbstractPointer
   // endregion
 
   /**
-   * Return true if SynthResult is empty, i.e., a nullary SynthResult, and not
+   * @return true if SynthResult is empty, i.e., a nullary SynthResult, and not
    * an actual result returned from a synthesis query.
    */
   public boolean isNull()
@@ -47,7 +47,7 @@ public class SynthResult extends AbstractPointer
   private native boolean isNull(long pointer);
 
   /**
-   * Return true if the synthesis query has a solution.
+   * @return true if the synthesis query has a solution.
    */
   public boolean hasSolution()
   {
@@ -57,7 +57,7 @@ public class SynthResult extends AbstractPointer
   private native boolean hasSolution(long pointer);
 
   /**
-   * Return true if the synthesis query has no solution. In this case, it was
+   * @return true if the synthesis query has no solution. In this case, it was
    * determined there was no solution.
    */
   public boolean hasNoSolution()
@@ -68,7 +68,7 @@ public class SynthResult extends AbstractPointer
   private native boolean hasNoSolution(long pointer);
 
   /**
-   * Return true if the result of the synthesis query could not be determined.
+   * @return true if the result of the synthesis query could not be determined.
    */
   public boolean isUnknown()
   {