Add bag inferences for operators: intersection, duplicate_removal, and empty bags (#5832)

This PR adds inferences for operators: intersection, duplicate_removal, and empty bags during post check.
It also fixes a bug in SolverState::getElements

6 files changed, 50 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 94be987f7..128f9c567 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1430,6 +1430,11 @@ set(regress_1_tests
   regress1/bug800.smt2
   regress1/bags/difference_remove1.smt2
   regress1/bags/disequality.smt2
+  regress1/bags/duplicate_removal1.smt2
+  regress1/bags/duplicate_removal2.smt2
+  regress1/bags/emptybag1.smt2
+  regress1/bags/intersection_min1.smt2
+  regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2
new file mode 100644
index 000000000..2b662c6e5
--- /dev/null
+++ b/test/regress/regress1/bags/duplicate_removal1.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(declare-fun A () (Bag String))
+(declare-fun B () (Bag String))
+(assert (= B (duplicate_removal A)))
+(assert (distinct (as emptybag (Bag String)) A B))
+(check-sat)
diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2
new file mode 100644
index 000000000..7dacaae43
--- /dev/null
+++ b/test/regress/regress1/bags/duplicate_removal2.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun A () (Bag String))
+(declare-fun B () (Bag String))
+(assert (= B (duplicate_removal A)))
+(assert (distinct (as emptybag (Bag String)) A B))
+(assert (= B (union_max A B)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2
new file mode 100644
index 000000000..f7f92599d
--- /dev/null
+++ b/test/regress/regress1/bags/emptybag1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun A () (Bag String))
+(declare-fun x () String)
+(declare-fun y () Int)
+(assert (= x "x"))
+(assert (= A (as emptybag (Bag String))))
+(assert (= (bag.count x A) y))
+(assert(> y 1))
+(check-sat)
diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2
new file mode 100644
index 000000000..f5a515b9c
--- /dev/null
+++ b/test/regress/regress1/bags/intersection_min1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(declare-fun A () (Bag String))
+(declare-fun B () (Bag String))
+(declare-fun C () (Bag String))
+(assert (= C (intersection_min A B)))
+(assert (distinct (as emptybag (Bag String)) C))
+(assert (distinct A B C))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2
new file mode 100644
index 000000000..66afa2f3a
--- /dev/null
+++ b/test/regress/regress1/bags/intersection_min2.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun A () (Bag String))
+(declare-fun B () (Bag String))
+(declare-fun C () (Bag String))
+(assert (= C (intersection_min A B)))
+(assert (= C (union_disjoint A B)))
+(assert (distinct (as emptybag (Bag String)) C))
+(check-sat)