/* Kind */
/* -------------------------------------------------------------------------- */
-// TODO(Gereon): Fix links that involve std::vector. See https://github.com/doxygen/doxygen/issues/8503
+// TODO(Gereon): Fix links that involve std::vector. See
+// https://github.com/doxygen/doxygen/issues/8503
+// clang-format off
/**
* The kind of a cvc5 term.
*
- * Note that the underlying type of Kind must be signed (to enable range
- * checks for validity). The size of this type depends on the size of
- * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
+ * \internal
+ *
+ * Note that the API type `cvc5::api::Kind` roughly corresponds to
+ * `cvc5::Kind`, but is a different type. It hides internal kinds that should
+ * not be exported to the API, and maps all kinds that we want to export to its
+ * corresponding internal kinds. The underlying type of `cvc5::api::Kind` must
+ * be signed (to enable range checks for validity). The size of this type
+ * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10
+ * bits, see expr/node_value.h).
*/
-enum CVC5_EXPORT Kind : int32_t
+enum Kind : int32_t
{
/**
* Internal kind.
* Lambda expression.
*
* Parameters:
- * - 1: BOUND_VAR_LIST
+ * - 1: VARIABLE_LIST
* - 2: Lambda body
*
* Create with:
LAMBDA,
/**
* The syntax of a witness term is similar to a quantified formula except that
- * only one bound variable is allowed.
+ * only one variable is allowed.
* The term `(witness ((x T)) F)` returns an element `x` of type `T`
* and asserts `F`.
*
* whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
*
* Parameters:
- * - 1: BOUND_VAR_LIST
+ * - 1: VARIABLE_LIST
* - 2: Witness body
*
* Create with:
* - `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: Term of sort S
- *
- * Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child1) const`
- * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
- */
- CARDINALITY_VALUE,
-#if 0
- /* Combined cardinality constraint. */
- COMBINED_CARDINALITY_CONSTRAINT,
- /* Partial uninterpreted function application. */
- PARTIAL_APPLY_UF,
-#endif
/**
* Higher-order applicative encoding of function application, left
* associative.
*/
MULT,
/**
- * Operator for Integer AND
+ * Operator for bit-wise AND over integers, parameterized by a (positive)
+ * bitwidth k.
+ *
+ * ((_ iand k) i1 i2) is equivalent to:
+ * (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
+ * for all integers i1, i2.
*
* Parameters:
* - 1: Size of the bit-vector that determines the semantics of the IAND
* Create with:
* - `Solver::mkOp(Kind kind, uint32_t param) const`
*
- * Apply integer conversion to bit-vector.
-
+ * Apply integer and.
+ *
* Parameters:
* - 1: Op of kind IAND
* - 2: Integer term
* - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
*/
IAND,
+ /**
+ * Operator for raising 2 to a non-negative integer power.
+ *
+ * Create with:
+ * - `Solver::mkOp(Kind kind) const`
+ *
+ * Parameters:
+ * - 1: Op of kind IAND
+ * - 2: Integer term
+ *
+ * Apply 2 to the power operator.
+ *
+ * Create with:
+ * - `Solver::mkTerm(const Op& op, const Term& child) const`
+ * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+ */
+ POW2,
#if 0
/* Synonym for MULT. */
NONLINEAR_MULT,
/**
* Pi constant.
*
+ * Note that PI is considered a special symbol of sort Real, but is not
+ * a real value, i.e., `Term::isRealValue() const` will return false.
+ *
* Create with:
* - `Solver::mkPi() const`
* - `Solver::mkTerm(Kind kind) 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,
+ BITVECTOR_ADD,
/**
* Subtraction of two bit-vectors.
*
*/
BITVECTOR_NEG,
/**
- * Unsigned division of two bit-vectors, truncating towards 0.
- *
- * Note: The semantics of this operator depends on `bv-div-zero-const`
- * (default is true). Depending on the setting, a division by zero is
- * treated as all ones (default, corresponds to SMT-LIB >=2.6) or an
- * uninterpreted value (corresponds to SMT-LIB <2.6).
+ * Unsigned division of two bit-vectors, truncating towards 0. If the divisor
+ * is zero, the result is all ones.
*
* Parameters:
* - 1..2: Terms of bit-vector sort (sorts must match)
*/
BITVECTOR_UDIV,
/**
- * Unsigned remainder from truncating division of two bit-vectors.
- *
- * Note: The semantics of this operator depends on `bv-div-zero-const`
- * (default is true). Depending on the setting, if the modulus is zero, the
- * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or
- * an uninterpreted value (corresponds to SMT-LIB <2.6).
+ * Unsigned remainder from truncating division of two bit-vectors. If the
+ * modulus is zero, the result is the dividend.
*
* Parameters:
* - 1..2: Terms of bit-vector sort (sorts must match)
*/
BITVECTOR_UREM,
/**
- * Two's complement signed division of two bit-vectors.
- *
- * Note: The semantics of this operator depends on `bv-div-zero-const`
- * (default is true). By default, the function returns all ones if the
- * dividend is positive and one if the dividend is negative (corresponds to
- * 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).
+ * Two's complement signed division of two bit-vectors. If the divisor is
+ * zero and the dividend is positive, the result is all ones. If the divisor
+ * is zero and the dividend is negative, the result is one.
*
* Parameters:
* - 1..2: Terms of bit-vector sort (sorts must match)
*/
BITVECTOR_SDIV,
/**
- * Two's complement signed remainder of two bit-vectors
- * (sign follows dividend).
- *
- * Note: The semantics of this operator depends on `bv-div-zero-const`
- * (default is true, corresponds to SMT-LIB >=2.6). Depending on the setting,
- * if the modulus is zero, the result is either the dividend (default) or an
- * uninterpreted value (corresponds to SMT-LIB <2.6).
+ * Two's complement signed remainder of two bit-vectors (sign follows
+ * dividend). If the modulus is zero, the result is the dividend.
*
* Parameters:
* - 1..2: Terms of bit-vector sort (sorts must match)
*/
BITVECTOR_SREM,
/**
- * Two's complement signed remainder
- * (sign follows divisor).
- *
- * Note: The semantics of this operator depends on `bv-div-zero-const`
- * (default is on). Depending on the setting, if the modulus is zero, the
- * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or
- * an uninterpreted value (corresponds to SMT-LIB <2.6).
+ * Two's complement signed remainder (sign follows divisor). If the modulus
+ * is zero, the result is the dividend.
*
* Parameters:
* - 1..2: Terms of bit-vector sort (sorts must match)
* - `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,
+ FLOATINGPOINT_ADD,
/**
* Floating-point sutraction.
*
* - `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
+ * @note We currently support the creation of constant arrays, but under some
* conditions when there is a chain of equalities connecting two constant
- * arrays, the solver doesn't know what to do and aborts (Issue <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>).
+ * arrays, the solver doesn't know what to do and aborts (Issue <a
+ * href="https://github.com/cvc5/cvc5/issues/1667">#1667</a>).
*/
CONST_ARRAY,
/**
*/
APPLY_CONSTRUCTOR,
/**
- * Datatype selector application.
+ * Datatype selector application, which is undefined if misapplied.
*
* Parameters:
* - 1: Selector (operator)
- * - 2: Datatype term (undefined if mis-applied)
+ * - 2: Datatype term
*
* Create with:
* - `Solver::mkTerm(const Op& op, const Term& child) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
APPLY_TESTER,
-#if 0
- /* Parametric datatype term. */
- PARAMETRIC_DATATYPE,
- /* type ascription, for datatype constructor applications;
- * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor
- * application being ascribed */
- APPLY_TYPE_ASCRIPTION,
-#endif
- /**
- * Operator for a tuple update.
- *
- * Parameters:
- * - 1: Index of the tuple to be updated
- *
- * Create with:
- * - `Solver::mkOp(Kind kind, uint32_t param) const`
- *
- * Apply tuple update.
- *
- * 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:
- * - `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.
+ * Datatype update application, which does not change the argument if
+ * misapplied.
*
* Parameters:
- * - 1: Name of the field to be updated
- *
- * Create with:
- * - `Solver::mkOp(Kind kind, const std::string& param) const`
- *
- * Record update.
- *
- * 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
+ * - 1: Updater (operator)
+ * - 2: Datatype term
+ * - 3: Value to update a field of the datatype term with
*
* Create with:
- * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(const Op& op,, const std::vector<Term>& children) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- RECORD_UPDATE,
+ APPLY_UPDATER,
/**
* Match expressions.
* For example, the smt2 syntax match term
* is represented by the AST
*
* (MATCH l
- * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
+ * (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h)
* (MATCH_CASE nil 0))
*
* The type of the last argument of each case term could be equal.
* A (non-constant) case expression to be used within a match expression.
*
* Parameters:
- * - 1: a BOUND_VAR_LIST Term containing the free variables of the case
+ * - 1: a VARIABLE_LIST Term containing the free variables of the case
* - 2: Term denoting the pattern expression
* - 3: Term denoting the return value
*
*/
SEP_NIL,
/**
- * Separation logic empty 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
- * that is constrained to be empty
+ * Separation logic empty heap constraint
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ * - `Solver::mkTerm(Kind kind) const`
*/
SEP_EMP,
/**
* Create with:
* - `Solver::mkEmptySet(const Sort& sort) const`
*/
- EMPTYSET,
+ SET_EMPTY,
/**
* Set union.
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- UNION,
+ SET_UNION,
/**
* Set intersection.
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- INTERSECTION,
+ SET_INTER,
/**
* Set subtraction.
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- SETMINUS,
+ SET_MINUS,
/**
* Subset predicate.
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- SUBSET,
+ SET_SUBSET,
/**
* Set membership predicate.
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- MEMBER,
+ SET_MEMBER,
/**
* Construct a singleton set from an element given as a parameter.
* The returned set has same type of the element.
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- SINGLETON,
+ SET_SINGLETON,
/**
* The set obtained by inserting elements;
*
* - `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_INSERT,
/**
* Set cardinality.
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- CARD,
+ SET_CARD,
/**
* Set complement with respect to finite universe.
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- COMPLEMENT,
+ SET_COMPLEMENT,
/**
* Finite universe set.
* All set variables must be interpreted as subsets of it.
*
+ * Note that SET_UNIVERSE is considered a special symbol of the theory of
+ * sets and is not considered as a set value,
+ * i.e., `Term::isSetValue() const` will return false.
+ *
* Create with:
* - `Solver::mkUniverseSet(const Sort& sort) const`
*/
- UNIVERSE_SET,
+ SET_UNIVERSE,
/**
- * Set join.
+ * Set comprehension
+ * A set comprehension is specified by a variable list x1 ... xn,
+ * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
+ * above form has members given by the following semantics:
+ * @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 @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
+ * y in the above formula.
*
* Parameters:
- * - 1..2: Terms of set sort
+ * - 1: Term VARIABLE_LIST
+ * - 2: Term denoting the predicate of the comprehension
+ * - 3: (optional) a Term denoting the generator for the comprehension
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- JOIN,
+ SET_COMPREHENSION,
/**
- * Set cartesian product.
+ * Returns an element from a given set.
+ * If a set A = {x}, then the term (set.choose A) is equivalent to the term x.
+ * If the set is empty, then (set.choose A) is an arbitrary value.
+ * If the set has cardinality > 1, then (set.choose A) will deterministically
+ * return an element in A.
*
* Parameters:
- * - 1..2: Terms of set sort
+ * - 1: Term of set sort
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- PRODUCT,
+ SET_CHOOSE,
/**
- * Set transpose.
+ * Set is_singleton predicate.
*
* Parameters:
- * - 1: Term of set sort
+ * - 1: Term of set sort, is [1] a singleton set?
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- TRANSPOSE,
+ SET_IS_SINGLETON,
/**
- * Set transitive closure.
+ * set.map operator applies the first argument, a function of type (-> T1 T2),
+ * to every element of the second argument, a set of type (Set T1),
+ * and returns a set of type (Set T2).
*
* Parameters:
- * - 1: Term of set sort
+ * - 1: a function of type (-> T1 T2)
+ * - 2: a set of type (Set T1)
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2)
+ * const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- TCLOSURE,
+ SET_MAP,
+
+ /* Relations ------------------------------------------------------------- */
+
/**
- * Set join image.
+ * Set join.
*
* Parameters:
* - 1..2: Terms of set sort
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- JOIN_IMAGE,
+ RELATION_JOIN,
/**
- * Set identity.
+ * Set cartesian product.
*
* Parameters:
- * - 1: Term of set sort
+ * - 1..2: Terms of set sort
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- IDEN,
+ RELATION_PRODUCT,
/**
- * Set comprehension
- * 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:
- * @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 @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
- * y in the above formula.
+ * Set transpose.
*
* Parameters:
- * - 1: Term BOUND_VAR_LIST
- * - 2: Term denoting the predicate of the comprehension
- * - 3: (optional) a Term denoting the generator for the comprehension
+ * - 1: Term of set sort
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
- * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- COMPREHENSION,
+ RELATION_TRANSPOSE,
/**
- * Returns an element from a given set.
- * If a set A = {x}, then the term (choose A) is equivalent to the term x.
- * 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.
+ * Set transitive closure.
*
* Parameters:
* - 1: Term of set sort
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- CHOOSE,
+ RELATION_TCLOSURE,
/**
- * Set is_singleton predicate.
+ * Set join image.
*
* Parameters:
- * - 1: Term of set sort, is [1] a singleton set?
+ * - 1..2: Terms of set sort
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ RELATION_JOIN_IMAGE,
+ /**
+ * Set identity.
+ *
+ * Parameters:
+ * - 1: Term of set sort
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- IS_SINGLETON,
+ RELATION_IDEN,
+
/* Bags ------------------------------------------------------------------ */
+
/**
* Empty bag constant.
*
* Create with:
* mkEmptyBag(const Sort& sort)
*/
- EMPTYBAG,
+ BAG_EMPTY,
/**
* Bag max union.
* Parameters:
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- UNION_MAX,
+ BAG_UNION_MAX,
/**
* Bag disjoint union (sum).
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- UNION_DISJOINT,
+ BAG_UNION_DISJOINT,
/**
* Bag intersection (min).
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- INTERSECTION_MIN,
+ BAG_INTER_MIN,
/**
* Bag difference subtract (subtracts multiplicities of the second from the
* first).
* - `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_SUBTRACT,
/**
* Bag difference 2 (removes shared elements in the two bags).
*
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- DIFFERENCE_REMOVE,
+ BAG_DIFFERENCE_REMOVE,
/**
* Inclusion predicate for bags
* (multiplicities of the first bag <= multiplicities of the second bag).
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- SUBBAG,
+ BAG_SUBBAG,
/**
* Element multiplicity in a bag
*
* - `Solver::mkTerm(Kind kind, const Term& child) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- DUPLICATE_REMOVAL,
+ BAG_DUPLICATE_REMOVAL,
/**
- * The bag of the single element given as a parameter.
+ * Construct a bag with the given element and given multiplicity.
*
* Parameters:
- * - 1: Single element
+ * - 1: The element
+ * - 2: The multiplicity of the element.
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child) const`
+ * - `Solver::mkTerm(Kind kind, const Term& child, const Term& child) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- MK_BAG,
+ BAG_MAKE,
/**
* Bag cardinality.
*
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
BAG_TO_SET,
+ /**
+ * bag.map operator applies the first argument, a function of type (-> T1 T2),
+ * to every element of the second argument, a bag of type (Bag T1),
+ * and returns a bag of type (Bag T2).
+ *
+ * Parameters:
+ * - 1: a function of type (-> T1 T2)
+ * - 2: a bag of type (Bag T1)
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2)
+ * const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ BAG_MAP,
+ /**
+ * bag.fold operator combines elements of a bag into a single value.
+ * (bag.fold f t B) folds the elements of bag B starting with term t and using
+ * the combining function f.
+ *
+ * Parameters:
+ * - 1: a binary operation of type (-> T1 T2 T2)
+ * - 2: an initial value of type T2
+ * - 2: a bag of type (Bag T1)
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2,
+ * const Term& child3) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ BAG_FOLD,
/* Strings --------------------------------------------------------------- */
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
STRING_INDEXOF,
+ /**
+ * String index-of regular expression match.
+ * Returns the first match of a regular expression r in a string s. If the
+ * index is negative or greater than the length of string s1, or r does not
+ * match a substring in s after index i, the result is -1.
+ *
+ * Parameters:
+ * - 1: Term of sort String (string s)
+ * - 2: Term of sort RegLan (regular expression r)
+ * - 3: Term of sort Integer (index i)
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ STRING_INDEXOF_RE,
/**
* String replace.
* Replaces a string s2 in a string s1 with string s3. If s2 does not appear
*/
REGEXP_LOOP,
/**
- * Regexp empty.
+ * Regexp none.
*
* Parameters: none
*
* Create with:
- * - `Solver::mkRegexpEmpty() const`
+ * - `Solver::mkRegexpNone() const`
* - `Solver::mkTerm(Kind kind) const`
*/
- REGEXP_EMPTY,
+ REGEXP_NONE,
/**
* Regexp all characters.
*
* Parameters: none
*
* Create with:
- * - `Solver::mkRegexpSigma() const`
+ * - `Solver::mkRegexpAllchar() const`
* - `Solver::mkTerm(Kind kind) const`
*/
- REGEXP_SIGMA,
+ REGEXP_ALLCHAR,
/**
* Regexp complement.
*
* (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::getSequenceValue()`.
*/
CONST_SEQUENCE,
/**
* Universally quantified formula.
*
* Parameters:
- * - 1: BOUND_VAR_LIST Term
+ * - 1: VARIABLE_LIST Term
* - 2: Quantifier body
* - 3: (optional) INST_PATTERN_LIST Term
*
* Existentially quantified formula.
*
* Parameters:
- * - 1: BOUND_VAR_LIST Term
+ * - 1: VARIABLE_LIST Term
* - 2: Quantifier body
* - 3: (optional) INST_PATTERN_LIST Term
*
*/
EXISTS,
/**
- * A list of bound variables (used to bind variables under a quantifier)
+ * A list of variables (used to bind variables under a quantifier)
*
* Parameters: n > 1
- * - 1..n: Terms with kind BOUND_VARIABLE
+ * - 1..n: Terms with kind VARIABLE
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- BOUND_VAR_LIST,
+ VARIABLE_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 of any sort
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* quantifier instantiation.
*
* Parameters: n > 1
- * - 1..n: Terms with kind BOUND_VARIABLE
+ * - 1..n: Terms of any sort
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
* Specifies a custom property for a quantified formula given by a
* term that is ascribed a user attribute.
*
- * Parameters:
- * - 1: Term with a user attribute.
+ * Parameters: n >= 1
+ * - 1: The keyword of the attribute (a term with kind CONST_STRING).
+ * - 2...n: The values of the attribute.
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child) const`
+ * - `mkTerm(Kind kind, Term child1, Term child2)
+ * - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
+ * - `mkTerm(Kind kind, const std::vector<Term>& children)
*/
INST_ATTRIBUTE,
/**
/** Marks the upper-bound of this enumeration. */
LAST_KIND
};
+// clang-format on
/**
* Get the string representation of a given kind.
*/
std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT;
+} // namespace api
+} // namespace cvc5
+
+namespace std {
+
/**
* Hash function for Kinds.
*/
-struct CVC5_EXPORT KindHashFunction
+template<>
+struct CVC5_EXPORT hash<cvc5::api::Kind>
{
/**
* Hashes a Kind to a size_t.
*/
- size_t operator()(Kind k) const;
+ size_t operator()(cvc5::api::Kind k) const;
};
-} // namespace api
-} // namespace cvc5
+}
#endif
projects / cvc5.git / blobdiff