Remove ExprSequence (#4724)

Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().

6 files changed, 54 insertions, 62 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 952f26691..00658d08b 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -95,10 +95,7 @@ void BaseSolver::checkInit()
                 Node oval = prev.isConst() ? n : prev;
                 Assert(oval.getKind() == SEQ_UNIT);
                 s = oval[0];
-                t = cchars[0]
-                        .getConst<ExprSequence>()
-                        .getSequence()
-                        .getVec()[0];
+                t = cchars[0].getConst<Sequence>().getVec()[0];
                 // oval is congruent (ignored) in this context
                 d_congruent.insert(oval);
               }
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 96ba82a44..21a435152 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -76,9 +76,9 @@ enumerator SEQUENCE_TYPE \
     "theory/strings/type_enumerator.h"
 
 constant CONST_SEQUENCE \
-    ::CVC4::ExprSequence \
-    ::CVC4::ExprSequenceHashFunction \
-    "expr/expr_sequence.h" \
+    ::CVC4::Sequence \
+    ::CVC4::SequenceHashFunction \
+    "expr/sequence.h" \
     "a sequence of characters"
 
 operator SEQ_UNIT 1 "a sequence of length one"
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index bb0fa1d97..110864c3b 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -3237,10 +3237,10 @@ Node SequencesRewriter::rewriteSeqUnit(Node node)
   NodeManager* nm = NodeManager::currentNM();
   if (node[0].isConst())
   {
-    std::vector<Expr> seq;
-    seq.push_back(node[0].toExpr());
+    std::vector<Node> seq;
+    seq.push_back(node[0]);
     TypeNode stype = node[0].getType();
-    Node ret = nm->mkConst(ExprSequence(stype.toType(), seq));
+    Node ret = nm->mkConst(Sequence(stype, seq));
     return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL);
   }
   return node;
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 192b4fd34..78b925ebe 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -20,7 +20,6 @@
 #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 #define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 
-#include "expr/expr_sequence.h"
 #include "expr/sequence.h"
 
 namespace CVC4 {
@@ -330,8 +329,7 @@ class ConstSequenceTypeRule
                                      bool check)
   {
     Assert(n.getKind() == kind::CONST_SEQUENCE);
-    return nodeManager->mkSequenceType(
-        n.getConst<ExprSequence>().getSequence().getType());
+    return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
   }
 };
 
@@ -364,9 +362,9 @@ struct SequenceProperties
   {
     Assert(type.isSequence());
     // empty sequence
-    std::vector<Expr> seq;
-    return NodeManager::currentNM()->mkConst(ExprSequence(
-        SequenceType(type.getSequenceElementType().toType()), seq));
+    std::vector<Node> seq;
+    return NodeManager::currentNM()->mkConst(
+        Sequence(type.getSequenceElementType(), seq));
   }
 }; /* struct SequenceProperties */
 
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index afedaed5c..ae88f63f7 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -211,7 +211,7 @@ bool SeqEnumLen::increment()
 
 void SeqEnumLen::mkCurr()
 {
-  std::vector<Expr> seq;
+  std::vector<Node> seq;
   const std::vector<unsigned>& data = d_witer->getData();
   for (unsigned i : data)
   {
@@ -220,7 +220,7 @@ void SeqEnumLen::mkCurr()
   }
   // make sequence from seq
   d_curr = NodeManager::currentNM()->mkConst(
-      ExprSequence(d_type.getSequenceElementType().toType(), seq));
+      Sequence(d_type.getSequenceElementType(), seq));
 }
 
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index fec567733..49221409e 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -32,9 +32,9 @@ Node Word::mkEmptyWord(TypeNode tn)
   }
   else if (tn.isSequence())
   {
-    std::vector<Expr> seq;
+    std::vector<Node> seq;
     return NodeManager::currentNM()->mkConst(
-        ExprSequence(tn.getSequenceElementType().toType(), seq));
+        Sequence(tn.getSequenceElementType(), seq));
   }
   Unimplemented();
   return Node::null();
@@ -59,20 +59,17 @@ Node Word::mkWordFlatten(const std::vector<Node>& xs)
   }
   else if (k == CONST_SEQUENCE)
   {
-    std::vector<Expr> seq;
+    std::vector<Node> seq;
     TypeNode tn = xs[0].getType();
     for (TNode x : xs)
     {
       Assert(x.getType() == tn);
-      const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+      const Sequence& sx = x.getConst<Sequence>();
       const std::vector<Node>& vecc = sx.getVec();
-      for (const Node& c : vecc)
-      {
-        seq.push_back(c.toExpr());
-      }
+      seq.insert(seq.end(), vecc.begin(), vecc.end());
     }
     return NodeManager::currentNM()->mkConst(
-        ExprSequence(tn.getSequenceElementType().toType(), seq));
+        Sequence(tn.getSequenceElementType(), seq));
   }
   Unimplemented();
   return Node::null();
