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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0561af144b982c757cbe5143db972c7287060758..9ef154246f6139c9da4959594b89fda8e4af2cb4 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -957,7 +957,6 @@ install(FILES
           expr/datatype.h
           expr/emptyset.h
           expr/expr_iomanip.h
-          expr/expr_sequence.h
           expr/record.h
           expr/symbol_table.h
           expr/type.h

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ebafc3cc8ea3873c8258cabbac044a52ab0ff8da..319257ac7d62522af5df2b8a5c8b6ad727f1c5a6 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1573,8 +1573,7 @@ std::vector<Term> Term::getConstSequenceElements() const
   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();
+  const std::vector<Node>& elems = d_expr->getConst<Sequence>().getVec();
   std::vector<Term> terms;
   for (const Node& t : elems)
   {
@@ -3443,8 +3442,9 @@ Term Solver::mkEmptySequence(Sort sort) const
   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));
+  std::vector<Node> seq;
+  Expr res =
+      d_exprMgr->mkConst(Sequence(TypeNode::fromType(*sort.d_type), seq));
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 9222393c499476dec07a5ee52e3e798b6b9943a2..bad2f1f424abea539901214931b296ef2ec1a077 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -12,8 +12,6 @@ libcvc4_add_sources(
   expr_iomanip.cpp
   expr_iomanip.h
   expr_manager_scope.h
-  expr_sequence.cpp
-  expr_sequence.h
   kind_map.h
   lazy_proof.cpp
   lazy_proof.h

diff --git a/src/expr/expr_sequence.cpp b/src/expr/expr_sequence.cpp
deleted file mode 100644 (file)
index aa58bba..0000000
--- a/src/expr/expr_sequence.cpp
+++ /dev/null
@@ -1,98 +0,0 @@
-/*********************                                                        */
-/*! \file expr_sequence.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of the sequence data type.
- **/
-
-#include "expr/expr_sequence.h"
-
-#include "expr/expr.h"
-#include "expr/node.h"
-#include "expr/sequence.h"
-#include "expr/type.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-
-ExprSequence::ExprSequence(const Type& t, const std::vector<Expr>& seq)
-{
-  d_type.reset(new Type(t));
-  std::vector<Node> nseq;
-  for (const Expr& e : seq)
-  {
-    nseq.push_back(Node::fromExpr(e));
-  }
-  d_sequence.reset(new Sequence(TypeNode::fromType(t), nseq));
-}
-ExprSequence::~ExprSequence() {}
-
-ExprSequence::ExprSequence(const ExprSequence& other)
-    : d_type(new Type(other.getType())),
-      d_sequence(new Sequence(other.getSequence()))
-{
-}
-
-ExprSequence& ExprSequence::operator=(const ExprSequence& other)
-{
-  (*d_type) = other.getType();
-  (*d_sequence) = other.getSequence();
-  return *this;
-}
-
-const Type& ExprSequence::getType() const { return *d_type; }
-
-const Sequence& ExprSequence::getSequence() const { return *d_sequence; }
-
-bool ExprSequence::operator==(const ExprSequence& es) const
-{
-  return getType() == es.getType() && getSequence() == es.getSequence();
-}
-
-bool ExprSequence::operator!=(const ExprSequence& es) const
-{
-  return !(*this == es);
-}
-
-bool ExprSequence::operator<(const ExprSequence& es) const
-{
-  return (getType() < es.getType())
-         || (getType() == es.getType() && getSequence() < es.getSequence());
-}
-
-bool ExprSequence::operator<=(const ExprSequence& es) const
-{
-  return (getType() < es.getType())
-         || (getType() == es.getType() && getSequence() <= es.getSequence());
-}
-
-bool ExprSequence::operator>(const ExprSequence& es) const
-{
-  return !(*this <= es);
-}
-
-bool ExprSequence::operator>=(const ExprSequence& es) const
-{
-  return !(*this < es);
-}
-
-std::ostream& operator<<(std::ostream& os, const ExprSequence& s)
-{
-  return os << "__expr_sequence__(" << s.getType() << ", " << s.getSequence()
-            << ")";
-}
-
-size_t ExprSequenceHashFunction::operator()(const ExprSequence& es) const
-{
-  uint64_t hash = fnv1a::fnv1a_64(TypeHashFunction()(es.getType()));
-  return static_cast<size_t>(SequenceHashFunction()(es.getSequence()), hash);
-}
-
-}  // namespace CVC4

