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

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 50ee85bf56c236f2be4b0e4f717690b34f29182c..5de54018cb81d4bcd7bb1906ceebb70f2de82015 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5051,7 +5051,10 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& 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 d674421987438e793f0ab195963136820bf0debf..99ca3b969c759e36fe9db6a96835e894132e37d5 100644 (file)
--- 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 (file)
index 0000000..21dc8f5
--- /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)