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, 98 insertions, 0 deletions

diff --git a/src/expr/expr_sequence.cpp b/src/expr/expr_sequence.cpp
new file mode 100644
index 000000000..4f761c8f7
--- /dev/null
+++ b/src/expr/expr_sequence.cpp
@@ -0,0 +1,98 @@
+/*********************                                                        */
+/*! \file expr_sequence.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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