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.

12 files changed, 223 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ff11897e9..e9be4dd3e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -923,6 +923,7 @@ 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/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index c5abf9b27..2cecf15e9 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -65,6 +65,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ExprSequence.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java
diff --git a/src/cvc4.i b/src/cvc4.i
index 01fd088a8..6b3598a2f 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -286,6 +286,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "expr/array_store_all.i"
 %include "expr/ascription_type.i"
 %include "expr/emptyset.i"
+%include "expr/expr_sequence.i"
 %include "expr/datatype.i"
 %include "expr/record.i"
 %include "proof/unsat_core.i"
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
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 06f05a8af..27ffe5d26 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -58,6 +58,12 @@ constant CONST_STRING \
     "util/string.h" \
     "a string of characters"
 
+constant CONST_SEQUENCE \
+    ::CVC4::ExprSequence \
+    ::CVC4::ExprSequenceHashFunction \
+    "expr/expr_sequence.h" \
+    "a sequence of characters"
+
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
 operator REGEXP_CONCAT 2: "regexp concat"