STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

2 files changed, 26 insertions, 0 deletions

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) {