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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f4717158a5beabc5778927f47474fb09536f960e..9b34b07cd44d99b6565807063412318e2346a595 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -261,8 +261,9 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN},
     {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT},
     {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE},
-    {BAG_IS_INCLUDED, CVC4::Kind::BAG_IS_INCLUDED},
+    {SUBBAG, CVC4::Kind::SUBBAG},
     {BAG_COUNT, CVC4::Kind::BAG_COUNT},
+    {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL},
     {MK_BAG, CVC4::Kind::MK_BAG},
     {EMPTYBAG, CVC4::Kind::EMPTYBAG},
     {BAG_CARD, CVC4::Kind::BAG_CARD},
@@ -566,8 +567,9 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN},
         {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT},
         {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE},
-        {CVC4::Kind::BAG_IS_INCLUDED, BAG_IS_INCLUDED},
+        {CVC4::Kind::SUBBAG, SUBBAG},
         {CVC4::Kind::BAG_COUNT, BAG_COUNT},
+        {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL},
         {CVC4::Kind::MK_BAG, MK_BAG},
         {CVC4::Kind::EMPTYBAG, EMPTYBAG},
         {CVC4::Kind::BAG_CARD, BAG_CARD},

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index d6ee24f1ebb55ccc20eb3dec784f2f1d35c7efcf..0bd4117dc35ad44d1ae4c539c14e831c63b2e722 100644 (file)
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2030,14 +2030,15 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   DIFFERENCE_REMOVE,
   /**
-   * Bag is included (first multiplicities <= second multiplicities).
+   * Inclusion predicate for bags
+   * (multiplicities of the first bag <= multiplicities of the second bag).
    * Parameters: 2
-   *   -[1]..[2]: Terms of set sort
+   *   -[1]..[2]: Terms of bag sort
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  BAG_IS_INCLUDED,
+  SUBBAG,
   /**
    * Element multiplicity in a bag
    * Parameters: 2
@@ -2047,6 +2048,16 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   BAG_COUNT,
+  /**
+   * Eliminate duplicates in a given bag. The returned bag contains exactly the
+   * same elements in the given bag, but with multiplicity one.
+   * Parameters: 1
+   *   -[1]: a term of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DUPLICATE_REMOVAL,
   /**
    * The bag of the single element given as a parameter.
    * Parameters: 1

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a226f7cbfdb6102c9c1c0f76b5ca16acec33f107..81a4bd4a6fcbfcaf1c4a4c2fa3b7296b55d0d2d3 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -695,9 +695,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addOperator(api::INTERSECTION_MIN, "intersection_min");
     addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract");
     addOperator(api::DIFFERENCE_REMOVE, "difference_remove");
-    addOperator(api::BAG_IS_INCLUDED, "bag.is_included");
+    addOperator(api::SUBBAG, "bag.is_included");
     addOperator(api::BAG_COUNT, "bag.count");
-    addOperator(api::MK_BAG, "mkBag");
+    addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal");
+    addOperator(api::MK_BAG, "bag");
     addOperator(api::BAG_CARD, "bag.card");
     addOperator(api::BAG_CHOOSE, "bag.choose");
     addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton");

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 26c54d4ecf6c430328556cecbb1f66d08dd553f8..f0540e9b78aee91011051ca19379e9c002c8679a 100644 (file)
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -63,6 +63,7 @@ RewriteResponse BagsRewriter::postRewrite(TNode n)
     {
       case MK_BAG: response = rewriteMakeBag(n); break;
       case BAG_COUNT: response = rewriteBagCount(n); break;
+      case DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break;
       case UNION_MAX: response = rewriteUnionMax(n); break;
       case UNION_DISJOINT: response = rewriteUnionDisjoint(n); break;
       case INTERSECTION_MIN: response = rewriteIntersectionMin(n); break;
@@ -98,7 +99,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n)
   switch (k)
   {
     case EQUAL: response = rewriteEqual(n); break;
-    case BAG_IS_INCLUDED: response = rewriteIsIncluded(n); break;
+    case SUBBAG: response = rewriteSubBag(n); break;
     default: response = BagsRewriteResponse(n, Rewrite::NONE);
   }
 
@@ -127,9 +128,9 @@ BagsRewriteResponse BagsRewriter::rewriteEqual(const TNode& n) const
   return BagsRewriteResponse(n, Rewrite::NONE);
 }
 
-BagsRewriteResponse BagsRewriter::rewriteIsIncluded(const TNode& n) const
+BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const
 {
-  Assert(n.getKind() == BAG_IS_INCLUDED);
+  Assert(n.getKind() == SUBBAG);
 
   // (bag.is_included A B) = ((difference_subtract A B) == emptybag)
   Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType()));
@@ -168,6 +169,21 @@ BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const
   return BagsRewriteResponse(n, Rewrite::NONE);
 }
 
+BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const
+{
+  Assert(n.getKind() == DUPLICATE_REMOVAL);
+  if (n[0].getKind() == MK_BAG && n[0][1].isConst()
+      && n[0][1].getConst<Rational>().sgn() == 1)
+  {
+    // (duplicate_removal (mkBag x n)) = (mkBag x 1)
+    //  where n is a positive constant
+    Node one = NodeManager::currentNM()->mkConst(Rational(1));
+    Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], one);
+    return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_MK_BAG);
+  }
+  return BagsRewriteResponse(n, Rewrite::NONE);
+}
+
 BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const
 {
   Assert(n.getKind() == UNION_MAX);
@@ -453,8 +469,8 @@ BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const
   {
     // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
     // where n is a positive constant and T is the type of the bag's elements
-    Node bag = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
-    return BagsRewriteResponse(bag, Rewrite::TO_SINGLETON);
+    Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
+    return BagsRewriteResponse(set, Rewrite::TO_SINGLETON);
   }
   return BagsRewriteResponse(n, Rewrite::NONE);
 }

diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index d36a21ccfdab5d914362be21ed267d0e376740ba..8be6b948acde7dfea1fef4b41242e083ab68600f 100644 (file)
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
 #define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
 
-#include "theory/rewriter.h"
 #include "theory/bags/rewrites.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -50,7 +50,7 @@ class BagsRewriter : public TheoryRewriter
    */
   RewriteResponse postRewrite(TNode n) override;
   /**
-   * preRewrite nodes with kinds: EQUAL, BAG_IS_INCLUDED.
+   * preRewrite nodes with kinds: EQUAL, SUBBAG.
    * See the rewrite rules for these kinds below.
    */
   RewriteResponse preRewrite(TNode n) override;
@@ -66,7 +66,7 @@ class BagsRewriter : public TheoryRewriter
    * rewrites for n include:
    * - (bag.is_included A B) = ((difference_subtract A B) == emptybag)
    */
-  BagsRewriteResponse rewriteIsIncluded(const TNode& n) const;
+  BagsRewriteResponse rewriteSubBag(const TNode& n) const;
 
   /**
    * rewrites for n include:
@@ -76,6 +76,7 @@ class BagsRewriter : public TheoryRewriter
    * - otherwise = n
    */
   BagsRewriteResponse rewriteMakeBag(const TNode& n) const;
+
   /**
    * rewrites for n include:
    * - (bag.count x emptybag) = 0
@@ -84,6 +85,13 @@ class BagsRewriter : public TheoryRewriter
    */
   BagsRewriteResponse rewriteBagCount(const TNode& n) const;
 
+  /**
+   *  rewrites for n include:
+   *  - (duplicate_removal (mkBag x n)) = (mkBag x 1)
+   *     where n is a positive constant
+   */
+  BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const;
+
   /**
    * rewrites for n include:
    * - (union_max A emptybag) = A

diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index 86e89e0bd274b431e2b5a29b0ed5485d962f6cc0..f84b811e761eaeafefcf8eef09dbfe6b31d78487 100644 (file)
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -45,8 +45,9 @@ operator DIFFERENCE_SUBTRACT    2  "bag difference1 (subtracts multiplicities)"
 # {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)}
 operator DIFFERENCE_REMOVE 2  "bag difference remove (removes shared elements)"
 
-operator BAG_IS_INCLUDED   2  "inclusion predicate for bags (less than or equal multiplicities)"
+operator SUBBAG            2  "inclusion predicate for bags (less than or equal multiplicities)"
 operator BAG_COUNT         2  "multiplicity of an element in a bag"
+operator DUPLICATE_REMOVAL 1  "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"
 
 constant MK_BAG_OP \
        ::CVC4::MakeBagOp \
@@ -74,8 +75,9 @@ typerule UNION_DISJOINT      ::CVC4::theory::bags::BinaryOperatorTypeRule
 typerule INTERSECTION_MIN    ::CVC4::theory::bags::BinaryOperatorTypeRule
 typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule
 typerule DIFFERENCE_REMOVE   ::CVC4::theory::bags::BinaryOperatorTypeRule
-typerule BAG_IS_INCLUDED     ::CVC4::theory::bags::IsIncludedTypeRule
+typerule SUBBAG              ::CVC4::theory::bags::SubBagTypeRule
 typerule BAG_COUNT           ::CVC4::theory::bags::CountTypeRule
+typerule DUPLICATE_REMOVAL   ::CVC4::theory::bags::DuplicateRemovalTypeRule
 typerule MK_BAG_OP           "SimpleTypeRule<RBuiltinOperator>"
 typerule MK_BAG              ::CVC4::theory::bags::MkBagTypeRule
 typerule EMPTYBAG            ::CVC4::theory::bags::EmptyBagTypeRule

diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp
index 6a535afc25fd3a8e2f3984a79564a51b71cf95d2..b6082278372aab3938c50ea2922c2df972d179ae 100644 (file)
--- a/src/theory/bags/make_bag_op.cpp
+++ b/src/theory/bags/make_bag_op.cpp
@@ -12,10 +12,11 @@
  ** \brief a class for MK_BAG operator
  **/
 
