diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-06 08:23:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-06 08:23:40 -0500 |
| commit | f3c6bb510a87f390c51bf3cecc079cc9c9615ea4 (patch) | |
| tree | e5db14ee34eb97886c2ae4ea9ab6c81fa9449c7f /src/api | |
| parent | cb54d547b2a0e99258cb4c754bc4d979abee93f8 (diff) | |
Add operators bag.from_set, bag.to_set to the theory of bags (#5186)
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 4 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 16 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 30e95714d..f19ee2bf7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -267,6 +267,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {BAG_CARD, CVC4::Kind::BAG_CARD}, {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE}, {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON}, + {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET}, + {BAG_TO_SET, CVC4::Kind::BAG_TO_SET}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -570,6 +572,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::BAG_CARD, BAG_CARD}, {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE}, {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, + {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET}, + {CVC4::Kind::BAG_TO_SET, BAG_TO_SET}, /* Strings --------------------------------------------------------- */ {CVC4::Kind::STRING_CONCAT, STRING_CONCAT}, {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 5910ef1c9..6f84a9959 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2074,6 +2074,22 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child) */ BAG_IS_SINGLETON, + /** + * Bag.from_set converts a set to a bag. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_FROM_SET, + /** + * Bag.to_set converts a bag to a set. + * Parameters: 1 + * -[1]: Term of bag sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_TO_SET, /* Strings --------------------------------------------------------------- */ |