Sets kinds documentation

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 12f114fc0bc48e5474642304c8939965ad721c0b..799261634f39757654b6c3b47e1088a3c40ecf90 100644 (file)
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -19,7 +19,7 @@ constant EMPTYSET \
     ::CVC4::EmptySet \
     ::CVC4::EmptySetHashFunction \
     "util/emptyset.h" \
-    "empty set"
+    "the empty set constant; payload is an instance of the CVC4::EmptySet class"
 
 # the type
 operator SET_TYPE 1 "set type"
@@ -38,9 +38,9 @@ enumerator SET_TYPE \
 operator UNION         2  "set union"
 operator INTERSECTION  2  "set intersection"
 operator SETMINUS      2  "set subtraction"
-operator SUBSET        2  "subset"
-operator MEMBER        2  "set membership"
-operator SET_SINGLETON 1  "singleton set"
+operator SUBSET        2  "subset predicate; first parameter a subset of second"
+operator MEMBER        2  "set membership predicate; first parameter a member of second"
+operator SET_SINGLETON 1  "the set of the single element given as a parameter"
 
 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3b2acd95698780080625d9189eab6933c57b2684..eff81622dd5470c2c0b9e19232dff16711fd36c0 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -105,7 +105,7 @@ struct MemberTypeRule {
     }
     return nodeManager->booleanType();
   }
-};/* struct SetInTypeRule */
+};/* struct MemberTypeRule */
 
 struct SetSingletonTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -118,7 +118,7 @@ struct SetSingletonTypeRule {
     Assert(n.getKind() == kind::SET_SINGLETON);
     return n[0].isConst();
   }
-};/* struct SetInTypeRule */
+};/* struct SetSingletonTypeRule */
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -128,7 +128,7 @@ struct EmptySetTypeRule {
     Type setType = emptySet.getType();
     return TypeNode::fromType(setType);
   }
-};
+};/* struct EmptySetTypeRule */
 
 
 struct SetsProperties {
@@ -146,7 +146,7 @@ struct SetsProperties {
     Assert(type.isSet());
     return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
   }
-};
+};/* struct SetsProperties */
 
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */