1 files changed, 41 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 76306d443..5223c9de6 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -380,6 +380,12 @@ class CVC4_PUBLIC Sort
   bool isSet() const;
 
   /**
+   * Is this a Sequence sort?
+   * @return true if the sort is a Sequence sort
+   */
+  bool isSequence() const;
+
+  /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
@@ -512,6 +518,13 @@ class CVC4_PUBLIC Sort
    */
   Sort getSetElementSort() const;
 
+  /* Sequence sort ------------------------------------------------------- */
+
+  /**
+   * @return the element sort of a sequence sort
+   */
+  Sort getSequenceElementSort() const;
+
   /* Uninterpreted sort -------------------------------------------------- */
 
   /**
@@ -907,6 +920,13 @@ class CVC4_PUBLIC Term
   Term getConstArrayBase() const;
 
   /**
+   *  Return the elements of a constant sequence
+   *  throws an exception if the kind is not CONST_SEQUENCE
+   *  @return the elements of the constant sequence.
+   */
+  std::vector<Term> getConstSequenceElements() const;
+
+  /**
    * Boolean negation.
    * @return the Boolean negation of this term
    */
@@ -1069,6 +1089,13 @@ class CVC4_PUBLIC Term
   bool isNullHelper() const;
 
   /**
+   * Helper function that returns the kind of the term, which takes into
+   * account special cases of the conversion for internal to external kinds.
+   * @return the kind of this term
+   */
+  Kind getKindHelper() const;
+
+  /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
    * memory allocation (CVC4::Expr is already ref counted, so this could be
@@ -2187,6 +2214,13 @@ class CVC4_PUBLIC Solver
   Sort mkSetSort(Sort elemSort) const;
 
   /**
+   * Create a sequence sort.
+   * @param elemSort the sort of the sequence elements
+   * @return the sequence sort
+   */
+  Sort mkSequenceSort(Sort elemSort) const;
+
+  /**
    * Create an uninterpreted sort.
    * @param symbol the name of the sort
    * @return the uninterpreted sort
@@ -2551,6 +2585,13 @@ class CVC4_PUBLIC Solver
   Term mkChar(const char* s) const;
 
   /**
+   * Create an empty sequence of the given element sort.
+   * @param sort The element sort of the sequence.
+   * @return the empty sequence with given element sort.
+   */
+  Term mkEmptySequence(Sort sort) const;
+
+  /**
    * Create a universe set of the given sort.
    * @param sort the sort of the set elements
    * @return the universe set constant