STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 28f990c984f3b33c47067aeae3291c515c1bb5c3..624fbd9a2ccde6eba83199c5a72e460606f8ec72 100644 (file)
--- 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 77b92c873393acf2162efc7ae88f4b6581e07253..18455688763d806f2401bdb3a602313a555cd50a 100644 (file)
--- 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 84ed786621292e0a2efbd0b1462e632464e2fab5..adba8087c4db515293b7c8bd3bde97807eeedfde 100644 (file)
--- 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 77cf97bb1c4e64ce6a374bd4db8c94ed1a419f0b..7e06a05ae6caa7b782e2380913179ad487e945bc 100644 (file)
--- 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 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.
  */

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 51d86904a08e8ae0ce46bb7454b851a656870b8f..77203bbb5f987517317cd44bb6a134ec11d287e3 100644 (file)
--- 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 966611764e0cd03693f1527390ceb6e5f2457c4d..553f83276fbc39d2b91e0395d8a77309905cc2e2 100644 (file)
--- 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 83a37272647b918d1637828a5e929f8a771dd126..50e4d53bbdd6d36dbdc45cb32c9ba1b61205eb4b 100644 (file)
--- 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 ce06b425971fce95abce668f0d419178967b9892..48a5d475d18bda383bd6f442bc80c4117362db4a 100644 (file)
--- 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 bd3fee5979781b118e29486f3f1069281e662ca4..6183c5208accc2d5f3f00b59279b1eedb4672305 100644 (file)
--- 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 7decc693bf8a0e9250caf6dc99d704262753267a..94ddf082f20fad696b8176f41b67fef9b18ecced 100644 (file)
--- 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\