diff options
| -rw-r--r-- | src/theory/sets/kinds | 8 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 8 |
2 files changed, 8 insertions, 8 deletions
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 */ |