diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-11-13 13:33:34 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-13 19:33:34 +0000 |
| commit | 805205a2047eeae7842b1c534859b52fa204ee0e (patch) | |
| tree | 1e0d581e451cbc92136b1072df1e500f44422d0e /src/theory/bags | |
| parent | 2b2f26191762856810cfe8391a35765eb26f45fb (diff) | |
Fix type error for rewriting bag.map bag.union_disjoint (#7640)
Fix type error for rewriting bag.map bag.union_disjoint
Diffstat (limited to 'src/theory/bags')
| -rw-r--r-- | src/theory/bags/bags_rewriter.cpp | 9 | ||||
| -rw-r--r-- | src/theory/bags/bags_rewriter.h | 13 |
2 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index f9cc990f4..7093d52fc 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -521,7 +521,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const Assert(n.getKind() == kind::BAG_MAP); if (n[1].isConst()) { - // (bag.map f bag.empty) = bag.empty + // (bag.map f (as bag.empty (Bag T1)) = (as bag.empty (Bag T2)) // (bag.map f (bag "a" 3)) = (bag (f "a") 3) std::map<Node, Rational> elements = NormalForm::getBagElements(n[1]); std::map<Node, Rational> mappedElements; @@ -541,6 +541,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const { case BAG_MAKE: { + // (bag.map f (bag x y)) = (bag (apply f x) y) Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]); Node ret = d_nm->mkBag(n[0].getType().getRangeType(), mappedElement, n[1][1]); @@ -549,8 +550,10 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const case BAG_UNION_DISJOINT: { - Node a = d_nm->mkNode(BAG_MAP, n[1][0]); - Node b = d_nm->mkNode(BAG_MAP, n[1][1]); + // (bag.map f (bag.union_disjoint A B)) = + // (bag.union_disjoint (bag.map f A) (bag.map f B)) + Node a = d_nm->mkNode(BAG_MAP, n[0], n[1][0]); + Node b = d_nm->mkNode(BAG_MAP, n[0], n[1][1]); Node ret = d_nm->mkNode(BAG_UNION_DISJOINT, a, b); return BagsRewriteResponse(ret, Rewrite::MAP_UNION_DISJOINT); } diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 36958a491..a938b3bd4 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -214,14 +214,11 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.map (lambda ((x U)) t) bag.empty) = bag.empty - * - (bag.map (lambda ((x U)) t) (bag y z)) = (bag (apply (lambda ((x U)) t) - * y) z) - * - (bag.map (lambda ((x U)) t) (bag.union_disjoint A B)) = - * (bag.union_disjoint - * (bag ((lambda ((x U)) t) "a") 3) - * (bag ((lambda ((x U)) t) "b") 4)) - * + * - (bag.map f (as bag.empty (Bag T1)) = (as bag.empty (Bag T2)) + * - (bag.map f (bag x y)) = (bag (apply f x) y) + * - (bag.map f (bag.union_disjoint A B)) = + * (bag.union_disjoint (bag.map f A) (bag.map f B)) + * where f: T1 -> T2 */ BagsRewriteResponse postRewriteMap(const TNode& n) const; |