diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 2891 |
1 files changed, 1721 insertions, 1170 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index eaa4e6079..d1b0a277b 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -27,6 +27,7 @@ namespace api { /* Kind */ /* -------------------------------------------------------------------------- */ +// TODO(Gereon): Fix links that involve std::vector. See https://github.com/doxygen/doxygen/issues/8503 /** * The kind of a CVC4 term. * @@ -47,8 +48,8 @@ enum CVC4_EXPORT Kind : int32_t */ UNDEFINED_KIND = -1, /** - * Null kind (kind of null term Term()). - * Do not explicitly create via API functions other than Term(). + * Null kind (kind of null term `Term::Term()`). + * Do not explicitly create via API functions other than `Term::Term()`. */ NULL_EXPR, @@ -56,20 +57,24 @@ enum CVC4_EXPORT Kind : int32_t /** * Uninterpreted constant. - * Parameters: 2 - * -[1]: Sort of the constant - * -[2]: Index of the constant + * + * Parameters: + * - 1: Sort of the constant + * - 2: Index of the constant + * * Create with: - * mkUninterpretedConst(Sort sort, int32_t index) + * - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const` */ UNINTERPRETED_CONSTANT, /** * Abstract value (other than uninterpreted sort constants). - * Parameters: 1 - * -[1]: Index of the abstract value + * + * Parameters: + * - 1: Index of the abstract value + * * Create with: - * mkAbstractValue(const std::string& index); - * mkAbstractValue(uint64_t index); + * - `Solver::mkAbstractValue(const std::string& index) const` + * - `Solver::mkAbstractValue(uint64_t index) const` */ ABSTRACT_VALUE, #if 0 @@ -78,106 +83,122 @@ enum CVC4_EXPORT Kind : int32_t #endif /** * Equality, chainable. + * * Parameters: n > 1 - * -[1]..[n]: Terms with same sorts + * - 1..n: Terms with same sorts + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ EQUAL, /** * Disequality. + * * Parameters: n > 1 - * -[1]..[n]: Terms with same sorts + * - 1..n: Terms with same sorts + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DISTINCT, /** * First-order constant. + * * Not permitted in bindings (forall, exists, ...). + * * Parameters: - * See mkConst(). + * - See @ref cvc5::api::Solver::mkConst() "mkConst()". + * * Create with: - * mkConst(const std::string& symbol, Sort sort) - * mkConst(Sort sort) + * - `Solver::mkConst(const Sort& sort, const std::string& symbol) const` + * - `Solver::mkConst(const Sort& sort) const` */ CONSTANT, /** * (Bound) variable. + * * Permitted in bindings and in the lambda and quantifier bodies only. + * * Parameters: - * See mkVar(). + * - See @ref cvc5::api::Solver::mkVar() "mkVar()". + * * Create with: - * mkVar(const std::string& symbol, Sort sort) - * mkVar(Sort sort) + * - `Solver::mkVar(const Sort& sort, const std::string& symbol) const` */ VARIABLE, #if 0 /* Skolem variable (internal only) */ SKOLEM, #endif - /* + /** * Symbolic expression. + * * Parameters: n > 0 - * -[1]..[n]: terms + * - 1..n: terms + * * Create with: - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEXPR, /** * Lambda expression. - * Parameters: 2 - * -[1]: BOUND_VAR_LIST - * -[2]: Lambda body + * + * Parameters: + * - 1: BOUND_VAR_LIST + * - 2: Lambda body + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ LAMBDA, /** * The syntax of a witness term is similar to a quantified formula except that * only one bound variable is allowed. - * The term (witness ((x T)) F) returns an element x of type T - * and asserts F. + * The term `(witness ((x T)) F)` returns an element `x` of type `T` + * and asserts `F`. * * The witness operator behaves like the description operator * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x * that satisfies F. But if such x exists, the witness operator does not * enforce the axiom that ensures uniqueness up to logical equivalence: - * \verbatim - * forall x. F \equiv G => witness x. F = witness x. G - * \endverbatim + * + * @f[ + * \forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G + * @f] * * For example if there are 2 elements of type T that satisfy F, then the * following formula is satisfiable: - * (distinct - * (witness ((x Int)) F) - * (witness ((x Int)) F)) + * + * (distinct + * (witness ((x Int)) F) + * (witness ((x Int)) F)) * * 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 + * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a valid * formula. If this is not the case, then the semantics in formulas that use * witness terms may be unintuitive. For example, the following formula is * unsatisfiable: - * (or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0)) - * whereas notice that (or (= z 0) (not (= z 0))) is true for any z. + * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))` + * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`. * - * Parameters: 2 - * -[1]: BOUND_VAR_LIST - * -[2]: Witness body + * Parameters: + * - 1: BOUND_VAR_LIST + * - 2: Witness body + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ WITNESS, @@ -185,80 +206,103 @@ enum CVC4_EXPORT Kind : int32_t /** * Boolean constant. - * Parameters: 1 - * -[1]: Boolean value of the constant + * + * Parameters: + * - 1: Boolean value of the constant + * * Create with: - * mkTrue() - * mkFalse() - * mkBoolean(bool val) + * - `Solver::mkTrue() const` + * - `Solver::mkFalse() const` + * - `Solver::mkBoolean(bool val) const` */ CONST_BOOLEAN, - /* Logical not. - * Parameters: 1 - * -[1]: Boolean Term to negate + /** + * Logical negation. + * + * Parameters: + * - 1: Boolean Term to negate + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ NOT, - /* Logical and. + /** + * Logical conjunction. + * * Parameters: n > 1 - * -[1]..[n]: Boolean Term of the conjunction + * - 1..n: Boolean Term of the conjunction + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ AND, /** * Logical implication. + * * Parameters: n > 1 - * -[1]..[n]: Boolean Terms, right associative + * - 1..n: Boolean Terms, right associative + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ IMPLIES, - /* Logical or. + /** + * Logical disjunction. + * * Parameters: n > 1 - * -[1]..[n]: Boolean Term of the disjunction + * - 1..n: Boolean Term of the disjunction + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ OR, - /* Logical exclusive or, left associative. + /** + * Logical exclusive disjunction, left associative. + * * Parameters: n > 1 - * -[1]..[n]: Boolean Terms, [1] xor ... xor [n] + * - 1..n: Boolean Terms, `[1] xor ... xor [n]` + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ XOR, - /* If-then-else. - * Parameters: 3 - * -[1] is a Boolean condition Term - * -[2] the 'then' Term - * -[3] the 'else' Term + /** + * If-then-else. + * + * Parameters: + * - 1: is a Boolean condition Term + * - 2: the 'then' Term + * - 3: the 'else' Term + * * 'then' and 'else' term must have same base sort. + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ ITE, /* UF -------------------------------------------------------------------- */ - /* Application of an uninterpreted function. + /** + * Application of an uninterpreted function. + * * Parameters: n > 1 - * -[1]: Function Term - * -[2]..[n]: Function argument instantiation Terms + * - 1: Function Term + * - 2..n: Function argument instantiation Terms + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ APPLY_UF, #if 0 @@ -269,23 +313,27 @@ enum CVC4_EXPORT Kind : int32_t * Cardinality constraint on uninterpreted sort S. * Interpreted as a predicate that is true when the cardinality of S * is less than or equal to the value of the second argument. - * Parameters: 2 - * -[1]: Term of sort S - * -[2]: Positive integer constant that bounds the cardinality of sort S + * + * Parameters: + * - 1: Term of sort S + * - 2: Positive integer constant that bounds the cardinality of sort S + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ CARDINALITY_CONSTRAINT, - /* + /** * Cardinality value for uninterpreted sort S. * An operator that returns an integer indicating the value of the cardinality * of sort S. - * Parameters: 1 - * -[1]: Term of sort S + * + * Parameters: + * - 1: Term of sort S + * * Create with: - * mkTerm(Kind kind, Term child1) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ CARDINALITY_VALUE, #if 0 @@ -297,13 +345,15 @@ enum CVC4_EXPORT Kind : int32_t /** * Higher-order applicative encoding of function application, left * associative. + * * Parameters: n > 1 - * -[1]: Function to apply - * -[2] ... [n]: Arguments of the function + * - 1: Function to apply + * - 2..n: Arguments of the function + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ HO_APPLY, @@ -311,39 +361,47 @@ enum CVC4_EXPORT Kind : int32_t /** * Arithmetic addition. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real (sorts must match) + * - 1..n: Terms of sort Integer, Real (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ PLUS, /** * Arithmetic multiplication. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real (sorts must match) + * - 1..n: Terms of sort Integer, Real (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ MULT, /** * Operator for Integer AND - * Parameter: 1 - * -[1]: Size of the bit-vector that determines the semantics of the IAND + * + * Parameters: + * - 1: Size of the bit-vector that determines the semantics of the IAND + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Apply integer conversion to bit-vector. - * Parameters: 2 - * -[1]: Op of kind IAND - * -[2]: Integer term - * -[3]: Integer term + + * Parameters: + * - 1: Op of kind IAND + * - 2: Integer term + * - 3: Integer term + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ IAND, #if 0 @@ -352,286 +410,341 @@ enum CVC4_EXPORT Kind : int32_t #endif /** * Arithmetic subtraction, left associative. - * Parameters: n - * -[1]..[n]: Terms of sort Integer, Real (sorts must match) + * + * Parameters: + * - 1..n: Terms of sort Integer, Real (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ MINUS, /** * Arithmetic negation. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ UMINUS, /** * Real division, division by 0 undefined, left associative. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real + * - 1..n: Terms of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DIVISION, /** * Integer division, division by 0 undefined, left associative. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer + * - 1..n: Terms of sort Integer + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INTS_DIVISION, /** * Integer modulus, division by 0 undefined. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer + * + * Parameters: + * - 1: Term of sort Integer + * - 2: Term of sort Integer + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INTS_MODULUS, /** * Absolute value. - * Parameters: 1 - * -[1]: Term of sort Integer + * + * Parameters: + * - 1: Term of sort Integer + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ABS, /** * Arithmetic power. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real + * + * Parameters: + * - 1: Term of sort Integer, Real + * - 2: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ POW, /** - * Exponential. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Exponential function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ EXPONENTIAL, /** - * Sine. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Sine function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SINE, /** - * Cosine. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Cosine function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ COSINE, /** - * Tangent. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Tangent function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ TANGENT, /** - * Cosecant. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Cosecant function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ COSECANT, /** - * Secant. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Secant function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SECANT, /** - * Cotangent. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Cotangent function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ COTANGENT, /** - * Arc sine. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc sine function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCSINE, /** - * Arc cosine. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc cosine function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCCOSINE, /** - * Arc tangent. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc tangent function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCTANGENT, /** - * Arc cosecant. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc cosecant function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCCOSECANT, /** - * Arc secant. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc secant function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCSECANT, /** - * Arc cotangent. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * Arc cotangent function. + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ ARCCOTANGENT, /** * Square root. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SQRT, /** * Operator for the divisibility-by-k predicate. - * Parameter: 1 - * -[1]: The k to divide by (sort Integer) + * + * Parameter: + * - 1: The k to divide by (sort Integer) + * * Create with: - * mkOp(Kind kind, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Apply divisibility-by-k predicate. - * Parameters: 2 - * -[1]: Op of kind DIVISIBLE - * -[2]: Integer Term + * + * Parameters: + * - 1: Op of kind DIVISIBLE + * - 2: Integer Term + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ DIVISIBLE, /** * Multiple-precision rational constant. + * * Parameters: - * See mkInteger(), mkReal(), mkRational() - * Create with: - * mkInteger(const char* s, uint32_t base = 10) - * mkInteger(const std::string& s, uint32_t base = 10) - * mkInteger(int32_t val) - * mkInteger(uint32_t val) - * mkInteger(int64_t val) - * mkInteger(uint64_t val) - * mkReal(const char* s, uint32_t base = 10) - * mkReal(const std::string& s, uint32_t base = 10) - * mkReal(int32_t val) - * mkReal(int64_t val) - * mkReal(uint32_t val) - * mkReal(uint64_t val) - * mkReal(int32_t num, int32_t den) - * mkReal(int64_t num, int64_t den) - * mkReal(uint32_t num, uint32_t den) - * mkReal(uint64_t num, uint64_t den) + * See @ref cvc5::api::Solver::mkInteger() "mkInteger()", @ref cvc5::api::Solver::mkReal() "mkReal()". + * + * Create with: + * - `Solver::mkInteger(const std::string& s) const` + * - `Solver::mkInteger(int64_t val) const` + * - `Solver::mkReal(const std::string& s) const` + * - `Solver::mkReal(int64_t val) const` + * - `Solver::mkReal(int64_t num, int64_t den) const` */ CONST_RATIONAL, /** * Less than, chainable. + * * Parameters: n - * -[1]..[n]: Terms of sort Integer, Real; [1] < ... < [n] + * - 1..n: Terms of sort Integer, Real; [1] < ... < [n] + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ LT, /** * Less than or equal, chainable. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real; [1] <= ... <= [n] + * - 1..n: Terms of sort Integer, Real; [1] <= ... <= [n] + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ LEQ, /** * Greater than, chainable. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real, [1] > ... > [n] + * - 1..n: Terms of sort Integer, Real, [1] > ... > [n] + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ GT, /** * Greater than or equal, chainable. + * * Parameters: n > 1 - * -[1]..[n]: Terms of sort Integer, Real; [1] >= ... >= [n] + * - 1..n: Terms of sort Integer, Real; [1] >= ... >= [n] + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ GEQ, /** * Is-integer predicate. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ IS_INTEGER, /** * Convert Term to Integer by the floor function. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * + * Parameters: + * - 1: Term of sort Integer, Real + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ TO_INTEGER, /** * Convert Term to Real. - * Parameters: 1 - * -[1]: Term of sort Integer, Real + * + * Parameters: + * + * - 1: Term of sort Integer, Real + * * This is a no-op in CVC4, as Integer is a subtype of Real. */ TO_REAL, /** * Pi constant. + * * Create with: - * mkPi() - * mkTerm(Kind kind) + * - `Solver::mkPi() const` + * - `Solver::mkTerm(Kind kind) const` */ PI, @@ -639,134 +752,162 @@ enum CVC4_EXPORT Kind : int32_t /** * Fixed-size bit-vector constant. + * * Parameters: - * See mkBitVector(). + * See @ref cvc5::api::Solver::mkBitVector() "mkBitVector()". + * * Create with: - * mkBitVector(uint32_t size, uint64_t val) - * mkBitVector(const char* s, uint32_t base = 2) - * mkBitVector(std::string& s, uint32_t base = 2) + * - `Solver::mkBitVector(uint32_t size, uint64_t val) const` + * - `Solver::mkBitVector(const std::string& s, uint32_t base) const` + * - `Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const` */ CONST_BITVECTOR, /** * Concatenation of two or more bit-vectors. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort + * - 1..n: Terms of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_CONCAT, /** * Bit-wise and. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_AND, /** * Bit-wise or. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_OR, /** * Bit-wise xor. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_XOR, /** * Bit-wise negation. - * Parameters: 1 - * -[1]: Term of bit-vector sort + * + * Parameters: + * - 1: Term of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BITVECTOR_NOT, /** * Bit-wise nand. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_NAND, /** * Bit-wise nor. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_NOR, /** * Bit-wise xnor, left associative. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_XNOR, /** * Equality comparison (returns bit-vector of size 1). - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_COMP, /** * Multiplication of two or more bit-vectors. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_MULT, /** * Addition of two or more bit-vectors. + * * Parameters: n > 1 - * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * - 1..n: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_PLUS, /** * Subtraction of two bit-vectors. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SUB, /** * Negation of a bit-vector (two's complement). - * Parameters: 1 - * -[1]: Term of bit-vector sort + * + * Parameters: + * - 1: Term of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BITVECTOR_NEG, /** @@ -777,11 +918,12 @@ enum CVC4_EXPORT Kind : int32_t * treated as all ones (default, corresponds to SMT-LIB >=2.6) or an * uninterpreted value (corresponds to SMT-LIB <2.6). * - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_UDIV, /** @@ -792,11 +934,12 @@ enum CVC4_EXPORT Kind : int32_t * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or * an uninterpreted value (corresponds to SMT-LIB <2.6). * - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_UREM, /** @@ -808,11 +951,12 @@ enum CVC4_EXPORT Kind : int32_t * SMT-LIB >=2.6). If the option is disabled, a division by zero is treated * as an uninterpreted value (corresponds to SMT-LIB <2.6). * - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SDIV, /** @@ -824,11 +968,12 @@ enum CVC4_EXPORT Kind : int32_t * if the modulus is zero, the result is either the dividend (default) or an * uninterpreted value (corresponds to SMT-LIB <2.6). * - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SREM, /** @@ -840,164 +985,201 @@ enum CVC4_EXPORT Kind : int32_t * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or * an uninterpreted value (corresponds to SMT-LIB <2.6). * - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SMOD, /** * Bit-vector shift left. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SHL, /** * Bit-vector logical shift right. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_LSHR, /** * Bit-vector arithmetic shift right. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_ASHR, /** * Bit-vector unsigned less than. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_ULT, /** * Bit-vector unsigned less than or equal. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_ULE, /** * Bit-vector unsigned greater than. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_UGT, /** * Bit-vector unsigned greater than or equal. * The two bit-vector parameters must have same width. - * Parameters: 2 + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_UGE, - /* Bit-vector signed less than. + /** + * Bit-vector signed less than. * The two bit-vector parameters must have same width. - * Parameters: 2 + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SLT, /** * Bit-vector signed less than or equal. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SLE, /** * Bit-vector signed greater than. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SGT, /** * Bit-vector signed greater than or equal. * The two bit-vector parameters must have same width. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SGE, /** * Bit-vector unsigned less than, returns bit-vector of size 1. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_ULTBV, /** * Bit-vector signed less than. returns bit-vector of size 1. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * + * Parameters: + * - 1..2: Terms of bit-vector sort (sorts must match) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_SLTBV, /** * Same semantics as regular ITE, but condition is bit-vector of size 1. - * Parameters: 3 - * -[1]: Term of bit-vector sort of size 1, representing the condition - * -[2]: Term reprsenting the 'then' branch - * -[3]: Term representing the 'else' branch + * + * Parameters: + * - 1: Term of bit-vector sort of size 1, representing the condition + * - 2: Term reprsenting the 'then' branch + * - 3: Term representing the 'else' branch + * * 'then' and 'else' term must have same base sort. + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BITVECTOR_ITE, /** * Bit-vector redor. - * Parameters: 1 - * -[1]: Term of bit-vector sort + * + * Parameters: + * - 1: Term of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BITVECTOR_REDOR, /** * Bit-vector redand. - * Parameters: 1 - * -[1]: Term of bit-vector sort + * + * Parameters: + * - 1: Term of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BITVECTOR_REDAND, #if 0 @@ -1013,99 +1195,123 @@ enum CVC4_EXPORT Kind : int32_t #endif /** * Operator for bit-vector extract (from index 'high' to 'low'). - * Parameters: 2 - * -[1]: The 'high' index - * -[2]: The 'low' index + * + * Parameters: + * - 1: The 'high' index + * - 2: The 'low' index + * * Create with: - * mkOp(Kind kind, uint32_t param, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const` * * Apply bit-vector extract. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_EXTRACT - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_EXTRACT + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_EXTRACT, /** * Operator for bit-vector repeat. - * Parameter 1: - * -[1]: Number of times to repeat a given bit-vector + * + * Parameter: + * - 1: Number of times to repeat a given bit-vector + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply bit-vector repeat. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_REPEAT - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_REPEAT + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_REPEAT, /** * Operator for bit-vector zero-extend. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be extended + * + * Parameter: + * - 1: Number of bits by which a given bit-vector is to be extended + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply bit-vector zero-extend. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_ZERO_EXTEND - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_ZERO_EXTEND + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_ZERO_EXTEND, /** * Operator for bit-vector sign-extend. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be extended + * + * Parameter: + * - 1: Number of bits by which a given bit-vector is to be extended + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply bit-vector sign-extend. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_SIGN_EXTEND - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_SIGN_EXTEND + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_SIGN_EXTEND, /** * Operator for bit-vector rotate left. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be rotated + * + * Parameter: + * - 1: Number of bits by which a given bit-vector is to be rotated + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply bit-vector rotate left. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_ROTATE_LEFT - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_ROTATE_LEFT + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_ROTATE_LEFT, /** * Operator for bit-vector rotate right. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be rotated + * + * Parameter: + * - 1: Number of bits by which a given bit-vector is to be rotated + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply bit-vector rotate right. - * Parameters: 2 - * -[1]: Op of kind BITVECTOR_ROTATE_RIGHT - * -[2]: Term of bit-vector sort + * + * Parameters: + * - 1: Op of kind BITVECTOR_ROTATE_RIGHT + * - 2: Term of bit-vector sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ BITVECTOR_ROTATE_RIGHT, #if 0 @@ -1114,26 +1320,32 @@ enum CVC4_EXPORT Kind : int32_t #endif /** * Operator for the conversion from Integer to bit-vector. - * Parameter: 1 - * -[1]: Size of the bit-vector to convert to + * + * Parameter: + * - 1: Size of the bit-vector to convert to + * * Create with: - * mkOp(Kind kind, uint32_t param). + * - `Solver::mkOp(Kind kind, uint32_t param) const`. * * Apply integer conversion to bit-vector. - * Parameters: 2 - * -[1]: Op of kind INT_TO_BITVECTOR - * -[2]: Integer term + * + * Parameters: + * - 1: Op of kind INT_TO_BITVECTOR + * - 2: Integer term + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ INT_TO_BITVECTOR, /** * Bit-vector conversion to (nonnegative) integer. - * Parameter: 1 - * -[1]: Term of bit-vector sort + * + * Parameter: + * - 1: Term of bit-vector sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BITVECTOR_TO_NAT, @@ -1141,441 +1353,536 @@ enum CVC4_EXPORT Kind : int32_t /** * Floating-point constant, constructed from a double or string. - * Parameters: 3 - * -[1]: Size of the exponent - * -[2]: Size of the significand - * -[3]: Value of the floating-point constant as a bit-vector term + * + * Parameters: + * - 1: Size of the exponent + * - 2: Size of the significand + * - 3: Value of the floating-point constant as a bit-vector term + * * Create with: - * mkFloatingPoint(uint32_t sig, uint32_t exp, Term val) + * - `Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const` */ CONST_FLOATINGPOINT, /** * Floating-point rounding mode term. + * * Create with: - * mkRoundingMode(RoundingMode rm) + * - `Solver::mkRoundingMode(RoundingMode rm) const` */ CONST_ROUNDINGMODE, /** * Create floating-point literal from bit-vector triple. - * Parameters: 3 - * -[1]: Sign bit as a bit-vector term - * -[2]: Exponent bits as a bit-vector term - * -[3]: Significand bits as a bit-vector term (without hidden bit) + * + * Parameters: + * - 1: Sign bit as a bit-vector term + * - 2: Exponent bits as a bit-vector term + * - 3: Significand bits as a bit-vector term (without hidden bit) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_FP, /** * Floating-point equality. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_EQ, /** * Floating-point absolute value. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ABS, /** * Floating-point negation. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_NEG, /** * Floating-point addition. - * Parameters: 3 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint - * -[3]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * - 3: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_PLUS, /** * Floating-point sutraction. - * Parameters: 3 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint - * -[3]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * - 3: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_SUB, /** * Floating-point multiply. - * Parameters: 3 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint - * -[3]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * - 3: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_MULT, /** * Floating-point division. - * Parameters: 3 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint - * -[3]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * - 3: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_DIV, /** * Floating-point fused multiply and add. - * Parameters: 4 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint - * -[3]: Term of sort FloatingPoint - * -[4]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * - 3: Term of sort FloatingPoint + * - 4: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_FMA, /** * Floating-point square root. - * Parameters: 2 - * -[1]: CONST_ROUNDINGMODE - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: CONST_ROUNDINGMODE + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_SQRT, /** * Floating-point remainder. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_REM, /** * Floating-point round to integral. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * -1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_RTI, /** * Floating-point minimum. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_MIN, /** * Floating-point maximum. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_MAX, /** * Floating-point less than or equal. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_LEQ, /** * Floating-point less than. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_LT, /** * Floating-point greater than or equal. - * Parameters: 2 - * -[1]..[2]: Terms of floating point sort + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_GEQ, /** * Floating-point greater than. - * Parameters: 2 + * + * Parameters: + * - 1..2: Terms of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FLOATINGPOINT_GT, /** * Floating-point is normal. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISN, /** * Floating-point is sub-normal. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISSN, /** * Floating-point is zero. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISZ, /** * Floating-point is infinite. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISINF, /** * Floating-point is NaN. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISNAN, /** * Floating-point is negative. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISNEG, /** * Floating-point is positive. - * Parameters: 1 - * -[1]: Term of floating point sort + * + * Parameters: + * - 1: Term of floating point sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_ISPOS, /** * Operator for to_fp from bit vector. - * Parameters: 2 - * -[1]: Exponent size - * -[2]: Significand size + * + * Parameters: + * - 1: Exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Conversion from an IEEE-754 bit vector to floating-point. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /** * Operator for to_fp from floating point. - * Parameters: 2 - * -[1]: Exponent size - * -[2]: Significand size + * + * Parameters: + * - 1: Exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Conversion between floating-point sorts. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_FLOATINGPOINT, /** * Operator for to_fp from real. - * Parameters: 2 - * -[1]: Exponent size - * -[2]: Significand size + * + * Parameters: + * - 1: Exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Conversion from a real to floating-point. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_REAL - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_REAL + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_REAL, - /* - * Operator for to_fp from signed bit vector. - * Parameters: 2 - * -[1]: Exponent size - * -[2]: Significand size + /** + * Operator for to_fp from signed bit vector + * + * Parameters: + * - 1: Exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Conversion from a signed bit vector to floating-point. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /** * Operator for to_fp from unsigned bit vector. - * Parameters: 2 - * -[1]: Exponent size - * -[2]: Significand size + * + * Parameters: + * - 1: Exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Converting an unsigned bit vector to floating-point. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /** * Operator for a generic to_fp. - * Parameters: 2 - * -[1]: exponent size - * -[2]: Significand size + * + * Parameters: + * - 1: exponent size + * - 2: Significand size + * * Create with: - * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` * * Generic conversion to floating-point, used in parsing only. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_GENERIC - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_FP_GENERIC, /** * Operator for to_ubv. - * Parameters: 1 - * -[1]: Size of the bit-vector to convert to + * + * Parameters: + * - 1: Size of the bit-vector to convert to + * * Create with: - * mkOp(Kind kind, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Conversion from a floating-point value to an unsigned bit vector. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_UBV + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_UBV, /** * Operator for to_sbv. - * Parameters: 1 - * -[1]: Size of the bit-vector to convert to + * + * Parameters: + * - 1: Size of the bit-vector to convert to + * * Create with: - * mkOp(Kind kind, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Conversion from a floating-point value to a signed bit vector. - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV - * -[2]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_SBV + * - 2: Term of sort FloatingPoint + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ FLOATINGPOINT_TO_SBV, /** * Floating-point to real. - * Parameters: 1 - * -[1]: Term of sort FloatingPoint + * + * Parameters: + * - 1: Term of sort FloatingPoint + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ FLOATINGPOINT_TO_REAL, /* Arrays ---------------------------------------------------------------- */ /** - * Aarray select. - * Parameters: 2 - * -[1]: Term of array sort - * -[2]: Selection index + * Array select. + * + * Parameters: + * - 1: Term of array sort + * - 2: Selection index + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ SELECT, /** * Array store. - * Parameters: 3 - * -[1]: Term of array sort - * -[2]: Store index - * -[3]: Term to store at the index + * + * Parameters: + * - 1: Term of array sort + * - 2: Store index + * - 3: Term to store at the index + * * Create with: - * mkTerm(Op op, Term child1, Term child2, Term child3) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ STORE, /** * Constant array. - * Parameters: 2 - * -[1]: Array sort - * -[2]: Term representing a constant + * + * Parameters: + * - 1: Array sort + * - 2: Term representing a constant + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` * * Note: We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant - * arrays, the solver doesn't know what to do and aborts (Issue #1667). + * arrays, the solver doesn't know what to do and aborts (Issue <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>). */ CONST_ARRAY, /** * Equality over arrays a and b over a given range [i,j], i.e., - * \verbatim - * \forall k . i <= k <= j --> a[k] = b[k] - * \endverbatim + * @f[ + * \forall k . i \leq k \leq j \Rightarrow a[k] = b[k] + * @f] * - * Parameters: 4 - * -[1]: First array - * -[2]: Second array - * -[3]: Lower bound of range (inclusive) - * -[4]: Uppper bound of range (inclusive) + * Parameters: + * - 1: First array + * - 2: Second array + * - 3: Lower bound of range (inclusive) + * - 4: Uppper bound of range (inclusive) + * * Create with: - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` * * Note: We currently support the creation of array equalities over index * types bit-vector, floating-point, integer and real. Option --arrays-exp is @@ -1597,34 +1904,40 @@ enum CVC4_EXPORT Kind : int32_t /** * Constructor application. + * * Paramters: n > 0 - * -[1]: Constructor (operator) - * -[2]..[n]: Parameters to the constructor + * - 1: Constructor (operator) + * - 2..n: Parameters to the constructor + * * Create with: - * mkTerm(Kind kind, Op op) - * mkTerm(Kind kind, Op op, Term child) - * mkTerm(Kind kind, Op op, Term child1, Term child2) - * mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op) const` + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ APPLY_CONSTRUCTOR, /** * Datatype selector application. - * Parameters: 1 - * -[1]: Selector (operator) - * -[2]: Datatype term (undefined if mis-applied) + * + * Parameters: + * - 1: Selector (operator) + * - 2: Datatype term (undefined if mis-applied) + * * Create with: - * mkTerm(Kind kind, Op op, Term child) + * - `Solver::mkTerm(const Op& op, const Term& child) const` */ APPLY_SELECTOR, /** * Datatype tester application. - * Parameters: 2 - * -[1]: Tester term - * -[2]: Datatype term + * + * Parameters: + * - 1: Tester term + * - 2: Datatype term + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ APPLY_TESTER, #if 0 @@ -1637,101 +1950,126 @@ enum CVC4_EXPORT Kind : int32_t #endif /** * Operator for a tuple update. - * Parameters: 1 - * -[1]: Index of the tuple to be updated + * + * Parameters: + * - 1: Index of the tuple to be updated + * * Create with: - * mkOp(Kind kind, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Apply tuple update. - * Parameters: 3 - * -[1]: Op of kind TUPLE_UPDATE (which references an index) - * -[2]: Tuple - * -[3]: Element to store in the tuple at the given index + * + * Parameters: + * - 1: Op of kind TUPLE_UPDATE (which references an index) + * - 2: Tuple + * - 3: Element to store in the tuple at the given index + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ TUPLE_UPDATE, /** * Operator for a record update. - * Parameters: 1 - * -[1]: Name of the field to be updated + * + * Parameters: + * - 1: Name of the field to be updated + * * Create with: - * mkOp(Kind kind, const std::string& param) + * - `Solver::mkOp(Kind kind, const std::string& param) const` * * Record update. - * Parameters: 3 - * -[1]: Op of kind RECORD_UPDATE (which references a field) - * -[2]: Record term to update - * -[3]: Element to store in the record in the given field + * + * Parameters: + * - 1: Op of kind RECORD_UPDATE (which references a field) + * - 2: Record term to update + * - 3: Element to store in the record in the given field + * * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op,, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(const Op& op,, const std::vector<Term>& children) const` */ RECORD_UPDATE, - /* Match expressions. + /** + * Match expressions. * For example, the smt2 syntax match term - * (match l (((cons h t) h) (nil 0))) + * `(match l (((cons h t) h) (nil 0)))` * is represented by the AST - * (MATCH l - * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h) - * (MATCH_CASE nil 0)) + * + * (MATCH l + * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h) + * (MATCH_CASE nil 0)) + * * The type of the last argument of each case term could be equal. + * * Parameters: n > 1 - * -[1]..[n]: Terms of kind MATCH_CASE or MATCH_BIND_CASE + * - 1..n: Terms of kind MATCH_CASE or MATCH_BIND_CASE + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` * */ MATCH, - /* Match case + /** + * Match case * A (constant) case expression to be used within a match expression. - * Parameters: 2 - * -[1] Term denoting the pattern expression - * -[2] Term denoting the return value + * + * Parameters: + * - 1: Term denoting the pattern expression + * - 2: Term denoting the return value + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ MATCH_CASE, - /* Match bind case + /** + * Match bind case * A (non-constant) case expression to be used within a match expression. - * Parameters: 3 - * -[1] a BOUND_VAR_LIST Term containing the free variables of the case - * -[2] Term denoting the pattern expression - * -[3] Term denoting the return value + * + * Parameters: + * - 1: a BOUND_VAR_LIST Term containing the free variables of the case + * - 2: Term denoting the pattern expression + * - 3: Term denoting the return value + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ MATCH_BIND_CASE, - /* + /** * Datatypes size * An operator mapping datatypes to an integer denoting the number of * non-nullary applications of constructors they contain. - * Parameters: 1 - * -[1]: Datatype term + * + * Parameters: + * - 1: Datatype term + * * Create with: - * mkTerm(Kind kind, Term child1) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DT_SIZE, /** * Operator for tuple projection indices - * Parameters: 1 - * -[1]: The tuple projection indices + * + * Parameters: + * - 1: The tuple projection indices + * * Create with: - * mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) + * - `Solver::mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) const` * - * constructs a new tuple from an existing one using the elements at the + * Constructs a new tuple from an existing one using the elements at the * given indices - * Parameters: 1 - * -[1]: a term of tuple sort + * + * Parameters: + * - 1: a term of tuple sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ TUPLE_PROJECT, #if 0 @@ -1751,52 +2089,62 @@ enum CVC4_EXPORT Kind : int32_t /** * Separation logic nil term. - * Parameters: 0 + * + * Parameters: none + * * Create with: - * mkSepNil(Sort sort) + * - `Solver::mkSepNil(const Sort& sort) const` */ SEP_NIL, /** * Separation logic empty heap. - * Parameters: 2 - * -[1]: Term of the same sort as the sort of the location of the heap + * + * Parameters: + * - 1: Term of the same sort as the sort of the location of the heap * that is constrained to be empty - * -[2]: Term of the same sort as the data sort of the heap that is + * - 2: Term of the same sort as the data sort of the heap that is * that is constrained to be empty + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEP_EMP, /** * Separation logic points-to relation. - * Parameters: 2 - * -[1]: Location of the points-to constraint - * -[2]: Data of the points-to constraint + * + * Parameters: + * - 1: Location of the points-to constraint + * - 2: Data of the points-to constraint + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEP_PTO, /** * Separation logic star. - * Parameters: n >= 2 - * -[1]..[n]: Child constraints that hold in disjoint (separated) heaps + * + * Parameters: n > 1 + * - 1..n: Child constraints that hold in disjoint (separated) heaps + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEP_STAR, /** * Separation logic magic wand. - * Parameters: 2 - * -[1]: Antecendant of the magic wand constraint - * -[2]: Conclusion of the magic wand constraint, which is asserted to + * + * Parameters: + * - 1: Antecendant of the magic wand constraint + * - 2: Conclusion of the magic wand constraint, which is asserted to * hold in all heaps that are disjoint extensions of the antecedent. + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEP_WAND, #if 0 @@ -1808,150 +2156,183 @@ enum CVC4_EXPORT Kind : int32_t /** * Empty set constant. - * Parameters: 1 - * -[1]: Sort of the set elements + * + * Parameters: + * - 1: Sort of the set elements + * * Create with: - * mkEmptySet(Sort sort) + * - `Solver::mkEmptySet(const Sort& sort) const` */ EMPTYSET, /** * Set union. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ UNION, /** * Set intersection. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INTERSECTION, /** * Set subtraction. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SETMINUS, /** * Subset predicate. - * Parameters: 2 - * -[1]..[2]: Terms of set sort, [1] a subset of set [2]? + * + * Parameters: + * - 1..2: Terms of set sort, [1] a subset of set [2]? + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SUBSET, /** * Set membership predicate. - * Parameters: 2 - * -[1]..[2]: Terms of set sort, [1] a member of set [2]? + * + * Parameters: + * - 1..2: Terms of set sort, [1] a member of set [2]? + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ MEMBER, /** * Construct a singleton set from an element given as a parameter. * The returned set has same type of the element. - * Parameters: 1 - * -[1]: Single element + * + * Parameters: + * - 1: Single element + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SINGLETON, /** * The set obtained by inserting elements; + * * Parameters: n > 0 - * -[1]..[n-1]: Elements inserted into set [n] - * -[n]: Set Term + * - 1..n-1: Elements inserted into set [n] + * - n: Set Term + * * Create with: - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INSERT, /** * Set cardinality. - * Parameters: 1 - * -[1]: Set to determine the cardinality of + * + * Parameters: + * - 1: Set to determine the cardinality of + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ CARD, /** * Set complement with respect to finite universe. - * Parameters: 1 - * -[1]: Set to complement + * + * Parameters: + * - 1: Set to complement + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ COMPLEMENT, /** * Finite universe set. * All set variables must be interpreted as subsets of it. + * * Create with: - * mkUniverseSet(Sort sort) + * - `Solver::mkUniverseSet(const Sort& sort) const` */ UNIVERSE_SET, /** * Set join. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ JOIN, /** * Set cartesian product. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ PRODUCT, /** * Set transpose. - * Parameters: 1 - * -[1]: Term of set sort + * + * Parameters: + * - 1: Term of set sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ TRANSPOSE, /** * Set transitive closure. - * Parameters: 1 - * -[1]: Term of set sort + * + * Parameters: + * - 1: Term of set sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ TCLOSURE, /** * Set join image. - * Parameters: 2 - * -[1]..[2]: Terms of set sort + * + * Parameters: + * - 1..2: Terms of set sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ JOIN_IMAGE, /** * Set identity. - * Parameters: 1 - * -[1]: Term of set sort + * + * Parameters: + * - 1: Term of set sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ IDEN, /** @@ -1959,20 +2340,22 @@ enum CVC4_EXPORT Kind : int32_t * A set comprehension is specified by a bound variable list x1 ... xn, * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the * above form has members given by the following semantics: - * \verbatim - * forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C) - * \endverbatim + * @f[ + * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) \Leftrightarrow (member y C) + * @f] * where y ranges over the element type of the (set) type of the - * comprehension. If t[x1..xn] is not provided, it is equivalent to y in the + * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to y in the * above formula. - * Parameters: 2 (3) - * -[1]: Term BOUND_VAR_LIST - * -[2]: Term denoting the predicate of the comprehension - * -[3]: (optional) a Term denoting the generator for the comprehension + * + * Parameters: + * - 1: Term BOUND_VAR_LIST + * - 2: Term denoting the predicate of the comprehension + * - 3: (optional) a Term denoting the generator for the comprehension + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ COMPREHENSION, /** @@ -1981,118 +2364,143 @@ enum CVC4_EXPORT Kind : int32_t * If the set is empty, then (choose A) is an arbitrary value. * If the set has cardinality > 1, then (choose A) will deterministically * return an element in A. - * Parameters: 1 - * -[1]: Term of set sort + * + * Parameters: + * - 1: Term of set sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ CHOOSE, /** * Set is_singleton predicate. - * Parameters: 1 - * -[1]: Term of set sort, is [1] a singleton set? + * + * Parameters: + * - 1: Term of set sort, is [1] a singleton set? + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ IS_SINGLETON, /* Bags ------------------------------------------------------------------ */ /** * Empty bag constant. - * Parameters: 1 - * -[1]: Sort of the bag elements + * + * Parameters: + * - 1: Sort of the bag elements + * * Create with: - * mkEmptyBag(Sort sort) + * mkEmptyBag(const Sort& sort) */ EMPTYBAG, /** * Bag max union. - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * Parameters: + * - 1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ UNION_MAX, /** * Bag disjoint union (sum). - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * + * Parameters: + * -1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ UNION_DISJOINT, /** * Bag intersection (min). - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * + * Parameters: + * - 1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INTERSECTION_MIN, /** * Bag difference subtract (subtracts multiplicities of the second from the * first). - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * + * Parameters: + * - 1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DIFFERENCE_SUBTRACT, /** * Bag difference 2 (removes shared elements in the two bags). - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * + * Parameters: + * - 1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DIFFERENCE_REMOVE, /** * Inclusion predicate for bags * (multiplicities of the first bag <= multiplicities of the second bag). - * Parameters: 2 - * -[1]..[2]: Terms of bag sort + * + * Parameters: + * - 1..2: Terms of bag sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SUBBAG, /** * Element multiplicity in a bag - * Parameters: 2 - * -[1]..[2]: Terms of bag sort (Bag E), [1] an element of sort E + * + * Parameters: + * - 1..2: Terms of bag sort (Bag E), [1] an element of sort E + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BAG_COUNT, /** * Eliminate duplicates in a given bag. The returned bag contains exactly the * same elements in the given bag, but with multiplicity one. - * Parameters: 1 - * -[1]: a term of bag sort + * + * Parameters: + * - 1: a term of bag sort + * * Create with: - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ DUPLICATE_REMOVAL, /** * The bag of the single element given as a parameter. - * Parameters: 1 - * -[1]: Single element + * + * Parameters: + * - 1: Single element + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ MK_BAG, /** * Bag cardinality. - * Parameters: 1 - * -[1]: Bag to determine the cardinality of + * + * Parameters: + * - 1: Bag to determine the cardinality of + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_CARD, /** @@ -2102,34 +2510,41 @@ enum CVC4_EXPORT Kind : int32_t * If the bag is empty, then (choose A) is an arbitrary value. * If the bag contains distinct elements, then (choose A) will * deterministically return an element in A. - * Parameters: 1 - * -[1]: Term of bag sort + * + * Parameters: + * - 1: Term of bag sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_CHOOSE, /** * Bag is_singleton predicate (single element with multiplicity exactly one). - * Parameters: 1 - * -[1]: Term of bag sort, is [1] a singleton bag? + * Parameters: + * - 1: Term of bag sort, is [1] a singleton bag? + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_IS_SINGLETON, /** * Bag.from_set converts a set to a bag. - * Parameters: 1 - * -[1]: Term of set sort + * + * Parameters: + * - 1: Term of set sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_FROM_SET, /** * Bag.to_set converts a bag to a set. - * Parameters: 1 - * -[1]: Term of bag sort + * + * Parameters: + * - 1: Term of bag sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_TO_SET, @@ -2137,30 +2552,36 @@ enum CVC4_EXPORT Kind : int32_t /** * String concat. + * * Parameters: n > 1 - * -[1]..[n]: Terms of String sort + * - 1..n: Terms of String sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_CONCAT, /** * String membership. - * Parameters: 2 - * -[1]: Term of String sort - * -[2]: Term of RegExp sort + * + * Parameters: + * - 1: Term of String sort + * - 2: Term of RegExp sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_IN_REGEXP, /** * String length. - * Parameters: 1 - * -[1]: Term of String sort + * + * Parameters: + * - 1: Term of String sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_LENGTH, /** @@ -2169,13 +2590,15 @@ enum CVC4_EXPORT Kind : int32_t * s. If the start index is negative, the start index is greater than the * length of the string, or the length is negative, the result is the empty * string. - * Parameters: 3 - * -[1]: Term of sort String - * -[2]: Term of sort Integer (index i) - * -[3]: Term of sort Integer (length l) + * + * Parameters: + * - 1: Term of sort String + * - 2: Term of sort Integer (index i) + * - 3: Term of sort Integer (length l) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_SUBSTR, /** @@ -2184,13 +2607,15 @@ enum CVC4_EXPORT Kind : int32_t * If the start index is negative, the start index is greater than the * length of the string, the result is s. Otherwise, the length of the * original string is preserved. - * Parameters: 3 - * -[1]: Term of sort String - * -[2]: Term of sort Integer (index i) - * -[3]: Term of sort String (replacement string t) + * + * Parameters: + * - 1: Term of sort String + * - 2: Term of sort Integer (index i) + * - 3: Term of sort String (replacement string t) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_UPDATE, /** @@ -2198,24 +2623,28 @@ enum CVC4_EXPORT Kind : int32_t * Returns the character at index i from a string s. If the index is negative * or the index is greater than the length of the string, the result is the * empty string. Otherwise the result is a string of length 1. - * Parameters: 2 - * -[1]: Term of sort String (string s) - * -[2]: Term of sort Integer (index i) + * + * Parameters: + * - 1: Term of sort String (string s) + * - 2: Term of sort Integer (index i) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_CHARAT, /** * String contains. * Checks whether a string s1 contains another string s2. If s2 is empty, the * result is always true. - * Parameters: 2 - * -[1]: Term of sort String (the string s1) - * -[2]: Term of sort String (the string s2) + * + * Parameters: + * - 1: Term of sort String (the string s1) + * - 2: Term of sort String (the string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_CONTAINS, /** @@ -2223,39 +2652,45 @@ enum CVC4_EXPORT Kind : int32_t * Returns the index of a substring s2 in a string s1 starting at index i. If * the index is negative or greater than the length of string s1 or the * substring s2 does not appear in string s1 after index i, the result is -1. - * Parameters: 3 - * -[1]: Term of sort String (substring s1) - * -[2]: Term of sort String (substring s2) - * -[3]: Term of sort Integer (index i) + * + * Parameters: + * - 1: Term of sort String (substring s1) + * - 2: Term of sort String (substring s2) + * - 3: Term of sort Integer (index i) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_INDEXOF, /** * String replace. * Replaces a string s2 in a string s1 with string s3. If s2 does not appear * in s1, s1 is returned unmodified. - * Parameters: 3 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort String (string s2) - * -[3]: Term of sort String (string s3) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort String (string s2) + * - 3: Term of sort String (string s3) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_REPLACE, /** * String replace all. * Replaces all occurrences of a string s2 in a string s1 with string s3. * If s2 does not appear in s1, s1 is returned unmodified. - * Parameters: 3 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort String (string s2) - * -[3]: Term of sort String (string s3) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort String (string s2) + * - 3: Term of sort String (string s3) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_REPLACE_ALL, /** @@ -2263,60 +2698,72 @@ enum CVC4_EXPORT Kind : int32_t * Replaces the first match of a regular expression r in string s1 with * string s2. If r does not match a substring of s1, s1 is returned * unmodified. - * Parameters: 3 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort Regexp (regexp r) - * -[3]: Term of sort String (string s2) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort Regexp (regexp r) + * - 3: Term of sort String (string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_REPLACE_RE, /** * String replace all regular expression matches. * Replaces all matches of a regular expression r in string s1 with string * s2. If r does not match a substring of s1, s1 is returned unmodified. - * Parameters: 3 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort Regexp (regexp r) - * -[3]: Term of sort String (string s2) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort Regexp (regexp r) + * - 3: Term of sort String (string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_REPLACE_RE_ALL, /** * String to lower case. - * Parameters: 1 - * -[1]: Term of String sort + * + * Parameters: + * - 1: Term of String sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_TOLOWER, /** * String to upper case. - * Parameters: 1 - * -[1]: Term of String sort + * + * Parameters: + * - 1: Term of String sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_TOUPPER, /** * String reverse. - * Parameters: 1 - * -[1]: Term of String sort + * + * Parameters: + * - 1: Term of String sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_REV, /** * String to code. * Returns the code point of a string if it has length one, or returns -1 * otherwise. - * Parameters: 1 - * -[1]: Term of String sort + * + * Parameters: + * - 1: Term of String sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_TO_CODE, /** @@ -2324,253 +2771,306 @@ enum CVC4_EXPORT Kind : int32_t * Returns a string containing a single character whose code point matches * the argument to this function, or the empty string if the argument is * out-of-bounds. - * Parameters: 1 - * -[1]: Term of Integer sort + * + * Parameters: + * - 1: Term of Integer sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_FROM_CODE, /** * String less than. * Returns true if string s1 is (strictly) less than s2 based on a * lexiographic ordering over code points. - * Parameters: 2 - * -[1]: Term of sort String (the string s1) - * -[2]: Term of sort String (the string s2) + * + * Parameters: + * - 1: Term of sort String (the string s1) + * - 2: Term of sort String (the string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_LT, /** * String less than or equal. * Returns true if string s1 is less than or equal to s2 based on a * lexiographic ordering over code points. - * Parameters: 2 - * -[1]: Term of sort String (the string s1) - * -[2]: Term of sort String (the string s2) + * + * Parameters: + * - 1: Term of sort String (the string s1) + * - 2: Term of sort String (the string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_LEQ, /** * String prefix-of. * Checks whether a string s1 is a prefix of string s2. If string s1 is * empty, this operator returns true. - * Parameters: 2 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort String (string s2) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort String (string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_PREFIX, /** * String suffix-of. * Checks whether a string s1 is a suffix of string 2. If string s1 is empty, * this operator returns true. - * Parameters: 2 - * -[1]: Term of sort String (string s1) - * -[2]: Term of sort String (string s2) + * + * Parameters: + * - 1: Term of sort String (string s1) + * - 2: Term of sort String (string s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_SUFFIX, /** * String is-digit. * Returns true if string s is digit (it is one of "0", ..., "9"). - * Parameters: 1 - * -[1]: Term of sort String + * + * Parameters: + * - 1: Term of sort String + * * Create with: - * mkTerm(Kind kind, Term child1) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ STRING_IS_DIGIT, /** * Integer to string. * If the integer is negative this operator returns the empty string. - * Parameters: 1 - * -[1]: Term of sort Integer + * + * Parameters: + * - 1: Term of sort Integer + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_FROM_INT, /** * String to integer (total function). * If the string does not contain an integer or the integer is negative, the * operator returns -1. - * Parameters: 1 - * -[1]: Term of sort String + * + * Parameters: + * - 1: Term of sort String + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_TO_INT, /** * Constant string. + * * Parameters: - * See mkString() + * - See @ref cvc5::api::Solver::mkString() "mkString()". + * * Create with: - * mkString(const char* s) - * mkString(const std::string& s) - * mkString(const unsigned char c) - * mkString(const std::vector<unsigned>& s) + * - `Solver::mkString(const std::string& s, bool useEscSequences) const` + * - `Solver::mkString(const unsigned char c) const` + * - `Solver::mkString(const std::vector<uint32_t>& s) const` */ CONST_STRING, /** * Conversion from string to regexp. - * Parameters: 1 - * -[1]: Term of sort String + * + * Parameters: + * - 1: Term of sort String + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ STRING_TO_REGEXP, /** - * Regexp Concatenation . - * Parameters: 2 - * -[1]..[2]: Terms of Regexp sort + * Regexp Concatenation. + * + * Parameters: + * - 1..2: Terms of Regexp sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ REGEXP_CONCAT, /** * Regexp union. - * Parameters: 2 - * -[1]..[2]: Terms of Regexp sort + * + * Parameters: + * - 1..2: Terms of Regexp sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ REGEXP_UNION, /** * Regexp intersection. - * Parameters: 2 - * -[1]..[2]: Terms of Regexp sort + * + * Parameters: + * - 1..2: Terms of Regexp sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ REGEXP_INTER, /** * Regexp difference. - * Parameters: 2 - * -[1]..[2]: Terms of Regexp sort + * + * Parameters: + * - 1..2: Terms of Regexp sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ REGEXP_DIFF, /** * Regexp *. - * Parameters: 1 - * -[1]: Term of sort Regexp + * + * Parameters: + * - 1: Term of sort Regexp + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ REGEXP_STAR, /** * Regexp +. - * Parameters: 1 - * -[1]: Term of sort Regexp + * + * Parameters: + * - 1: Term of sort Regexp + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ REGEXP_PLUS, /** * Regexp ?. - * Parameters: 1 - * -[1]: Term of sort Regexp + * + * Parameters: + * - 1: Term of sort Regexp + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ REGEXP_OPT, /** * Regexp range. - * Parameters: 2 - * -[1]: Lower bound character for the range - * -[2]: Upper bound character for the range + * + * Parameters: + * - 1: Lower bound character for the range + * - 2: Upper bound character for the range + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ REGEXP_RANGE, /** * Operator for regular expression repeat. - * Parameters: 1 - * -[1]: The number of repetitions + * + * Parameters: + * - 1: The number of repetitions + * * Create with: - * mkOp(Kind kind, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Apply regular expression loop. - * Parameters: 2 - * -[1]: Op of kind REGEXP_REPEAT - * -[2]: Term of regular expression sort + * + * Parameters: + * - 1: Op of kind REGEXP_REPEAT + * - 2: Term of regular expression sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ REGEXP_REPEAT, /** * Operator for regular expression loop, from lower bound to upper bound * number of repetitions. - * Parameters: 2 - * -[1]: The lower bound - * -[2]: The upper bound + * + * Parameters: + * - 1: The lower bound + * - 2: The upper bound + * * Create with: - * mkOp(Kind kind, uint32_t param, uint32_t param) + * - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const` * * Apply regular expression loop. - * Parameters: 2 - * -[1]: Op of kind REGEXP_LOOP - * -[2]: Term of regular expression sort + * + * Parameters: + * - 1: Op of kind REGEXP_LOOP + * - 2: Term of regular expression sort + * * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector<Term>& children) + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ REGEXP_LOOP, /** * Regexp empty. - * Parameters: 0 + * + * Parameters: none + * * Create with: - * mkRegexpEmpty() - * mkTerm(Kind kind) + * - `Solver::mkRegexpEmpty() const` + * - `Solver::mkTerm(Kind kind) const` */ REGEXP_EMPTY, /** * Regexp all characters. - * Parameters: 0 + * + * Parameters: none + * * Create with: - * mkRegexpSigma() - * mkTerm(Kind kind) + * - `Solver::mkRegexpSigma() const` + * - `Solver::mkTerm(Kind kind) const` */ REGEXP_SIGMA, /** * Regexp complement. - * Parameters: 1 - * -[1]: Term of sort RegExp + * + * Parameters: + * - 1: Term of sort RegExp + * * Create with: - * mkTerm(Kind kind, Term child1) + * - `Solver::mkTerm(Kind kind, const Term& child1) const` */ REGEXP_COMPLEMENT, /** * Sequence concat. + * * Parameters: n > 1 - * -[1]..[n]: Terms of Sequence sort + * - 1..n: Terms of Sequence sort + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_CONCAT, /** * Sequence length. - * Parameters: 1 - * -[1]: Term of Sequence sort + * + * Parameters: + * - 1: Term of Sequence sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SEQ_LENGTH, /** @@ -2578,13 +3078,16 @@ enum CVC4_EXPORT Kind : int32_t * Extracts a subsequence, starting at index i and of length l, from a * sequence s. If the start index is negative, the start index is greater * than the length of the sequence, or the length is negative, the result is - * the empty sequence. Parameters: 3 - * -[1]: Term of sort Sequence - * -[2]: Term of sort Integer (index i) - * -[3]: Term of sort Integer (length l) + * the empty sequence. + * + * Parameters: + * - 1: Term of sort Sequence + * - 2: Term of sort Integer (index i) + * - 3: Term of sort Integer (length l) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_EXTRACT, /** @@ -2593,13 +3096,15 @@ enum CVC4_EXPORT Kind : int32_t * If the start index is negative, the start index is greater than the * length of the sequence, the result is s. Otherwise, the length of the * original sequence is preserved. - * Parameters: 3 - * -[1]: Term of sort Sequence - * -[2]: Term of sort Integer (index i) - * -[3]: Term of sort Sequence (replacement sequence t) + * + * Parameters: + * - 1: Term of sort Sequence + * - 2: Term of sort Integer (index i) + * - 3: Term of sort Sequence (replacement sequence t) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_UPDATE, /** @@ -2607,23 +3112,28 @@ enum CVC4_EXPORT Kind : int32_t * Returns the element at index i from a sequence s. If the index is negative * or the index is greater or equal to the length of the sequence, the result * is the empty sequence. Otherwise the result is a sequence of length 1. - * Parameters: 2 - * -[1]: Term of sequence sort (string s) - * -[2]: Term of sort Integer (index i) + * + * Parameters: + * - 1: Term of sequence sort (string s) + * - 2: Term of sort Integer (index i) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_AT, /** * Sequence contains. * Checks whether a sequence s1 contains another sequence s2. If s2 is empty, - * the result is always true. Parameters: 2 - * -[1]: Term of sort Sequence (the sequence s1) - * -[2]: Term of sort Sequence (the sequence s2) + * the result is always true. + * + * Parameters: + * - 1: Term of sort Sequence (the sequence s1) + * - 2: Term of sort Sequence (the sequence s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_CONTAINS, /** @@ -2631,99 +3141,123 @@ enum CVC4_EXPORT Kind : int32_t * Returns the index of a subsequence s2 in a sequence s1 starting at index i. * If the index is negative or greater than the length of sequence s1 or the * subsequence s2 does not appear in sequence s1 after index i, the result is - * -1. Parameters: 3 - * -[1]: Term of sort Sequence (subsequence s1) - * -[2]: Term of sort Sequence (subsequence s2) - * -[3]: Term of sort Integer (index i) + * -1. + * + * Parameters: + * - 1: Term of sort Sequence (subsequence s1) + * - 2: Term of sort Sequence (subsequence s2) + * - 3: Term of sort Integer (index i) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_INDEXOF, /** * Sequence replace. * Replaces the first occurrence of a sequence s2 in a sequence s1 with * sequence s3. If s2 does not appear in s1, s1 is returned unmodified. - * Parameters: 3 - * -[1]: Term of sort Sequence (sequence s1) - * -[2]: Term of sort Sequence (sequence s2) - * -[3]: Term of sort Sequence (sequence s3) + * + * Parameters: + * - 1: Term of sort Sequence (sequence s1) + * - 2: Term of sort Sequence (sequence s2) + * - 3: Term of sort Sequence (sequence s3) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_REPLACE, /** * Sequence replace all. * Replaces all occurrences of a sequence s2 in a sequence s1 with sequence - * s3. If s2 does not appear in s1, s1 is returned unmodified. Parameters: 3 - * -[1]: Term of sort Sequence (sequence s1) - * -[2]: Term of sort Sequence (sequence s2) - * -[3]: Term of sort Sequence (sequence s3) + * s3. If s2 does not appear in s1, s1 is returned unmodified. + * + * Parameters: + * - 1: Term of sort Sequence (sequence s1) + * - 2: Term of sort Sequence (sequence s2) + * - 3: Term of sort Sequence (sequence s3) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_REPLACE_ALL, /** * Sequence reverse. - * Parameters: 1 - * -[1]: Term of Sequence sort + * + * Parameters: + * - 1: Term of Sequence sort + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ SEQ_REV, /** * Sequence prefix-of. * Checks whether a sequence s1 is a prefix of sequence s2. If sequence s1 is * empty, this operator returns true. - * Parameters: 2 - * -[1]: Term of sort Sequence (sequence s1) - * -[2]: Term of sort Sequence (sequence s2) + * + * Parameters: + * - 1: Term of sort Sequence (sequence s1) + * - 2: Term of sort Sequence (sequence s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_PREFIX, /** * Sequence suffix-of. * Checks whether a sequence s1 is a suffix of sequence s2. If sequence s1 is - * empty, this operator returns true. Parameters: 2 - * -[1]: Term of sort Sequence (sequence s1) - * -[2]: Term of sort Sequence (sequence s2) + * empty, this operator returns true. + * + * Parameters: + * - 1: Term of sort Sequence (sequence s1) + * - 2: Term of sort Sequence (sequence s2) + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ SEQ_SUFFIX, /** * Constant sequence. + * * Parameters: - * See mkEmptySequence() + * - See @ref cvc5::api::Solver::mkEmptySequence() "mkEmptySequence()". + * * Create with: - * mkEmptySequence(Sort sort) + * - `Solver::mkEmptySequence(const Sort& sort) const` + * * Note that a constant sequence is a term that is equivalent to: - * (seq.++ (seq.unit c1) ... (seq.unit cn)) + * + * (seq.++ (seq.unit c1) ... (seq.unit cn)) + * * where n>=0 and c1, ..., cn are constants of some sort. The elements - * can be extracted by Term::getConstSequenceElements(). + * can be extracted by `Term::getConstSequenceElements()`. */ CONST_SEQUENCE, /** * Sequence unit, corresponding to a sequence of length one with the given * term. - * Parameters: 1 - * -[1] Element term. + * + * Parameters: + * - 1: Element term. + * * Create with: - * mkTerm(Kind kind, Term child1) + * - `Solver::mkTerm(Kind kind, const Term& child1) const` */ SEQ_UNIT, /** * Sequence nth, corresponding to the nth element of a sequence. - * Parameters: 2 - * -[1] Sequence term. - * -[2] Integer term. + * + * Parameters: + * - 1: Sequence term. + * - 2: Integer term. + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` */ SEQ_NTH, @@ -2731,81 +3265,95 @@ enum CVC4_EXPORT Kind : int32_t /** * Universally quantified formula. - * Parameters: 2 (3) - * -[1]: BOUND_VAR_LIST Term - * -[2]: Quantifier body - * -[3]: (optional) INST_PATTERN_LIST Term + * + * Parameters: + * - 1: BOUND_VAR_LIST Term + * - 2: Quantifier body + * - 3: (optional) INST_PATTERN_LIST Term + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ FORALL, /** * Existentially quantified formula. - * Parameters: 2 (3) - * -[1]: BOUND_VAR_LIST Term - * -[2]: Quantifier body - * -[3]: (optional) INST_PATTERN_LIST Term + * + * Parameters: + * - 1: BOUND_VAR_LIST Term + * - 2: Quantifier body + * - 3: (optional) INST_PATTERN_LIST Term + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ EXISTS, - /* + /** * A list of bound variables (used to bind variables under a quantifier) + * * Parameters: n > 1 - * -[1]..[n]: Terms with kind BOUND_VARIABLE + * - 1..n: Terms with kind BOUND_VARIABLE + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ BOUND_VAR_LIST, - /* + /** * An instantiation pattern. * Specifies a (list of) terms to be used as a pattern for quantifier * instantiation. + * * Parameters: n > 1 - * -[1]..[n]: Terms with kind BOUND_VARIABLE + * - 1..n: Terms with kind BOUND_VARIABLE + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INST_PATTERN, - /* + /** * An instantiation no-pattern. * Specifies a (list of) terms that should not be used as a pattern for * quantifier instantiation. + * * Parameters: n > 1 - * -[1]..[n]: Terms with kind BOUND_VARIABLE + * - 1..n: Terms with kind BOUND_VARIABLE + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INST_NO_PATTERN, - /* + /** * An instantiation attribute * Specifies a custom property for a quantified formula given by a * term that is ascribed a user attribute. - * Parameters: 1 - * -[1]: Term with a user attribute. + * + * Parameters: + * - 1: Term with a user attribute. + * * Create with: - * mkTerm(Kind kind, Term child) + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ INST_ATTRIBUTE, - /* + /** * A list of instantiation patterns and/or attributes. + * * Parameters: n > 1 - * -[1]..[n]: Terms with kind INST_PATTERN, INST_NO_PATTERN, or + * - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or * INST_ATTRIBUTE. + * * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ INST_PATTERN_LIST, #if 0 @@ -2845,7 +3393,7 @@ enum CVC4_EXPORT Kind : int32_t #endif /* ----------------------------------------------------------------------- */ - /* marks the upper-bound of this enumeration */ + /** Marks the upper-bound of this enumeration. */ LAST_KIND }; @@ -2869,6 +3417,9 @@ std::ostream& operator<<(std::ostream& out, Kind k) CVC4_EXPORT; */ struct CVC4_EXPORT KindHashFunction { + /** + * Hashes a Kind to a size_t. + */ size_t operator()(Kind k) const; }; |