STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

[cvc5.git] / src / expr / type.h

diff --git a/src/expr/type.h b/src/expr/type.h
index b5aa18262b5fc93baff1950f97d3867ee68603e1..0b50fbd3ca27e7c4bef302c8d1557265ee7f7532 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -47,6 +47,7 @@ class BooleanType;
 class IntegerType;
 class RealType;
 class PseudobooleanType;
+class StringType;
 class BitVectorType;
 class ArrayType;
 class DatatypeType;
@@ -253,6 +254,18 @@ public:
    */
   operator PseudobooleanType() const throw(AssertionException);
 
+  /**
+   * Is this the string type?
+   * @return true if the type is the string type
+   */
+  bool isString() const;
+
+  /**
+   * Cast this type to a string type
+   * @return the StringType
+   */
+  operator StringType() const throw(AssertionException);
+
   /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
@@ -448,6 +461,17 @@ public:
   PseudobooleanType(const Type& type) throw(AssertionException);
 };/* class PseudobooleanType */
 
+/**
+ * Singleton class encapsulating the string type.
+ */
+class CVC4_PUBLIC StringType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  StringType(const Type& type) throw(AssertionException);
+};/* class StringType */
+
 /**
  * Class encapsulating a function type.
  */