From 8e4dbbe1ef9a82622a784f0a905d01ce4fdc1e7d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Feb 2020 12:00:14 -0600 Subject: [PATCH] Add missing kinds for the new API (#3757) --- src/api/cvc4cpp.cpp | 38 +++++++ src/api/cvc4cppkind.h | 233 ++++++++++++++++++++++++++++++++++++++---- 2 files changed, 253 insertions(+), 18 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f2c4d3dd3..ef7296089 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -85,9 +85,13 @@ const static std::unordered_map s_kinds{ {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}, @@ -225,6 +229,7 @@ const static std::unordered_map s_kinds{ {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}, @@ -249,6 +254,7 @@ const static std::unordered_map s_kinds{ {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}, @@ -258,6 +264,13 @@ const static std::unordered_map s_kinds{ {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}, @@ -277,6 +290,12 @@ const static std::unordered_map s_kinds{ /* 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}, }; @@ -304,9 +323,13 @@ const static std::unordered_map {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}, @@ -471,6 +494,7 @@ const static std::unordered_map {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}, @@ -495,6 +519,7 @@ const static std::unordered_map {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}, @@ -504,6 +529,13 @@ const static std::unordered_map {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}, @@ -523,6 +555,12 @@ const static std::unordered_map /* 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}, }; diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 2242c8e00..213dec56a 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -245,7 +245,9 @@ enum CVC4_PUBLIC Kind : int32_t 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 @@ -254,14 +256,22 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& 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& 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. @@ -1666,9 +1676,56 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Op op,, const std::vector& 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& 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& 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& 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& children) + */ DT_SIZE, +#if 0 /* datatypes height bound */ DT_HEIGHT_BOUND, /* datatypes height bound */ @@ -1887,6 +1944,25 @@ enum CVC4_PUBLIC Kind : int32_t * 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& children) + */ + COMPREHENSION, /* Strings --------------------------------------------------------------- */ @@ -1903,7 +1979,8 @@ enum CVC4_PUBLIC Kind : int32_t /** * 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& children) @@ -1984,6 +2061,77 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& 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& 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& 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& children) + */ + STRING_LEQ, /** * String prefix-of. * Checks whether a string s1 is a prefix of string s2. If string s1 is @@ -2166,21 +2314,70 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& 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& 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& 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& 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& children) + */ INST_PATTERN_LIST, - /* predicate for specifying term in instantiation closure. */ - INST_CLOSURE, +#if 0 /* Sort Kinds ------------------------------------------------------------ */ -- 2.30.2