diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-09-09 13:19:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-09 13:19:40 -0500 |
| commit | b115aecf296b8d712363c506daecfab364f71712 (patch) | |
| tree | 17d88f6733011fdf3eda136be71524d9f497e79d /src/theory/sets/kinds | |
| parent | 1d3bb6048085342e2d85bf5193367afcd96885fa (diff) | |
Add is_singleton operator to the theory of sets (#5033)
This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:
(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index d3c42ef27..fd941ab29 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -67,6 +67,9 @@ operator COMPREHENSION 3 "set comprehension specified by a bound variable list, # 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" +# The operator is_singleton returns whether the given set is a singleton +operator IS_SINGLETON 1 "return whether the given set is a singleton" + operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" @@ -87,6 +90,7 @@ 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 IS_SINGLETON ::CVC4::theory::sets::IsSingletonTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule @@ -96,19 +100,6 @@ typerule JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule typerule IDEN ::CVC4::theory::sets::RelIdenTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule -construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule -construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule 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 -construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule -construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule -construle JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule -construle IDEN ::CVC4::theory::sets::RelIdenTypeRule endtheory |