Add the sequence type (#4539)

This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.

The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 2cecf15e9b6a966c48aae3f18f8825dfe9583808..4e1b96af9f40a75731cf36a877de28f1c3d9fd9e 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -138,6 +138,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__pairT_CVC4__Expr_CVC4__Expr_t_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__vectorT_std__string_t_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SelectorType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SequenceType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SetType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index feec9b78256efcae137606d4ed462e35b1c1e5fb..7bc98f65d8aad4a42371180947325d361af1bc7b 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -495,6 +495,17 @@ Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, cons
   return n;
 }
 
+TypeNode NodeManager::mkSequenceType(TypeNode elementType)
+{
+  CheckArgument(
+      !elementType.isNull(), elementType, "unexpected NULL element type");
+  CheckArgument(elementType.isFirstClass(),
+                elementType,
+                "cannot store types that are not first-class in sequences. Try "
+                "option --uf-ho.");
+  return mkTypeNode(kind::SEQUENCE_TYPE, elementType);
+}
+
 TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
                                         TypeNode range) {
   vector<TypeNode> sorts;

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index aea49d979bd9acc4838da9f7c16483a48421ff35..45d3d5b7d8fcd73d9b9204a7ada5e5dbd3bf17e6 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -875,9 +875,12 @@ public:
   /** Make the type of arrays with the given parameterization */
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
-  /** Make the type of arrays with the given parameterization */
+  /** Make the type of set with the given parameterization */
   inline TypeNode mkSetType(TypeNode elementType);
 
+  /** Make the type of sequences with the given parameterization */
+  TypeNode mkSequenceType(TypeNode elementType);
+
   /** Make a type representing a constructor with the given parameterization */
   TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
   /**

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 031dcb3f092f7a6d254831f01f05ebc3473bbe2e..2067beef54279929eca60042104cfa68af902829 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -353,6 +353,12 @@ bool Type::isSet() const {
   return d_typeNode->isSet();
 }
 
+bool Type::isSequence() const
+{
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSequence();
+}
+
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -516,6 +522,11 @@ SetType::SetType(const Type& t) : Type(t)
   PrettyCheckArgument(isNull() || isSet(), this);
 }
 
+SequenceType::SequenceType(const Type& t) : Type(t)
+{
+  PrettyCheckArgument(isNull() || isSequence(), this);
+}
+
 SortType::SortType(const Type& t) : Type(t)
 {
   PrettyCheckArgument(isNull() || isSort(), this);
@@ -550,6 +561,11 @@ Type SetType::getElementType() const {
   return makeType(d_typeNode->getSetElementType());
 }
 
+Type SequenceType::getElementType() const
+{
+  return makeType(d_typeNode->getSequenceElementType());
+}
+
 DatatypeType ConstructorType::getRangeType() const {
   return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
 }

diff --git a/src/expr/type.h b/src/expr/type.h
index 529c409302c3346785875847f8ac7edd4a3a995e..0cdf556262bf05d562eafee7511ff48f5519c833 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -373,7 +373,13 @@ protected:
    */
   bool isSet() const;
 
- /**
+  /**
+   * Is this a Sequence type?
+   * @return true if the type is a Sequence type
+   */
+  bool isSequence() const;
+
+  /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
@@ -515,15 +521,26 @@ class CVC4_PUBLIC ArrayType : public Type {
   Type getConstituentType() const;
 };/* class ArrayType */
 
-/** Class encapsulating an set type. */
+/** Class encapsulating a set type. */
 class CVC4_PUBLIC SetType : public Type {
  public:
   /** Construct from the base type */
   SetType(const Type& type = Type());
 
-  /** Get the index type */
+  /** Get the element type */
+  Type getElementType() const;
+}; /* class SetType */
+
+/** Class encapsulating a sequence type. */
+class CVC4_PUBLIC SequenceType : public Type
+{
+ public:
+  /** Construct from the base type */
+  SequenceType(const Type& type = Type());
+
+  /** Get the element type */
   Type getElementType() const;
-};/* class SetType */
+}; /* class SetType */
 
 /** Class encapsulating a user-defined sort. */
 class CVC4_PUBLIC SortType : public Type {

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 110db6162a1face7017ea8916fa2f06c9f01580b..e191be0c202165c267d7c6d57c50a6684f1866e2 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -122,7 +122,7 @@ bool TypeNode::isFiniteInternal(bool usortFinite)
   {
     ret = true;
   }
-  else if (isString() || isRegExp() || isReal())
+  else if (isString() || isRegExp() || isSequence() || isReal())
   {
     ret = false;
   }
@@ -245,6 +245,10 @@ bool TypeNode::isClosedEnumerable()
     {
       ret = getSetElementType().isClosedEnumerable();
     }
+    else if (isSequence())
+    {
+      ret = getSequenceElementType().isClosedEnumerable();
+    }
     else if (isDatatype())
     {
       // avoid infinite loops: initially set to true
@@ -353,6 +357,12 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   return false;
 }
 
+TypeNode TypeNode::getSequenceElementType() const
+{
+  Assert(isSequence());
+  return (*this)[0];
+}
+
 TypeNode TypeNode::getBaseType() const {
   TypeNode realt = NodeManager::currentNM()->realType();
   if (isSubtypeOf(realt)) {

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 70392fb0187229341f978827b244930e365eebc5..c9771bd3d4761f3c4b6e8c7bf529a88dc640ec1d 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -518,6 +518,9 @@ public:
   /** Is this a Set type? */
   bool isSet() const;
 
+  /** Is this a Sequence type? */
+  bool isSequence() const;
+
   /** Get the index type (for array types) */
   TypeNode getArrayIndexType() const;
 
@@ -536,6 +539,8 @@ public:
   /** Get the element type (for set types) */
   TypeNode getSetElementType() const;
 
+  /** Get the element type (for sequence types) */
+  TypeNode getSequenceElementType() const;
   /**
    * Is this a function type?  Function-like things (e.g. datatype
    * selectors) that aren't actually functions are NOT considered
@@ -964,6 +969,11 @@ inline bool TypeNode::isSet() const {
   return getKind() == kind::SET_TYPE;
 }
 
+inline bool TypeNode::isSequence() const
+{
+  return getKind() == kind::SEQUENCE_TYPE;
+}
+
 inline TypeNode TypeNode::getSetElementType() const {
   Assert(isSet());
   return (*this)[0];

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 27ffe5d265275e0c3d335195ce459a8174f2edfb..800847ffe472080d26015d21daeb920de49fe6ac 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -58,12 +58,27 @@ constant CONST_STRING \
     "util/string.h" \
     "a string of characters"
 
+# the type
+operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements"
+cardinality SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \
+    "theory/strings/theory_strings_type_rules.h"
+well-founded SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \
+    "theory/strings/theory_strings_type_rules.h"
+enumerator SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceEnumerator" \
+    "theory/strings/type_enumerator.h"
+
 constant CONST_SEQUENCE \
     ::CVC4::ExprSequence \
     ::CVC4::ExprSequenceHashFunction \
     "expr/expr_sequence.h" \
     "a sequence of characters"
 
+operator SEQ_UNIT 1 "a sequence of length one"
+
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
 operator REGEXP_CONCAT 2: "regexp concat"
@@ -144,4 +159,9 @@ typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
 
+### sequence specific operators
+
+typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule
+typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule
+
 endtheory

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index 2953a2b3c7aab2b2328c7dd1c37ed938d0670226..a4055c4f9476bc5559beb58bbade93470df51c57 100644 (file)
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -200,6 +200,7 @@ const char* toString(Rewrite r)
     case Rewrite::LEN_REPL_INV: return "LEN_REPL_INV";
     case Rewrite::LEN_CONV_INV: return "LEN_CONV_INV";
     case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
+    case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
     default: return "?";
   }
 }

diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index 7a315ebd3114ca27f1836cf75fe43b5ebd44cb96..96a3b65fd287dc64793746b59498822163bb9023 100644 (file)
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -202,7 +202,8 @@ enum class Rewrite : uint32_t
   LEN_CONCAT,
   LEN_REPL_INV,
   LEN_CONV_INV,
-  CHARAT_ELIM
+  CHARAT_ELIM,
+  SEQ_UNIT_EVAL
 };
 
 /**

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 2d2ec0af0cab30f87af1f3511023e2556acd26e8..55d58b860f731a090e9225595f6c5ac20803dfc6 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1461,6 +1461,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
   {
     retNode = rewriteRepeatRegExp(node);
   }
+  else if (nk == SEQ_UNIT)
+  {
+    retNode = rewriteSeqUnit(node);
+  }
 
   Trace("sequences-postrewrite")
       << "Strings::SequencesRewriter::postRewrite returning " << retNode
@@ -3095,6 +3099,19 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
   return res;
 }
 
+Node SequencesRewriter::rewriteSeqUnit(Node node)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (node[0].isConst())
+  {
+    std::vector<Expr> seq;
+    seq.push_back(node[0].toExpr());
+    TypeNode stype = nm->mkSequenceType(node[0].getType());
+    Node ret = nm->mkConst(ExprSequence(stype.toType(), seq));
+    return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL);
+  }
+  return node;
+}
 
 Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
 {

diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 56b74f5364802c5858a02244a1829f5cd33a1d72..490dd8b3cdfd46b1ebead66a9509300811dd36a3 100644 (file)
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -224,6 +224,12 @@ class SequencesRewriter : public TheoryRewriter
    * Returns the rewritten form of node.
    */
   Node rewriteStringToCode(Node node);
+  /** rewrite seq.unit
+   * This is the entry point for post-rewriting terms n of the form
+   *   seq.unit( t )
+   * Returns the rewritten form of node.
+   */
+  Node rewriteSeqUnit(Node node);
 
   /** length preserving rewrite
    *

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 93a32f26eac731fb407f38f0982efb3badef3c24..3229e66310457d8209533e4dd574d1e60fdd18a1 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -20,6 +20,9 @@
 #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 #define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 
+#include "expr/expr_sequence.h"
+#include "expr/sequence.h"
+
 namespace CVC4 {
 namespace theory {
 namespace strings {
@@ -318,6 +321,53 @@ public:
   }
 };
 
+class ConstSequenceTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::CONST_SEQUENCE);
+    return n.getConst<ExprSequence>().getSequence().getType();
+  }
+};
+
+class SeqUnitTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    return nodeManager->mkSequenceType(n[0].getType(check));
+  }
+};
+
+/** Properties of the sequence type */
+struct SequenceProperties
+{
+  static Cardinality computeCardinality(TypeNode type)
+  {
+    Assert(type.getKind() == kind::SEQUENCE_TYPE);
+    return Cardinality::INTEGERS;
+  }
+  /** A sequence is well-founded if its element type is */
+  static bool isWellFounded(TypeNode type)
+  {
+    return type[0].isWellFounded();
+  }
+  /** Make ground term for sequence type (return the empty sequence) */
+  static Node mkGroundTerm(TypeNode type)
+  {
+    Assert(type.isSequence());
+    // empty sequence
+    std::vector<Expr> seq;
+    return NodeManager::currentNM()->mkConst(
+        ExprSequence(SequenceType(type.toType()), seq));
+  }
+}; /* struct SequenceProperties */
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index d242068605cede89bddcfdbaf791f3479848cd62..c25363e65d8d1fad5ca00435ccf5de04cd619513 100644 (file)
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -158,6 +158,67 @@ void StringEnumLen::mkCurr()
   d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
 }
 
+SeqEnumLen::SeqEnumLen(TypeNode tn,
+                       TypeEnumeratorProperties* tep,
+                       uint32_t startLength)
+    : SEnumLen(tn, startLength)
+{
+  d_elementEnumerator.reset(
+      new TypeEnumerator(d_type.getSequenceElementType(), tep));
+  mkCurr();
+}
+
+SeqEnumLen::SeqEnumLen(TypeNode tn,
+                       TypeEnumeratorProperties* tep,
+                       uint32_t startLength,
+                       uint32_t endLength)
+    : SEnumLen(tn, startLength, endLength)
+{
+  d_elementEnumerator.reset(
+      new TypeEnumerator(d_type.getSequenceElementType(), tep));
+  mkCurr();
+}
+
+SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
+    : SEnumLen(wenum),
+      d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
+      d_elementDomain(wenum.d_elementDomain)
+{
+}
+
+bool SeqEnumLen::increment()
+{
+  if (!d_elementEnumerator->isFinished())
+  {
+    // yet to establish domain
+    Assert(d_elementEnumerator != nullptr);
+    d_elementDomain.push_back((**d_elementEnumerator).toExpr());
+    ++(*d_elementEnumerator);
+  }
+  // the current cardinality is the domain size of the element
+  if (!d_witer->increment(d_elementDomain.size()))
+  {
+    Assert(d_elementEnumerator->isFinished());
+    d_curr = Node::null();
+    return false;
+  }
+  mkCurr();
+  return true;
+}
+
+void SeqEnumLen::mkCurr()
+{
+  std::vector<Expr> seq;
+  const std::vector<unsigned>& data = d_witer->getData();
+  for (unsigned i : data)
+  {
+    seq.push_back(d_elementDomain[i]);
+  }
+  // make sequence from seq
+  d_curr =
+      NodeManager::currentNM()->mkConst(ExprSequence(d_type.toType(), seq));
+}
+
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
     : TypeEnumeratorBase<StringEnumerator>(type),
       d_wenum(0, utils::getAlphabetCardinality())
@@ -182,6 +243,28 @@ StringEnumerator& StringEnumerator::operator++()
 
 bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
 
+SequenceEnumerator::SequenceEnumerator(TypeNode type,
+                                       TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
+{
+}
+
+SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
+    : TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
+      d_wenum(enumerator.d_wenum)
+{
+}
+
+Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
+
+SequenceEnumerator& SequenceEnumerator::operator++()
+{
+  d_wenum.increment();
+  return *this;
+}
+
+bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); }
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index b379ce5c3fbb0eeb9896c7d5f9e286e8596d0b9a..c82892624faeea35fa6cf80bc43cff78b251c3dc 100644 (file)
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -136,6 +136,34 @@ class StringEnumLen : public SEnumLen
   void mkCurr();
 };
 
