From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 27 May 2020 23:05:07 +0000 (-0500)
Subject: Add the Expr-level sequence datatype (#4526)
X-Git-Tag: cvc5-1.0.0~3283
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4df14f1e09549be607123c66b7dd206e8e244c89;p=cvc5.git

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 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"