diff options
34 files changed, 626 insertions, 28 deletions
@@ -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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction> {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<ArrayStoreAll>().getExpr()); } +std::vector<Term> 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<Node>& elems = + d_expr->getConst<ExprSequence>().getSequence().getVec(); + std::vector<Term> 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<Expr> 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 @@ -380,6 +380,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 -------------------------------------------------- */ /** @@ -907,6 +920,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<Term> getConstSequenceElements() const; + + /** * Boolean negation. * @return the Boolean negation of this term */ @@ -1069,6 +1089,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 * memory allocation (CVC4::Expr is already ref counted, so this could be @@ -2187,6 +2214,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 * @return the uninterpreted sort @@ -2551,6 +2585,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 * @return the universe set constant 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Node>& 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<api::Term>()); } | 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 <vector> #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<String>().toString() << '"'; break; } + case kind::CONST_SEQUENCE: + { + const Sequence& sn = n.getConst<ExprSequence>().getSequence(); + const std::vector<Node>& 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<TypeConstant>()) { 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<ExprSequence>().getSequence(); + const std::vector<Node>& 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<ArrayStoreAll>(); @@ -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<unsigned>& tvec = c.getConst<String>().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<Node>& n1, { if (n2[index1].isConst()) { - Assert(n2[index1].getType().isString()); + Assert(n2[index1].getType().isString()); // string-only CVC4::String t = n2[index1].getConst<String>(); 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<ExprSequence>().getSequence().getType(); + return nodeManager->mkSequenceType( + n.getConst<ExprSequence>().getSequence().getType()); } }; @@ -363,8 +365,8 @@ struct SequenceProperties Assert(type.isSequence()); // empty sequence std::vector<Expr> 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<unsigned>& 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<ExprSequence>().getSequence(); + const std::vector<Node>& vecc = sx.getVec(); + std::vector<Node> 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<Term> 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&); +} |