From 1f486408d66e125a3fc45446601cd088fa4d39cc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Apr 2022 13:09:14 -0500 Subject: [PATCH] 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 | 5 ++++- test/regress/cli/CMakeLists.txt | 1 + .../parser/set-bag-left-associative.smt2 | 19 +++++++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/parser/set-bag-left-associative.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 50ee85bf5..5de54018c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5051,7 +5051,10 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const if (echildren.size() > 2) { if (kind == INTS_DIVISION || kind == XOR || kind == SUB || kind == DIVISION - || kind == HO_APPLY || kind == REGEXP_DIFF) + || kind == HO_APPLY || kind == REGEXP_DIFF || kind == SET_UNION + || kind == SET_INTER || kind == SET_MINUS || kind == BAG_INTER_MIN + || kind == BAG_UNION_MAX || kind == BAG_UNION_DISJOINT + || kind == BAG_DIFFERENCE_REMOVE || kind == BAG_DIFFERENCE_SUBTRACT) { // left-associative, but cvc5 internally only supports 2 args res = d_nodeMgr->mkLeftAssociative(k, echildren); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index d67442198..99ca3b969 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -889,6 +889,7 @@ set(regress_0_tests regress0/parser/proj-issue370-push-pop-global.smt2 regress0/parser/quoted-define-fun.smt2 regress0/parser/real-numerals.smt2 + regress0/parser/set-bag-left-associative.smt2 regress0/parser/shadow_fun_symbol_all.smt2 regress0/parser/shadow_fun_symbol_nirat.smt2 regress0/parser/strings20.smt2 diff --git a/test/regress/cli/regress0/parser/set-bag-left-associative.smt2 b/test/regress/cli/regress0/parser/set-bag-left-associative.smt2 new file mode 100644 index 000000000..21dc8f540 --- /dev/null +++ b/test/regress/cli/regress0/parser/set-bag-left-associative.smt2 @@ -0,0 +1,19 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun A () (Bag Int)) +(declare-fun B () (Bag Int)) +(declare-fun C () (Bag Int)) +(declare-fun D () (Set Int)) +(declare-fun E () (Set Int)) +(declare-fun F () (Set Int)) + +(assert (and +(= (bag.union_max A B C) (bag.union_max (bag.union_max A B) C)) +(= (bag.union_disjoint A B C) (bag.union_disjoint (bag.union_disjoint A B) C)) +(= (bag.difference_subtract A B C) (bag.difference_subtract (bag.difference_subtract A B) C)) +(= (set.inter D E F) (set.inter (set.inter D E) F)) +(= (set.union D E F) (set.union (set.union D E) F)) +(= (set.minus D E F) (set.minus (set.minus D E) F)) +)) + +(check-sat) -- 2.30.2