1 files changed, 105 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
new file mode 100644
index 000000000..814276a7c
--- /dev/null
+++ b/src/theory/strings/kinds
@@ -0,0 +1,105 @@
+# kinds [for strings theory]
+#
+
+theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
+
+properties check parametric propagate
+
+rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
+
+typechecker "theory/strings/theory_strings_type_rules.h"
+
+
+operator STRING_CONCAT 2: "string concat"
+
+operator STRING_IN_REGEXP 2 "membership"
+
+operator STRING_LENGTH 1 "string length"
+
+#sort CHAR_TYPE \
+#    Cardinality::INTEGERS \
+#    well-founded \
+#        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
+#        "util/regexp.h" \
+#    "String type"
+
+sort STRING_TYPE \
+    Cardinality::INTEGERS \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
+        "util/regexp.h" \
+    "String type"
+
+sort REGEXP_TYPE \
+    Cardinality::INTEGERS \
+    well-founded \
+        "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \
+        "util/regexp.h" \
+    "RegExp type"
+
+enumerator STRING_TYPE \
+    "::CVC4::theory::strings::StringEnumerator" \
+    "theory/strings/type_enumerator.h"
+
+#enumerator REGEXP_TYPE \
+#    "::CVC4::theory::strings::RegExpEnumerator" \
+#    "theory/strings/type_enumerator.h"
+
+constant CONST_STRING \
+    ::CVC4::String \
+    ::CVC4::strings::StringHashFunction \
+    "util/regexp.h" \
+    "a string of characters"
+
+constant CONST_REGEXP \
+    ::CVC4::RegExp \
+    ::CVC4::RegExpHashFunction \
+    "util/regexp.h" \
+    "a regular expression"
+
+typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
+typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
+
+# equal equal / less than / output
+operator STRING_TO_REGEXP 1 "convert string to regexp"
+operator REGEXP_CONCAT 2: "regexp concat"
+operator REGEXP_OR 2: "regexp or"
+operator REGEXP_INTER 2: "regexp intersection"
+operator REGEXP_STAR 1 "regexp *"
+operator REGEXP_PLUS 1 "regexp +"
+operator REGEXP_OPT 1 "regexp ?"
+
+#constant REGEXP_EMPTY \
+#	::CVC4::RegExp \
+#	::CVC4::RegExpHashFunction \
+#	"util/string.h" \
+#	"a regexp contains nothing"
+
+#constant REGEXP_ALL \
+#	::CVC4::RegExp \
+#	::CVC4::RegExpHashFunction \
+#	"util/string.h" \
+#	"a regexp contains all strings"
+
+#constant REGEXP_SIGMA \
+#	::CVC4::RegExp \
+#	::CVC4::RegExpHashFunction \
+#	"util/string.h" \
+#	"a regexp contains an arbitrary charactor"
+
+typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
+typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule
+typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
+typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
+typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
+typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
+
+typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
+
+
+typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
+typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
+
+typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
+
+endtheory