summaryrefslogtreecommitdiff
path: root/src/theory/sets/kinds
diff options
context:
space:
mode:
authormudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>2020-04-08 18:24:16 -0500
committerGitHub <noreply@github.com>2020-04-08 18:24:16 -0500
commitdf1ea6b9cdc1f424073151d0f7fda639d4405622 (patch)
treef28bd734c6f78e7399f91e92d517343a779c09c3 /src/theory/sets/kinds
parenta48cafdd09c3ff8cb9984bad930343958c30ce56 (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/kinds8
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback