diff options
| author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-04-08 18:24:16 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-08 18:24:16 -0500 |
| commit | df1ea6b9cdc1f424073151d0f7fda639d4405622 (patch) | |
| tree | f28bd734c6f78e7399f91e92d517343a779c09c3 /src/api | |
| parent | a48cafdd09c3ff8cb9984bad930343958c30ce56 (diff) | |
Added CHOOSE operator for sets (#4211)
This PR enables THEORY_UF by default for sets and adds the operator CHOOSE for sets which returns an element from a given set. The semantics is as follows:
If a set A = {x}, then the term (choose A) is equivalent to the term x.
If the set is empty, then (choose A) is an arbitrary value.
If the set has cardinality > 1, then (choose A) will deterministically return an element in A.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 12 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8d6de0ade..ea5eca391 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -245,6 +245,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE}, {IDEN, CVC4::Kind::IDEN}, {COMPREHENSION, CVC4::Kind::COMPREHENSION}, + {CHOOSE, CVC4::Kind::CHOOSE}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -513,6 +514,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE}, {CVC4::Kind::IDEN, IDEN}, {CVC4::Kind::COMPREHENSION, COMPREHENSION}, + {CVC4::Kind::CHOOSE, CHOOSE}, /* 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 f8e1fb90c..6c1a2256b 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1852,6 +1852,18 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ COMPREHENSION, + /** + * Returns an element from a given set. + * If a set A = {x}, then the term (choose A) is equivalent to the term x. + * If the set is empty, then (choose A) is an arbitrary value. + * If the set has cardinality > 1, then (choose A) will deterministically + * return an element in A. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + CHOOSE, /* Strings --------------------------------------------------------------- */ |