Fix soundess issue for bags with negative multiplicity (#7539)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
One error was with the rewrite rule (bag.count x (bag x c) = c which did not account for cases when c is negative.
This conflicts with fact that all multiplicities are non-negative.
Another error was that the difference_remove inference rule didn't consider the negative case for (count e B)

(= (count e (difference_remove A B)) (ite (=  (count e B) 0) (count e A) 0))) ; not enough
(= (count e (difference_remove A B)) (ite (<= (count e B) 0) (count e A) 0))) ; the right rule

4 files changed, 53 insertions, 13 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3f099cf67..5d1ff9b49 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1591,6 +1591,8 @@ set(regress_1_tests
   regress1/bags/fuzzy1.smt2
   regress1/bags/fuzzy2.smt2
   regress1/bags/fuzzy3.smt2
+  regress1/bags/fuzzy4.smt2
+  regress1/bags/fuzzy5.smt2
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2
new file mode 100644
index 000000000..b733a4862
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy4.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+ (not
+  (=
+   (= A (bag d (+ c (bag.count d (union_disjoint A A)))))
+   (= A (difference_remove (bag d c) A)))))
+(assert (= A (bag (tuple 0 0) 5)))
+(assert (= c (- 5)))
+(assert (= d (tuple 0 0)))
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2
new file mode 100644
index 000000000..2dea236a5
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy5.smt2
@@ -0,0 +1,21 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+
+(assert
+ (let ((c_plus_1 (+ c 1)))
+   (and
+    (not
+     (= (= A (bag (tuple 0 c) (+ c c)))
+        (= A (difference_remove (bag d c) A))))
+    (not
+     (= (= A (bag (tuple 0 1) c_plus_1))
+        (= A (bag (tuple c 1) c_plus_1)))))))
+
+;(assert (= A (bag (tuple 0 1) 2)))
+;(assert (= c 1))
+;(assert (= d (tuple 0 1)))
+(check-sat)
\ No newline at end of file
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index 025d5aec7..7250f581c 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -165,25 +165,29 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 
 TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 {
-  int n = 3;
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node three = d_nodeManager->mkConst(Rational(3));
   Node skolem =
       d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
-  Node bag = d_nodeManager->mkBag(
-      d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(n)));
 
   // (bag.count x emptybag) = 0
   Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag);
   RewriteResponse response1 = d_rewriter->postRewrite(n1);
   ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL
-              && response1.d_node == d_nodeManager->mkConst(Rational(0)));
+              && response1.d_node == zero);
 
-  // (bag.count x (mkBag x c) = c where c > 0 is a constant
+  // (bag.count x (mkBag x c) = (ite (>= c 1) c 0)
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three);
   Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag);
   RewriteResponse response2 = d_rewriter->postRewrite(n2);
+
+  Node geq = d_nodeManager->mkNode(GEQ, three, one);
+  Node ite = d_nodeManager->mkNode(ITE, geq, three, zero);
   ASSERT_TRUE(response2.d_status == REWRITE_AGAIN_FULL
-              && response2.d_node == d_nodeManager->mkConst(Rational(n)));
+              && response2.d_node == ite);
 }
 
 TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
@@ -715,12 +719,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   std::vector<Node> elements = getNStrings(2);
   Node a = d_nodeManager->mkConst(String("a"));
   Node b = d_nodeManager->mkConst(String("b"));
-  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
-                                a,
-                                d_nodeManager->mkConst(Rational(3)));
-  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
-                                b,
-                                d_nodeManager->mkConst(Rational(4)));
+  Node A = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), a, d_nodeManager->mkConst(Rational(3)));
+  Node B = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), b, d_nodeManager->mkConst(Rational(4)));
   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 
   ASSERT_TRUE(unionDisjointAB.isConst());
@@ -729,7 +731,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   //   (bag "" 7))
   Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
 
-  Node rewritten = Rewriter:: rewrite(n2);
+  Node rewritten = Rewriter::rewrite(n2);
   Node bag = d_nodeManager->mkBag(
       d_nodeManager->stringType(), empty, d_nodeManager->mkConst(Rational(7)));
   ASSERT_TRUE(rewritten == bag);