1 files changed, 55 insertions, 0 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
new file mode 100644
index 000000000..bae0c5f1d
--- /dev/null
+++ b/src/theory/sets/kinds
@@ -0,0 +1,55 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
+typechecker "theory/sets/theory_sets_type_rules.h"
+rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
+
+properties check propagate #presolve postsolve
+
+# Theory content goes here.
+
+# constants...
+constant EMPTYSET \
+    ::CVC4::EmptySet \
+    ::CVC4::EmptySetHashFunction \
+    "util/emptyset.h" \
+    "empty set"
+
+# types...
+operator SET_TYPE 1 "set type"   # the type
+cardinality SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+well-founded SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+enumerator SET_TYPE \
+    "::CVC4::theory::sets::SetEnumerator" \
+    "theory/sets/theory_sets_type_enumerator.h"
+
+# operators...
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset"
+operator IN 2 "set membership"
+
+operator SET_SINGLETON 1 "singleton set"
+
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
+typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
+typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
+typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+
+construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
+construle UNION ::CVC4::theory::sets::SetConstTypeRule
+
+endtheory