+#include "make_bag_op.h"
+
 #include <iostream>
 
 #include "expr/type_node.h"
-#include "make_bag_op.h"
 
 namespace CVC4 {
 

diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index f2dea62d384538d4c83421091878b36f230603c7..081ed77aaf5e7c814b5184c24fc5295943e951ee 100644 (file)
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -94,6 +94,7 @@ Node NormalForm::evaluate(TNode n)
   {
     case MK_BAG: return evaluateMakeBag(n);
     case BAG_COUNT: return evaluateBagCount(n);
+    case DUPLICATE_REMOVAL: return evaluateDuplicateRemoval(n);
     case UNION_DISJOINT: return evaluateUnionDisjoint(n);
     case UNION_MAX: return evaluateUnionMax(n);
     case INTERSECTION_MIN: return evaluateIntersectionMin(n);
@@ -240,6 +241,30 @@ Node NormalForm::evaluateBagCount(TNode n)
   return nm->mkConst(Rational(0));
 }
 
+Node NormalForm::evaluateDuplicateRemoval(TNode n)
+{
+  Assert(n.getKind() == DUPLICATE_REMOVAL);
+
+  // 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)
+
+  std::map<Node, Rational> oldElements = getBagElements(n[0]);
+  // copy elements from the old bag
+  std::map<Node, Rational> newElements(oldElements);
+  Rational one = Rational(1);
+  std::map<Node, Rational>::iterator it;
+  for (it = newElements.begin(); it != newElements.end(); it++)
+  {
+    it->second = one;
+  }
+  Node bag = constructBagFromElements(n[0].getType(), newElements);
+  return bag;
+}
+
 Node NormalForm::evaluateUnionDisjoint(TNode n)
 {
   Assert(n.getKind() == UNION_DISJOINT);

diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
index ef0edefff5e75674593b2d04f034a5ed8f78ce06..5a7936fa3dc36a2845f41ebd4542cff9bd8b243a 100644 (file)
--- a/src/theory/bags/normal_form.h
+++ b/src/theory/bags/normal_form.h
@@ -114,6 +114,13 @@ class NormalForm
    */
   static Node evaluateBagCount(TNode n);
 
+  /**
+   * @param n has the form (duplicate_removal A) where A is a constant bag
+   * @return a constant bag constructed from the elements in A where each
+   * element has multiplicity one
+   */
+  static Node evaluateDuplicateRemoval(TNode n);
+
   /**
    * evaluates union disjoint node such that the returned node is a canonical
    * bag that has the form

diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp
index be3b3cc714c451eb2c317cd19f2e8a636092516d..d640bcdce49110eeea104041daf7f4b99391e630 100644 (file)
--- a/src/theory/bags/rewrites.cpp
+++ b/src/theory/bags/rewrites.cpp
@@ -31,6 +31,7 @@ const char* toString(Rewrite r)
     case Rewrite::CONSTANT_EVALUATION: return "CONSTANT_EVALUATION";
     case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY";
     case Rewrite::COUNT_MK_BAG: return "COUNT_MK_BAG";
+    case Rewrite::DUPLICATE_REMOVAL_MK_BAG: return "DUPLICATE_REMOVAL_MK_BAG";
     case Rewrite::FROM_SINGLETON: return "FROM_SINGLETON";
     case Rewrite::IDENTICAL_NODES: return "IDENTICAL_NODES";
     case Rewrite::INTERSECTION_EMPTY_LEFT: return "INTERSECTION_EMPTY_LEFT";

diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h
index dc1921e244fd055ff4f6e27ace18f76d850d1e01..36e30ca688467ccc2a43b078715e34f1f23e733d 100644 (file)
--- a/src/theory/bags/rewrites.h
+++ b/src/theory/bags/rewrites.h
@@ -36,6 +36,7 @@ enum class Rewrite : uint32_t
   CONSTANT_EVALUATION,
   COUNT_EMPTY,
   COUNT_MK_BAG,
+  DUPLICATE_REMOVAL_MK_BAG,
   FROM_SINGLETON,
   IDENTICAL_NODES,
   INTERSECTION_EMPTY_LEFT,

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 9dcad9bb13da16ace73f1bf42fefb95bc848f103..9f62ea1c62ffb5941adf42fbe2a6bc30c164fe95 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -63,6 +63,7 @@ void TheoryBags::finishInit()
   d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
   d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
   d_equalityEngine->addFunctionKind(BAG_COUNT);
+  d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
   d_equalityEngine->addFunctionKind(MK_BAG);
   d_equalityEngine->addFunctionKind(BAG_CARD);
   d_equalityEngine->addFunctionKind(BAG_FROM_SET);

diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 7767938edee5af85bf30f88f9ac88315e784782a..cece40c9ea0bb3641b3e4383b50ca70f74f84059 100644 (file)
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -61,18 +61,17 @@ struct BinaryOperatorTypeRule
   }
 }; /* struct BinaryOperatorTypeRule */
 
-struct IsIncludedTypeRule
+struct SubBagTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::BAG_IS_INCLUDED);
+    Assert(n.getKind() == kind::SUBBAG);
     TypeNode bagType = n[0].getType(check);
     if (check)
     {
       if (!bagType.isBag())
       {
-        throw TypeCheckingExceptionPrivate(
-            n, "BAG_IS_INCLUDED operating on non-bag");
+        throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
       }
       TypeNode secondBagType = n[1].getType(check);
       if (secondBagType != bagType)
@@ -80,13 +79,13 @@ struct IsIncludedTypeRule
         if (!bagType.isComparableTo(secondBagType))
         {
           throw TypeCheckingExceptionPrivate(
-              n, "BAG_IS_INCLUDED operating on bags of different types");
+              n, "SUBBAG operating on bags of different types");
         }
       }
     }
     return nodeManager->booleanType();
   }
-}; /* struct IsIncludedTypeRule */
+}; /* struct SubBagTypeRule */
 
 struct CountTypeRule
 {
@@ -118,6 +117,25 @@ struct CountTypeRule
   }
 }; /* struct CountTypeRule */
 
+struct DuplicateRemovalTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        std::stringstream ss;
+        ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return bagType;
+  }
+}; /* struct DuplicateRemovalTypeRule */
+
 struct MkBagTypeRule
 {
   static TypeNode computeType(NodeManager* nm, TNode n, bool check)

diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h
index 6f7d5bd8d76be204f2e412e1395d3bb53c80fbbe..4e19ba90e4fb47c674fbf1b67ad851cbdd851246 100644 (file)
--- 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 b1c75fdbd4f50e5f6ca5dc26c44a6971976e4594..f2cc09240f0ea89ec048b7b9f575ada5f05377c7 100644 (file)
--- 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 5622a30007b2c7c20178e544b20019d5eb5eeb23..e454dfa280011ee8ba2bee9fcbe24f8ada9b1204 100644 (file)
--- 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: