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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4899c8a8..6d69a3388 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -684,6 +684,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::CARD, "card"); addOperator(api::COMPLEMENT, "complement"); addOperator(api::CHOOSE, "choose"); + addOperator(api::IS_SINGLETON, "is_singleton"); addOperator(api::JOIN, "join"); addOperator(api::PRODUCT, "product"); addOperator(api::TRANSPOSE, "transpose"); |