{OR, CVC4::Kind::OR},
{XOR, CVC4::Kind::XOR},
{ITE, CVC4::Kind::ITE},
+ {MATCH, CVC4::Kind::MATCH},
+ {MATCH_CASE, CVC4::Kind::MATCH_CASE},
+ {MATCH_BIND_CASE, CVC4::Kind::MATCH_BIND_CASE},
/* UF ------------------------------------------------------------------ */
{APPLY_UF, CVC4::Kind::APPLY_UF},
{CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT},
+ {CARDINALITY_VALUE, CVC4::Kind::CARDINALITY_VALUE},
{HO_APPLY, CVC4::Kind::HO_APPLY},
/* Arithmetic ---------------------------------------------------------- */
{PLUS, CVC4::Kind::PLUS},
{APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
{TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
{RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
+ {DT_SIZE, CVC4::Kind::DT_SIZE},
/* Separation Logic ---------------------------------------------------- */
{SEP_NIL, CVC4::Kind::SEP_NIL},
{SEP_EMP, CVC4::Kind::SEP_EMP},
{TCLOSURE, CVC4::Kind::TCLOSURE},
{JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE},
{IDEN, CVC4::Kind::IDEN},
+ {COMPREHENSION, CVC4::Kind::COMPREHENSION},
/* Strings ------------------------------------------------------------- */
{STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
{STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
{STRING_STRCTN, CVC4::Kind::STRING_STRCTN},
{STRING_STRIDOF, CVC4::Kind::STRING_STRIDOF},
{STRING_STRREPL, CVC4::Kind::STRING_STRREPL},
+ {STRING_STRREPLALL, CVC4::Kind::STRING_STRREPLALL},
+ {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER},
+ {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER},
+ {STRING_REV, CVC4::Kind::STRING_REV},
+ {STRING_CODE, CVC4::Kind::STRING_CODE},
+ {STRING_LT, CVC4::Kind::STRING_LT},
+ {STRING_LEQ, CVC4::Kind::STRING_LEQ},
{STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
{STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
{STRING_ITOS, CVC4::Kind::STRING_ITOS},
/* Quantifiers --------------------------------------------------------- */
{FORALL, CVC4::Kind::FORALL},
{EXISTS, CVC4::Kind::EXISTS},
+ {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST},
+ {INST_CLOSURE, CVC4::Kind::INST_CLOSURE},
+ {INST_PATTERN, CVC4::Kind::INST_PATTERN},
+ {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN},
+ {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE},
+ {INST_PATTERN_LIST, CVC4::Kind::INST_PATTERN_LIST},
{LAST_KIND, CVC4::Kind::LAST_KIND},
};
{CVC4::Kind::OR, OR},
{CVC4::Kind::XOR, XOR},
{CVC4::Kind::ITE, ITE},
+ {CVC4::Kind::MATCH, MATCH},
+ {CVC4::Kind::MATCH_CASE, MATCH_CASE},
+ {CVC4::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE},
/* UF -------------------------------------------------------------- */
{CVC4::Kind::APPLY_UF, APPLY_UF},
{CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
+ {CVC4::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE},
{CVC4::Kind::HO_APPLY, HO_APPLY},
/* Arithmetic ------------------------------------------------------ */
{CVC4::Kind::PLUS, PLUS},
{CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
{CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
{CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
+ {CVC4::Kind::DT_SIZE, DT_SIZE},
/* Separation Logic ------------------------------------------------ */
{CVC4::Kind::SEP_NIL, SEP_NIL},
{CVC4::Kind::SEP_EMP, SEP_EMP},
{CVC4::Kind::TCLOSURE, TCLOSURE},
{CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE},
{CVC4::Kind::IDEN, IDEN},
+ {CVC4::Kind::COMPREHENSION, COMPREHENSION},
/* Strings --------------------------------------------------------- */
{CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
{CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
{CVC4::Kind::STRING_STRCTN, STRING_STRCTN},
{CVC4::Kind::STRING_STRIDOF, STRING_STRIDOF},
{CVC4::Kind::STRING_STRREPL, STRING_STRREPL},
+ {CVC4::Kind::STRING_STRREPLALL, STRING_STRREPLALL},
+ {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER},
+ {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER},
+ {CVC4::Kind::STRING_REV, STRING_REV},
+ {CVC4::Kind::STRING_CODE, STRING_CODE},
+ {CVC4::Kind::STRING_LT, STRING_LT},
+ {CVC4::Kind::STRING_LEQ, STRING_LEQ},
{CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
{CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
{CVC4::Kind::STRING_ITOS, STRING_ITOS},
/* Quantifiers ----------------------------------------------------- */
{CVC4::Kind::FORALL, FORALL},
{CVC4::Kind::EXISTS, EXISTS},
+ {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
+ {CVC4::Kind::INST_CLOSURE, INST_CLOSURE},
+ {CVC4::Kind::INST_PATTERN, INST_PATTERN},
+ {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
+ {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
+ {CVC4::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST},
/* ----------------------------------------------------------------- */
{CVC4::Kind::LAST_KIND, LAST_KIND},
};
BOOLEAN_TERM_VARIABLE,
#endif
/**
- * Cardinality constraint on sort S.
+ * 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
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
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
+ * Create with:
+ * mkTerm(Kind kind, Term child1)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ CARDINALITY_VALUE,
#if 0
/* Combined cardinality constraint. */
COMBINED_CARDINALITY_CONSTRAINT,
/* Partial uninterpreted function application. */
PARTIAL_APPLY_UF,
- /* cardinality value of sort S:
- * first parameter is (any) term of sort S */
- CARDINALITY_VALUE,
#endif
/**
* Higher-order applicative encoding of function application.
* mkTerm(Op op,, const std::vector<Term>& children)
*/
RECORD_UPDATE,
-#if 0
- /* datatypes size */
+ /* Match expressions.
+ * For example, the smt2 syntax match term
+ * (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))
+ * 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
+ * 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)
+ *
+ */
+ MATCH,
+ /* 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
+ * Create with:
+ * mkTerm(Kind kind, Term child1, Term child2)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ MATCH_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
+ * Create with:
+ * mkTerm(Kind kind, Term child1, Term child2, Term child3)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ 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
+ * Create with:
+ * mkTerm(Kind kind, Term child1)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
DT_SIZE,
+#if 0
/* datatypes height bound */
DT_HEIGHT_BOUND,
/* datatypes height bound */
* mkTerm(Kind kind, Term child)
*/
IDEN,
+ /**
+ * 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:
+ * forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
+ * 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
+ * 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
+ * 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)
+ */
+ COMPREHENSION,
/* Strings --------------------------------------------------------------- */
/**
* String membership.
* Parameters: 2
- * -[1]..[2]: Terms of String sort
+ * -[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)
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
STRING_STRREPL,
+ /**
+ * 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)
+ * Create with:
+ * mkTerm(Kind kind, Term child1, Term child2, Term child3)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ STRING_STRREPLALL,
+ /**
+ * String to lower case.
+ * Parameters: 1
+ * -[1]: Term of String sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ STRING_TOLOWER,
+ /**
+ * String to upper case.
+ * Parameters: 1
+ * -[1]: Term of String sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ STRING_TOUPPER,
+ /**
+ * String reverse.
+ * Parameters: 1
+ * -[1]: Term of String sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ STRING_REV,
+ /**
+ * String code.
+ * Returns the code point of a string if it has length one, or returns -1
+ * otherwise.
+ * Parameters: 1
+ * -[1]: Term of String sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ STRING_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)
+ * Create with:
+ * mkTerm(Kind kind, Term child1, Term child2)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ 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)
+ * Create with:
+ * mkTerm(Kind kind, Term child1, Term child2)
+ * mkTerm(Kind kind, const std::vector<Term>& children)
+ */
+ STRING_LEQ,
/**
* String prefix-of.
* Checks whether a string s1 is a prefix of string s2. If string s1 is
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
EXISTS,
-#if 0
- /* instantiation constant */
- INST_CONSTANT,
- /* instantiation pattern */
- INST_PATTERN,
- /* a list of bound variables (used to bind variables under a quantifier) */
+ /*
+ * A list of bound variables (used to bind variables under a quantifier)
+ * Parameters: n > 1
+ * -[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)
+ */
BOUND_VAR_LIST,
- /* instantiation no-pattern */
+ /*
+ * A predicate for specifying term in instantiation closure.
+ * Parameters: 1
+ * -[1]: Term
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ INST_CLOSURE,
+ /*
+ * 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
+ * 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)
+ */
+ 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
+ * 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)
+ */
INST_NO_PATTERN,
- /* instantiation attribute */
+ /*
+ * 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.
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
INST_ATTRIBUTE,
- /* a list of instantiation patterns */
+ /*
+ * A list of instantiation patterns and/or attributes.
+ * Parameters: n > 1
+ * -[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)
+ */
INST_PATTERN_LIST,
- /* predicate for specifying term in instantiation closure. */
- INST_CLOSURE,
+#if 0
/* Sort Kinds ------------------------------------------------------------ */
projects / cvc5.git / commitdiff