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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ff11897e991fb97b64d5213884633b2a2e0111e9..e9be4dd3eacb9137268eb10448ff540dfeacf6ea 100644 (file)
--- 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 c5abf9b27393c8ba0a6479b08fffb413586fbdfe..2cecf15e9b6a966c48aae3f18f8825dfe9583808 100644 (file)
--- 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 01fd088a8b553d35ec7d282d1fd77bb1cc6a7e12..6b3598a2fa1b9a42a529f4de03576bfe5319a852 100644 (file)
--- 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 f2a4377d0728f8000364fd6e1dab83719cc2ed82..413041213e763dad4a299d2af7a0353566b33897 100644 (file)
--- 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 14ccf213ce3e048362e6dba55a402baf7edb3ef5..14228d7c587ade8cc8f6f916f5b12e318a2e4959 100644 (file)
--- 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 f8251e752a0a718bb6a866f9d1d98330ceb46dab..5a5e7a9d48a9d942f10148dc71b602bd15918810 100644 (file)
--- 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 (file)
index 0000000..4f761c8
--- /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 (file)
index 0000000..9515a92
--- /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 (file)
index 0000000..42e1304
--- /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 e42a67bbe1cb33def241a9e7a5e26035a0c66b58..f70a70027103badb44be876b3923e24b8d30696c 100644 (file)
--- 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 833e7944163483b91266ca364033ab8d08270180..2e0721b4acd567b0ea3cfba4d8b15c9cb0d92e5e 100644 (file)
--- 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 06f05a8af8b10d65a20e927f70762dda7b58b191..27ffe5d265275e0c3d335195ce459a8174f2edfb 100644 (file)
--- 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"