@@ -87,7 +84,7 @@ size_t Word::getLength(TNode x)
   }
   else if (k == CONST_SEQUENCE)
   {
-    return x.getConst<ExprSequence>().getSequence().size();
+    return x.getConst<Sequence>().size();
   }
   Unimplemented() << "Word::getLength on " << x;
   return 0;
@@ -113,12 +110,12 @@ std::vector<Node> Word::getChars(TNode x)
   }
   else if (k == CONST_SEQUENCE)
   {
-    Type t = x.getConst<ExprSequence>().getType();
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    TypeNode t = x.getConst<Sequence>().getType();
+    const Sequence& sx = x.getConst<Sequence>();
     const std::vector<Node>& vec = sx.getVec();
     for (const Node& v : vec)
     {
-      ret.push_back(nm->mkConst(ExprSequence(t, {v.toExpr()})));
+      ret.push_back(nm->mkConst(Sequence(t, {v})));
     }
     return ret;
   }
@@ -141,8 +138,8 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.strncmp(sy, n);
   }
   Unimplemented();
@@ -162,8 +159,8 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.rstrncmp(sy, n);
   }
   Unimplemented();
@@ -183,8 +180,8 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.find(sy, start);
   }
   Unimplemented();
@@ -204,8 +201,8 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.rfind(sy, start);
   }
   Unimplemented();
@@ -225,8 +222,8 @@ bool Word::hasPrefix(TNode x, TNode y)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.hasPrefix(sy);
   }
   Unimplemented();
@@ -246,8 +243,8 @@ bool Word::hasSuffix(TNode x, TNode y)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.hasSuffix(sy);
   }
   Unimplemented();
@@ -271,11 +268,11 @@ Node Word::replace(TNode x, TNode y, TNode t)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
     Assert(t.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
-    const Sequence& st = t.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
+    const Sequence& st = t.getConst<Sequence>();
     Sequence res = sx.replace(sy, st);
-    return nm->mkConst(res.toExprSequence());
+    return nm->mkConst(res);
   }
   Unimplemented();
   return Node::null();
@@ -291,9 +288,9 @@ Node Word::substr(TNode x, std::size_t i)
   }
   else if (k == CONST_SEQUENCE)
   {
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
     Sequence res = sx.substr(i);
-    return nm->mkConst(res.toExprSequence());
+    return nm->mkConst(res);
   }
   Unimplemented();
   return Node::null();
@@ -309,9 +306,9 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j)
   }
   else if (k == CONST_SEQUENCE)
   {
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
     Sequence res = sx.substr(i, j);
-    return nm->mkConst(res.toExprSequence());
+    return nm->mkConst(res);
   }
   Unimplemented();
   return Node::null();
@@ -330,9 +327,9 @@ Node Word::suffix(TNode x, std::size_t i)
   }
   else if (k == CONST_SEQUENCE)
   {
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
     Sequence res = sx.suffix(i);
-    return nm->mkConst(res.toExprSequence());
+    return nm->mkConst(res);
   }
   Unimplemented();
   return Node::null();
@@ -351,8 +348,8 @@ bool Word::noOverlapWith(TNode x, TNode y)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.noOverlapWith(sy);
   }
   Unimplemented();
@@ -372,8 +369,8 @@ std::size_t Word::overlap(TNode x, TNode y)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.overlap(sy);
   }
   Unimplemented();
@@ -393,8 +390,8 @@ std::size_t Word::roverlap(TNode x, TNode y)
   else if (k == CONST_SEQUENCE)
   {
     Assert(y.getKind() == CONST_SEQUENCE);
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
-    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& sy = y.getConst<Sequence>();
     return sx.roverlap(sy);
   }
   Unimplemented();
@@ -410,7 +407,7 @@ bool Word::isRepeated(TNode x)
   }
   else if (k == CONST_SEQUENCE)
   {
-    return x.getConst<ExprSequence>().getSequence().isRepeated();
+    return x.getConst<Sequence>().isRepeated();
   }
   Unimplemented();
   return false;
@@ -454,12 +451,12 @@ Node Word::reverse(TNode x)
   }
   else if (k == CONST_SEQUENCE)
   {
-    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sx = x.getConst<Sequence>();
     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());
+    return nm->mkConst(res);
   }
   Unimplemented();
   return Node::null();