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/theory/sets/kinds | |
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/theory/sets/kinds')
-rw-r--r-- | src/theory/sets/kinds | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 058a20aeb..452acfea0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -61,6 +61,12 @@ nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be i # finite sets with quantified formulas. operator COMPREHENSION 3 "set comprehension specified by a bound variable list, a predicate, and a term." +# The operator choose returns an element from a given set. +# If 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. +operator CHOOSE 1 "return an element in the set given as a parameter" + operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" @@ -80,6 +86,7 @@ typerule CARD ::CVC4::theory::sets::CardTypeRule typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule typerule UNIVERSE_SET ::CVC4::theory::sets::UniverseSetTypeRule typerule COMPREHENSION ::CVC4::theory::sets::ComprehensionTypeRule +typerule CHOOSE ::CVC4::theory::sets::ChooseTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule @@ -95,6 +102,7 @@ construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule construle CARD ::CVC4::theory::sets::CardTypeRule construle COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule +construle CHOOSE ::CVC4::theory::sets::ChooseTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule |