add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

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