src/theory/bags/bags_rewriter.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed, Gereon Kremer, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Bags theory rewriter.
  14  */
  15
  16 #include "theory/bags/bags_rewriter.h"
  17
  18 #include "expr/emptybag.h"
  19 #include "theory/bags/normal_form.h"
  20 #include "util/rational.h"
  21 #include "util/statistics_registry.h"
  22
  23 using namespace cvc5::kind;
  24
  25 namespace cvc5 {
  26 namespace theory {
  27 namespace bags {
  28
  29 BagsRewriteResponse::BagsRewriteResponse()
  30     : d_node(Node::null()), d_rewrite(Rewrite::NONE)
  31 {
  32 }
  33
  34 BagsRewriteResponse::BagsRewriteResponse(Node n, Rewrite rewrite)
  35     : d_node(n), d_rewrite(rewrite)
  36 {
  37 }
  38
  39 BagsRewriteResponse::BagsRewriteResponse(const BagsRewriteResponse& r)
  40     : d_node(r.d_node), d_rewrite(r.d_rewrite)
  41 {
  42 }
  43
  44 BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics)
  45     : d_statistics(statistics)
  46 {
  47   d_nm = NodeManager::currentNM();
  48   d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
  49   d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
  50 }
  51
  52 RewriteResponse BagsRewriter::postRewrite(TNode n)
  53 {
  54   BagsRewriteResponse response;
  55   if (n.isConst())
  56   {
  57     // no need to rewrite n if it is already in a normal form
  58     response = BagsRewriteResponse(n, Rewrite::NONE);
  59   }
  60   else if (n.getKind() == EQUAL)
  61   {
  62     response = postRewriteEqual(n);
  63   }
  64   else if (n.getKind() == BAG_CHOOSE)
  65   {
  66     response = rewriteChoose(n);
  67   }
  68   else if (NormalForm::areChildrenConstants(n))
  69   {
  70     Node value = NormalForm::evaluate(n);
  71     response = BagsRewriteResponse(value, Rewrite::CONSTANT_EVALUATION);
  72   }
  73   else
  74   {
  75     Kind k = n.getKind();
  76     switch (k)
  77     {
  78       case BAG_MAKE: response = rewriteMakeBag(n); break;
  79       case BAG_COUNT: response = rewriteBagCount(n); break;
  80       case BAG_DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break;
  81       case BAG_UNION_MAX: response = rewriteUnionMax(n); break;
  82       case BAG_UNION_DISJOINT: response = rewriteUnionDisjoint(n); break;
  83       case BAG_INTER_MIN: response = rewriteIntersectionMin(n); break;
  84       case BAG_DIFFERENCE_SUBTRACT:
  85         response = rewriteDifferenceSubtract(n);
  86         break;
  87       case BAG_DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break;
  88       case BAG_CARD: response = rewriteCard(n); break;
  89       case BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break;
  90       case BAG_FROM_SET: response = rewriteFromSet(n); break;
  91       case BAG_TO_SET: response = rewriteToSet(n); break;
  92       case BAG_MAP: response = postRewriteMap(n); break;
  93       default: response = BagsRewriteResponse(n, Rewrite::NONE); break;
  94     }
  95   }
  96
  97   Trace("bags-rewrite") << "postRewrite " << n << " to " << response.d_node
  98                         << " by " << response.d_rewrite << "." << std::endl;
  99
 100   if (d_statistics != nullptr)
 101   {
 102     (*d_statistics) << response.d_rewrite;
 103   }
 104   if (response.d_node != n)
 105   {
 106     return RewriteResponse(RewriteStatus::REWRITE_AGAIN_FULL, response.d_node);
 107   }
 108   return RewriteResponse(RewriteStatus::REWRITE_DONE, n);
 109 }
 110
 111 RewriteResponse BagsRewriter::preRewrite(TNode n)
 112 {
 113   BagsRewriteResponse response;
 114   Kind k = n.getKind();
 115   switch (k)
 116   {
 117     case EQUAL: response = preRewriteEqual(n); break;
 118     case BAG_SUBBAG: response = rewriteSubBag(n); break;
 119     default: response = BagsRewriteResponse(n, Rewrite::NONE);
 120   }
 121
 122   Trace("bags-rewrite") << "preRewrite " << n << " to " << response.d_node
 123                         << " by " << response.d_rewrite << "." << std::endl;
 124
 125   if (d_statistics != nullptr)
 126   {
 127     (*d_statistics) << response.d_rewrite;
 128   }
 129   if (response.d_node != n)
 130   {
 131     return RewriteResponse(RewriteStatus::REWRITE_AGAIN_FULL, response.d_node);
 132   }
 133   return RewriteResponse(RewriteStatus::REWRITE_DONE, n);
 134 }
 135
 136 BagsRewriteResponse BagsRewriter::preRewriteEqual(const TNode& n) const
 137 {
 138   Assert(n.getKind() == EQUAL);
 139   if (n[0] == n[1])
 140   {
 141     // (= A A) = true where A is a bag
 142     return BagsRewriteResponse(d_nm->mkConst(true), Rewrite::IDENTICAL_NODES);
 143   }
 144   return BagsRewriteResponse(n, Rewrite::NONE);
 145 }
 146
 147 BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const
 148 {
 149   Assert(n.getKind() == BAG_SUBBAG);
 150
 151   // (bag.subbag A B) = ((bag.difference_subtract A B) == bag.empty)
 152   Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType()));
 153   Node subtract = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, n[0], n[1]);
 154   Node equal = subtract.eqNode(emptybag);
 155   return BagsRewriteResponse(equal, Rewrite::SUB_BAG);
 156 }
 157
 158 BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const
 159 {
 160   Assert(n.getKind() == BAG_MAKE);
 161   // return bag.empty for negative or zero multiplicity
 162   if (n[1].isConst() && n[1].getConst<Rational>().sgn() != 1)
 163   {
 164     // (bag x c) = bag.empty where c <= 0
 165     Node emptybag = d_nm->mkConst(EmptyBag(n.getType()));
 166     return BagsRewriteResponse(emptybag, Rewrite::BAG_MAKE_COUNT_NEGATIVE);
 167   }
 168   return BagsRewriteResponse(n, Rewrite::NONE);
 169 }
 170
 171 BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const
 172 {
 173   Assert(n.getKind() == BAG_COUNT);
 174   if (n[1].isConst() && n[1].getKind() == BAG_EMPTY)
 175   {
 176     // (bag.count x bag.empty) = 0
 177     return BagsRewriteResponse(d_zero, Rewrite::COUNT_EMPTY);
 178   }
 179   if (n[1].getKind() == BAG_MAKE && n[0] == n[1][0])
 180   {
 181     // (bag.count x (bag x c)) = (ite (>= c 1) c 0)
 182     Node c = n[1][1];
 183     Node geq = d_nm->mkNode(GEQ, c, d_one);
 184     Node ite = d_nm->mkNode(ITE, geq, c, d_zero);
 185     return BagsRewriteResponse(ite, Rewrite::COUNT_BAG_MAKE);
 186   }
 187   return BagsRewriteResponse(n, Rewrite::NONE);
 188 }
 189
 190 BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const
 191 {
 192   Assert(n.getKind() == BAG_DUPLICATE_REMOVAL);
 193   if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()
 194       && n[0][1].getConst<Rational>().sgn() == 1)
 195   {
 196     // (bag.duplicate_removal (bag x n)) = (bag x 1)
 197     //  where n is a positive constant
 198     Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], d_one);
 199     return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE);
 200   }
 201   return BagsRewriteResponse(n, Rewrite::NONE);
 202 }
 203
 204 BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const
 205 {
 206   Assert(n.getKind() == BAG_UNION_MAX);
 207   if (n[1].getKind() == BAG_EMPTY || n[0] == n[1])
 208   {
 209     // (bag.union_max A A) = A
 210     // (bag.union_max A bag.empty) = A
 211     return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_SAME_OR_EMPTY);
 212   }
 213   if (n[0].getKind() == BAG_EMPTY)
 214   {
 215     // (bag.union_max bag.empty A) = A
 216     return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_EMPTY);
 217   }
 218
 219   if ((n[1].getKind() == BAG_UNION_MAX || n[1].getKind() == BAG_UNION_DISJOINT)
 220       && (n[0] == n[1][0] || n[0] == n[1][1]))
 221   {
 222     // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B)
 223     // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A)
 224     // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B)
 225     // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A)
 226     return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_UNION_LEFT);
 227   }
 228
 229   if ((n[0].getKind() == BAG_UNION_MAX || n[0].getKind() == BAG_UNION_DISJOINT)
 230       && (n[0][0] == n[1] || n[0][1] == n[1]))
 231   {
 232     // (bag.union_max (bag.union_max A B) A)) = (bag.union_max A B)
 233     // (bag.union_max (bag.union_max B A) A)) = (bag.union_max B A)
 234     // (bag.union_max (bag.union_disjoint A B) A)) = (bag.union_disjoint A B)
 235     // (bag.union_max (bag.union_disjoint B A) A)) = (bag.union_disjoint B A)
 236     return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_UNION_RIGHT);
 237   }
 238   return BagsRewriteResponse(n, Rewrite::NONE);
 239 }
 240
 241 BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const
 242 {
 243   Assert(n.getKind() == BAG_UNION_DISJOINT);
 244   if (n[1].getKind() == BAG_EMPTY)
 245   {
 246     // (bag.union_disjoint A bag.empty) = A
 247     return BagsRewriteResponse(n[0], Rewrite::UNION_DISJOINT_EMPTY_RIGHT);
 248   }
 249   if (n[0].getKind() == BAG_EMPTY)
 250   {
 251     // (bag.union_disjoint bag.empty A) = A
 252     return BagsRewriteResponse(n[1], Rewrite::UNION_DISJOINT_EMPTY_LEFT);
 253   }
 254   if ((n[0].getKind() == BAG_UNION_MAX && n[1].getKind() == BAG_INTER_MIN)
 255       || (n[1].getKind() == BAG_UNION_MAX && n[0].getKind() == BAG_INTER_MIN))
 256
 257   {
 258     // (bag.union_disjoint (bag.union_max A B) (bag.inter_min A B)) =
 259     //         (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
 260     // check if the operands of bag.union_max and bag.inter_min are the
 261     // same
 262     std::set<Node> left(n[0].begin(), n[0].end());
 263     std::set<Node> right(n[1].begin(), n[1].end());
 264     if (left == right)
 265     {
 266       Node rewritten = d_nm->mkNode(BAG_UNION_DISJOINT, n[0][0], n[0][1]);
 267       return BagsRewriteResponse(rewritten, Rewrite::UNION_DISJOINT_MAX_MIN);
 268     }
 269   }
 270   return BagsRewriteResponse(n, Rewrite::NONE);
 271 }
 272
 273 BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const
 274 {
 275   Assert(n.getKind() == BAG_INTER_MIN);
 276   if (n[0].getKind() == BAG_EMPTY)
 277   {
 278     // (bag.inter_min bag.empty A) = bag.empty
 279     return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_EMPTY_LEFT);
 280   }
 281   if (n[1].getKind() == BAG_EMPTY)
 282   {
 283     // (bag.inter_min A bag.empty) = bag.empty
 284     return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_EMPTY_RIGHT);
 285   }
 286   if (n[0] == n[1])
 287   {
 288     // (bag.inter_min A A) = A
 289     return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SAME);
 290   }
 291   if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX)
 292   {
 293     if (n[0] == n[1][0] || n[0] == n[1][1])
 294     {
 295       // (bag.inter_min A (bag.union_disjoint A B)) = A
 296       // (bag.inter_min A (bag.union_disjoint B A)) = A
 297       // (bag.inter_min A (bag.union_max A B)) = A
 298       // (bag.inter_min A (bag.union_max B A)) = A
 299       return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SHARED_LEFT);
 300     }
 301   }
 302
 303   if (n[0].getKind() == BAG_UNION_DISJOINT || n[0].getKind() == BAG_UNION_MAX)
 304   {
 305     if (n[1] == n[0][0] || n[1] == n[0][1])
 306     {
 307       // (bag.inter_min (bag.union_disjoint A B) A) = A
 308       // (bag.inter_min (bag.union_disjoint B A) A) = A
 309       // (bag.inter_min (bag.union_max A B) A) = A
 310       // (bag.inter_min (bag.union_max B A) A) = A
 311       return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_SHARED_RIGHT);
 312     }
 313   }
 314
 315   return BagsRewriteResponse(n, Rewrite::NONE);
 316 }
 317
 318 BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract(
 319     const TNode& n) const
 320 {
 321   Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT);
 322   if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY)
 323   {
 324     // (bag.difference_subtract A bag.empty) = A
 325     // (bag.difference_subtract bag.empty A) = bag.empty
 326     return BagsRewriteResponse(n[0], Rewrite::SUBTRACT_RETURN_LEFT);
 327   }
 328   if (n[0] == n[1])
 329   {
 330     // (bag.difference_subtract A A) = bag.empty
 331     Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 332     return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_SAME);
 333   }
 334
 335   if (n[0].getKind() == BAG_UNION_DISJOINT)
 336   {
 337     if (n[1] == n[0][0])
 338     {
 339       // (bag.difference_subtract (bag.union_disjoint A B) A) = B
 340       return BagsRewriteResponse(n[0][1],
 341                                  Rewrite::SUBTRACT_DISJOINT_SHARED_LEFT);
 342     }
 343     if (n[1] == n[0][1])
 344     {
 345       // (bag.difference_subtract (bag.union_disjoint B A) A) = B
 346       return BagsRewriteResponse(n[0][0],
 347                                  Rewrite::SUBTRACT_DISJOINT_SHARED_RIGHT);
 348     }
 349   }
 350
 351   if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX)
 352   {
 353     if (n[0] == n[1][0] || n[0] == n[1][1])
 354     {
 355       // (bag.difference_subtract A (bag.union_disjoint A B)) = bag.empty
 356       // (bag.difference_subtract A (bag.union_disjoint B A)) = bag.empty
 357       // (bag.difference_subtract A (bag.union_max A B)) = bag.empty
 358       // (bag.difference_subtract A (bag.union_max B A)) = bag.empty
 359       Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 360       return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_FROM_UNION);
 361     }
 362   }
 363
 364   if (n[0].getKind() == BAG_INTER_MIN)
 365   {
 366     if (n[1] == n[0][0] || n[1] == n[0][1])
 367     {
 368       // (bag.difference_subtract (bag.inter_min A B) A) = bag.empty
 369       // (bag.difference_subtract (bag.inter_min B A) A) = bag.empty
 370       Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 371       return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_MIN);
 372     }
 373   }
 374
 375   return BagsRewriteResponse(n, Rewrite::NONE);
 376 }
 377
 378 BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const
 379 {
 380   Assert(n.getKind() == BAG_DIFFERENCE_REMOVE);
 381
 382   if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY)
 383   {
 384     // (bag.difference_remove A bag.empty) = A
 385     // (bag.difference_remove bag.empty B) = bag.empty
 386     return BagsRewriteResponse(n[0], Rewrite::REMOVE_RETURN_LEFT);
 387   }
 388
 389   if (n[0] == n[1])
 390   {
 391     // (bag.difference_remove A A) = bag.empty
 392     Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 393     return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_SAME);
 394   }
 395
 396   if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX)
 397   {
 398     if (n[0] == n[1][0] || n[0] == n[1][1])
 399     {
 400       // (bag.difference_remove A (bag.union_disjoint A B)) = bag.empty
 401       // (bag.difference_remove A (bag.union_disjoint B A)) = bag.empty
 402       // (bag.difference_remove A (bag.union_max A B)) = bag.empty
 403       // (bag.difference_remove A (bag.union_max B A)) = bag.empty
 404       Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 405       return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_FROM_UNION);
 406     }
 407   }
 408
 409   if (n[0].getKind() == BAG_INTER_MIN)
 410   {
 411     if (n[1] == n[0][0] || n[1] == n[0][1])
 412     {
 413       // (bag.difference_remove (bag.inter_min A B) A) = bag.empty
 414       // (bag.difference_remove (bag.inter_min B A) A) = bag.empty
 415       Node emptyBag = d_nm->mkConst(EmptyBag(n.getType()));
 416       return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_MIN);
 417     }
 418   }
 419
 420   return BagsRewriteResponse(n, Rewrite::NONE);
 421 }
 422
 423 BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const
 424 {
 425   Assert(n.getKind() == BAG_CHOOSE);
 426   if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()
 427       && n[0][1].getConst<Rational>() > 0)
 428   {
 429     // (bag.choose (bag x c)) = x where c is a constant > 0
 430     return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_BAG_MAKE);
 431   }
 432   return BagsRewriteResponse(n, Rewrite::NONE);
 433 }
 434
 435 BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const
 436 {
 437   Assert(n.getKind() == BAG_CARD);
 438   if (n[0].getKind() == BAG_MAKE && n[0][1].isConst())
 439   {
 440     // (bag.card (bag x c)) = c where c is a constant > 0
 441     return BagsRewriteResponse(n[0][1], Rewrite::CARD_BAG_MAKE);
 442   }
 443
 444   if (n[0].getKind() == BAG_UNION_DISJOINT)
 445   {
 446     // (bag.card (bag.union-disjoint A B)) = (+ (bag.card A) (bag.card B))
 447     Node A = d_nm->mkNode(BAG_CARD, n[0][0]);
 448     Node B = d_nm->mkNode(BAG_CARD, n[0][1]);
 449     Node plus = d_nm->mkNode(PLUS, A, B);
 450     return BagsRewriteResponse(plus, Rewrite::CARD_DISJOINT);
 451   }
 452   return BagsRewriteResponse(n, Rewrite::NONE);
 453 }
 454
 455 BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const
 456 {
 457   Assert(n.getKind() == BAG_IS_SINGLETON);
 458   if (n[0].getKind() == BAG_MAKE)
 459   {
 460     // (bag.is_singleton (bag x c)) = (c == 1)
 461     Node equal = n[0][1].eqNode(d_one);
 462     return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_BAG_MAKE);
 463   }
 464   return BagsRewriteResponse(n, Rewrite::NONE);
 465 }
 466
 467 BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const
 468 {
 469   Assert(n.getKind() == BAG_FROM_SET);
 470   if (n[0].getKind() == SET_SINGLETON)
 471   {
 472     // (bag.from_set (set.singleton (SetSingletonOp Int) x)) = (bag x 1)
 473     TypeNode type = n[0].getType().getSetElementType();
 474     Node bag = d_nm->mkBag(type, n[0][0], d_one);
 475     return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON);
 476   }
 477   return BagsRewriteResponse(n, Rewrite::NONE);
 478 }
 479
 480 BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const
 481 {
 482   Assert(n.getKind() == BAG_TO_SET);
 483   if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()
 484       && n[0][1].getConst<Rational>().sgn() == 1)
 485   {
 486     // (bag.to_set (bag x n)) = (set.singleton (SetSingletonOp T) x)
 487     // where n is a positive constant and T is the type of the bag's elements
 488     Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
 489     return BagsRewriteResponse(set, Rewrite::TO_SINGLETON);
 490   }
 491   return BagsRewriteResponse(n, Rewrite::NONE);
 492 }
 493
 494 BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const
 495 {
 496   Assert(n.getKind() == kind::EQUAL);
 497   if (n[0] == n[1])
 498   {
 499     Node ret = d_nm->mkConst(true);
 500     return BagsRewriteResponse(ret, Rewrite::EQ_REFL);
 501   }
 502
 503   if (n[0].isConst() && n[1].isConst())
 504   {
 505     Node ret = d_nm->mkConst(false);
 506     return BagsRewriteResponse(ret, Rewrite::EQ_CONST_FALSE);
 507   }
 508
 509   // standard ordering
 510   if (n[0] > n[1])
 511   {
 512     Node ret = d_nm->mkNode(kind::EQUAL, n[1], n[0]);
 513     return BagsRewriteResponse(ret, Rewrite::EQ_SYM);
 514   }
 515   return BagsRewriteResponse(n, Rewrite::NONE);
 516 }
 517
 518 BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const
 519 {
 520   Assert(n.getKind() == kind::BAG_MAP);
 521   if (n[1].isConst())
 522   {
 523     // (bag.map f (as bag.empty (Bag T1)) = (as bag.empty (Bag T2))
 524     // (bag.map f (bag "a" 3)) = (bag (f "a") 3)
 525     std::map<Node, Rational> elements = NormalForm::getBagElements(n[1]);
 526     std::map<Node, Rational> mappedElements;
 527     std::map<Node, Rational>::iterator it = elements.begin();
 528     while (it != elements.end())
 529     {
 530       Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], it->first);
 531       mappedElements[mappedElement] = it->second;
 532       ++it;
 533     }
 534     TypeNode t = d_nm->mkBagType(n[0].getType().getRangeType());
 535     Node ret = NormalForm::constructConstantBagFromElements(t, mappedElements);
 536     return BagsRewriteResponse(ret, Rewrite::MAP_CONST);
 537   }
 538   Kind k = n[1].getKind();
 539   switch (k)
 540   {
 541     case BAG_MAKE:
 542     {
 543       // (bag.map f (bag x y)) = (bag (apply f x) y)
 544       Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]);
 545       Node ret =
 546           d_nm->mkBag(n[0].getType().getRangeType(), mappedElement, n[1][1]);
 547       return BagsRewriteResponse(ret, Rewrite::MAP_BAG_MAKE);
 548     }
 549
 550     case BAG_UNION_DISJOINT:
 551     {
 552       // (bag.map f (bag.union_disjoint A B)) =
 553       //    (bag.union_disjoint (bag.map f A) (bag.map f B))
 554       Node a = d_nm->mkNode(BAG_MAP, n[0], n[1][0]);
 555       Node b = d_nm->mkNode(BAG_MAP, n[0], n[1][1]);
 556       Node ret = d_nm->mkNode(BAG_UNION_DISJOINT, a, b);
 557       return BagsRewriteResponse(ret, Rewrite::MAP_UNION_DISJOINT);
 558     }
 559
 560     default: return BagsRewriteResponse(n, Rewrite::NONE);
 561   }
 562 }
 563 }  // namespace bags
 564 }  // namespace theory
 565 }  // namespace cvc5