diff options
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 71d5fce4a..0c1cc0452 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -80,11 +80,15 @@ operator SET_CHOOSE 1 "return an element in the set given as a parameter # The operator is_singleton returns whether the given set is a singleton operator SET_IS_SINGLETON 1 "return whether the given set is a singleton" +# The set.map operator applies the first argument, a function of type (-> T1 T2), to every element +# of the second argument, a set of type (Set T1), and returns a set of type (Set T2). +operator SET_MAP 2 "set map function" + operator RELATION_JOIN 2 "relation join" operator RELATION_PRODUCT 2 "relation cartesian product" -operator RELATION_TRANSPOSE 1 "relation transpose" -operator RELATION_TCLOSURE 1 "relation transitive closure" -operator RELATION_JOIN_IMAGE 2 "relation join image" +operator RELATION_TRANSPOSE 1 "relation transpose" +operator RELATION_TCLOSURE 1 "relation transitive closure" +operator RELATION_JOIN_IMAGE 2 "relation join image" operator RELATION_IDEN 1 "relation identity" typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule @@ -102,6 +106,7 @@ typerule SET_UNIVERSE ::cvc5::theory::sets::UniverseSetTypeRule typerule SET_COMPREHENSION ::cvc5::theory::sets::ComprehensionTypeRule typerule SET_CHOOSE ::cvc5::theory::sets::ChooseTypeRule typerule SET_IS_SINGLETON ::cvc5::theory::sets::IsSingletonTypeRule +typerule SET_MAP ::cvc5::theory::sets::SetMapTypeRule typerule RELATION_JOIN ::cvc5::theory::sets::RelBinaryOperatorTypeRule typerule RELATION_PRODUCT ::cvc5::theory::sets::RelBinaryOperatorTypeRule |