diff --git a/src/expr/expr_sequence.h b/src/expr/expr_sequence.h
deleted file mode 100644 (file)
index 8d14f1d..0000000
--- a/src/expr/expr_sequence.h
+++ /dev/null
@@ -1,78 +0,0 @@
-/*********************                                                        */
-/*! \file expr_sequence.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The sequence data type.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__EXPR__EXPR_SEQUENCE_H
-#define CVC4__EXPR__EXPR_SEQUENCE_H
-
-#include <iosfwd>
-#include <memory>
-#include <vector>
-
-namespace CVC4 {
-
-// messy; Expr needs ExprSequence (because it's the payload of a
-// CONSTANT-kinded expression), and ExprSequence needs Expr.
-class Type;
-class Expr;
-class Sequence;
-
-/** The CVC4 sequence class
- *
- * This data structure is the domain of values for the sequence type.
- */
-class CVC4_PUBLIC ExprSequence
-{
- public:
-  /** constructors for ExprSequence
-   *
-   * Internally, a CVC4::ExprSequence is represented by a vector of Nodes
-   * (d_seq), where each Node in this vector must be a constant.
-   */
-  ExprSequence(const Type& type, const std::vector<Expr>& seq);
-  ~ExprSequence();
-
-  ExprSequence(const ExprSequence& other);
-  ExprSequence& operator=(const ExprSequence& other);
-
-  bool operator==(const ExprSequence& es) const;
-  bool operator!=(const ExprSequence& es) const;
-  bool operator<(const ExprSequence& es) const;
-  bool operator<=(const ExprSequence& es) const;
-  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:
-  /** The element type of the sequence */
-  std::unique_ptr<Type> d_type;
-  /** The data of the sequence */
-  std::unique_ptr<Sequence> d_sequence;
-}; /* class ExprSequence */
-
-struct CVC4_PUBLIC ExprSequenceHashFunction
-{
-  size_t operator()(const ::CVC4::ExprSequence& s) const;
-}; /* struct ExprSequenceHashFunction */
-
-std::ostream& operator<<(std::ostream& os, const ExprSequence& s) CVC4_PUBLIC;
-
-}  // namespace CVC4
-
-#endif /* CVC4__EXPR__SEQUENCE_H */

diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 0eb8401e6521b2a03c2041337725d8efde1cf70c..816b894e060e0e04cfbf92d7cf30ae49de5382d6 100644 (file)
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -14,38 +14,52 @@
 
 #include "expr/sequence.h"
 
