diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-27 18:05:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-27 16:05:07 -0700 |
commit | 4df14f1e09549be607123c66b7dd206e8e244c89 (patch) | |
tree | 3104897629ebe9efe4d14983ad89fb0d8778d4f2 /src/expr/sequence.cpp | |
parent | 449cf281987eb8a2d43a572817db5c870a010c08 (diff) |
Add the Expr-level sequence datatype (#4526)
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
Diffstat (limited to 'src/expr/sequence.cpp')
-rw-r--r-- | src/expr/sequence.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index e42a67bbe..f70a70027 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -14,6 +14,8 @@ #include "expr/sequence.h" +#include "expr/expr_sequence.h" + using namespace std; namespace CVC4 { @@ -297,6 +299,16 @@ bool Sequence::noOverlapWith(const Sequence& y) const size_t Sequence::maxSize() { return std::numeric_limits<uint32_t>::max(); } +ExprSequence Sequence::toExprSequence() +{ + std::vector<Expr> seq; + for (const Node& n : d_seq) + { + seq.push_back(n.toExpr()); + } + return ExprSequence(d_type.toType(), seq); +} + std::ostream& operator<<(std::ostream& os, const Sequence& s) { const std::vector<Node>& vec = s.getVec(); |