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.

8 files changed, 214 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index f2a4377d0..413041213 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -12,6 +12,8 @@ libcvc4_add_sources(
   expr_iomanip.cpp
   expr_iomanip.h
   expr_manager_scope.h
+  expr_sequence.cpp
+  expr_sequence.h
   kind_map.h
   match_trie.cpp
   match_trie.h
@@ -32,6 +34,8 @@ libcvc4_add_sources(
   node_traversal.h
   node_value.cpp
   node_value.h
+  sequence.cpp
+  sequence.h
   node_visitor.h
   proof.cpp
   proof.h
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 14ccf213c..14228d7c5 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -146,6 +146,7 @@ namespace CVC4 {
 %template(getConstBoolean) CVC4::Expr::getConst<bool>;
 %template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>;
 %template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>;
+%template(getConstExprSequence) CVC4::Expr::getConst<CVC4::ExprSequence>;
 %template(getConstFloatingPoint) CVC4::Expr::getConst<CVC4::FloatingPoint>;
 %template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>;
 %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index f8251e752..5a5e7a9d4 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -57,6 +57,7 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::ExprSequence>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>;
 #ifdef SWIGPYTHON
 /* The python bindings cannot differentiate between bool and other basic
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
diff --git a/src/expr/expr_sequence.h b/src/expr/expr_sequence.h
new file mode 100644
index 000000000..9515a9244
--- /dev/null
+++ b/src/expr/expr_sequence.h
@@ -0,0 +1,76 @@
+/*********************                                                        */
+/*! \file expr_sequence.h
+ ** \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 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;
+
+  const Type& getType() const;
+  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/expr_sequence.i b/src/expr/expr_sequence.i
new file mode 100644
index 000000000..42e130466
--- /dev/null
+++ b/src/expr/expr_sequence.i
@@ -0,0 +1,18 @@
+%{
+#include "expr/expr_sequence.h"
+%}
+
+%rename(equals) CVC4::ExprSequence::operator==(const ExprSequence&) const;
+%ignore CVC4::ExprSequence::operator!=(const ExprSequence&) const;
+%ignore CVC4::ExprSequence::getSequence() const;
+
+%rename(less) CVC4::ExprSequence::operator<(const ExprSequence&) const;
+%rename(lessEqual) CVC4::ExprSequence::operator<=(const ExprSequence&) const;
+%rename(greater) CVC4::ExprSequence::operator>(const ExprSequence&) const;
+%rename(greaterEqual) CVC4::ExprSequence::operator>=(const ExprSequence&) const;
+
+%rename(apply) CVC4::ExprSequenceHashFunction::operator()(const ExprSequence&) const;
+
+%ignore CVC4::operator<<(std::ostream& out, const ExprSequence& es);
+
+%include "expr/expr_sequence.h"
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();
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 833e79441..2e0721b4a 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -144,6 +144,10 @@ class Sequence
    */
   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