STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

11 files changed, 99 insertions, 1 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;
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 83a372726..50e4d53bb 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -301,6 +301,23 @@ well-founded TUPLE_TYPE \
     "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
+# These will eventually move to a theory of strings.
+#
+# For now these are unbounded strings over a fixed, finite alphabet
+# (this may change).
+sort STRING_TYPE \
+    Cardinality::INTEGERS \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(::std::string())" \
+        "string" \
+    "String type"
+constant CONST_STRING \
+    ::std::string \
+    ::CVC4::StringHashStrategy \
+    "util/hash.h" \
+    "a string of characters"
+typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
+
 typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index ce06b4259..48a5d475d 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -130,6 +130,15 @@ public:
   }
 };/* class TupleTypeRule */
 
+class StringConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::CONST_STRING);
+    return nodeManager->stringType();
+  }
+};/* class StringConstantTypeRule */
+
+
 class FunctionProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/util/hash.h b/src/util/hash.h
index bd3fee597..6183c5208 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -36,6 +36,12 @@ struct StringHashFunction {
   }
 };/* struct StringHashFunction */
 
+struct StringHashStrategy {
+  static size_t hash(const std::string& str) {
+    return std::hash<const char*>()(str.c_str());
+  }
+};/* struct StringHashStrategy */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__HASH_H */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 7decc693b..94ddf082f 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -102,7 +102,7 @@ Options::Options() :
 static const string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:\n\
    --version | -V         identify this CVC4 binary\n\
-   --help | -h            this command line reference\n\
+   --help | -h            full command line reference\n\
    --lang | -L            force input language (default is `auto'; see --lang help)\n\
    --output-lang          force output language (default is `auto'; see --lang help)\n\
    --verbose | -v         increase verbosity (may be repeated)\n\