From 9678f58a7fedab4fc061761c58382f4023686108 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Jul 2020 18:48:10 -0500 Subject: [PATCH] Front end support for sequences (#4690) With this PR, we now support a preliminary draft of a theory of sequences. This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them. As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term. We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++). --- NEWS | 2 + src/api/cvc4cpp.cpp | 107 ++++++++++++- src/api/cvc4cpp.h | 41 +++++ src/api/cvc4cppkind.h | 151 +++++++++++++++++- src/expr/expr_manager_template.cpp | 8 + src/expr/expr_manager_template.h | 3 + src/expr/expr_sequence.h | 2 + src/expr/sequence.h | 2 +- src/expr/type_node.cpp | 3 +- src/parser/cvc/Cvc.g | 3 + src/parser/parser.cpp | 16 ++ src/parser/smt2/Smt2.g | 8 +- src/parser/smt2/smt2.cpp | 25 ++- src/printer/cvc/cvc_printer.cpp | 28 +++- src/printer/smt2/smt2_printer.cpp | 30 +++- .../quantifiers/sygus/sygus_grammar_cons.cpp | 2 +- src/theory/strings/strings_entail.cpp | 4 +- src/theory/strings/term_registry.cpp | 2 +- .../strings/theory_strings_type_rules.h | 10 +- src/theory/strings/type_enumerator.cpp | 8 +- src/theory/strings/word.cpp | 9 ++ test/regress/CMakeLists.txt | 9 ++ test/regress/regress0/seq/seq-2var.smt2 | 8 + test/regress/regress0/seq/seq-ex1.smt2 | 10 ++ test/regress/regress0/seq/seq-ex2.smt2 | 9 ++ test/regress/regress0/seq/seq-ex3.smt2 | 18 +++ test/regress/regress0/seq/seq-ex4.smt2 | 8 + test/regress/regress0/seq/seq-ex5-dd.smt2 | 8 + test/regress/regress0/seq/seq-ex5.smt2 | 9 ++ test/regress/regress0/seq/seq-nemp.smt2 | 6 + test/regress/regress0/seq/seq-rewrites.smt2 | 44 +++++ test/unit/api/solver_black.h | 23 +++ test/unit/api/sort_black.h | 11 ++ test/unit/api/term_black.h | 27 ++++ 34 files changed, 626 insertions(+), 28 deletions(-) create mode 100644 test/regress/regress0/seq/seq-2var.smt2 create mode 100644 test/regress/regress0/seq/seq-ex1.smt2 create mode 100644 test/regress/regress0/seq/seq-ex2.smt2 create mode 100644 test/regress/regress0/seq/seq-ex3.smt2 create mode 100644 test/regress/regress0/seq/seq-ex4.smt2 create mode 100644 test/regress/regress0/seq/seq-ex5-dd.smt2 create mode 100644 test/regress/regress0/seq/seq-ex5.smt2 create mode 100644 test/regress/regress0/seq/seq-nemp.smt2 create mode 100644 test/regress/regress0/seq/seq-rewrites.smt2 diff --git a/NEWS b/NEWS index e453e7dbb..ee01b5212 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,8 @@ Changes since 1.8 ================= New Features: +* A new parametric theory of sequences whose syntax is compatible with the + syntax for sequences used by Z3. * Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true if arrays `a` and `b` are equal on all indices within indices `i` and `j`. diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 1e14e9b3a..49093acf5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -44,6 +44,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_manager.h" +#include "expr/sequence.h" #include "expr/type.h" #include "options/main_options.h" #include "options/options.h" @@ -288,6 +289,20 @@ const static std::unordered_map s_kinds{ {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY}, {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA}, {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT}, + // maps to the same kind as the string versions + {SEQ_CONCAT, CVC4::Kind::STRING_CONCAT}, + {SEQ_LENGTH, CVC4::Kind::STRING_LENGTH}, + {SEQ_EXTRACT, CVC4::Kind::STRING_SUBSTR}, + {SEQ_AT, CVC4::Kind::STRING_CHARAT}, + {SEQ_CONTAINS, CVC4::Kind::STRING_STRCTN}, + {SEQ_INDEXOF, CVC4::Kind::STRING_STRIDOF}, + {SEQ_REPLACE, CVC4::Kind::STRING_STRREPL}, + {SEQ_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL}, + {SEQ_REV, CVC4::Kind::STRING_REV}, + {SEQ_PREFIX, CVC4::Kind::STRING_PREFIX}, + {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX}, + {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE}, + {SEQ_UNIT, CVC4::Kind::SEQ_UNIT}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -559,6 +574,8 @@ const static std::unordered_map {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, + {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, + {CVC4::Kind::SEQ_UNIT, SEQ_UNIT}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, @@ -913,6 +930,8 @@ bool Sort::isArray() const { return d_type->isArray(); } bool Sort::isSet() const { return d_type->isSet(); } +bool Sort::isSequence() const { return d_type->isSequence(); } + bool Sort::isUninterpretedSort() const { return d_type->isSort(); } bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); } @@ -1021,6 +1040,14 @@ Sort Sort::getSetElementSort() const return Sort(d_solver, SetType(*d_type).getElementType()); } +/* Set sort ------------------------------------------------------------ */ + +Sort Sort::getSequenceElementSort() const +{ + CVC4_API_CHECK(isSequence()) << "Not a sequence sort."; + return Sort(d_solver, SequenceType(*d_type).getElementType()); +} + /* Uninterpreted sort -------------------------------------------------- */ std::string Sort::getUninterpretedSortName() const @@ -1364,6 +1391,36 @@ bool Term::isNullHelper() const return d_expr->isNull(); } +Kind Term::getKindHelper() const +{ + // Sequence kinds do not exist internally, so we must convert their internal + // (string) versions back to sequence. All operators where this is + // necessary are such that their first child is of sequence type, which + // we check here. + if (getNumChildren() > 0 && (*this)[0].getSort().isSequence()) + { + switch (d_expr->getKind()) + { + case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; + case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; + case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT; + case CVC4::Kind::STRING_CHARAT: return SEQ_AT; + case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS; + case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF; + case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE; + case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL; + case CVC4::Kind::STRING_REV: return SEQ_REV; + case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX; + case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX; + default: + // fall through to conversion below + break; + } + } + + return intToExtKind(d_expr->getKind()); +} + bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } @@ -1415,7 +1472,7 @@ uint64_t Term::getId() const Kind Term::getKind() const { CVC4_API_CHECK_NOT_NULL; - return intToExtKind(d_expr->getKind()); + return getKindHelper(); } Sort Term::getSort() const @@ -1484,10 +1541,9 @@ Op Term::getOp() const CVC4::Expr op = d_expr->getOperator(); return Op(d_solver, intToExtKind(d_expr->getKind()), op); } - else - { - return Op(d_solver, intToExtKind(d_expr->getKind())); - } + // Notice this is the only case where getKindHelper is used, since the + // cases above do have special cases for intToExtKind. + return Op(d_solver, getKindHelper()); } bool Term::isNull() const { return isNullHelper(); } @@ -1507,6 +1563,22 @@ Term Term::getConstArrayBase() const return Term(d_solver, d_expr->getConst().getExpr()); } +std::vector Term::getConstSequenceElements() const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::CONST_SEQUENCE) + << "Expecting a CONST_SEQUENCE Term when calling " + "getConstSequenceElements()"; + const std::vector& elems = + d_expr->getConst().getSequence().getVec(); + std::vector terms; + for (const Node& t : elems) + { + terms.push_back(Term(d_solver, t.toExpr())); + } + return terms; +} + Term Term::notTerm() const { CVC4_API_CHECK_NOT_NULL; @@ -3108,6 +3180,18 @@ Sort Solver::mkSetSort(Sort elemSort) const CVC4_API_SOLVER_TRY_CATCH_END; } +Sort Solver::mkSequenceSort(Sort elemSort) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) + << "non-null element sort"; + CVC4_API_SOLVER_CHECK_SORT(elemSort); + + return Sort(this, d_exprMgr->mkSequenceType(*elemSort.d_type)); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Sort Solver::mkUninterpretedSort(const std::string& symbol) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3350,6 +3434,19 @@ Term Solver::mkChar(const char* s) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkEmptySequence(Sort sort) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + CVC4_API_SOLVER_CHECK_SORT(sort); + + std::vector seq; + Expr res = d_exprMgr->mkConst(ExprSequence(*sort.d_type, seq)); + return Term(this, res); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkUniverseSet(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 76306d443..5223c9de6 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -379,6 +379,12 @@ class CVC4_PUBLIC Sort */ bool isSet() const; + /** + * Is this a Sequence sort? + * @return true if the sort is a Sequence sort + */ + bool isSequence() const; + /** * Is this a sort kind? * @return true if this is a sort kind @@ -512,6 +518,13 @@ class CVC4_PUBLIC Sort */ Sort getSetElementSort() const; + /* Sequence sort ------------------------------------------------------- */ + + /** + * @return the element sort of a sequence sort + */ + Sort getSequenceElementSort() const; + /* Uninterpreted sort -------------------------------------------------- */ /** @@ -906,6 +919,13 @@ class CVC4_PUBLIC Term */ Term getConstArrayBase() const; + /** + * Return the elements of a constant sequence + * throws an exception if the kind is not CONST_SEQUENCE + * @return the elements of the constant sequence. + */ + std::vector getConstSequenceElements() const; + /** * Boolean negation. * @return the Boolean negation of this term @@ -1068,6 +1088,13 @@ class CVC4_PUBLIC Term */ bool isNullHelper() const; + /** + * Helper function that returns the kind of the term, which takes into + * account special cases of the conversion for internal to external kinds. + * @return the kind of this term + */ + Kind getKindHelper() const; + /** * The internal expression wrapped by this term. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -2186,6 +2213,13 @@ class CVC4_PUBLIC Solver */ Sort mkSetSort(Sort elemSort) const; + /** + * Create a sequence sort. + * @param elemSort the sort of the sequence elements + * @return the sequence sort + */ + Sort mkSequenceSort(Sort elemSort) const; + /** * Create an uninterpreted sort. * @param symbol the name of the sort @@ -2550,6 +2584,13 @@ class CVC4_PUBLIC Solver */ Term mkChar(const char* s) const; + /** + * Create an empty sequence of the given element sort. + * @param sort The element sort of the sequence. + * @return the empty sequence with given element sort. + */ + Term mkEmptySequence(Sort sort) const; + /** * Create a universe set of the given sort. * @param sort the sort of the set elements diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index cf9074129..b3e88c98c 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2315,10 +2315,153 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1) */ REGEXP_COMPLEMENT, -#if 0 - /* regexp rv (internal use only) */ - REGEXP_RV, -#endif + + /** + * Sequence concat. + * Parameters: n > 1 + * -[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& children) + */ + SEQ_CONCAT, + /** + * Sequence length. + * Parameters: 1 + * -[1]: Term of Sequence sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + SEQ_LENGTH, + /** + * Sequence extract. + * 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + SEQ_EXTRACT, + /** + * Sequence element at. + * 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + SEQ_CONTAINS, + /** + * Sequence index-of. + * 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + SEQ_REPLACE_ALL, + /** + * Sequence reverse. + * Parameters: 1 + * -[1]: Term of Sequence sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + 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) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector& children) + */ + SEQ_SUFFIX, + /** + * Constant sequence. + * Parameters: + * See mkEmptySequence() + * Create with: + * mkEmptySequence(Sort sort) + * Note that a constant sequence is a term that is equivalent to: + * (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(). + */ + CONST_SEQUENCE, + /** + * Sequence unit, corresponding to a sequence of length one with the given + * term. + * Parameters: 1 + * -[1] Element term. + * Create with: + * mkTerm(Kind kind, Term child1) + */ + SEQ_UNIT, /* Quantifiers ----------------------------------------------------------- */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d499b8bb7..d69dc73f9 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -661,6 +661,14 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } +SequenceType ExprManager::mkSequenceType(Type elementType) const +{ + NodeManagerScope nms(d_nodeManager); + return SequenceType(Type( + d_nodeManager, + new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode)))); +} + DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags) { // Not worth a special implementation; this doesn't need to be fast diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3a4498ab7..4dfd77686 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -393,6 +393,9 @@ class CVC4_PUBLIC ExprManager { /** Make the type of set with the given parameterization. */ SetType mkSetType(Type elementType) const; + /** Make the type of sequence with the given parameterization. */ + SequenceType mkSequenceType(Type elementType) const; + /** Bits for use in mkDatatypeType() flags. * * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed diff --git a/src/expr/expr_sequence.h b/src/expr/expr_sequence.h index 90a140fc2..8d14f1dcb 100644 --- a/src/expr/expr_sequence.h +++ b/src/expr/expr_sequence.h @@ -54,7 +54,9 @@ class CVC4_PUBLIC ExprSequence bool operator>(const ExprSequence& es) const; bool operator>=(const ExprSequence& es) const; + /** Get the element type of the sequence */ const Type& getType() const; + /** Get the underlying sequence */ const Sequence& getSequence() const; private: diff --git a/src/expr/sequence.h b/src/expr/sequence.h index 0e5cf6a1d..763534274 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -130,7 +130,7 @@ class Sequence */ size_t roverlap(const Sequence& y) const; - /** get type */ + /** get the element type of the sequence */ TypeNode getType() const { return d_type; } /** get the internal Node representation of this sequence */ const std::vector& getVec() const { return d_seq; } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ff4de9dc8..ff6bdbde0 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -575,7 +575,8 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::TESTER_TYPE: case kind::ARRAY_TYPE: case kind::DATATYPE_TYPE: - case kind::PARAMETRIC_DATATYPE: return TypeNode(); + case kind::PARAMETRIC_DATATYPE: + case kind::SEQUENCE_TYPE: return TypeNode(); case kind::SET_TYPE: { // take the least common subtype of element types diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b504d290b..fe5f5e636 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -244,6 +244,7 @@ tokens { REGEXP_EMPTY_TOK = 'RE_EMPTY'; REGEXP_SIGMA_TOK = 'RE_SIGMA'; REGEXP_COMPLEMENT_TOK = 'RE_COMPLEMENT'; + SEQ_UNIT_TOK = 'SEQ_UNIT'; SETS_CARD_TOK = 'CARD'; @@ -2080,6 +2081,8 @@ stringTerm[CVC4::api::Term& f] } | REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN { f = MK_TERM(CVC4::api::REGEXP_COMPLEMENT, f); } + | SEQ_UNIT_TOK LPAREN formula[f] RPAREN + { f = MK_TERM(CVC4::api::SEQ_UNIT, f); } | REGEXP_EMPTY_TOK { f = MK_TERM(CVC4::api::REGEXP_EMPTY, std::vector()); } | REGEXP_SIGMA_TOK diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5d80dd55f..a5ce1bed0 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -563,6 +563,22 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { t = d_solver->mkEmptySet(s); } + else if (k == api::CONST_SEQUENCE) + { + if (!s.isSequence()) + { + std::stringstream ss; + ss << "Type ascription on empty sequence must be a sequence, got " << s; + parseError(ss.str()); + } + if (!t.getConstSequenceElements().empty()) + { + std::stringstream ss; + ss << "Cannot apply a type ascription to a non-empty sequence"; + parseError(ss.str()); + } + t = d_solver->mkEmptySequence(s.getSequenceElementSort()); + } else if (k == api::UNIVERSE_SET) { t = d_solver->mkUniverseSet(s); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 703696cf5..cc87306e3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2122,7 +2122,13 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Illegal set type."); } t = SOLVER->mkSetSort( args[0] ); - } else if(name == "Tuple") { + } else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() && + PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) { + if(args.size() != 1) { + PARSER_STATE->parseError("Illegal sequence type."); + } + t = SOLVER->mkSequenceSort( args[0] ); + } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) { t = SOLVER->mkTupleSort(args); } else if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 68b1945fc..aba409109 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -156,6 +156,10 @@ void Smt2::addStringOperators() { addOperator(api::STRING_CHARAT, "str.at"); addOperator(api::STRING_INDEXOF, "str.indexof"); addOperator(api::STRING_REPLACE, "str.replace"); + addOperator(api::STRING_PREFIX, "str.prefixof"); + addOperator(api::STRING_SUFFIX, "str.suffixof"); + addOperator(api::STRING_FROM_CODE, "str.from_code"); + addOperator(api::STRING_IS_DIGIT, "str.is_digit"); addOperator(api::STRING_REPLACE_RE, "str.replace_re"); addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); if (!strictModeEnabled()) @@ -163,11 +167,20 @@ void Smt2::addStringOperators() { addOperator(api::STRING_TOLOWER, "str.tolower"); addOperator(api::STRING_TOUPPER, "str.toupper"); addOperator(api::STRING_REV, "str.rev"); + // sequence versions + addOperator(api::SEQ_CONCAT, "seq.++"); + addOperator(api::SEQ_LENGTH, "seq.len"); + addOperator(api::SEQ_EXTRACT, "seq.extract"); + addOperator(api::SEQ_AT, "seq.at"); + addOperator(api::SEQ_CONTAINS, "seq.contains"); + addOperator(api::SEQ_INDEXOF, "seq.indexof"); + addOperator(api::SEQ_REPLACE, "seq.replace"); + addOperator(api::SEQ_PREFIX, "seq.prefixof"); + addOperator(api::SEQ_SUFFIX, "seq.suffixof"); + addOperator(api::SEQ_REV, "seq.rev"); + addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all"); + addOperator(api::SEQ_UNIT, "seq.unit"); } - addOperator(api::STRING_PREFIX, "str.prefixof"); - addOperator(api::STRING_SUFFIX, "str.suffixof"); - addOperator(api::STRING_FROM_CODE, "str.from_code"); - addOperator(api::STRING_IS_DIGIT, "str.is_digit"); // at the moment, we only use this syntax for smt2.6 if (getLanguage() == language::input::LANG_SMTLIB_V2_6 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -692,6 +705,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } defineVar("re.allchar", d_solver->mkRegexpSigma()); + // Boolean is a placeholder + defineVar("seq.empty", + d_solver->mkEmptySequence(d_solver->getBooleanSort())); + addStringOperators(); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 65117c9db..afbd7ee58 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -25,9 +25,11 @@ #include #include "expr/dtype.h" -#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/expr_sequence.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" +#include "expr/sequence.h" #include "options/language.h" // for LANG_AST #include "options/smt_options.h" #include "printer/dagification_visitor.h" @@ -165,6 +167,30 @@ void CvcPrinter::toStream( out << '"' << n.getConst().toString() << '"'; break; } + case kind::CONST_SEQUENCE: + { + const Sequence& sn = n.getConst().getSequence(); + const std::vector& snvec = sn.getVec(); + if (snvec.size() > 1) + { + out << "CONCAT("; + } + bool first = true; + for (const Node& snvc : snvec) + { + if (!first) + { + out << ", "; + } + out << "SEQ_UNIT(" << snvc << ")"; + first = false; + } + if (snvec.size() > 1) + { + out << ")"; + } + break; + } case kind::TYPE_CONSTANT: switch(TypeConstant tc = n.getConst()) { case REAL_TYPE: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 784e321a0..6077601bc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -23,8 +23,10 @@ #include "api/cvc4cpp.h" #include "expr/dtype.h" +#include "expr/expr_sequence.h" #include "expr/node_manager_attributes.h" #include "expr/node_visitor.h" +#include "expr/sequence.h" #include "options/bv_options.h" #include "options/language.h" #include "options/printer_options.h" @@ -211,6 +213,28 @@ void Smt2Printer::toStream(std::ostream& out, out << '"'; break; } + case kind::CONST_SEQUENCE: + { + const Sequence& sn = n.getConst().getSequence(); + const std::vector& snvec = sn.getVec(); + if (snvec.empty()) + { + out << "(as seq.empty " << n.getType() << ")"; + } + if (snvec.size() > 1) + { + out << "(seq.++ "; + } + for (const Node& snvc : snvec) + { + out << "(seq.unit " << snvc << ")"; + } + if (snvec.size() > 1) + { + out << ")"; + } + break; + } case kind::STORE_ALL: { ArrayStoreAll asa = n.getConst(); @@ -631,7 +655,9 @@ void Smt2Printer::toStream(std::ostream& out, case kind::REGEXP_LOOP: case kind::REGEXP_COMPLEMENT: case kind::REGEXP_EMPTY: - case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break; + case kind::REGEXP_SIGMA: + case kind::SEQ_UNIT: + case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break; case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; @@ -1196,6 +1222,8 @@ static string smtKindString(Kind k, Variant v) case kind::REGEXP_RANGE: return "re.range"; case kind::REGEXP_LOOP: return "re.loop"; case kind::REGEXP_COMPLEMENT: return "re.comp"; + case kind::SEQUENCE_TYPE: return "Seq"; + case kind::SEQ_UNIT: return "seq.unit"; //sep theory case kind::SEP_STAR: return "sep"; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 074b023a2..cb30a408e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -409,7 +409,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, else if (type.isStringLike()) { ops.push_back(strings::Word::mkEmptyWord(type)); - if (type.isString()) + if (type.isString()) // string-only { // Dummy character "A". This is not necessary for sequences which // have the generic constructor seq.unit. diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 9f502e1f6..928414523 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -60,7 +60,7 @@ bool StringsEntail::canConstantContainConcat(Node c, } else if (n[i].getKind() == STRING_ITOS && ArithEntail::check(n[i][0])) { - Assert(c.getType().isString()); + Assert(c.getType().isString()); // string-only const std::vector& tvec = c.getConst().getVec(); // find the first occurrence of a digit starting at pos while (pos < tvec.size() && !String::isDigit(tvec[pos])) @@ -594,7 +594,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector& n1, { if (n2[index1].isConst()) { - Assert(n2[index1].getType().isString()); + Assert(n2[index1].getType().isString()); // string-only CVC4::String t = n2[index1].getConst(); if (n1.size() == 1) { diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index b4fbbed98..d21cf069d 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -179,7 +179,7 @@ void TermRegistry::preRegisterTerm(TNode n) ss << "Regular expression variables are not supported."; throw LogicException(ss.str()); } - if (tn.isString()) + if (tn.isString()) // string-only { // all characters of constants should fall in the alphabet if (n.isConst()) diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 9f66c5f82..192b4fd34 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -291,7 +291,8 @@ public: for(int i=0; i<2; ++i) { TypeNode t = (*it).getType(check); - if (!t.isString()) { + if (!t.isString()) // string-only + { throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range"); } if (!(*it).isConst()) @@ -329,7 +330,8 @@ class ConstSequenceTypeRule bool check) { Assert(n.getKind() == kind::CONST_SEQUENCE); - return n.getConst().getSequence().getType(); + return nodeManager->mkSequenceType( + n.getConst().getSequence().getType()); } }; @@ -363,8 +365,8 @@ struct SequenceProperties Assert(type.isSequence()); // empty sequence std::vector seq; - return NodeManager::currentNM()->mkConst( - ExprSequence(SequenceType(type.toType()), seq)); + return NodeManager::currentNM()->mkConst(ExprSequence( + SequenceType(type.getSequenceElementType().toType()), seq)); } }; /* struct SequenceProperties */ diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 6d3949514..afedaed5c 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -176,6 +176,9 @@ SeqEnumLen::SeqEnumLen(TypeNode tn, { d_elementEnumerator.reset( new TypeEnumerator(d_type.getSequenceElementType(), tep)); + // ensure non-empty element domain + d_elementDomain.push_back((**d_elementEnumerator).toExpr()); + ++(*d_elementEnumerator); mkCurr(); } @@ -212,11 +215,12 @@ void SeqEnumLen::mkCurr() const std::vector& data = d_witer->getData(); for (unsigned i : data) { + Assert(i < d_elementDomain.size()); seq.push_back(d_elementDomain[i]); } // make sequence from seq - d_curr = - NodeManager::currentNM()->mkConst(ExprSequence(d_type.toType(), seq)); + d_curr = NodeManager::currentNM()->mkConst( + ExprSequence(d_type.getSequenceElementType().toType(), seq)); } StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep) diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 35b315e35..fec567733 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -452,6 +452,15 @@ Node Word::reverse(TNode x) std::reverse(nvec.begin(), nvec.end()); return nm->mkConst(String(nvec)); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst().getSequence(); + const std::vector& vecc = sx.getVec(); + std::vector vecr(vecc.begin(), vecc.end()); + std::reverse(vecr.begin(), vecr.end()); + Sequence res(sx.getType(), vecr); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 10e2f414e..5f82aedf1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,15 @@ set(regress_0_tests regress0/sep/skolem_emp.smt2 regress0/sep/trees-1.smt2 regress0/sep/wand-crash.smt2 + regress0/seq/seq-2var.smt2 + regress0/seq/seq-ex1.smt2 + regress0/seq/seq-ex2.smt2 + regress0/seq/seq-ex3.smt2 + regress0/seq/seq-ex4.smt2 + regress0/seq/seq-ex5-dd.smt2 + regress0/seq/seq-ex5.smt2 + regress0/seq/seq-nemp.smt2 + regress0/seq/seq-rewrites.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 regress0/sets/abt-te-exh2.smt2 diff --git a/test/regress/regress0/seq/seq-2var.smt2 b/test/regress/regress0/seq/seq-2var.smt2 new file mode 100644 index 000000000..3a0d8934f --- /dev/null +++ b/test/regress/regress0/seq/seq-2var.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) + +(assert (not (= x y))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex1.smt2 b/test/regress/regress0/seq/seq-ex1.smt2 new file mode 100644 index 000000000..817ee5f8e --- /dev/null +++ b/test/regress/regress0/seq/seq-ex1.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_UFSLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun f ((Seq Int)) (Seq Bool)) + +(assert (not (= x y))) +(assert (not (= (f x) (f y)))) + +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex2.smt2 b/test/regress/regress0/seq/seq-ex2.smt2 new file mode 100644 index 000000000..89b9d3100 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex2.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) +(assert (> z 10)) +(assert (= (seq.len x) (seq.len y))) +(assert (= (seq.++ x (seq.unit z)) (seq.++ y (seq.unit 5)))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2 new file mode 100644 index 000000000..abafdeddf --- /dev/null +++ b/test/regress/regress0/seq/seq-ex3.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () (Seq (Seq Int))) +(declare-fun xp () (Seq (Seq Int))) +(declare-fun y () (Seq (Seq Int))) +(declare-fun yp () (Seq (Seq Int))) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun n () Int) +(assert (> i j)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (= (seq.extract w n 1) (seq.unit j))) +(assert (= x (seq.++ (seq.unit z) xp))) +(assert (= y (seq.++ (seq.unit w) yp))) +(assert (= x y)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2 new file mode 100644 index 000000000..93fed72c7 --- /dev/null +++ b/test/regress/regress0/seq/seq-ex4.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (= (seq.extract z n 1) (seq.unit i))) +(assert (< (seq.len z) n)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2 new file mode 100644 index 000000000..d9ef5c8ba --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5-dd.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun i () Int) +(declare-fun n () Int) +(assert (> i 777)) +(assert (= (seq.extract z n 1) (seq.unit i))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-ex5.smt2 b/test/regress/regress0/seq/seq-ex5.smt2 new file mode 100644 index 000000000..9fa72bc6b --- /dev/null +++ b/test/regress/regress0/seq/seq-ex5.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun i () Int) +(assert (> i 777)) +(assert (not (= (seq.replace z (seq.unit i) w) z))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-nemp.smt2 b/test/regress/regress0/seq/seq-nemp.smt2 new file mode 100644 index 000000000..4eaee062f --- /dev/null +++ b/test/regress/regress0/seq/seq-nemp.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () (Seq Int)) +(assert (not (= x (as seq.empty (Seq Int))))) +(assert (= (seq.len x) 16)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-rewrites.smt2 b/test/regress/regress0/seq/seq-rewrites.smt2 new file mode 100644 index 000000000..a8bd7c1f2 --- /dev/null +++ b/test/regress/regress0/seq/seq-rewrites.smt2 @@ -0,0 +1,44 @@ +(set-logic QF_UFSLIA) +(set-info :status unsat) +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) +(declare-fun z () Int) + +(assert +(or + +(not (= +(seq.replace (seq.++ (seq.unit 0) x) (seq.unit 1) (seq.unit 2)) +(seq.++ (seq.unit 0) (seq.replace x (seq.unit 1) (seq.unit 2))) +)) + +(not (= +(seq.at (seq.++ x (seq.unit 14)) (seq.len x)) +(seq.unit 14) +)) + +(not (= +(seq.at x z) +(seq.extract x z 1) +)) + +(not (= +(seq.contains (seq.++ x y) y) +true +)) + +(not (= +(seq.prefixof (seq.unit z) (seq.unit 4)) +(seq.suffixof (seq.unit z) (seq.unit 4)) +)) + +(not (= +(seq.rev (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +(seq.++ (seq.unit 3) (seq.unit 2) (seq.unit 1)) +)) + +)) + + + +(check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index ddff63352..4a7b74c8e 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -46,6 +46,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPredicateSort(); void testMkRecordSort(); void testMkSetSort(); + void testMkSequenceSort(); void testMkSortConstructorSort(); void testMkTupleSort(); void testMkUninterpretedSort(); @@ -56,6 +57,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkConst(); void testMkConstArray(); void testMkEmptySet(); + void testMkEmptySequence(); void testMkFalse(); void testMkFloatingPoint(); void testMkNaN(); @@ -388,6 +390,17 @@ void SolverBlack::testMkSetSort() CVC4ApiException&); } +void SolverBlack::testMkSequenceSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver->mkSequenceSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort( + d_solver->mkSequenceSort(d_solver->getIntegerSort()))); + Solver slv; + TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()), + CVC4ApiException&); +} + void SolverBlack::testMkUninterpretedSort() { TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u")); @@ -540,6 +553,16 @@ void SolverBlack::testMkEmptySet() TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } +void SolverBlack::testMkEmptySequence() +{ + Solver slv; + Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s)); + TS_ASSERT_THROWS_NOTHING( + d_solver->mkEmptySequence(d_solver->getBooleanSort())); + TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&); +} + void SolverBlack::testMkFalse() { TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 944b9309f..abaded5a1 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -35,6 +35,7 @@ class SortBlack : public CxxTest::TestSuite void testGetArrayIndexSort(); void testGetArrayElementSort(); void testGetSetElementSort(); + void testGetSequenceElementSort(); void testGetUninterpretedSortName(); void testIsUninterpretedSortParameterized(); void testGetUninterpretedSortParamSorts(); @@ -196,6 +197,16 @@ void SortBlack::testGetSetElementSort() TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); } +void SortBlack::testGetSequenceElementSort() +{ + Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); + TS_ASSERT(seqSort.isSequence()); + TS_ASSERT_THROWS_NOTHING(seqSort.getSequenceElementSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT(!bvSort.isSequence()); + TS_ASSERT_THROWS(bvSort.getSequenceElementSort(), CVC4ApiException&); +} + void SortBlack::testGetUninterpretedSortName() { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index d23f560ae..6ca02c9f1 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -44,6 +44,7 @@ class TermBlack : public CxxTest::TestSuite void testSubstitute(); void testIsConst(); void testConstArray(); + void testConstSequenceElements(); private: Solver d_solver; @@ -110,6 +111,13 @@ void TermBlack::testGetKind() TS_ASSERT_THROWS_NOTHING(p_0.getKind()); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); TS_ASSERT_THROWS_NOTHING(p_f_y.getKind()); + + // Sequence kinds do not exist internally, test that the API properly + // converts them back. + Sort seqSort = d_solver.mkSequenceSort(intSort); + Term s = d_solver.mkConst(seqSort, "s"); + Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); + TS_ASSERT(ss.getKind() == SEQ_CONCAT); } void TermBlack::testGetSort() @@ -769,3 +777,22 @@ void TermBlack::testConstArray() TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one); TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&); } + +void TermBlack::testConstSequenceElements() +{ + Sort realsort = d_solver.getRealSort(); + Sort seqsort = d_solver.mkSequenceSort(realsort); + Term s = d_solver.mkEmptySequence(seqsort); + + TS_ASSERT(s.isConst()); + + TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE); + // empty sequence has zero elements + std::vector cs = s.getConstSequenceElements(); + TS_ASSERT(cs.empty()); + + // A seq.unit app is not a constant sequence (regardless of whether it is + // applied to a constant). + Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1)); + TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&); +} -- 2.30.2