diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-08-30 18:26:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-30 23:26:43 +0000 |
| commit | 22c83c12097da6105e6f03e0df70385527e651a4 (patch) | |
| tree | fceebd94973d6ffbb02d88c389ebd7c165847b82 /src/api/cpp | |
| parent | 321694d4efde0cef18e313d93c8b69835aac3b72 (diff) | |
Add kind BAG_MAP and its type rule to bags (#6503)
This PR adds kind BAG_MAP to bags.
Diffstat (limited to 'src/api/cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 2 | ||||
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 15 |
2 files changed, 17 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index e245dc415..626edf7bb 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -308,6 +308,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {BAG_IS_SINGLETON, cvc5::Kind::BAG_IS_SINGLETON}, {BAG_FROM_SET, cvc5::Kind::BAG_FROM_SET}, {BAG_TO_SET, cvc5::Kind::BAG_TO_SET}, + {BAG_MAP, cvc5::Kind::BAG_MAP}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, cvc5::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, cvc5::Kind::STRING_IN_REGEXP}, @@ -617,6 +618,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, {cvc5::Kind::BAG_FROM_SET, BAG_FROM_SET}, {cvc5::Kind::BAG_TO_SET, BAG_TO_SET}, + {cvc5::Kind::BAG_MAP,BAG_MAP}, /* Strings --------------------------------------------------------- */ {cvc5::Kind::STRING_CONCAT, STRING_CONCAT}, {cvc5::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index e8b876b55..94a8a6f92 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2515,6 +2515,21 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child) const` */ BAG_TO_SET, + /** + * bag.map operator applies the first argument, a function of type (-> T1 T2), + * to every element of the second argument, a bag of type (Bag T1), + * and returns a bag of type (Bag T2). + * + * Parameters: + * - 1: a function of type (-> T1 T2) + * - 2: a bag of type (Bag T1) + * + * Create with: + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) + * const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` + */ + BAG_MAP, /* Strings --------------------------------------------------------------- */ |