STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

7 files changed, 66 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 28f990c98..624fbd9a2 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -125,6 +125,11 @@ BooleanType ExprManager::booleanType() const {
   return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
 }
 
+StringType ExprManager::stringType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
+}
+
 KindType ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
   return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 77b92c873..184556887 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -120,6 +120,9 @@ public:
   /** Get the type for booleans */
   BooleanType booleanType() const;
 
+  /** Get the type for strings. */
+  StringType stringType() const;
+
   /** Get the type for sorts. */
   KindType kindType() const;
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 84ed78662..adba8087c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -515,6 +515,9 @@ public:
   /** Get the (singleton) type for pseudobooleans. */
   inline TypeNode pseudobooleanType();
 
+  /** Get the (singleton) type for strings. */
+  inline TypeNode stringType();
+
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
@@ -780,6 +783,11 @@ inline TypeNode NodeManager::pseudobooleanType() {
   return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
 }
 
+/** Get the (singleton) type for strings. */
+inline TypeNode NodeManager::stringType() {
+  return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
+}
+
 /** Get the (singleton) type for sorts. */
 inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 77cf97bb1..7e06a05ae 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -227,6 +227,19 @@ Type::operator PseudobooleanType() const throw(AssertionException) {
   return PseudobooleanType(*this);
 }
 
+/** Is this the string type? */
+bool Type::isString() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isString();
+}
+
+/** Cast to a string type */
+Type::operator StringType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isString());
+  return StringType(*this);
+}
+
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
@@ -465,6 +478,11 @@ PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
   Assert(isNull() || isPseudoboolean());
 }
 
+StringType::StringType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isString());
+}
+
 BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isNull() || isBitVector());
diff --git a/src/expr/type.h b/src/expr/type.h
index b5aa18262..0b50fbd3c 100644
--- 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;
@@ -254,6 +255,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
    */
@@ -449,6 +462,17 @@ public:
 };/* 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.
  */
 class CVC4_PUBLIC FunctionType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 51d86904a..77203bbb5 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -95,6 +95,11 @@ bool TypeNode::isPseudoboolean() const {
     getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
 }
 
+bool TypeNode::isString() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == STRING_TYPE;
+}
+
 bool TypeNode::isArray() const {
   return getKind() == kind::ARRAY_TYPE;
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 966611764..553f83276 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -449,6 +449,9 @@ public:
   /** Is this the Pseudoboolean type? */
   bool isPseudoboolean() const;
 
+  /** Is this the String type? */
+  bool isString() const;
+
   /** Is this an array type? */
   bool isArray() const;