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

1 files changed, 19 insertions, 15 deletions

diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 763534274..c3b710592 100644
--- 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;
 };