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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 10 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
2 files changed, 10 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 32604d03f..3f03ca43d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -205,6 +205,9 @@ tokens { BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + // Sets + SETS_CHOOSE_TOK = 'CHOOSE'; + // Relations JOIN_TOK = 'JOIN'; TRANSPOSE_TOK = 'TRANSPOSE'; @@ -327,7 +330,8 @@ int getOperatorPrecedence(int type) { case PRODUCT_TOK: case IDEN_TOK: case JOIN_IMAGE_TOK: - case TRANSCLOSURE_TOK: return 24; + case TRANSCLOSURE_TOK: + case SETS_CHOOSE_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -367,10 +371,12 @@ api::Kind getOperatorKind(int type, bool& negate) { case XOR_TOK: return api::XOR; case AND_TOK: return api::AND; + case SETS_CHOOSE_TOK: return api::CHOOSE; case PRODUCT_TOK: return api::PRODUCT; case JOIN_TOK: return api::JOIN; case JOIN_IMAGE_TOK: return api::JOIN_IMAGE; + // comparisonBinop case EQUAL_TOK: return api::EQUAL; case DISEQUAL_TOK: negate = true; return api::EQUAL; @@ -2097,6 +2103,8 @@ setsTerm[CVC4::api::Term& f] /* Sets prefix operators */ : SETS_CARD_TOK LPAREN formula[f] RPAREN { f = MK_TERM(CVC4::api::CARD, f); } + | SETS_CHOOSE_TOK LPAREN formula[f] RPAREN + { f = MK_TERM(CVC4::api::CHOOSE, f); } | simpleTerm[f] ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3233ee7e8..2405b3402 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -670,6 +670,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::INSERT, "insert"); addOperator(api::CARD, "card"); addOperator(api::COMPLEMENT, "complement"); + addOperator(api::CHOOSE, "choose"); addOperator(api::JOIN, "join"); addOperator(api::PRODUCT, "product"); addOperator(api::TRANSPOSE, "transpose"); |