From a57702d1f24ffa9f84a6e50887138a00a48dac07 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 1 Apr 2022 15:03:58 -0700 Subject: [PATCH] api kinds: Refactor docs for kinds to properly render in Python. (#8510) --- src/api/cpp/cvc5.h | 2 +- src/api/cpp/cvc5_kind.h | 2503 ++++++++++++++++++++++----------- src/api/python/genenums.py.in | 13 +- 3 files changed, 1688 insertions(+), 830 deletions(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 65337fc51..2ad9d41c2 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2032,7 +2032,7 @@ class CVC5_EXPORT DatatypeConstructor * (par (T) ((nil) (cons (head T) (tail (List T)))))) * \endverbatim * - * The type of nil terms need to be provided by the user. In SMT version 2.6, + * The type of nil terms must be provided by the user. In SMT version 2.6, * this is done via the syntax for qualified identifiers: * * \verbatim embed:rst:leading-asterisk diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index e8fe14a4b..464415372 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -33,12 +33,12 @@ namespace cvc5 { * \internal * * Note that the API type `cvc5::Kind` roughly corresponds to - * `cvc5::internal::Kind`, but is a different type. It hides internal kinds that should - * not be exported to the API, and maps all kinds that we want to export to its - * corresponding internal kinds. The underlying type of `cvc5::Kind` must - * be signed (to enable range checks for validity). The size of this type - * depends on the size of `cvc5::internal::Kind` (`NodeValue::NBITS_KIND`, currently 10 - * bits, see expr/node_value.h). + * `cvc5::internal::Kind`, but is a different type. It hides internal kinds + * that should not be exported to the API, and maps all kinds that we want to + * export to its corresponding internal kinds. The underlying type of + * `cvc5::Kind` must be signed (to enable range checks for validity). The size + * of this type depends on the size of `cvc5::internal::Kind` + * (`NodeValue::NBITS_KIND`, currently 10 bits, see expr/node_value.h). */ enum Kind : int32_t { @@ -49,13 +49,17 @@ enum Kind : int32_t * via the API but may appear in terms returned by API functions, e.g., * when querying the simplified form of a term. * - * @note Should never be created via the API. + * \rst + * .. note:: Should never be created via the API. + * \endrst */ INTERNAL_KIND = -2, /** * Undefined kind. * - * @note Should never be exposed or created via the API. + * \rst + * .. note:: Should never be exposed or created via the API. + * \endrst */ UNDEFINED_KIND = -1, /** @@ -63,8 +67,10 @@ enum Kind : int32_t * * The kind of a null term (Term::Term()). * - * @note May not be explicitly created via API functions other than - * Term::Term(). + * \rst + * .. note:: May not be explicitly created via API functions other than + * :cpp:func:`Term::Term()`. + * \endrst */ NULL_TERM, @@ -73,45 +79,57 @@ 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 and may not appear in - * assertions. + * \rst + * .. note:: May be returned as the result of an API call, but terms of this + * kind may not be created explicitly via the API and may not + * appear in assertions. + * \endrst */ UNINTERPRETED_SORT_VALUE, /** * Equality, chainable. * - * - Arity: `n > 1` - * - `1..n:` Terms of the same Sort + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of the same Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ EQUAL, /** * Disequality. * - * - Arity: `n > 1` - * - `1..n:` Terms of the same Sort + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of the same Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ DISTINCT, /** * Free constant symbol. * - * @note Not permitted in bindings (e.g., #FORALL, #EXISTS). + * \rst + * .. note:: Not permitted in bindings (e.g., :cpp:enumerator:`FORALL`, + * :cpp:enumerator:`EXISTS`). + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkConst(const Sort&, const std::string&) const * - Solver::mkConst(const Sort&) const */ @@ -119,23 +137,29 @@ enum Kind : int32_t /** * (Bound) variable. * - * @note Only permitted in bindings and in lambda and quantifier bodies. + * \rst + * .. note:: Only permitted in bindings and in lambda and quantifier bodies. + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkVar(const Sort&, const std::string&) const */ VARIABLE, /** * Symbolic expression. * - * - Arity: `n > 0` - * - `1..n:` Terms with same sorts + * - Arity: ``n > 0`` + * + * - ``1..n:`` Terms with same sorts * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -147,15 +171,18 @@ enum Kind : int32_t /** * Lambda expression. * - * - Arity: `2` - * - `1:` Term of kind #VARIABLE_LIST - * - `2:` Term of any Sort (the body of the lambda) + * - Arity: ``2`` + * + * - ``1:`` Term of kind :cpp:enumerator:`VARIABLE_LIST` + * - ``2:`` Term of any Sort (the body of the lambda) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ LAMBDA, @@ -169,52 +196,57 @@ enum Kind : int32_t * .. code:: smtlib * * (witness ((x S)) F) - * \endrst - * returns an element @f$x@f$ of Sort @f$S@f$ and asserts formula @f$F@f$. + * + * returns an element :math:`x` of Sort :math:`S` and asserts formula + * :math:`F`. * * The witness operator behaves like the description operator * (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: + * no :math:`x` that satisfies :math:`F`. But if such :math:`x` 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] + * .. math:: * - * For example, if there are two elements of Sort @f$S@f$ that satisfy - * formula @f$F@f$, then the following formula is satisfiable: + * \forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G + * + * For example, if there are two elements of Sort :math:`S` that satisfy + * formula :math:`F`, then the following formula is satisfiable: * - * \rst * .. code:: smtlib * * (distinct * (witness ((x Int)) F) * (witness ((x Int)) F)) + * + * .. 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 :math:`z`. * \endrst * - * @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`` * - * - 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 + * - ``1:`` Term of kind :cpp:enumerator:`VARIABLE_LIST` + * - ``2:`` Term of Sort Bool (the body of the witness) + * - ``3:`` (optional) Term of kind :cpp:enumerator:`INST_PATTERN`_LIST * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ WITNESS, @@ -225,6 +257,7 @@ enum Kind : int32_t * Boolean constant. * * - Create Term of this Kind with: + * * - Solver::mkTrue() const * - Solver::mkFalse() const * - Solver::mkBoolean(bool) const @@ -233,86 +266,104 @@ enum Kind : int32_t /** * Logical negation. * - * - Arity: `1` - * - `1:` Term of Sort Bool + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Bool * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ NOT, /** * Logical conjunction. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Bool + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Bool * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ AND, /** * Logical implication. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Bool + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Bool * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ IMPLIES, /** * Logical disjunction. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Bool + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Bool * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ OR, /** * Logical exclusive disjunction, left associative. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Bool + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Bool * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ XOR, /** * If-then-else. * - * - 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 + * - 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 * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ITE, @@ -322,26 +373,33 @@ enum Kind : int32_t /** * Application of an uninterpreted function. * - * - Arity: `n > 1` - * - `1:` Function Term - * - `2..n:` Function argument instantiation Terms of any first-class Sort + * - Arity: ``n > 1`` + * + * - ``1:`` Function Term + * - ``2..n:`` Function argument instantiation Terms of any first-class Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_UF, /** * Cardinality constraint on uninterpreted sort. * + * \rst * Interpreted as a predicate that is true when the cardinality of - * uinterpreted Sort @f$S@f$ is less than or equal to an upper bound. + * uinterpreted Sort :math:`S` is less than or equal to an upper bound. + * \endrst + * + * - Arity: ``0`` * - * - Arity: `0` * - Create Term of this Kind with: + * * - Solver::mkCardinalityConstraint(const Sort&, uint32_t) const * * \rst @@ -354,15 +412,18 @@ enum Kind : int32_t * Higher-order applicative encoding of function application, left * associative. * - * - Arity: `n = 2` - * - `1:` Function Term - * - `2:` Argument Term of the domain Sort of the function + * - Arity: ``n = 2`` + * + * - ``1:`` Function Term + * - ``2:`` Argument Term of the domain Sort of the function * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ HO_APPLY, @@ -372,388 +433,469 @@ enum Kind : int32_t /** * Arithmetic addition. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ADD, /** * Arithmetic multiplication. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ MULT, /** * Integer and. * - * Operator for bit-wise `AND` over integers, parameterized by a (positive) - * bit-width @f$k@f$. - * * \rst + * Operator for bit-wise ``AND`` over integers, parameterized by a (positive) + * bit-width :math:`k`. + * * .. code:: smtlib * * ((_ iand k) i_1 i_2) - * \endrst * is equivalent to - * \rst + * * .. code:: smtlib * * ((_ iand k) i_1 i_2) * (bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2))) - * \endrst - * for all integers `i_1`, `i_2`. + * for all integers ``i_1``, ``i_2``. + * + * - Arity: ``2`` + * + * - ``1..2:`` Terms of Sort Int * - * - Arity: `2` - * - `1..2:` Terms of Sort Int + * - Indices: ``1`` * - * - Indices: `1` - * - `1:` Bit-width @f$k@f$ + * - ``1:`` Bit-width :math:`k` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ IAND, /** * Power of two. * - * Operator for raising `2` to a non-negative integer power. + * Operator for raising ``2`` to a non-negative integer power. + * + * - Arity: ``1`` * - * - Arity: `1` - * - `1:` Term of Sort Int + * - ``1:`` Term of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ POW2, /** * Arithmetic subtraction, left associative. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SUB, /** * Arithmetic negation. * - * - Arity: `1` - * - `1:` Term of Sort Int or Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int or Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ NEG, /** * Real division, division by 0 undefined, left associative. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Real + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ DIVISION, /** * Integer division, division by 0 undefined, left associative. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INTS_DIVISION, /** * Integer modulus, modulus by 0 undefined. * - * - Arity: `2` - * - `1:` Term of Sort Int - * - `2:` Term of Sort Int + * - Arity: ``2`` + * + * - ``1:`` Term of Sort Int + * - ``2:`` Term of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INTS_MODULUS, /** * Absolute value. * - * - Arity: `1` - * - `1:` Term of Sort Int or Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int or Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ABS, /** * Arithmetic power. * - * - Arity: `2` - * - `1..2:` Term of Sort Int or Real (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Term of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ POW, /** * Exponential function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ EXPONENTIAL, /** * Sine function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SINE, /** * Cosine function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ COSINE, /** * Tangent function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ TANGENT, /** * Cosecant function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ COSECANT, /** * Secant function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SECANT, /** * Cotangent function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ COTANGENT, /** * Arc sine function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCSINE, /** * Arc cosine function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOSINE, /** * Arc tangent function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCTANGENT, /** * Arc cosecant function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOSECANT, /** * Arc secant function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCSECANT, /** * Arc cotangent function. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOTANGENT, /** * Square root. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SQRT, /** - * Operator for the divisibility-by-@f$k@f$ predicate. + * \rst + * Operator for the divisibility-by-:math:`k` predicate. + * + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int * - * - Arity: `1` - * - `1:` Term of Sort Int + * - Indices: ``1`` * - * - Indices: `1` - * - `1:` The integer @f$k@f$ to divide by. + * - ``1:`` The integer :math:`k` to divide by. + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ DIVISIBLE, @@ -761,6 +903,7 @@ enum Kind : int32_t * Multiple-precision rational constant. * * - Create Term of this Kind with: + * * - Solver::mkInteger(const std::string&) const * - Solver::mkInteger(int64_t) const * - Solver::mkReal(const std::string&) const @@ -771,108 +914,133 @@ enum Kind : int32_t /** * Less than, chainable. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ LT, /** * Less than or equal, chainable. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ LEQ, /** * Greater than, chainable. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ GT, /** * Greater than or equal, chainable. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort Int or Real (sorts must match) + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort Int or Real (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ GEQ, /** * Is-integer predicate. * - * - Arity: `1` - * - `1:` Term of Sort Int or Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int or Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ IS_INTEGER, /** * Convert Term of sort Int or Real to Int via the floor function. * - * - Arity: `1` - * - `1:` Term of Sort Int or Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int or Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ TO_INTEGER, /** * Convert Term of Sort Int or Real to Real. * - * - Arity: `1` - * - `1:` Term of Sort Int or Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int or Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ TO_REAL, /** * Pi constant. * - * @note #PI is considered a special symbol of Sort Real, but is not - * a Real value, i.e., Term::isRealValue() will return `false`. + * \rst + * .. note:: :cpp:enumerator:`PI` is considered a special symbol of Sort + * Real, but is not a Real value, i.e., + * :cpp:func:`Term::isRealValue()` will return ``false``. + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkPi() const */ PI, @@ -883,6 +1051,7 @@ enum Kind : int32_t * Fixed-size bit-vector constant. * * - Create Term of this Kind with: + * * - Solver::mkBitVector(uint32_t, uint64_t) const * - Solver::mkBitVector(uint32_t, const std::string&, uint32_t) const */ @@ -890,198 +1059,240 @@ enum Kind : int32_t /** * Concatenation of two or more bit-vectors. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_CONCAT, /** * Bit-wise and. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_AND, /** * Bit-wise or. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_OR, /** * Bit-wise xor. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_XOR, /** * Bit-wise negation. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NOT, /** * Bit-wise nand. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NAND, /** * Bit-wise nor. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NOR, /** * Bit-wise xnor, left associative. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_XNOR, /** - * Equality comparison (returns bit-vector of size `1`). + * Equality comparison (returns bit-vector of size ``1``). + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_COMP, /** * Multiplication of two or more bit-vectors. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_MULT, /** * Addition of two or more bit-vectors. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ADD, /** * Subtraction of two bit-vectors. * - * - Arity: `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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SUB, /** * Negation of a bit-vector (two's complement). * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NEG, /** * Unsigned bit-vector division. * - * Truncates towards `0`. If the divisor is zero, the result is all ones. + * Truncates towards ``0``. If the divisor is zero, the result is all ones. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UDIV, @@ -1091,14 +1302,17 @@ enum Kind : int32_t * Remainder from unsigned bit-vector division. If the modulus is zero, the * result is the dividend. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UREM, @@ -1109,14 +1323,17 @@ enum Kind : int32_t * 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. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SDIV, @@ -1126,14 +1343,17 @@ enum Kind : int32_t * 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. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SREM, @@ -1143,369 +1363,450 @@ enum Kind : int32_t * Two's complement signed remainder where the sign follows the divisor. If * the modulus is zero, the result is the dividend. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SMOD, /** * Bit-vector shift left. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SHL, /** * Bit-vector logical shift right. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_LSHR, /** * Bit-vector arithmetic shift right. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ASHR, /** * Bit-vector unsigned less than. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULT, /** * Bit-vector unsigned less than or equal. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULE, /** * Bit-vector unsigned greater than. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UGT, /** * Bit-vector unsigned greater than or equal. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UGE, /** * Bit-vector signed less than. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLT, /** * Bit-vector signed less than or equal. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLE, /** * Bit-vector signed greater than. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SGT, /** * Bit-vector signed greater than or equal. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SGE, /** * Bit-vector unsigned less than returning a bit-vector of size 1. * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULTBV, /** - * Bit-vector signed less than returning a bit-vector of size `1`. + * Bit-vector signed less than returning a bit-vector of size ``1``. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1..2:` Terms of bit-vector Sort (sorts must match) + * - ``1..2:`` Terms of bit-vector Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLTBV, /** * Bit-vector if-then-else. * - * Same semantics as regular ITE, but condition is bit-vector of size `1`. + * Same semantics as regular ITE, but condition is bit-vector of size ``1``. * - * - Arity: `3` - * - `1:` Term of bit-vector Sort of size `1` - * - `1..3:` Terms of bit-vector sort (sorts must match) + * - Arity: ``3`` + * + * - ``1:`` Term of bit-vector Sort of size `1` + * - ``1..3:`` Terms of bit-vector sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ITE, /** * Bit-vector redor. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REDOR, /** * Bit-vector redand. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REDAND, /** * Bit-vector extract. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `2` - * - `1:` The upper bit index. - * - `2:` The lower bit index. + * - Indices: ``2`` + * + * - ``1:`` The upper bit index. + * - ``2:`` The lower bit index. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_EXTRACT, /** * Bit-vector repeat. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `1` - * - `1:` The number of times to repeat the given term. + * - Indices: ``1`` + * + * - ``1:`` The number of times to repeat the given term. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REPEAT, /** * Bit-vector zero extension. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `1` - * - `1:` The number of zeroes to extend the given term with. + * - Indices: ``1`` + * + * - ``1:`` The number of zeroes to extend the given term with. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ZERO_EXTEND, /** * Bit-vector sign extension. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `1` - * - `1:` The number of bits (of the value of the sign bit) to extend - * the given term with. + * - Indices: ``1`` + * + * - ``1:`` The number of bits (of the value of the sign bit) to extend the given term with. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SIGN_EXTEND, /** * Bit-vector rotate left. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `1` - * - `1:` The number of bits to rotate the given term left. + * - Indices: ``1`` + * + * - ``1:`` The number of bits to rotate the given term left. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ROTATE_LEFT, /** * Bit-vector rotate right. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * - * - Indices: `1` - * - `1:` The number of bits to rotate the given term right. + * - Indices: ``1`` + * + * - ``1:`` The number of bits to rotate the given term right. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ROTATE_RIGHT, /** * Conversion from Int to bit-vector. * - * - Arity: `1` - * - `1:` Term of Sort Int + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int * - * - Indices: `1` - * - `1:` The size of the bit-vector to convert to. + * - Indices: ``1`` + * + * - ``1:`` The size of the bit-vector to convert to. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INT_TO_BITVECTOR, /** * Bit-vector conversion to (non-negative) integer. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bit-vector Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_TO_NAT, @@ -1517,507 +1818,615 @@ enum Kind : int32_t * of the floating-point value. * * - Create Term of this Kind with: - * - Term mkFloatingPoint(uint32_t, uint32_t, Term) const; + * + * - Solver::mkFloatingPoint(uint32_t, uint32_t, Term) const */ CONST_FLOATINGPOINT, /** * RoundingMode constant. * * - Create Term of this Kind with: + * * - Solver::mkRoundingMode(RoundingMode) const */ CONST_ROUNDINGMODE, /** * Create floating-point literal from bit-vector triple. * - * - 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) + * + * - 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_FP, /** * Floating-point equality. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_EQ, /** * Floating-point absolute value. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_ABS, /** * Floating-point negation. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_NEG, /** * Floating-point addition. * - * - Arity: `3` - * - `1:` Term of Sort RoundingMode - * - `2..3:` Terms of floating-point Sort (sorts must match) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2..3:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_ADD, /** * Floating-point sutraction. * - * - Arity: `3` - * - `1:` Term of Sort RoundingMode - * - `2..3:` Terms of floating-point Sort (sorts must match) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2..3:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_SUB, /** * Floating-point multiply. * - * - Arity: `3` - * - `1:` Term of Sort RoundingMode - * - `2..3:` Terms of floating-point Sort (sorts must match) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2..3:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MULT, /** * Floating-point division. * - * - Arity: `3` - * - `1:` Term of Sort RoundingMode - * - `2..3:` Terms of floating-point Sort (sorts must match) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2..3:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_DIV, /** * Floating-point fused multiply and add. * - * - Arity: `4` - * - `1:` Term of Sort RoundingMode - * - `2..4:` Terms of floating-point Sort (sorts must match) + * - Arity: ``4`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2..4:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_FMA, /** * Floating-point square root. * - * - Arity: `2` - * - `1:` Term of Sort RoundingMode - * - `2:` Term of floating-point Sort + * - Arity: ``2`` + * + * - ``1:`` Term of Sort RoundingMode + * - ``2:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_SQRT, /** * Floating-point remainder. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_REM, /** * Floating-point round to integral. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_RTI, /** * Floating-point minimum. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MIN, /** * Floating-point maximum. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MAX, /** * Floating-point less than or equal. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_LEQ, /** * Floating-point less than. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_LT, /** * Floating-point greater than or equal. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_GEQ, /** * Floating-point greater than. * - * - Arity: `2` - * - `1..2:` Terms of floating-point Sort (sorts must match) + * - Arity: ``2`` + * + * - ``1..2:`` Terms of floating-point Sort (sorts must match) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_GT, /** * Floating-point is normal tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NORMAL, /** * Floating-point is sub-normal tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_SUBNORMAL, /** * Floating-point is zero tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_ZERO, /** * Floating-point is infinite tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_INF, /** * Floating-point is NaN tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NAN, /** * Floating-point is negative tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NEG, /** * Floating-point is positive tester. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` + * + * - ``1:`` Term of floating-point Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_POS, /** * Conversion to floating-point from IEEE-754 bit-vector. * - * - Arity: `1` - * - `1:` Term of bit-vector Sort + * - Arity: ``1`` * - * - Indices: `2` - * - `1:` The exponent size - * - `2:` The significand size + * - ``1:`` Term of bit-vector Sort + * + * - Indices: ``2`` + * + * - ``1:`` The exponent size + * - ``2:`` The significand size * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_IEEE_BV, /** * Conversion to floating-point from floating-point. * - * - Arity: `2` - * - `1:` Term of Sort RoundingMode - * - `2:` Term of floating-point Sort + * - Arity: ``2`` * - * - Indices: `2` - * - `1:` The exponent size - * - `2:` The significand size + * - ``1:`` Term of Sort RoundingMode + * - ``2:`` Term of floating-point Sort + * + * - Indices: ``2`` + * + * - ``1:`` The exponent size + * - ``2:`` The significand size * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_FP, /** * Conversion to floating-point from Real. * - * - Arity: `2` - * - `1:` Term of Sort RoundingMode - * - `2:` Term of Sort Real + * - Arity: ``2`` * - * - Indices: `2` - * - `1:` The exponent size - * - `2:` The significand size + * - ``1:`` Term of Sort RoundingMode + * - ``2:`` Term of Sort Real + * + * - Indices: ``2`` + * + * - ``1:`` The exponent size + * - ``2:`` The significand size * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_REAL, /** * Conversion to floating-point from signed bit-vector. * - * - Arity: `2` - * - `1:` Term of Sort RoundingMode - * - `2:` Term of bit-vector Sort + * - Arity: ``2`` * - * - Indices: `2` - * - `1:` The exponent size - * - `2:` The significand size + * - ``1:`` Term of Sort RoundingMode + * - ``2:`` Term of bit-vector Sort + * + * - Indices: ``2`` + * + * - ``1:`` The exponent size + * - ``2:`` The significand size * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_SBV, /** * Conversion to floating-point from unsigned bit-vector. * - * - Arity: `2` - * - `1:` Term of Sort RoundingMode - * - `2:` Term of bit-vector Sort + * - Arity: ``2`` * - * - Indices: `2` - * - `1:` The exponent size - * - `2:` The significand size + * - ``1:`` Term of Sort RoundingMode + * - ``2:`` Term of bit-vector Sort + * + * - Indices: ``2`` + * + * - ``1:`` The exponent size + * - ``2:`` The significand size * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_UBV, /** * Conversion to unsigned bit-vector from floating-point. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` * - * - Indices: `1` - * - `1:` The size of the bit-vector to convert to. + * - ``1:`` Term of floating-point Sort + * + * - Indices: ``1`` + * + * - ``1:`` The size of the bit-vector to convert to. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_UBV, /** * Conversion to signed bit-vector from floating-point. * - * - Arity: `1` - * - `1:` Term of floating-point Sort + * - Arity: ``1`` * - * - Indices: `1` - * - `1:` The size of the bit-vector to convert to. + * - ``1:`` Term of floating-point Sort + * + * - Indices: ``1`` + * + * - ``1:`` The size of the bit-vector to convert to. * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_SBV, /** * Conversion to Real from floating-point. * - * - Arity: `1` - * - `1:` Term of Sort Real + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Real * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_REAL, @@ -2027,73 +2436,87 @@ enum Kind : int32_t /** * Array select. * - * - Arity: `2` - * - `1:` Term of array Sort - * - `2:` Term of array index Sort + * - Arity: ``2`` + * + * - ``1:`` Term of array Sort + * - ``2:`` Term of array index Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SELECT, /** * Array store. * - * - Arity: `3` - * - `1:` Term of array Sort - * - `2:` Term of array index Sort - * - `3:` Term of array element Sort + * - Arity: ``3`` + * + * - ``1:`` Term of array Sort + * - ``2:`` Term of array index Sort + * - ``3:`` Term of array element Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STORE, /** * Constant array. * - * - Arity: `2` - * - `1:` Term of array Sort - * - `2:` Term of array element Sort (value) + * - Arity: ``2`` + * + * - ``1:`` Term of array Sort + * - ``2:`` Term of array element Sort (value) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ CONST_ARRAY, /** - * Equality over arrays @f$a@f$ and @f$b@f$ over a given range @f$[i,j]@f$, - * i.e., - * @f[ + * \rst + * Equality over arrays :math:`a` and :math:`b` over a given range + * :math:`[i,j]`, i.e., + * + * .. math:: + * * \forall k . i \leq k \leq j \Rightarrow a[k] = b[k] - * @f] * - * @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`. - * \endverbatim + * .. note:: We currently support the creation of array equalities over index + * Sorts bit-vector, floating-point, Int and Real. + * Requires to enable option + * :ref:`arrays-exp`. + * \endrst + * + * - Arity: ``4`` * - * - 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) + * - ``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&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2108,111 +2531,121 @@ enum Kind : int32_t /** * Datatype constructor application. * - * - Arity: `n > 0` - * - `1:` DatatypeConstructor Term - * (see DatatypeConstructor::getConstructorTerm() const) - * - `2..n:` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor) + * - Arity: ``n > 0`` + * + * - ``1:`` DatatypeConstructor Term (see DatatypeConstructor::getConstructorTerm() const) + * - ``2..n:`` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_CONSTRUCTOR, /** * Datatype selector application. * - * @note Undefined if misapplied. + * \rst + * .. note:: Undefined if misapplied. + * \endrst + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` DatatypeSelector Term - * (see DatatypeSelector::getSelectorTerm() const, - * DatatypeConstructor::getSelectorTerm(const std::string&) const) - * - `2:` Term of the codomain Sort of the selector + * - ``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&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_SELECTOR, /** * Datatype tester application. * - * - Arity: `2` - * - `1:` Datatype tester Term - * (see DatatypeConstructor::getTesterTerm() const) - * - `2:` Term of Datatype Sort (DatatypeConstructor must belong to this - * Datatype Sort) + * - Arity: ``2`` + * + * - ``1:`` Datatype tester Term (see DatatypeConstructor::getTesterTerm() const) + * - ``2:`` Term of Datatype Sort (DatatypeConstructor must belong to this Datatype Sort) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_TESTER, /** * Datatype update application. * - * @note Does not change the datatype argument if misapplied. + * \rst + * .. note:: Does not change the datatype argument if misapplied. + * \endrst + * + * - Arity: ``3`` * - * - 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) + * - ``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&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_UPDATER, /** * Match expression. - + * * This kind is primarily used in the parser to support the - * SMT-LIBv2 `match` expression. + * SMT-LIBv2 ``match`` expression. * * For example, the SMT-LIBv2 syntax for the following match term * \rst * .. code:: smtlib * * (match l (((cons h t) h) (nil 0))) - * \endrst * is represented by the AST * - * \rst * .. code:: lisp * * (MATCH l * (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h) * (MATCH_CASE nil 0)) - * \endrst * - * 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. + * Terms of kind :cpp:enumerator:`MATCH_CASE` are constant case expressions, + * which are used for nullary constructors. Kind + * :cpp:enumerator:`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. + * + * - Arity: ``n > 1`` * - * - Arity: `n > 1` - * - `1..n:` Terms of kind #MATCH_CASE and #MATCH_BIND_CASE + * - ``1..n:`` Terms of kind :cpp:enumerator:`MATCH_CASE` and :cpp:enumerator:`MATCH_BIND_CASE` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ MATCH, @@ -2221,15 +2654,21 @@ enum Kind : int32_t * * A (constant) case expression to be used within a match expression. * - * - Arity: `2` - * - `1:` Term of kind #APPLY_CONSTRUCTOR (the pattern to match against) - * - `2:` Term of any Sort (the term the match term evaluates to) + * \rst + * - Arity: ``2`` + * + * - ``1:`` Term of kind :cpp:enumerator:`APPLY_CONSTRUCTOR` (the pattern to match against) + * - ``2:`` Term of any Sort (the term the match term evaluates to) + * + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ MATCH_CASE, @@ -2239,25 +2678,29 @@ enum Kind : int32_t * * A (non-constant) case expression to be used within a match expression. * - * - Arity: `3` + * \rst + * - 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) + * + * - ``1:`` Term of kind :cpp:enumerator:`VARIABLE_LIST` (containing the free variable of the case) + * - ``2:`` Term of kind :cpp:enumerator:`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 match term evaluates to) + * + * - ``1:`` Term of kind :cpp:enumerator:`VARIABLE_LIST` (containing the free variable of the case) + * - ``2:`` Term of kind :cpp:enumerator:`APPLY_CONSTRUCTOR` (the pattern expression, applying the set of variables to the constructor) + * - ``3:`` Term of any Sort (the term the match term evaluates to) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ MATCH_BIND_CASE, @@ -2280,16 +2723,20 @@ enum Kind : int32_t * (tuple 20 30 30 40 20) * \endrst * - * - Arity: `1` - * - `1:` Term of tuple Sort + * - Arity: ``1`` + * + * - ``1:`` Term of tuple Sort * - * - Indices: `n` - * - `1..n:` The tuple indices to project + * - Indices: ``n`` + * + * - ``1..n:`` The tuple indices to project * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ TUPLE_PROJECT, @@ -2300,6 +2747,7 @@ enum Kind : int32_t * Separation logic nil. * * - Create Term of this Kind with: + * * - Solver::mkSepNil(const Sort&) const * * \rst @@ -2312,6 +2760,7 @@ enum Kind : int32_t * Separation logic empty heap. * * - Create Term of this Kind with: + * * - Solver::mkSepEmp() const * * \rst @@ -2323,15 +2772,18 @@ enum Kind : int32_t /** * Separation logic points-to relation. * - * - Arity: `2` - * - `1:` Term denoting the location of the points-to constraint - * - `2:` Term denoting the 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2343,15 +2795,18 @@ enum Kind : int32_t /** * Separation logic star. * - * - Arity: `n > 1` - * - `1..n:` Terms of sort Bool (the 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2363,17 +2818,20 @@ enum Kind : int32_t /** * Separation logic magic wand. * - * - 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, + * - 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2389,48 +2847,58 @@ enum Kind : int32_t * Empty set. * * - Create Term of this Kind with: + * * - Solver::mkEmptySet(const Sort&) const */ SET_EMPTY, /** * Set union. * - * - Arity: `2` - * - `1..2:` Terms of set Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_UNION, /** * Set intersection. * - * - Arity: `2` - * - `1..2:` Terms of set Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_INTER, /** * Set subtraction. * - * - Arity: `2` - * - `1..2:` Terms of set Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_MINUS, @@ -2439,14 +2907,17 @@ enum Kind : int32_t * * Determines if the first set is a subset of the second set. * - * - Arity: `2` - * - `1..2:` Terms of set Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_SUBSET, @@ -2455,16 +2926,18 @@ enum Kind : int32_t * * Determines if the given set element is a member of the second set. * - * - Arity: `2` - * - `1:` Term of any Sort (must match the element Sort of the - * given set Term) - * - `2:` Term of set Sort + * - 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&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_MEMBER, @@ -2474,58 +2947,69 @@ enum Kind : int32_t * Construct a singleton set from an element given as a parameter. * The returned set has the same Sort as the element. * - * - Arity: `1` - * - `1:` Term of any Sort (the set element) + * - Arity: ``1`` + * + * - ``1:`` Term of any Sort (the set element) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_SINGLETON, /** * The set obtained by inserting elements; * - * - 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 + * - 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_INSERT, /** * Set cardinality. * - * - Arity: `1` - * - `1:` Term of set Sort + * - Arity: ``1`` + * + * - ``1:`` Term of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_CARD, /** * Set complement with respect to finite universe. * - * - Arity: `1` - * - `1:` Term of set Sort + * - Arity: ``1`` + * + * - ``1:`` Term of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SET_COMPLEMENT, @@ -2534,39 +3018,49 @@ enum Kind : int32_t * * All set variables must be interpreted as subsets of it. * - * @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`. + * \rst + * .. note:: :cpp:enumerator:`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``. + * \endrst * * - Create Op of this kind with: + * * - Solver::mkUniverseSet(const Sort&) const */ SET_UNIVERSE, /** * Set comprehension * - * 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 + * \rst + * A set comprehension is specified by a variable list :math:`x_1 ... x_n`, + * a predicate :math:`P[x_1...x_n]`, and a term :math:`t[x_1...x_n]`. A + * comprehension :math:`C` with the above form has members given by the * following semantics: - * @f[ + * + * .. math:: + * * \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 @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. + * \Leftrightarrow (set.member \; y \; C) + * + * where :math:`y` ranges over the element Sort of the (set) Sort of the + * comprehension. If :math:`t[x_1..x_n]` is not provided, it is equivalent + * to :math:`y` in the above formula. + * + * - Arity: ``3`` * - * - 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 + * - ``1:`` Term of Kind :cpp:enumerator:`VARIABLE_LIST` + * - ``2:`` Term of sort Bool (the predicate of the comprehension) + * - ``3:`` (optional) Term denoting the generator for the comprehension + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2578,19 +3072,24 @@ enum Kind : int32_t /** * Set choose. * - * 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$. + * \rst + * Select an element from a given set. For a set :math:`A = \{x\}`, the term + * (set.choose :math:`A`) is equivalent to the term :math:`x_1`. For an empty + * set, it is an arbitrary value. For a set with cardinality > 1, it will + * deterministically return an element in :math:`A`. + * \endrst + * + * - Arity: ``1`` * - * - Arity: `1` - * - `1:` Term of set Sort + * - ``1:`` Term of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2602,14 +3101,17 @@ enum Kind : int32_t /** * Set is singleton tester. * - * - Arity: `1` - * - `1:` Term of set Sort + * - Arity: ``1`` + * + * - ``1:`` Term of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2621,20 +3123,25 @@ enum Kind : int32_t /** * Set map. * + * \rst * 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$). + * Sort :math:`(\rightarrow S_1 \; S_2)`, to every element of the second + * argument, a set of Sort (Set :math:`S_1`), and returns a set of Sort + * (Set :math:`S_2`). * - * - Arity: `2` - * - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$ - * - `2:` Term of set Sort (Set @f$S_1@f$) + * - Arity: ``2`` + * + * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2)` + * - ``2:`` Term of set Sort (Set :math:`S_1`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2649,70 +3156,85 @@ enum Kind : int32_t /** * Relation join. * - * - Arity: `2` - * - `1..2:` Terms of relation Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_JOIN, /** * Relation cartesian product. * - * - Arity: `2` - * - `1..2:` Terms of relation Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_PRODUCT, /** * Relation transpose. * - * - Arity: `1` - * - `1:` Term of relation Sort + * - Arity: ``1`` + * + * - ``1:`` Term of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_TRANSPOSE, /** * Relation transitive closure. * - * - Arity: `1` - * - `1:` Term of relation Sort + * - Arity: ``1`` + * + * - ``1:`` Term of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_TCLOSURE, /** * Relation join image. * - * - Arity: `2` - * - `1..2:` Terms of relation Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2724,14 +3246,17 @@ enum Kind : int32_t /** * Relation identity. * - * - Arity: `1` - * - `1:` Term of relation Sort + * - Arity: ``1`` + * + * - ``1:`` Term of relation Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2747,48 +3272,58 @@ enum Kind : int32_t * Empty bag. * * - Create Term of this Kind with: + * * - Solver::mkEmptyBag(const Sort&) const */ BAG_EMPTY, /** * Bag max union. * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_UNION_MAX, /** * Bag disjoint union (sum). * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_UNION_DISJOINT, /** * Bag intersection (min). * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_INTER_MIN, @@ -2797,14 +3332,17 @@ enum Kind : int32_t * * Subtracts multiplicities of the second from the first. * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_DIFFERENCE_SUBTRACT, @@ -2813,14 +3351,17 @@ enum Kind : int32_t * * Removes shared elements in the two bags. * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_DIFFERENCE_REMOVE, @@ -2830,24 +3371,25 @@ enum Kind : int32_t * Determine if multiplicities of the first bag are less than or equal to * multiplicities of the second bag. * - * - Arity: `2` - * - `1..2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_SUBBAG, /** * Bag element multiplicity. * - * Parameters: - * - 1..2: Terms of bag sort (Bag E), [1] an element of sort E - * * Create with: + * * - Solver::mkTerm(Kind, const Term&, const Term&) const * - Solver::mkTerm(Kind, const std::vector&) const */ @@ -2855,16 +3397,18 @@ enum Kind : int32_t /** * Bag membership predicate. * - * - Arity: `2` - * - `1:` Term of any Sort (must match the element Sort of the - * given bag Term) - * - `2:` Terms of bag Sort + * - Arity: ``2`` + * + * - ``1:`` Term of any Sort (must match the element Sort of the given bag Term) + * - ``2:`` Terms of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_MEMBER, @@ -2874,14 +3418,17 @@ enum Kind : int32_t * Eliminate duplicates in a given bag. The returned bag contains exactly the * same elements in the given bag, but with multiplicity one. * - * - Arity: `1` - * - `1:` Term of bag Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2895,29 +3442,35 @@ enum Kind : int32_t * * Construct a bag with the given element and given multiplicity. * - * - Arity: `2` - * - `1:` Term of any Sort (the bag element) - * - `2:` Term of Sort Int (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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ BAG_MAKE, /** * Bag cardinality. * - * - Arity: `1` - * - `1:` Term of bag Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2931,19 +3484,24 @@ enum Kind : int32_t * * Select an element from a given bag. * - * 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$. + * \rst + * For a bag :math:`A = \{(x,n)\}` where :math:`n` is the multiplicity, then + * the term (choose :math:`A`) is equivalent to the term :math:`x`. For an + * empty bag, then it is an arbitrary value. For a bag that contains distinct + * elements, it will deterministically return an element in :math:`A`. + * \endrst + * + * - Arity: ``1`` * - * - Arity: `1` - * - `1:` Term of bag Sort + * - ``1:`` Term of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2955,14 +3513,17 @@ enum Kind : int32_t /** * Bag is singleton tester. * - * - Arity: `1` - * - `1:` Term of bag Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2974,14 +3535,17 @@ enum Kind : int32_t /** * Conversion from set to bag. * - * - Arity: `1` - * - `1:` Term of set Sort + * - Arity: ``1`` + * + * - ``1:`` Term of set Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -2993,14 +3557,17 @@ enum Kind : int32_t /** * Conversion from bag to set. * - * - Arity: `1` - * - `1:` Term of bag Sort + * - Arity: ``1`` + * + * - ``1:`` Term of bag Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -3012,20 +3579,25 @@ enum Kind : int32_t /** * Bag map. * + * \rst * 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$). + * Sort :math:`(\rightarrow S_1 \; S_2)`, to every element of the second + * argument, a set of Sort (Bag :math:`S_1`), and returns a set of Sort + * (Bag :math:`S_2`). * - * - Arity: `2` - * - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$ - * - `2:` Term of bag Sort (Bag @f$S_1@f$) + * - Arity: ``2`` + * + * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2)` + * - ``2:`` Term of bag Sort (Bag :math:`S_1`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -3037,22 +3609,27 @@ enum Kind : int32_t /** * Bag filter. * + * \rst * 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. + * (bag.filter :math:`p \; B`) takes a predicate :math:`p` of Sort + * :math:`(\rightarrow S_1 \; S_2)` as a first argument, and a bag :math:`B` + * of Sort (Bag :math:`S`) as a second argument, and returns a subbag of Sort + * (Bag :math:`T`) that includes all elements of :math:`B` that satisfy + * :math:`p` with the same multiplicity. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of function Sort @f$(\rightarrow S_1 \; S_2)@f$ - * - `2:` Term of bag Sort (Bag @f$S_1@f$) + * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2)` + * - ``2:`` Term of bag Sort (Bag :math:`S_1`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -3064,20 +3641,25 @@ enum Kind : int32_t /** * Bag fold. * + * \rst * 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$. + * (bag.fold :math:`f \; t \; B`) folds the elements of bag :math:`B` + * starting with Term :math:`t` and using the combining function :math:`f`. + * + * - Arity: ``2`` * - * - 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$) + * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2 \; S_2)` + * - ``2:`` Term of Sort :math:`S_2` (the initial value) + * - ``3:`` Term of bag Sort (Bag :math:`S_1`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -3089,14 +3671,17 @@ enum Kind : int32_t /** * Table cross product. * - * - Arity: `2` - * - `1..2:` Terms of table Sort + * - Arity: ``2`` + * + * - ``1..2:`` Terms of table Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -3111,286 +3696,355 @@ enum Kind : int32_t /** * String concat. * - * - Arity: `n > 1` - * - `1..n:` Terms of Sort String + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CONCAT, /** * String membership. * - * - Arity: `2` - * - `1:` Term of Sort String - * - `2:` Term of Sort RegLan + * - Arity: ``2`` + * + * - ``1:`` Term of Sort String + * - ``2:`` Term of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_IN_REGEXP, /** * String length. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LENGTH, /** * String substring. * - * 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 + * \rst + * Extracts a substring, starting at index :math:`i` and of length :math:`l`, + * from a string :math:`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. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort String + * - ``2:`` Term of Sort Int (index :math:`i`) + * - ``3:`` Term of Sort Int (length :math:`l`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_SUBSTR, /** * String update. * - * 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, + * \rst + * Updates a string :math:`s` by replacing its context starting at an index + * with string :math:`t`. If the start index is negative, the start index is + * greater than the length of the string, the result is :math:`s`. Otherwise, * the length of the original string is preserved. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort String + * - ``2:`` Term of Sort Int (index :math:`i`) + * - ``3:`` Term of Sort Strong (replacement string :math:`t`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_UPDATE, /** * String character at. * - * 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$. + * \rst + * Returns the character at index :math:`i` from a string :math:`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. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of Sort String (string @f$s@f$) - * - `2:` Term of Sort Int (index @f$i@f$) + * - ``1:`` Term of Sort String (string :math:`s`) + * - ``2:`` Term of Sort Int (index :math:`i`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CHARAT, /** * String contains. * - * 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`. + * \rst + * Determines whether a string :math:`s_1` contains another string + * :math:`s_2`. If :math:`s_2` is empty, the result is always ``true``. * - * - Arity: `2` - * - `1:` Term of Sort String (the string @f$s_1@f$) - * - `2:` Term of Sort String (the string @f$s_2@f$) + * - Arity: ``2`` + * + * - ``1:`` Term of Sort String (the string :math:`s_1`) + * - ``2:`` Term of Sort String (the string :math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CONTAINS, /** * String index-of. * - * 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`. + * \rst + * Returns the index of a substring :math:`s_2` in a string :math:`s_1` + * starting at index :math:`i`. If the index is negative or greater than the + * length of string :math:`s_1` or the substring :math:`s_2` does not appear + * in string :math:`s_1` after index :math:`i`, the result is -1. * - * - 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$) + * - Arity: ``2`` + * + * - ``1:`` Term of Sort String (substring :math:`s_1`) + * - ``2:`` Term of Sort String (substring :math:`s_2`) + * - ``3:`` Term of Sort Int (index :math:`i`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_INDEXOF, /** * String index-of regular expression match. * - * 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`. + * \rst + * Returns the first match of a regular expression :math:`r` in a + * string :math:`s`. If the index is negative or greater than the length of + * string :math:`s_1`, or :math:`r` does not match a substring in :math:`s` + * after index :math:`i`, the result is -1. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of Sort String (string :math:`s`) + * - ``2:`` Term of Sort RegLan (regular expression :math:`r`) + * - ``3:`` Term of Sort Int (index :math:`i`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_INDEXOF_RE, /** * String replace. * - * 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. + * \rst + * Replaces a string :math:`s_2` in a string :math:`s_1` with string + * :math:`s_3`. If :math:`s_2` does not appear in :math:`s_1`, :math:`s_1` is + * returned unmodified. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort String (string :math:`s_1`) + * - ``2:`` Term of Sort String (string :math:`s_2`) + * - ``3:`` Term of Sort String (string :math:`s_3`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE, /** * String replace all. * - * 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. + * \rst + * Replaces all occurrences of a string :math:`s_2` in a string :math:`s_1` + * with string :math:`s_3`. If :math:`s_2` does not appear in :math:`s_1`, + * :math:`s_1` is returned unmodified. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort String (:math:`s_2`) + * - ``3:`` Term of Sort String (:math:`s_3`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_ALL, /** * String replace regular expression match. * - * 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. + * \rst + * Replaces the first match of a regular expression :math:`r` in + * string :math:`s_1` with string :math:`s_2`. If :math:`r` does not match a + * substring of :math:`s_1`, :math:`s_1` is returned unmodified. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort RegLan + * - ``3:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_RE, /** * String replace all regular expression matches. * - * 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. + * \rst + * Replaces all matches of a regular expression :math:`r` in string + * :math:`s_1` with string :math:`s_2`. If :math:`r` does not match a + * substring of :math:`s_1`, string :math:`s_1` is returned unmodified. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort RegLan + * - ``3:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_RE_ALL, /** * String to lower case. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_LOWER, /** * String to upper case. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_UPPER, /** * String reverse. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REV, @@ -3400,14 +4054,17 @@ enum Kind : int32_t * Returns the code point of a string if it has length one, or returns `-1` * otherwise. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_CODE, @@ -3418,102 +4075,129 @@ enum Kind : int32_t * the argument to this function, or the empty string if the argument is * out-of-bounds. * - * - Arity: `1` - * - `1:` Term of Sort Int + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_FROM_CODE, /** * String less than. * - * Returns true if string @f$s_1@f$ is (strictly) less than @f$s_2@f$ based - * on a lexiographic ordering over code points. + * \rst + * Returns true if string :math:`s_1` is (strictly) less than :math:`s_2` + * based on a lexiographic ordering over code points. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of Sort String (@f$s_1@f$) - * - `2:` Term of Sort String (@f$s_2@f$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LT, /** * String less than or equal. * - * 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. + * \rst + * Returns true if string :math:`s_1` is less than or equal to :math:`s_2` + * based on a lexiographic ordering over code points. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of Sort String (@f$s_1@f$) - * - `2:` Term of Sort String (@f$s_2@f$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LEQ, /** * String prefix-of. * - * 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`. + * \rst + * Determines whether a string :math:`s_1` is a prefix of string :math:`s_2`. + * If string s1 is empty, this operator returns ``true``. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of Sort String (@f$s_1@f$) - * - `2:` Term of Sort String (@f$s_2@f$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_PREFIX, /** * String suffix-of. * - * 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`. + * \rst + * Determines whether a string :math:`s_1` is a suffix of the second string. + * If string :math:`s_1` is empty, this operator returns ``true``. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of Sort String (@f$s_1@f$) - * - `2:` Term of Sort String (@f$s_2@f$) + * - ``1:`` Term of Sort String (:math:`s_1`) + * - ``2:`` Term of Sort String (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_SUFFIX, /** * String is-digit. * - * Returns true if given string is a digit (it is one of `"0"`, ..., `"9"`). + * Returns true if given string is a digit (it is one of ``"0"``, ..., + * ``"9"``). + * + * - Arity: ``1`` * - * - Arity: `1` - * - `1:` Term of Sort String + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_IS_DIGIT, @@ -3522,14 +4206,17 @@ enum Kind : int32_t * * If the integer is negative this operator returns the empty string. * - * - Arity: `1` - * - `1:` Term of Sort Int + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_FROM_INT, @@ -3539,14 +4226,17 @@ enum Kind : int32_t * If the string does not contain an integer or the integer is negative, the * operator returns `-1`. * - * - Arity: `1` - * - `1:` Term of Sort Int + * - Arity: ``1`` + * + * - ``1:`` Term of Sort Int * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_INT, @@ -3554,6 +4244,7 @@ enum Kind : int32_t * Constant string. * * - Create Term of this Kind with: + * * - Solver::mkString(const std::string&, bool) const * - Solver::mkString(const std::wstring&) const */ @@ -3561,143 +4252,174 @@ enum Kind : int32_t /** * Conversion from string to regexp. * - * - Arity: `1` - * - `1:` Term of Sort String + * - Arity: ``1`` + * + * - ``1:`` Term of Sort String * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_REGEXP, /** * Regular expression concatenation. * - * - Arity: `2` - * - `1..2:` Terms of Sort RegLan + * - Arity: ``2`` + * + * - ``1..2:`` Terms of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_CONCAT, /** * Regular expression union. * - * - Arity: `2` - * - `1..2:` Terms of Sort RegLan + * - Arity: ``2`` + * + * - ``1..2:`` Terms of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_UNION, /** * Regular expression intersection. * - * - Arity: `2` - * - `1..2:` Terms of Sort RegLan + * - Arity: ``2`` + * + * - ``1..2:`` Terms of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_INTER, /** * Regular expression difference. * - * - Arity: `2` - * - `1..2:` Terms of Sort RegLan + * - Arity: ``2`` + * + * - ``1..2:`` Terms of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_DIFF, /** * Regular expression \*. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_STAR, /** * Regular expression +. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_PLUS, /** * Regular expression ?. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_OPT, /** * Regular expression 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) + * - 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_RANGE, /** * Operator for regular expression repeat. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan + * + * - Indices: ``1`` * - * - Indices: `1` - * - `1:` The number of repetitions + * - ``1:`` The number of repetitions * * - Create Term of this Kind with: + * * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_REPEAT, @@ -3707,18 +4429,22 @@ enum Kind : int32_t * Regular expression loop from lower bound to upper bound number of * repetitions. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan * - * - Indices: `1` - * - `1:` The lower bound - * - `2:` The upper bound + * - Indices: ``1`` + * + * - ``1:`` The lower bound + * - ``2:`` The upper bound * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_LOOP, @@ -3726,6 +4452,7 @@ enum Kind : int32_t * Regular expression none. * * - Create Term of this Kind with: + * * - Solver::mkRegexpNone() const */ REGEXP_NONE, @@ -3733,6 +4460,7 @@ enum Kind : int32_t * Regular expression all. * * - Create Term of this Kind with: + * * - Solver::mkRegexpAll() const */ REGEXP_ALL, @@ -3740,20 +4468,24 @@ enum Kind : int32_t * Regular expression all characters. * * - Create Term of this Kind with: + * * - Solver::mkRegexpAllchar() const */ REGEXP_ALLCHAR, /** * Regular expression complement. * - * - Arity: `1` - * - `1:` Term of Sort RegLan + * - Arity: ``1`` + * + * - ``1:`` Term of Sort RegLan * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_COMPLEMENT, @@ -3761,219 +4493,273 @@ enum Kind : int32_t /** * Sequence concat. * - * - Arity: `n > 1` - * - `1..n:` Terms of sequence Sort + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of sequence Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_CONCAT, /** * Sequence length. * - * - Arity: `1` - * - `1:` Term of sequence Sort + * - Arity: ``1`` + * + * - ``1:`` Term of sequence Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_LENGTH, /** * Sequence extract. * - * 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 + * \rst + * Extracts a subsequence, starting at index :math:`i` and of length :math:`l`, + * from a sequence :math:`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. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of sequence Sort + * - ``2:`` Term of Sort Int (index :math:`i`) + * - ``3:`` Term of Sort Int (length :math:`l`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_EXTRACT, /** * Sequence update. * - * 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, + * \rst + * Updates a sequence :math:`s` by replacing its context starting at an index + * with string :math:`t`. If the start index is negative, the start index is + * greater than the length of the sequence, the result is :math:`s`. Otherwise, * the length of the original sequence is preserved. * - * - 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$) + * - Arity: ``3`` + * + * - ``1:`` Term of sequence Sort + * - ``2:`` Term of Sort Int (index :math:`i`) + * - ``3:`` Term of sequence Sort (replacement sequence :math:`t`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_UPDATE, /** * Sequence element at. * - * Returns the element at index @f$i@f$ from a sequence @f$s@f$. If the index + * \rst + * Returns the element at index :math:`i` from a sequence :math:`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`. + * sequence of length ``1``. * - * - Arity: `2` - * - `1:` Term of sequence Sort - * - `2:` Term of Sort Int (index @f$i@f$) + * - Arity: ``2`` + * + * - ``1:`` Term of sequence Sort + * - ``2:`` Term of Sort Int (index :math:`i`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_AT, /** * Sequence contains. * - * 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`. + * \rst + * Checks whether a sequence :math:`s_1` contains another sequence + * :math:`s_2`. If :math:`s_2` is empty, the result is always ``true``. + * + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` Term of sequence Sort (@f$s_1@f$) - * - `2:` Term of sequence Sort (@f$s_2@f$) + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_CONTAINS, /** * Sequence index-of. * - * 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`. + * \rst + * Returns the index of a subsequence :math:`s_2` in a sequence :math:`s_1` + * starting at index :math:`i`. If the index is negative or greater than the + * length of sequence :math:`s_1` or the subsequence :math:`s_2` does not + * appear in sequence :math:`s_1` after index :math:`i`, the result is -1. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * - ``3:`` Term of Sort Int (:math:`i`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_INDEXOF, /** * Sequence replace. * - * 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. + * \rst + * Replaces the first occurrence of a sequence :math:`s_2` in a + * sequence :math:`s_1` with sequence :math:`s_3`. If :math:`s_2` does not + * appear in :math:`s_1`, :math:`s_1` is returned unmodified. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * - ``3:`` Term of sequence Sort (:math:`s_3`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REPLACE, /** * Sequence replace all. * - * 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. + * \rst + * Replaces all occurrences of a sequence :math:`s_2` in a sequence + * :math:`s_1` with sequence :math:`s_3`. If :math:`s_2` does not appear in + * :math:`s_1`, sequence :math:`s_1` is returned unmodified. + * + * - Arity: ``3`` * - * - 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$) + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * - ``3:`` Term of sequence Sort (:math:`s_3`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REPLACE_ALL, /** * Sequence reverse. * - * - Arity: `1` - * - `1:` Term of sequence Sort + * - Arity: ``1`` + * + * - ``1:`` Term of sequence Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REV, /** * Sequence prefix-of. * - * 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`. + * \rst + * Checks whether a sequence :math:`s_1` is a prefix of sequence :math:`s_2`. + * If sequence :math:`s_1` is empty, this operator returns ``true``. * - * - Arity: `1` - * - `1:` Term of sequence Sort (@f$s_1@f$) - * - `2:` Term of sequence Sort (@f$s_2@f$) + * - Arity: ``1`` + * + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_PREFIX, /** * Sequence suffix-of. * - * 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`. + * \rst + * Checks whether a sequence :math:`s_1` is a suffix of sequence :math:`s_2`. + * If sequence :math:`s_1` is empty, this operator returns ``true``. + * + * - Arity: ``1`` * - * - Arity: `1` - * - `1:` Term of sequence Sort (@f$s_1@f$) - * - `2:` Term of sequence Sort (@f$s_2@f$) + * - ``1:`` Term of sequence Sort (:math:`s_1`) + * - ``2:`` Term of sequence Sort (:math:`s_2`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_SUFFIX, @@ -3985,11 +4771,12 @@ enum Kind : int32_t * .. code:: smtlib * * (seq.++ (seq.unit c1) ... (seq.unit cn)) + * where :math:`n \leq 0` and :math:`c_1, ..., c_n` are constants of some + * sort. The elements can be extracted with Term::getSequenceValue(). * \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(). * * - Create Term of this Kind with: + * * - Solver::mkEmptySequence(const Sort&) const */ CONST_SEQUENCE, @@ -3998,14 +4785,17 @@ enum Kind : int32_t * * Corresponds to a sequence of length one with the given term. * - * - Arity: `1` - * - `1:` Term of any Sort (the element term) + * - Arity: ``1`` + * + * - ``1:`` Term of any Sort (the element term) * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_UNIT, @@ -4014,15 +4804,20 @@ enum Kind : int32_t * * Corresponds to the nth element of a sequence. * - * - Arity: `2` - * - `1:` Term of sequence Sort - * - `2:` Term of Sort Int (@f$n@f$) + * \rst + * - Arity: ``2`` + * + * - ``1:`` Term of sequence Sort + * - ``2:`` Term of Sort Int (:math:`n`) + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_NTH, @@ -4032,32 +4827,42 @@ enum Kind : int32_t /** * Universally quantified formula. * - * - Arity: `3` - * - `1:` Term of Kind #VARIABLE_LIST - * - `2:` Term of Sort Bool (the quantifier body) - * - `3:` (optional) Term of Kind #INST_PATTERN + * \rst + * - Arity: ``3`` + * + * - ``1:`` Term of Kind :cpp:enumerator:`VARIABLE_LIST` + * - ``2:`` Term of Sort Bool (the quantifier body) + * - ``3:`` (optional) Term of Kind :cpp:enumerator:`INST_PATTERN` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ FORALL, /** * Existentially quantified formula. * - * - Arity: `3` - * - `1:` Term of Kind #VARIABLE_LIST - * - `2:` Term of Sort Bool (the quantifier body) - * - `3:` (optional) Term of Kind #INST_PATTERN + * \rst + * - Arity: ``3`` + * + * - ``1:`` Term of Kind :cpp:enumerator:`VARIABLE_LIST` + * - ``2:`` Term of Sort Bool (the quantifier body) + * - ``3:`` (optional) Term of Kind :cpp:enumerator:`INST_PATTERN` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ EXISTS, @@ -4066,14 +4871,19 @@ enum Kind : int32_t * * A list of variables (used to bind variables under a quantifier) * - * - Arity: `n > 0` - * - `1..n:` Terms of Kind #VARIABLE + * \rst + * - Arity: ``n > 0`` + * + * - ``1..n:`` Terms of Kind :cpp:enumerator:`VARIABLE` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ VARIABLE_LIST, @@ -4083,16 +4893,22 @@ enum Kind : int32_t * Specifies a (list of) terms to be used as a pattern for quantifier * instantiation. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator`INST_PATTERN_LIST`. + * \endrst + * + * - Arity: ``n > 0`` * - * - Arity: `n > 0` - * - `1..n:` Terms of any Sort + * - ``1..n:`` Terms of any Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INST_PATTERN, @@ -4102,16 +4918,22 @@ enum Kind : int32_t * Specifies a (list of) terms that should not be used as a pattern for * quantifier instantiation. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst + * + * - Arity: ``n > 0`` * - * - Arity: `n > 0` - * - `1..n:` Terms of any Sort + * - ``1..n:`` Terms of any Sort * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INST_NO_PATTERN, @@ -4120,7 +4942,10 @@ enum Kind : int32_t * * Specifies an annotation for pool based instantiation. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst * * In detail, pool symbols can be declared via the method * - Solver::declarePool(const std::string&, const Sort&, const std::vector&) const @@ -4134,24 +4959,25 @@ enum Kind : int32_t * .. code:: lisp * * (FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL p q))) + * + * if :math:`x` and :math:`y` have Sorts :math:`S_1` and :math:`S_2`, then + * pool symbols :math:`p` and :math:`q` should have Sorts (Set :math:`S_1`) + * and (Set :math:`S_2`), respectively. This annotation specifies that the + * quantified formula above should be instantiated with the product of all + * terms that occur in the sets :math:`p` and :math:`q`. * \endrst * - * if @f$x@f$ and @f$y@f$ have Sorts @f$S_1@f$ and @f$S_2@f$, - * then pool symbols @f$p@f$ and @f$q@f$ should have Sorts - * (Set @f$S_1@f$) and (Set @f$S_2@f$), respectively. - * This annotation specifies that the quantified formula above should be - * instantiated with the product of all terms that occur in the sets @f$p@f$ - * and @f$q@f$. - * - * - 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 + * - 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 Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -4163,7 +4989,10 @@ enum Kind : int32_t /** * A instantantiation-add-to-pool annotation. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst * * An instantantiation-add-to-pool annotation indicates that when a quantified * formula is instantiated, the instantiated version of a term should be @@ -4174,23 +5003,26 @@ enum Kind : int32_t * \rst * .. code:: lisp * - * (FORALL (VARIABLE_LIST x) F + * (FORALL (VARIABLE_LIST x) F * (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p))) + * + * where assume that :math:`x` has type Int. When this quantified formula is + * instantiated with, e.g., the term :math:`t`, the term ``(ADD t 1)`` is + * added to pool :math:`p`. * \endrst * - * where assume that @f$x@f$ has type Int. When this quantified formula is - * instantiated with, e.g., the term @f$t@f$, the term `(ADD t 1)` is added to pool @f$p@f$. + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` The Term whose free variables are bound by the quantified formula. - * - `2:` The pool to add to, whose Sort should be a set of elements that - * match the Sort of the first argument. + * - ``1:`` The Term whose free variables are bound by the quantified formula. + * - ``2:`` The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument. * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -4202,7 +5034,10 @@ enum Kind : int32_t /** * A skolemization-add-to-pool annotation. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * \endrst * * An skolemization-add-to-pool annotation indicates that when a quantified * formula is skolemized, the skolemized version of a term should be added to @@ -4215,22 +5050,24 @@ enum Kind : int32_t * * (FORALL (VARIABLE_LIST x) F * (INST_PATTERN_LIST (SKOLEM_ADD_TO_POOL (ADD x 1) p))) + * + * where assume that :math:`x` has type Int. When this quantified formula is + * skolemized, e.g., with :math:`k` of type Int, then the term ``(ADD k 1)`` + * is added to the pool :math:`p`. * \endrst * - * where assume that @f$x@f$ has type Int. When this quantified formula is - * skolemized, e.g., with @f$k@f$ of type Int, then the term `(ADD k 1)` is - * added to the pool @f$p@f$. + * - Arity: ``2`` * - * - Arity: `2` - * - `1:` The Term whose free variables are bound by the quantified formula. - * - `2:` The pool to add to, whose Sort should be a set of elements that - * match the Sort of the first argument. + * - ``1:`` The Term whose free variables are bound by the quantified formula. + * - ``2:`` The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument. * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const * * \rst @@ -4245,32 +5082,42 @@ enum Kind : int32_t * Specifies a custom property for a quantified formula given by a * term that is ascribed a user attribute. * - * @note Should only be used as a child of #INST_PATTERN_LIST. + * \rst + * .. note:: Should only be used as a child of + * :cpp:enumerator:`INST_PATTERN_LIST`. + * + * - Arity: ``n > 0`` * - * - Arity: `n > 0` - * - `1:` Term of Kind #CONST_STRING (the keyword of the attribute) - * - `2...n:` Terms representing the values of the attribute + * - ``1:`` Term of Kind :cpp:enumerator:`CONST_STRING` (the keyword of the attribute) + * - ``2...n:`` Terms representing the values of the attribute + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INST_ATTRIBUTE, /** * A list of instantiation patterns, attributes or annotations. * - * - Arity: `n > 1` - * - `1..n:` Terms of Kind #INST_PATTERN, #INST_NO_PATTERN, #INST_POOL, - * #INST_ADD_TO_POOL, #SKOLEM_ADD_TO_POOL, #INST_ATTRIBUTE + * \rst + * - Arity: ``n > 1`` + * + * - ``1..n:`` Terms of Kind :cpp:enumerator:`INST_PATTERN`, :cpp:enumerator:`INST_NO_PATTERN`, :cpp:enumerator:`INST_POOL`, :cpp:enumerator:`INST_ADD_TO_POOL`, :cpp:enumerator:`SKOLEM_ADD_TO_POOL`, :cpp:enumerator:`INST_ATTRIBUTE` + * \endrst * * - Create Term of this Kind with: + * * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: + * * - Solver::mkOp(Kind, const std::vector&) const */ INST_PATTERN_LIST, diff --git a/src/api/python/genenums.py.in b/src/api/python/genenums.py.in index a8d20d7c3..ccab48a82 100644 --- a/src/api/python/genenums.py.in +++ b/src/api/python/genenums.py.in @@ -63,7 +63,18 @@ ENUMS_ATTR_TEMPLATE = r''' {name}=c_{enum}.{cpp_name}, """{doc}""" ''' comment_repls = { - '`Solver::([a-zA-Z]+)\(([^)]*)\)[^`]*`': ':py:meth:`pycvc5.Solver.\\1`', + 'Term::([a-zA-Z]+)\(([^)]*)\)': ':py:meth:`Term.\\1()`', + 'Solver::([a-zA-Z]+)\(([^)]*)\) const': ':py:meth:`Solver.\\1()`', + 'Solver::([a-zA-Z]+)\(([^)]*)\)': ':py:meth:`Solver.\\1()`', + 'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\) const': ':py:meth:`DatatypeConstructor.\\1()`', + 'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\)': ':py:meth:`DatatypeConstructor.\\1()`', + 'Datatype::([a-zA-Z]+)\(([^)]*)\) const': ':py:meth:`Datatype.\\1()`', + 'Datatype::([a-zA-Z]+)\(([^)]*)\)': ':py:meth:`Datatype.\\1()`', + 'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\) const': ':py:meth:`DatatypeSelector.\\1()`', + 'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\)': ':py:meth:`DatatypeSelector.\\1()`', + ':cpp:func:`(.*?)`': '\\1', + ':cpp:enumerator:`(.*?)`': ':py:obj:`\\1`', + '\\\\': '\\\\\\\\', } -- 2.30.2