From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 18:09:14 +0000 (-0500)
Subject: Make sets and bags operators left-associative (#8584)
X-Git-Tag: cvc5-1.0.1~287
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f486408d66e125a3fc45446601cd088fa4d39cc;p=cvc5.git

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 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<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 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)