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.

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();