diff options
Diffstat (limited to 'src/theory/bags/bags_rewriter.cpp')
| -rw-r--r-- | src/theory/bags/bags_rewriter.cpp | 233 |
1 files changed, 118 insertions, 115 deletions
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 31c33b901..f9cc990f4 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -75,14 +75,16 @@ RewriteResponse BagsRewriter::postRewrite(TNode n) Kind k = n.getKind(); switch (k) { - case MK_BAG: response = rewriteMakeBag(n); break; + case BAG_MAKE: 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; - case DIFFERENCE_SUBTRACT: response = rewriteDifferenceSubtract(n); break; - case DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break; + case BAG_DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break; + case BAG_UNION_MAX: response = rewriteUnionMax(n); break; + case BAG_UNION_DISJOINT: response = rewriteUnionDisjoint(n); break; + case BAG_INTER_MIN: response = rewriteIntersectionMin(n); break; + case BAG_DIFFERENCE_SUBTRACT: + response = rewriteDifferenceSubtract(n); + break; + case BAG_DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break; case BAG_CARD: response = rewriteCard(n); break; case BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break; case BAG_FROM_SET: response = rewriteFromSet(n); break; @@ -113,7 +115,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n) switch (k) { case EQUAL: response = preRewriteEqual(n); break; - case SUBBAG: response = rewriteSubBag(n); break; + case BAG_SUBBAG: response = rewriteSubBag(n); break; default: response = BagsRewriteResponse(n, Rewrite::NONE); } @@ -144,24 +146,24 @@ BagsRewriteResponse BagsRewriter::preRewriteEqual(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const { - Assert(n.getKind() == SUBBAG); + Assert(n.getKind() == BAG_SUBBAG); - // (bag.is_included A B) = ((difference_subtract A B) == emptybag) + // (bag.subbag A B) = ((bag.difference_subtract A B) == bag.empty) Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType())); - Node subtract = d_nm->mkNode(DIFFERENCE_SUBTRACT, n[0], n[1]); + Node subtract = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, n[0], n[1]); Node equal = subtract.eqNode(emptybag); return BagsRewriteResponse(equal, Rewrite::SUB_BAG); } BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const { - Assert(n.getKind() == MK_BAG); - // return emptybag for negative or zero multiplicity + Assert(n.getKind() == BAG_MAKE); + // return bag.empty for negative or zero multiplicity if (n[1].isConst() && n[1].getConst<Rational>().sgn() != 1) { - // (mkBag x c) = emptybag where c <= 0 + // (bag x c) = bag.empty where c <= 0 Node emptybag = d_nm->mkConst(EmptyBag(n.getType())); - return BagsRewriteResponse(emptybag, Rewrite::MK_BAG_COUNT_NEGATIVE); + return BagsRewriteResponse(emptybag, Rewrite::BAG_MAKE_COUNT_NEGATIVE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -169,68 +171,68 @@ BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const { Assert(n.getKind() == BAG_COUNT); - if (n[1].isConst() && n[1].getKind() == EMPTYBAG) + if (n[1].isConst() && n[1].getKind() == BAG_EMPTY) { - // (bag.count x emptybag) = 0 + // (bag.count x bag.empty) = 0 return BagsRewriteResponse(d_zero, Rewrite::COUNT_EMPTY); } - if (n[1].getKind() == MK_BAG && n[0] == n[1][0]) + if (n[1].getKind() == BAG_MAKE && n[0] == n[1][0]) { - // (bag.count x (mkBag x c)) = (ite (>= c 1) c 0) + // (bag.count x (bag x c)) = (ite (>= c 1) c 0) Node c = n[1][1]; Node geq = d_nm->mkNode(GEQ, c, d_one); Node ite = d_nm->mkNode(ITE, geq, c, d_zero); - return BagsRewriteResponse(ite, Rewrite::COUNT_MK_BAG); + return BagsRewriteResponse(ite, Rewrite::COUNT_BAG_MAKE); } 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() + Assert(n.getKind() == BAG_DUPLICATE_REMOVAL); + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst<Rational>().sgn() == 1) { - // (duplicate_removal (mkBag x n)) = (mkBag x 1) + // (bag.duplicate_removal (bag x n)) = (bag x 1) // where n is a positive constant Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], d_one); - return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_MK_BAG); + return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const { - Assert(n.getKind() == UNION_MAX); - if (n[1].getKind() == EMPTYBAG || n[0] == n[1]) + Assert(n.getKind() == BAG_UNION_MAX); + if (n[1].getKind() == BAG_EMPTY || n[0] == n[1]) { - // (union_max A A) = A - // (union_max A emptybag) = A + // (bag.union_max A A) = A + // (bag.union_max A bag.empty) = A return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_SAME_OR_EMPTY); } - if (n[0].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY) { - // (union_max emptybag A) = A + // (bag.union_max bag.empty A) = A return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_EMPTY); } - if ((n[1].getKind() == UNION_MAX || n[1].getKind() == UNION_DISJOINT) + if ((n[1].getKind() == BAG_UNION_MAX || n[1].getKind() == BAG_UNION_DISJOINT) && (n[0] == n[1][0] || n[0] == n[1][1])) { - // (union_max A (union_max A B)) = (union_max A B) - // (union_max A (union_max B A)) = (union_max B A) - // (union_max A (union_disjoint A B)) = (union_disjoint A B) - // (union_max A (union_disjoint B A)) = (union_disjoint B A) + // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_UNION_LEFT); } - if ((n[0].getKind() == UNION_MAX || n[0].getKind() == UNION_DISJOINT) + if ((n[0].getKind() == BAG_UNION_MAX || n[0].getKind() == BAG_UNION_DISJOINT) && (n[0][0] == n[1] || n[0][1] == n[1])) { - // (union_max (union_max A B) A)) = (union_max A B) - // (union_max (union_max B A) A)) = (union_max B A) - // (union_max (union_disjoint A B) A)) = (union_disjoint A B) - // (union_max (union_disjoint B A) A)) = (union_disjoint B A) + // (bag.union_max (bag.union_max A B) A)) = (bag.union_max A B) + // (bag.union_max (bag.union_max B A) A)) = (bag.union_max B A) + // (bag.union_max (bag.union_disjoint A B) A)) = (bag.union_disjoint A B) + // (bag.union_max (bag.union_disjoint B A) A)) = (bag.union_disjoint B A) return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_UNION_RIGHT); } return BagsRewriteResponse(n, Rewrite::NONE); @@ -238,29 +240,30 @@ BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const { - Assert(n.getKind() == UNION_DISJOINT); - if (n[1].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_UNION_DISJOINT); + if (n[1].getKind() == BAG_EMPTY) { - // (union_disjoint A emptybag) = A + // (bag.union_disjoint A bag.empty) = A return BagsRewriteResponse(n[0], Rewrite::UNION_DISJOINT_EMPTY_RIGHT); } - if (n[0].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY) { - // (union_disjoint emptybag A) = A + // (bag.union_disjoint bag.empty A) = A return BagsRewriteResponse(n[1], Rewrite::UNION_DISJOINT_EMPTY_LEFT); } - if ((n[0].getKind() == UNION_MAX && n[1].getKind() == INTERSECTION_MIN) - || (n[1].getKind() == UNION_MAX && n[0].getKind() == INTERSECTION_MIN)) + if ((n[0].getKind() == BAG_UNION_MAX && n[1].getKind() == BAG_INTER_MIN) + || (n[1].getKind() == BAG_UNION_MAX && n[0].getKind() == BAG_INTER_MIN)) { - // (union_disjoint (union_max A B) (intersection_min A B)) = - // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) - // check if the operands of union_max and intersection_min are the same + // (bag.union_disjoint (bag.union_max A B) (bag.inter_min A B)) = + // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + // check if the operands of bag.union_max and bag.inter_min are the + // same std::set<Node> left(n[0].begin(), n[0].end()); std::set<Node> right(n[1].begin(), n[1].end()); if (left == right) { - Node rewritten = d_nm->mkNode(UNION_DISJOINT, n[0][0], n[0][1]); + Node rewritten = d_nm->mkNode(BAG_UNION_DISJOINT, n[0][0], n[0][1]); return BagsRewriteResponse(rewritten, Rewrite::UNION_DISJOINT_MAX_MIN); } } @@ -269,42 +272,42 @@ BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const { - Assert(n.getKind() == INTERSECTION_MIN); - if (n[0].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_INTER_MIN); + if (n[0].getKind() == BAG_EMPTY) { - // (intersection_min emptybag A) = emptybag + // (bag.inter_min bag.empty A) = bag.empty return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_EMPTY_LEFT); } - if (n[1].getKind() == EMPTYBAG) + if (n[1].getKind() == BAG_EMPTY) { - // (intersection_min A emptybag) = emptybag + // (bag.inter_min A bag.empty) = bag.empty return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_EMPTY_RIGHT); } if (n[0] == n[1]) { - // (intersection_min A A) = A + // (bag.inter_min A A) = A return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SAME); } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (intersection_min A (union_disjoint A B)) = A - // (intersection_min A (union_disjoint B A)) = A - // (intersection_min A (union_max A B)) = A - // (intersection_min A (union_max B A)) = A + // (bag.inter_min A (bag.union_disjoint A B)) = A + // (bag.inter_min A (bag.union_disjoint B A)) = A + // (bag.inter_min A (bag.union_max A B)) = A + // (bag.inter_min A (bag.union_max B A)) = A return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SHARED_LEFT); } } - if (n[0].getKind() == UNION_DISJOINT || n[0].getKind() == UNION_MAX) + if (n[0].getKind() == BAG_UNION_DISJOINT || n[0].getKind() == BAG_UNION_MAX) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (intersection_min (union_disjoint A B) A) = A - // (intersection_min (union_disjoint B A) A) = A - // (intersection_min (union_max A B) A) = A - // (intersection_min (union_max B A) A) = A + // (bag.inter_min (bag.union_disjoint A B) A) = A + // (bag.inter_min (bag.union_disjoint B A) A) = A + // (bag.inter_min (bag.union_max A B) A) = A + // (bag.inter_min (bag.union_max B A) A) = A return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_SHARED_RIGHT); } } @@ -315,55 +318,55 @@ BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract( const TNode& n) const { - Assert(n.getKind() == DIFFERENCE_SUBTRACT); - if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT); + if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY) { - // (difference_subtract A emptybag) = A - // (difference_subtract emptybag A) = emptybag + // (bag.difference_subtract A bag.empty) = A + // (bag.difference_subtract bag.empty A) = bag.empty return BagsRewriteResponse(n[0], Rewrite::SUBTRACT_RETURN_LEFT); } if (n[0] == n[1]) { - // (difference_subtract A A) = emptybag + // (bag.difference_subtract A A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_SAME); } - if (n[0].getKind() == UNION_DISJOINT) + if (n[0].getKind() == BAG_UNION_DISJOINT) { if (n[1] == n[0][0]) { - // (difference_subtract (union_disjoint A B) A) = B + // (bag.difference_subtract (bag.union_disjoint A B) A) = B return BagsRewriteResponse(n[0][1], Rewrite::SUBTRACT_DISJOINT_SHARED_LEFT); } if (n[1] == n[0][1]) { - // (difference_subtract (union_disjoint B A) A) = B + // (bag.difference_subtract (bag.union_disjoint B A) A) = B return BagsRewriteResponse(n[0][0], Rewrite::SUBTRACT_DISJOINT_SHARED_RIGHT); } } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (difference_subtract A (union_disjoint A B)) = emptybag - // (difference_subtract A (union_disjoint B A)) = emptybag - // (difference_subtract A (union_max A B)) = emptybag - // (difference_subtract A (union_max B A)) = emptybag + // (bag.difference_subtract A (bag.union_disjoint A B)) = bag.empty + // (bag.difference_subtract A (bag.union_disjoint B A)) = bag.empty + // (bag.difference_subtract A (bag.union_max A B)) = bag.empty + // (bag.difference_subtract A (bag.union_max B A)) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_FROM_UNION); } } - if (n[0].getKind() == INTERSECTION_MIN) + if (n[0].getKind() == BAG_INTER_MIN) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (difference_subtract (intersection_min A B) A) = emptybag - // (difference_subtract (intersection_min B A) A) = emptybag + // (bag.difference_subtract (bag.inter_min A B) A) = bag.empty + // (bag.difference_subtract (bag.inter_min B A) A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_MIN); } @@ -374,41 +377,41 @@ BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract( BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const { - Assert(n.getKind() == DIFFERENCE_REMOVE); + Assert(n.getKind() == BAG_DIFFERENCE_REMOVE); - if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY) { - // (difference_remove A emptybag) = A - // (difference_remove emptybag B) = emptybag + // (bag.difference_remove A bag.empty) = A + // (bag.difference_remove bag.empty B) = bag.empty return BagsRewriteResponse(n[0], Rewrite::REMOVE_RETURN_LEFT); } if (n[0] == n[1]) { - // (difference_remove A A) = emptybag + // (bag.difference_remove A A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_SAME); } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (difference_remove A (union_disjoint A B)) = emptybag - // (difference_remove A (union_disjoint B A)) = emptybag - // (difference_remove A (union_max A B)) = emptybag - // (difference_remove A (union_max B A)) = emptybag + // (bag.difference_remove A (bag.union_disjoint A B)) = bag.empty + // (bag.difference_remove A (bag.union_disjoint B A)) = bag.empty + // (bag.difference_remove A (bag.union_max A B)) = bag.empty + // (bag.difference_remove A (bag.union_max B A)) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_FROM_UNION); } } - if (n[0].getKind() == INTERSECTION_MIN) + if (n[0].getKind() == BAG_INTER_MIN) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (difference_remove (intersection_min A B) A) = emptybag - // (difference_remove (intersection_min B A) A) = emptybag + // (bag.difference_remove (bag.inter_min A B) A) = bag.empty + // (bag.difference_remove (bag.inter_min B A) A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_MIN); } @@ -420,11 +423,11 @@ BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const { Assert(n.getKind() == BAG_CHOOSE); - if (n[0].getKind() == MK_BAG && n[0][1].isConst() + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst<Rational>() > 0) { - // (bag.choose (mkBag x c)) = x where c is a constant > 0 - return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_MK_BAG); + // (bag.choose (bag x c)) = x where c is a constant > 0 + return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -432,15 +435,15 @@ BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const { Assert(n.getKind() == BAG_CARD); - if (n[0].getKind() == MK_BAG && n[0][1].isConst()) + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()) { - // (bag.card (mkBag x c)) = c where c is a constant > 0 - return BagsRewriteResponse(n[0][1], Rewrite::CARD_MK_BAG); + // (bag.card (bag x c)) = c where c is a constant > 0 + return BagsRewriteResponse(n[0][1], Rewrite::CARD_BAG_MAKE); } - if (n[0].getKind() == UNION_DISJOINT) + if (n[0].getKind() == BAG_UNION_DISJOINT) { - // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) + // (bag.card (bag.union-disjoint A B)) = (+ (bag.card A) (bag.card B)) Node A = d_nm->mkNode(BAG_CARD, n[0][0]); Node B = d_nm->mkNode(BAG_CARD, n[0][1]); Node plus = d_nm->mkNode(PLUS, A, B); @@ -453,11 +456,11 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const { Assert(n.getKind() == BAG_IS_SINGLETON); - if (n[0].getKind() == MK_BAG) + if (n[0].getKind() == BAG_MAKE) { - // (bag.is_singleton (mkBag x c)) = (c == 1) + // (bag.is_singleton (bag x c)) = (c == 1) Node equal = n[0][1].eqNode(d_one); - return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_MK_BAG); + return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -467,7 +470,7 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const Assert(n.getKind() == BAG_FROM_SET); if (n[0].getKind() == SET_SINGLETON) { - // (bag.from_set (set.singleton (singleton_op Int) x)) = (mkBag x 1) + // (bag.from_set (set.singleton (SetSingletonOp Int) x)) = (bag x 1) TypeNode type = n[0].getType().getSetElementType(); Node bag = d_nm->mkBag(type, n[0][0], d_one); return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); @@ -478,10 +481,10 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const { Assert(n.getKind() == BAG_TO_SET); - if (n[0].getKind() == MK_BAG && n[0][1].isConst() + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst<Rational>().sgn() == 1) { - // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // (bag.to_set (bag x n)) = (set.singleton (SetSingletonOp T) x) // where n is a positive constant and T is the type of the bag's elements Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]); return BagsRewriteResponse(set, Rewrite::TO_SINGLETON); @@ -518,7 +521,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const Assert(n.getKind() == kind::BAG_MAP); if (n[1].isConst()) { - // (bag.map f emptybag) = emptybag + // (bag.map f bag.empty) = bag.empty // (bag.map f (bag "a" 3)) = (bag (f "a") 3) std::map<Node, Rational> elements = NormalForm::getBagElements(n[1]); std::map<Node, Rational> mappedElements; @@ -536,19 +539,19 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const Kind k = n[1].getKind(); switch (k) { - case MK_BAG: + case BAG_MAKE: { 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]); - return BagsRewriteResponse(ret, Rewrite::MAP_MK_BAG); + return BagsRewriteResponse(ret, Rewrite::MAP_BAG_MAKE); } - case UNION_DISJOINT: + case BAG_UNION_DISJOINT: { Node a = d_nm->mkNode(BAG_MAP, n[1][0]); Node b = d_nm->mkNode(BAG_MAP, n[1][1]); - Node ret = d_nm->mkNode(UNION_DISJOINT, a, b); + Node ret = d_nm->mkNode(BAG_UNION_DISJOINT, a, b); return BagsRewriteResponse(ret, Rewrite::MAP_UNION_DISJOINT); } |