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.++).
=================
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`.
#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"
{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},
{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},
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(); }
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
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; }
Kind Term::getKind() const
{
CVC4_API_CHECK_NOT_NULL;
- return intToExtKind(d_expr->getKind());
+ return getKindHelper();
}
Sort Term::getSort() 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(); }
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;
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;
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;
*/
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
*/
Sort getSetElementSort() const;
+ /* Sequence sort ------------------------------------------------------- */
+
+ /**
+ * @return the element sort of a sequence sort
+ */
+ Sort getSequenceElementSort() const;
+
/* Uninterpreted sort -------------------------------------------------- */
/**
*/
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
*/
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
*/
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
*/
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
* 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 ----------------------------------------------------------- */
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
/** 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
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:
*/
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; }
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
REGEXP_EMPTY_TOK = 'RE_EMPTY';
REGEXP_SIGMA_TOK = 'RE_SIGMA';
REGEXP_COMPLEMENT_TOK = 'RE_COMPLEMENT';
+ SEQ_UNIT_TOK = 'SEQ_UNIT';
SETS_CARD_TOK = 'CARD';
}
| 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
{
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);
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)) {
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())
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)
}
defineVar("re.allchar", d_solver->mkRegexpSigma());
+ // Boolean is a placeholder
+ defineVar("seq.empty",
+ d_solver->mkEmptySequence(d_solver->getBooleanSort()));
+
addStringOperators();
}
#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"
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:
#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"
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>();
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;
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";
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.
}
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]))
{
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)
{
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())
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())
bool check)
{
Assert(n.getKind() == kind::CONST_SEQUENCE);
- return n.getConst<ExprSequence>().getSequence().getType();
+ return nodeManager->mkSequenceType(
+ n.getConst<ExprSequence>().getSequence().getType());
}
};
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 */
{
d_elementEnumerator.reset(
new TypeEnumerator(d_type.getSequenceElementType(), tep));
+ // ensure non-empty element domain
+ d_elementDomain.push_back((**d_elementEnumerator).toExpr());
+ ++(*d_elementEnumerator);
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)
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();
}
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
--- /dev/null
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+
+(assert (not (= x y)))
+
+(check-sat)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
void testMkPredicateSort();
void testMkRecordSort();
void testMkSetSort();
+ void testMkSequenceSort();
void testMkSortConstructorSort();
void testMkTupleSort();
void testMkUninterpretedSort();
void testMkConst();
void testMkConstArray();
void testMkEmptySet();
+ void testMkEmptySequence();
void testMkFalse();
void testMkFloatingPoint();
void testMkNaN();
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"));
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());
void testGetArrayIndexSort();
void testGetArrayElementSort();
void testGetSetElementSort();
+ void testGetSequenceElementSort();
void testGetUninterpretedSortName();
void testIsUninterpretedSortParameterized();
void testGetUninterpretedSortParamSorts();
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");
void testSubstitute();
void testIsConst();
void testConstArray();
+ void testConstSequenceElements();
private:
Solver d_solver;
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()
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&);
+}
projects / cvc5.git / commitdiff