Add DUPICATE_REMOVAL operator to bags (#5336)

This PR adds duplicate removal operator to bags (also known as delta or squash).
Other changes:

print MK_BAG operator as "bag" in smt2 instead of "mkBag"
renamed BAG_IS_INCLUDED operator to SUBBAG.

3 files changed, 59 insertions, 8 deletions

diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h
index 6f7d5bd8d..4e19ba90e 100644
--- a/test/unit/theory/theory_bags_normal_form_white.h
+++ b/test/unit/theory/theory_bags_normal_form_white.h
@@ -136,6 +136,40 @@ class BagsNormalFormWhite : public CxxTest::TestSuite
     TS_ASSERT(output4 == NormalForm::evaluate(input4));
   }
 
+  void testDuplicateRemoval()
+  {
+    // Examples
+    // --------
+    //  - (duplicate_removal (emptybag String)) = (emptybag String)
+    //  - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1)
+    //  - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
+    //     (disjoint_union (mkBag "x" 1) (mkBag "y" 1)
+
+    Node emptybag =
+        d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType())));
+    Node input1 = d_nm->mkNode(DUPLICATE_REMOVAL, emptybag);
+    Node output1 = emptybag;
+    TS_ASSERT(output1 == NormalForm::evaluate(input1));
+
+    Node x = d_nm->mkConst(String("x"));
+    Node y = d_nm->mkConst(String("y"));
+
+    Node x_1 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1)));
+    Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1)));
+
+    Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4)));
+    Node y_5 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(5)));
+
+    Node input2 = d_nm->mkNode(DUPLICATE_REMOVAL, x_4);
+    Node output2 = x_1;
+    TS_ASSERT(output2 == NormalForm::evaluate(input2));
+
+    Node normalBag = d_nm->mkNode(UNION_DISJOINT, x_4, y_5);
+    Node input3 = d_nm->mkNode(DUPLICATE_REMOVAL, normalBag);
+    Node output3 = d_nm->mkNode(UNION_DISJOINT, x_1, y_1);
+    TS_ASSERT(output3 == NormalForm::evaluate(input3));
+  }
+
   void testUnionMax()
   {
     // Example
diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h
index b1c75fdbd..f2cc09240 100644
--- a/test/unit/theory/theory_bags_rewriter_white.h
+++ b/test/unit/theory/theory_bags_rewriter_white.h
@@ -161,6 +161,20 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
               && response2.d_node == d_nm->mkConst(Rational(n)));
   }
 
+  void testDuplicateRemoval()
+  {
+    Node x = d_nm->mkSkolem("x", d_nm->stringType());
+    Node bag = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(5)));
+
+    // (duplicate_removal (mkBag x n)) = (mkBag x 1)
+    Node n = d_nm->mkNode(DUPLICATE_REMOVAL, bag);
+    RewriteResponse response = d_rewriter->postRewrite(n);
+    Node noDuplicate =
+        d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1)));
+    TS_ASSERT(response.d_node == noDuplicate
+              && response.d_status == REWRITE_AGAIN_FULL);
+  }
+
   void testUnionMax()
   {
     int n = 3;
diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h
index 5622a3000..e454dfa28 100644
--- a/test/unit/theory/theory_bags_type_rules_white.h
+++ b/test/unit/theory/theory_bags_type_rules_white.h
@@ -74,6 +74,15 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
                      TypeCheckingExceptionPrivate&);
   }
 
+  void testDuplicateRemovalOperator()
+  {
+    vector<Node> elements = getNStrings(1);
+    Node bag = d_nm->mkBag(
+        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
+    TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(DUPLICATE_REMOVAL, bag));
+    TS_ASSERT(d_nm->mkNode(DUPLICATE_REMOVAL, bag).getType() == bag.getType());
+  }
+
   void testMkBagOperator()
   {
     vector<Node> elements = getNStrings(1);
@@ -101,16 +110,10 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
   void testToSetOperator()
   {
     vector<Node> elements = getNStrings(1);
-    Node bag = d_nm->mkBag(d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
+    Node bag = d_nm->mkBag(
+        d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10)));
     TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_TO_SET, bag));
     TS_ASSERT(d_nm->mkNode(BAG_TO_SET, bag).getType().isSet());
-    std::cout<<"Rational(4, 4).isIntegral() " << d_nm->mkConst(Rational(4,4)).getType()<<  std::endl;
-    std::cout<<"Rational(8, 4).isIntegral() " << d_nm->mkConst(Rational(8,4)).getType()<<  std::endl;
-    std::cout<<"Rational(1, 4).isIntegral() " << d_nm->mkConst(Rational(1,4)).getType()<<  std::endl;
-
-    std::cout<<"Rational(4, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(4,4))).getType()<<  std::endl;
-    std::cout<<"Rational(8, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(8,4))).getType()<<  std::endl;
-    std::cout<<"Rational(1, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(1,4))).getType()<<  std::endl;
   }
 
  private: