projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e51c4d6) | patch
Make sets and bags operators left-associative (#8584)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 7 Apr 2022 18:09:14 +0000 (13:09 -0500)
committerGitHub <noreply@github.com>
Thu, 7 Apr 2022 18:09:14 +0000 (13:09 -0500)
commit1f486408d66e125a3fc45446601cd088fa4d39cc
tree716a989551acb17cc16c2bfc9175996b92c9862dtree
parente51c4d62523d160058f0f06cb15fef75771f3cebcommit | diff
Make sets and bags operators left-associative (#8584)

Makes it so that we parse n-ary applications of e.g. set.union in smt2.
Left associativity seems to be the case for difference operators in databases.
See
https://docs.microsoft.com/en-us/sql/t-sql/language-elements/set-operators-except-and-intersect-transact-sql?view=sql-server-ver15
src/api/cpp/cvc5.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/parser/set-bag-left-associative.smt2 [new file with mode: 0644] blob