[Unit Tests] Fix bags rewrite test (#7114)

PR #7103 did not quite fix the unit test: The types of the lambda and
the expected bags were still off. This fixes the unit test.

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index f2af950878fc6b7bf61638c9c9edc5e7ea505bb4..646bb28cf37d3a06cc227f699b3b2cf17de68439 100644 (file)
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -512,7 +512,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const
   if (n[1].isConst())
   {
     // (bag.map f emptybag) = emptybag
-    // (bag.map f (bag "a" 3) = (bag (f "a") 3)
+    // (bag.map f (bag "a" 3)) = (bag (f "a") 3)
     std::map<Node, Rational> elements = NormalForm::getBagElements(n[1]);
     std::map<Node, Rational> mappedElements;
     std::map<Node, Rational>::iterator it = elements.begin();

diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index a05d7643742ea99e53fadbc034e257c479bbb6a1..025d5aec7af48f0bb0194c9b9276f57a80ca60d2 100644 (file)
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -701,19 +701,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
       d_nodeManager->mkBagType(d_nodeManager->stringType());
   Node emptybagString = d_nodeManager->mkConst(EmptyBag(bagStringType));
 
-  Node one = d_nodeManager->mkConst(Rational(1));
-  Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
-  std::vector<Node> args;
-  args.push_back(x);
-  Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, args);
-  Node lambda = d_nodeManager->mkNode(LAMBDA, bound, one);
+  Node empty = d_nodeManager->mkConst(String(""));
+  Node xString = d_nodeManager->mkBoundVar("x", d_nodeManager->stringType());
+  Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, xString);
+  Node lambda = d_nodeManager->mkNode(LAMBDA, bound, empty);
 
   // (bag.map (lambda ((x U))  t) emptybag) = emptybag
   Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString);
   RewriteResponse response1 = d_rewriter->postRewrite(n1);
-  TypeNode bagIntType = d_nodeManager->mkBagType(d_nodeManager->integerType());
-  Node emptybagInteger = d_nodeManager->mkConst(EmptyBag(bagIntType));
-  ASSERT_TRUE(response1.d_node == emptybagInteger
+  ASSERT_TRUE(response1.d_node == emptybagString
               && response1.d_status == REWRITE_AGAIN_FULL);
 
   std::vector<Node> elements = getNStrings(2);
@@ -728,17 +724,14 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 
   ASSERT_TRUE(unionDisjointAB.isConst());
-  // - (bag.map (lambda ((x Int)) 1) (union_disjoint (bag "a" 3) (bag "b" 4))) =
-  //        (bag 1 7))
-  Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
 
-  std::cout << n2 << std::endl;
+  // (bag.map (lambda ((x Int)) "") (union_disjoint (bag "a" 3) (bag "b" 4))) =
+  //   (bag "" 7))
+  Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
 
   Node rewritten = Rewriter:: rewrite(n2);
-  std::cout << rewritten << std::endl;
-
-  Node bag = d_nodeManager->mkBag(d_nodeManager->integerType(),
-                                  one,               d_nodeManager->mkConst(Rational(7)));
+  Node bag = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), empty, d_nodeManager->mkConst(Rational(7)));
   ASSERT_TRUE(rewritten == bag);
 }