From b11a6d57ded753885e272ce69612ff15a591c592 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 1 Sep 2021 21:14:56 -0700 Subject: [PATCH] [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. --- src/theory/bags/bags_rewriter.cpp | 2 +- .../theory/theory_bags_rewriter_white.cpp | 27 +++++++------------ 2 files changed, 11 insertions(+), 18 deletions(-) diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index f2af95087..646bb28cf 100644 --- 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 elements = NormalForm::getBagElements(n[1]); std::map mappedElements; std::map::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 a05d76437..025d5aec7 100644 --- 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 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 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); } -- 2.30.2