STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

[cvc5.git] / src / theory / builtin / theory_builtin_type_rules.h

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