-#include "expr/expr_sequence.h"
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
 
 using namespace std;
 
 namespace CVC4 {
 
-Sequence::Sequence(TypeNode t, const std::vector<Node>& s) : d_type(t), d_seq(s)
+Sequence::Sequence(const TypeNode& t, const std::vector<Node>& s)
+    : d_type(new TypeNode(t)), d_seq(s)
+{
+}
+
+Sequence::Sequence(const Sequence& seq)
+    : d_type(new TypeNode(seq.getType())), d_seq(seq.getVec())
 {
 }
 
+Sequence::~Sequence() {}
+
 Sequence& Sequence::operator=(const Sequence& y)
 {
   if (this != &y)
   {
-    d_type = y.d_type;
-    d_seq = y.d_seq;
+    d_type.reset(new TypeNode(y.getType()));
+    d_seq = y.getVec();
   }
   return *this;
 }
 
 int Sequence::cmp(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  if (getType() != y.getType())
+  {
+    return getType() < y.getType() ? -1 : 1;
+  }
   if (size() != y.size())
   {
     return size() < y.size() ? -1 : 1;
   }
   for (size_t i = 0, sz = size(); i < sz; ++i)
   {
-    if (d_seq[i] != y.d_seq[i])
+    if (nth(i) != y.nth(i))
     {
-      return d_seq[i] < y.d_seq[i] ? -1 : 1;
+      return nth(i) < y.nth(i) ? -1 : 1;
     }
   }
   return 0;
@@ -53,15 +67,15 @@ int Sequence::cmp(const Sequence& y) const
 
 Sequence Sequence::concat(const Sequence& other) const
 {
-  Assert(d_type == other.d_type);
+  Assert(getType() == other.getType());
   std::vector<Node> ret_vec(d_seq);
   ret_vec.insert(ret_vec.end(), other.d_seq.begin(), other.d_seq.end());
-  return Sequence(d_type, ret_vec);
+  return Sequence(getType(), ret_vec);
 }
 
 bool Sequence::strncmp(const Sequence& y, size_t n) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   size_t b = (size() >= y.size()) ? size() : y.size();
   size_t s = (size() <= y.size()) ? size() : y.size();
   if (n > s)
@@ -74,7 +88,7 @@ bool Sequence::strncmp(const Sequence& y, size_t n) const
   }
   for (size_t i = 0; i < n; ++i)
   {
-    if (d_seq[i] != y.d_seq[i])
+    if (nth(i) != y.nth(i))
     {
       return false;
     }
@@ -97,7 +111,7 @@ bool Sequence::rstrncmp(const Sequence& y, size_t n) const
   }
   for (size_t i = 0; i < n; ++i)
   {
-    if (d_seq[size() - i - 1] != y.d_seq[y.size() - i - 1])
+    if (nth(size() - i - 1) != y.nth(y.size() - i - 1))
     {
       return false;
     }
@@ -105,21 +119,31 @@ bool Sequence::rstrncmp(const Sequence& y, size_t n) const
   return true;
 }
 
-Node Sequence::front() const
+bool Sequence::empty() const { return d_seq.empty(); }
+
+size_t Sequence::size() const { return d_seq.size(); }
+
+const Node& Sequence::front() const
 {
   Assert(!d_seq.empty());
   return d_seq.front();
 }
 
-Node Sequence::back() const
+const Node& Sequence::back() const
 {
   Assert(!d_seq.empty());
   return d_seq.back();
 }
 
+const Node& Sequence::nth(size_t i) const
+{
+  Assert(i < size());
+  return d_seq[i];
+}
+
 size_t Sequence::overlap(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   size_t i = size() < y.size() ? size() : y.size();
   for (; i > 0; i--)
   {
@@ -135,7 +159,7 @@ size_t Sequence::overlap(const Sequence& y) const
 
 size_t Sequence::roverlap(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   size_t i = size() < y.size() ? size() : y.size();
   for (; i > 0; i--)
   {
@@ -149,14 +173,18 @@ size_t Sequence::roverlap(const Sequence& y) const
   return i;
 }
 
+const TypeNode& Sequence::getType() const { return *d_type; }
+
+const std::vector<Node>& Sequence::getVec() const { return d_seq; }
+
 bool Sequence::isRepeated() const
 {
   if (size() > 1)
   {
-    Node f = d_seq[0];
+    Node f = nth(0);
     for (unsigned i = 1, sz = size(); i < sz; ++i)
     {
-      if (f != d_seq[i])
+      if (f != nth(i))
       {
         return false;
       }
@@ -167,7 +195,7 @@ bool Sequence::isRepeated() const
 
 size_t Sequence::find(const Sequence& y, size_t start) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   if (size() < y.size() + start)
   {
     return std::string::npos;
@@ -191,7 +219,7 @@ size_t Sequence::find(const Sequence& y, size_t start) const
 
 size_t Sequence::rfind(const Sequence& y, size_t start) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   if (size() < y.size() + start)
   {
     return std::string::npos;
@@ -215,7 +243,7 @@ size_t Sequence::rfind(const Sequence& y, size_t start) const
 
 bool Sequence::hasPrefix(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   size_t s = size();
   size_t ys = y.size();
   if (ys > s)
@@ -224,7 +252,7 @@ bool Sequence::hasPrefix(const Sequence& y) const
   }
   for (size_t i = 0; i < ys; i++)
   {
-    if (d_seq[i] != y.d_seq[i])
+    if (nth(i) != y.nth(i))
     {
       return false;
     }
@@ -234,7 +262,7 @@ bool Sequence::hasPrefix(const Sequence& y) const
 
 bool Sequence::hasSuffix(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   size_t s = size();
   size_t ys = y.size();
   if (ys > s)
@@ -244,7 +272,7 @@ bool Sequence::hasSuffix(const Sequence& y) const
   size_t idiff = s - ys;
   for (size_t i = 0; i < ys; i++)
   {
-    if (d_seq[i + idiff] != y.d_seq[i])
+    if (nth(i + idiff) != y.nth(i))
     {
       return false;
     }
@@ -254,8 +282,8 @@ bool Sequence::hasSuffix(const Sequence& y) const
 
 Sequence Sequence::replace(const Sequence& s, const Sequence& t) const
 {
-  Assert(d_type == s.d_type);
-  Assert(d_type == t.d_type);
+  Assert(getType() == s.getType());
+  Assert(getType() == t.getType());
   size_t ret = find(s);
   if (ret != std::string::npos)
   {
@@ -263,7 +291,7 @@ Sequence Sequence::replace(const Sequence& s, const Sequence& t) const
     vec.insert(vec.begin(), d_seq.begin(), d_seq.begin() + ret);
     vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end());
     vec.insert(vec.end(), d_seq.begin() + ret + s.size(), d_seq.end());
-    return Sequence(d_type, vec);
+    return Sequence(getType(), vec);
   }
   return *this;
 }
@@ -272,10 +300,8 @@ Sequence Sequence::substr(size_t i) const
 {
   Assert(i >= 0);
   Assert(i <= size());
-  std::vector<Node> ret_vec;
-  std::vector<Node>::const_iterator itr = d_seq.begin() + i;
-  ret_vec.insert(ret_vec.end(), itr, d_seq.end());
-  return Sequence(d_type, ret_vec);
+  std::vector<Node> retVec(d_seq.begin() + i, d_seq.end());
+  return Sequence(getType(), retVec);
 }
 
 Sequence Sequence::substr(size_t i, size_t j) const
@@ -283,15 +309,14 @@ Sequence Sequence::substr(size_t i, size_t j) const
   Assert(i >= 0);
   Assert(j >= 0);
   Assert(i + j <= size());
-  std::vector<Node> ret_vec;
   std::vector<Node>::const_iterator itr = d_seq.begin() + i;
-  ret_vec.insert(ret_vec.end(), itr, itr + j);
-  return Sequence(d_type, ret_vec);
+  std::vector<Node> retVec(itr, itr + j);
+  return Sequence(getType(), retVec);
 }
 
 bool Sequence::noOverlapWith(const Sequence& y) const
 {
-  Assert(d_type == y.d_type);
+  Assert(getType() == y.getType());
   return y.find(*this) == std::string::npos
          && this->find(y) == std::string::npos && this->overlap(y) == 0
          && y.overlap(*this) == 0;
@@ -299,16 +324,6 @@ 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();

diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 763534274bec23e7596eb1559bc2fa70f659324a..c3b7105921fede9e89ab18241e027a14d113b1f6 100644 (file)
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -12,17 +12,20 @@
  ** \brief The sequence data type.
  **/
 
-#include "cvc4_private.h"
+#include "cvc4_public.h"
 
 #ifndef CVC4__EXPR__SEQUENCE_H
 #define CVC4__EXPR__SEQUENCE_H
 
+#include <memory>
 #include <vector>
-#include "expr/node.h"
 
 namespace CVC4 {
 
-class ExprSequence;
+template <bool ref_count>
+class NodeTemplate;
+typedef NodeTemplate<true> Node;
+class TypeNode;
 
 /** The CVC4 sequence class
  *
@@ -37,7 +40,10 @@ class Sequence
    * where each Node in this vector must be a constant.
    */
   Sequence() = default;
-  explicit Sequence(TypeNode t, const std::vector<Node>& s);
+  explicit Sequence(const TypeNode& t, const std::vector<Node>& s);
+  Sequence(const Sequence& seq);
+
+  ~Sequence();
 
   Sequence& operator=(const Sequence& y);
 
@@ -54,11 +60,11 @@ class Sequence
   bool rstrncmp(const Sequence& y, size_t n) const;
 
   /** is this the empty sequence? */
-  bool empty() const { return d_seq.empty(); }
+  bool empty() const;
   /** is less than or equal to sequence y */
   bool isLeq(const Sequence& y) const;
   /** Return the length of the sequence */
-  size_t size() const { return d_seq.size(); }
+  size_t size() const;
 
   /** Return true if this sequence is a repetition of the same element */
   bool isRepeated() const;
@@ -131,23 +137,21 @@ class Sequence
   size_t roverlap(const Sequence& y) const;
 
   /** get the element type of the sequence */
-  TypeNode getType() const { return d_type; }
+  const TypeNode& getType() const;
   /** get the internal Node representation of this sequence */
-  const std::vector<Node>& getVec() const { return d_seq; }
+  const std::vector<Node>& getVec() const;
   /** get the internal node value of the first element in this sequence */
-  Node front() const;
+  const Node& front() const;
   /** get the internal node value of the last element in this sequence */
-  Node back() const;
+  const Node& back() const;
+  /** @return The element at the i-th position */
+  const Node& nth(size_t i) const;
   /**
    * Returns the maximum sequence length representable by this class.
    * Corresponds to the maximum size of d_seq.
    */
   static size_t maxSize();
 
-  //!!!!!!!!!!!!!!! temporary
-  ExprSequence toExprSequence();
-  //!!!!!!!!!!!!!!! end temporary
-
  private:
   /**
    * Returns a negative number if *this < y, 0 if *this and y are equal and a
@@ -155,7 +159,7 @@ class Sequence
    */
   int cmp(const Sequence& y) const;
   /** The element type of the sequence */
-  TypeNode d_type;
+  std::unique_ptr<TypeNode> d_type;
   /** The data of the sequence */
   std::vector<Node> d_seq;
 };

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index afbd7ee58e69797454021657a0cd5a4b8f5f8e0b..216fb051767261f1d79978ff6abed79fbd69b128 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -26,7 +26,6 @@
 
 #include "expr/dtype.h"
 #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"
@@ -169,7 +168,7 @@ void CvcPrinter::toStream(
     }
     case kind::CONST_SEQUENCE:
     {
-      const Sequence& sn = n.getConst<ExprSequence>().getSequence();
+      const Sequence& sn = n.getConst<Sequence>();
       const std::vector<Node>& snvec = sn.getVec();
       if (snvec.size() > 1)
       {

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bb3870ee5adee12c0fded95ba17188e85343f30b..10357904a21c3a21993e65e7e853dd077ab711df 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -23,7 +23,6 @@
 
 #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"
@@ -215,7 +214,7 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     case kind::CONST_SEQUENCE:
     {
-      const Sequence& sn = n.getConst<ExprSequence>().getSequence();
+      const Sequence& sn = n.getConst<Sequence>();
       const std::vector<Node>& snvec = sn.getVec();
       if (snvec.empty())
       {

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 952f2669146acefd53f39c6768417f64f9edbc1f..00658d08b8f833fb76fcccc8c5a5ac32f9fb0d94 100644 (file)
--- 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 96ba82a44dbe3ec6c6578abba146d47b28cf109d..21a435152f496f5858c57a8e8e7809aa14b845ee 100644 (file)
--- 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 bb0fa1d9737d98a3ed5f353b1b04eac5d3813d5b..110864c3b20186ce7376b299b51c30bc8613a46d 100644 (file)
--- 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 192b4fd34ed1f6a11990cd93137c2d22eb8f25cf..78b925ebe84092b7b8968a7c023cb9b5fa97d453 100644 (file)
--- 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 afedaed5ce2ade61728ea4e967c6149597b4cc48..ae88f63f73922aedbb9a2d76458dd5d4533c9e53 100644 (file)
--- 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 fec5677332020d151f9892eee8a72b4350a704e9..49221409e5c4921b8458595a12c0b56c456fa634 100644 (file)
--- 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();