+/**
+ * Enumerates sequence values for a given length.
+ */
+class SeqEnumLen : public SEnumLen
+{
+ public:
+  /** For sequences */
+  SeqEnumLen(TypeNode tn, TypeEnumeratorProperties* tep, uint32_t startLength);
+  SeqEnumLen(TypeNode tn,
+             TypeEnumeratorProperties* tep,
+             uint32_t startLength,
+             uint32_t endLength);
+  /** copy constructor */
+  SeqEnumLen(const SeqEnumLen& wenum);
+  /** destructor */
+  ~SeqEnumLen() {}
+  /** increment */
+  bool increment() override;
+
+ private:
+  /** an enumerator for the elements' type */
+  std::unique_ptr<TypeEnumerator> d_elementEnumerator;
+  /** The domain */
+  std::vector<Expr> d_elementDomain;
+  /** Make the current term from d_data */
+  void mkCurr();
+};
+
 class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
 {
  public:
@@ -154,6 +182,21 @@ class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
   StringEnumLen d_wenum;
 }; /* class StringEnumerator */
 
+class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator>
+{
+ public:
+  SequenceEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+  SequenceEnumerator(const SequenceEnumerator& enumerator);
+  ~SequenceEnumerator() {}
+  Node operator*() override;
+  SequenceEnumerator& operator++() override;
+  bool isFinished() override;
+
+ private:
+  /** underlying sequence enumerator */
+  SeqEnumLen d_wenum;
+}; /* class SequenceEnumerator */
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */