From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 23:59:48 +0000 (-0400)
Subject: Sets kinds documentation
X-Git-Tag: cvc5-1.0.0~6712^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44d05f7def63e5f675f80dab8829c5759db7e065;p=cvc5.git

Sets kinds documentation
---

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 12f114fc0..799261634 100644
--- 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 3b2acd956..eff81622d 100644
--- 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 */