test/unit/theory/theory_bags_rewriter_white.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
   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  * White box testing of bags rewriter
  14  */
  15
  16 #include "expr/dtype.h"
  17 #include "test_smt.h"
  18 #include "theory/bags/bags_rewriter.h"
  19 #include "theory/strings/type_enumerator.h"
  20
  21 namespace cvc5 {
  22
  23 using namespace theory;
  24 using namespace kind;
  25 using namespace theory::bags;
  26
  27 namespace test {
  28
  29 typedef expr::Attribute<Node, Node> attribute;
  30
  31 class TestTheoryWhiteBagsRewriter : public TestSmt
  32 {
  33  protected:
  34   void SetUp() override
  35   {
  36     TestSmt::SetUp();
  37     d_rewriter.reset(new BagsRewriter(nullptr));
  38   }
  39
  40   std::vector<Node> getNStrings(size_t n)
  41   {
  42     std::vector<Node> elements(n);
  43     for (size_t i = 0; i < n; i++)
  44     {
  45       elements[i] =
  46           d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
  47     }
  48     return elements;
  49   }
  50
  51   std::unique_ptr<BagsRewriter> d_rewriter;
  52 };
  53
  54 TEST_F(TestTheoryWhiteBagsRewriter, empty_bag_normal_form)
  55 {
  56   Node emptybag = d_nodeManager->mkConst(EmptyBag(d_nodeManager->stringType()));
  57   // empty bags are in normal form
  58   ASSERT_TRUE(emptybag.isConst());
  59   RewriteResponse response = d_rewriter->postRewrite(emptybag);
  60   ASSERT_TRUE(emptybag == response.d_node && response.d_status == REWRITE_DONE);
  61 }
  62
  63 TEST_F(TestTheoryWhiteBagsRewriter, bag_equality)
  64 {
  65   std::vector<Node> elements = getNStrings(2);
  66   Node x = elements[0];
  67   Node y = elements[1];
  68   Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
  69   Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType());
  70   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
  71   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d);
  72   Node emptyBag = d_nodeManager->mkConst(
  73       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
  74   Node emptyString = d_nodeManager->mkConst(String(""));
  75   Node constantBag = d_nodeManager->mkBag(d_nodeManager->stringType(),
  76                                           emptyString,
  77                                           d_nodeManager->mkConst(Rational(1)));
  78
  79   // (= A A) = true where A is a bag
  80   Node n1 = A.eqNode(A);
  81   RewriteResponse response1 = d_rewriter->preRewrite(n1);
  82   ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(true)
  83               && response1.d_status == REWRITE_AGAIN_FULL);
  84
  85   // (= A B) = false if A and B are different bag constants
  86   Node n2 = constantBag.eqNode(emptyBag);
  87   RewriteResponse response2 = d_rewriter->postRewrite(n2);
  88   ASSERT_TRUE(response2.d_node == d_nodeManager->mkConst(false)
  89               && response2.d_status == REWRITE_AGAIN_FULL);
  90
  91   // (= B A) = (= A B) if A < B and at least one of A or B is not a constant
  92   Node n3 = B.eqNode(A);
  93   RewriteResponse response3 = d_rewriter->postRewrite(n3);
  94   ASSERT_TRUE(response3.d_node == A.eqNode(B)
  95               && response3.d_status == REWRITE_AGAIN_FULL);
  96
  97   // (= A B) = (= A B) no rewrite
  98   Node n4 = A.eqNode(B);
  99   RewriteResponse response4 = d_rewriter->postRewrite(n4);
 100   ASSERT_TRUE(response4.d_node == n4 && response4.d_status == REWRITE_DONE);
 101 }
 102
 103 TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
 104 {
 105   std::vector<Node> elements = getNStrings(1);
 106   Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
 107                                        elements[0],
 108                                        d_nodeManager->mkConst(Rational(-1)));
 109   Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
 110                                    elements[0],
 111                                    d_nodeManager->mkConst(Rational(0)));
 112   Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
 113                                        elements[0],
 114                                        d_nodeManager->mkConst(Rational(1)));
 115   Node emptybag = d_nodeManager->mkConst(
 116       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 117   RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
 118   RewriteResponse zeroResponse = d_rewriter->postRewrite(zero);
 119   RewriteResponse positiveResponse = d_rewriter->postRewrite(positive);
 120
 121   // bags with non-positive multiplicity are rewritten as empty bags
 122   ASSERT_TRUE(negativeResponse.d_status == REWRITE_AGAIN_FULL
 123               && negativeResponse.d_node == emptybag);
 124   ASSERT_TRUE(zeroResponse.d_status == REWRITE_AGAIN_FULL
 125               && zeroResponse.d_node == emptybag);
 126
 127   // no change for positive
 128   ASSERT_TRUE(positiveResponse.d_status == REWRITE_DONE
 129               && positive == positiveResponse.d_node);
 130 }
 131
 132 TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 133 {
 134   Node skolem =
 135       d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 136   Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
 137                                        skolem,
 138                                        d_nodeManager->mkConst(Rational(-1)));
 139   Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
 140                                        skolem,
 141                                        d_nodeManager->mkConst(Rational(-1)));
 142   Node zero = d_nodeManager->mkBag(
 143       d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(0)));
 144   Node positive = d_nodeManager->mkBag(
 145       d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(1)));
 146   Node emptybag = d_nodeManager->mkConst(
 147       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 148   RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
 149   RewriteResponse zeroResponse = d_rewriter->postRewrite(zero);
 150   RewriteResponse positiveResponse = d_rewriter->postRewrite(positive);
 151
 152   // bags with non-positive multiplicity are rewritten as empty bags
 153   ASSERT_TRUE(negativeResponse.d_status == REWRITE_AGAIN_FULL
 154               && negativeResponse.d_node == emptybag);
 155   ASSERT_TRUE(zeroResponse.d_status == REWRITE_AGAIN_FULL
 156               && zeroResponse.d_node == emptybag);
 157
 158   // no change for positive
 159   ASSERT_TRUE(positiveResponse.d_status == REWRITE_DONE
 160               && positive == positiveResponse.d_node);
 161 }
 162
 163 TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 164 {
 165   int n = 3;
 166   Node skolem =
 167       d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 168   Node emptyBag = d_nodeManager->mkConst(
 169       EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
 170   Node bag = d_nodeManager->mkBag(
 171       d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(n)));
 172
 173   // (bag.count x emptybag) = 0
 174   Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag);
 175   RewriteResponse response1 = d_rewriter->postRewrite(n1);
 176   ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL
 177               && response1.d_node == d_nodeManager->mkConst(Rational(0)));
 178
 179   // (bag.count x (mkBag x c) = c where c > 0 is a constant
 180   Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag);
 181   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 182   ASSERT_TRUE(response2.d_status == REWRITE_AGAIN_FULL
 183               && response2.d_node == d_nodeManager->mkConst(Rational(n)));
 184 }
 185
 186 TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
 187 {
 188   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 189   Node bag = d_nodeManager->mkBag(
 190       d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
 191
 192   // (duplicate_removal (mkBag x n)) = (mkBag x 1)
 193   Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag);
 194   RewriteResponse response = d_rewriter->postRewrite(n);
 195   Node noDuplicate = d_nodeManager->mkBag(
 196       d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
 197   ASSERT_TRUE(response.d_node == noDuplicate
 198               && response.d_status == REWRITE_AGAIN_FULL);
 199 }
 200
 201 TEST_F(TestTheoryWhiteBagsRewriter, union_max)
 202 {
 203   int n = 3;
 204   std::vector<Node> elements = getNStrings(2);
 205   Node emptyBag = d_nodeManager->mkConst(
 206       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 207   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 208                                 elements[0],
 209                                 d_nodeManager->mkConst(Rational(n)));
 210   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 211                                 elements[1],
 212                                 d_nodeManager->mkConst(Rational(n + 1)));
 213   Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
 214   Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
 215   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 216   Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
 217
 218   // (union_max A emptybag) = A
 219   Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag);
 220   RewriteResponse response1 = d_rewriter->postRewrite(unionMax1);
 221   ASSERT_TRUE(response1.d_node == A
 222               && response1.d_status == REWRITE_AGAIN_FULL);
 223
 224   // (union_max emptybag A) = A
 225   Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A);
 226   RewriteResponse response2 = d_rewriter->postRewrite(unionMax2);
 227   ASSERT_TRUE(response2.d_node == A
 228               && response2.d_status == REWRITE_AGAIN_FULL);
 229
 230   // (union_max A A) = A
 231   Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A);
 232   RewriteResponse response3 = d_rewriter->postRewrite(unionMax3);
 233   ASSERT_TRUE(response3.d_node == A
 234               && response3.d_status == REWRITE_AGAIN_FULL);
 235
 236   // (union_max A (union_max A B)) = (union_max A B)
 237   Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB);
 238   RewriteResponse response4 = d_rewriter->postRewrite(unionMax4);
 239   ASSERT_TRUE(response4.d_node == unionMaxAB
 240               && response4.d_status == REWRITE_AGAIN_FULL);
 241
 242   // (union_max A (union_max B A)) = (union_max B A)
 243   Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA);
 244   RewriteResponse response5 = d_rewriter->postRewrite(unionMax5);
 245   ASSERT_TRUE(response5.d_node == unionMaxBA
 246               && response4.d_status == REWRITE_AGAIN_FULL);
 247
 248   // (union_max (union_max A B) A) = (union_max A B)
 249   Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A);
 250   RewriteResponse response6 = d_rewriter->postRewrite(unionMax6);
 251   ASSERT_TRUE(response6.d_node == unionMaxAB
 252               && response6.d_status == REWRITE_AGAIN_FULL);
 253
 254   // (union_max (union_max B A) A) = (union_max B A)
 255   Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A);
 256   RewriteResponse response7 = d_rewriter->postRewrite(unionMax7);
 257   ASSERT_TRUE(response7.d_node == unionMaxBA
 258               && response7.d_status == REWRITE_AGAIN_FULL);
 259
 260   // (union_max A (union_disjoint A B)) = (union_disjoint A B)
 261   Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB);
 262   RewriteResponse response8 = d_rewriter->postRewrite(unionMax8);
 263   ASSERT_TRUE(response8.d_node == unionDisjointAB
 264               && response8.d_status == REWRITE_AGAIN_FULL);
 265
 266   // (union_max A (union_disjoint B A)) = (union_disjoint B A)
 267   Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA);
 268   RewriteResponse response9 = d_rewriter->postRewrite(unionMax9);
 269   ASSERT_TRUE(response9.d_node == unionDisjointBA
 270               && response9.d_status == REWRITE_AGAIN_FULL);
 271
 272   // (union_max (union_disjoint A B) A) = (union_disjoint A B)
 273   Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A);
 274   RewriteResponse response10 = d_rewriter->postRewrite(unionMax10);
 275   ASSERT_TRUE(response10.d_node == unionDisjointAB
 276               && response10.d_status == REWRITE_AGAIN_FULL);
 277
 278   // (union_max (union_disjoint B A) A) = (union_disjoint B A)
 279   Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A);
 280   RewriteResponse response11 = d_rewriter->postRewrite(unionMax11);
 281   ASSERT_TRUE(response11.d_node == unionDisjointBA
 282               && response11.d_status == REWRITE_AGAIN_FULL);
 283 }
 284
 285 TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint)
 286 {
 287   int n = 3;
 288   std::vector<Node> elements = getNStrings(3);
 289   Node emptyBag = d_nodeManager->mkConst(
 290       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 291   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 292                                 elements[0],
 293                                 d_nodeManager->mkConst(Rational(n)));
 294   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 295                                 elements[1],
 296                                 d_nodeManager->mkConst(Rational(n + 1)));
 297   Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
 298                                 elements[2],
 299                                 d_nodeManager->mkConst(Rational(n + 2)));
 300
 301   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 302   Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
 303   Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
 304   Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C);
 305   Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
 306   Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
 307   Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
 308
 309   // (union_disjoint A emptybag) = A
 310   Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag);
 311   RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1);
 312   ASSERT_TRUE(response1.d_node == A
 313               && response1.d_status == REWRITE_AGAIN_FULL);
 314
 315   // (union_disjoint emptybag A) = A
 316   Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A);
 317   RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2);
 318   ASSERT_TRUE(response2.d_node == A
 319               && response2.d_status == REWRITE_AGAIN_FULL);
 320
 321   // (union_disjoint (union_max A B) (intersection_min B A)) =
 322   //          (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
 323   Node unionDisjoint3 =
 324       d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA);
 325   RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3);
 326   ASSERT_TRUE(response3.d_node == unionDisjointAB
 327               && response3.d_status == REWRITE_AGAIN_FULL);
 328
 329   // (union_disjoint (intersection_min B A)) (union_max A B) =
 330   //          (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
 331   Node unionDisjoint4 =
 332       d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA);
 333   RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4);
 334   ASSERT_TRUE(response4.d_node == unionDisjointBA
 335               && response4.d_status == REWRITE_AGAIN_FULL);
 336
 337   // (union_disjoint (intersection_min B A)) (union_max A B) =
 338   //          (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
 339   Node unionDisjoint5 =
 340       d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB);
 341   RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5);
 342   ASSERT_TRUE(response5.d_node == unionDisjoint5
 343               && response5.d_status == REWRITE_DONE);
 344 }
 345
 346 TEST_F(TestTheoryWhiteBagsRewriter, intersection_min)
 347 {
 348   int n = 3;
 349   std::vector<Node> elements = getNStrings(2);
 350   Node emptyBag = d_nodeManager->mkConst(
 351       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 352   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 353                                 elements[0],
 354                                 d_nodeManager->mkConst(Rational(n)));
 355   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 356                                 elements[1],
 357                                 d_nodeManager->mkConst(Rational(n + 1)));
 358   Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
 359   Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
 360   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 361   Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
 362
 363   // (intersection_min A emptybag) = emptyBag
 364   Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag);
 365   RewriteResponse response1 = d_rewriter->postRewrite(n1);
 366   ASSERT_TRUE(response1.d_node == emptyBag
 367               && response1.d_status == REWRITE_AGAIN_FULL);
 368
 369   // (intersection_min emptybag A) = emptyBag
 370   Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A);
 371   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 372   ASSERT_TRUE(response2.d_node == emptyBag
 373               && response2.d_status == REWRITE_AGAIN_FULL);
 374
 375   // (intersection_min A A) = A
 376   Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A);
 377   RewriteResponse response3 = d_rewriter->postRewrite(n3);
 378   ASSERT_TRUE(response3.d_node == A
 379               && response3.d_status == REWRITE_AGAIN_FULL);
 380
 381   // (intersection_min A (union_max A B) = A
 382   Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB);
 383   RewriteResponse response4 = d_rewriter->postRewrite(n4);
 384   ASSERT_TRUE(response4.d_node == A
 385               && response4.d_status == REWRITE_AGAIN_FULL);
 386
 387   // (intersection_min A (union_max B A) = A
 388   Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA);
 389   RewriteResponse response5 = d_rewriter->postRewrite(n5);
 390   ASSERT_TRUE(response5.d_node == A
 391               && response4.d_status == REWRITE_AGAIN_FULL);
 392
 393   // (intersection_min (union_max A B) A) = A
 394   Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A);
 395   RewriteResponse response6 = d_rewriter->postRewrite(n6);
 396   ASSERT_TRUE(response6.d_node == A
 397               && response6.d_status == REWRITE_AGAIN_FULL);
 398
 399   // (intersection_min (union_max B A) A) = A
 400   Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A);
 401   RewriteResponse response7 = d_rewriter->postRewrite(n7);
 402   ASSERT_TRUE(response7.d_node == A
 403               && response7.d_status == REWRITE_AGAIN_FULL);
 404
 405   // (intersection_min A (union_disjoint A B) = A
 406   Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB);
 407   RewriteResponse response8 = d_rewriter->postRewrite(n8);
 408   ASSERT_TRUE(response8.d_node == A
 409               && response8.d_status == REWRITE_AGAIN_FULL);
 410
 411   // (intersection_min A (union_disjoint B A) = A
 412   Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA);
 413   RewriteResponse response9 = d_rewriter->postRewrite(n9);
 414   ASSERT_TRUE(response9.d_node == A
 415               && response9.d_status == REWRITE_AGAIN_FULL);
 416
 417   // (intersection_min (union_disjoint A B) A) = A
 418   Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A);
 419   RewriteResponse response10 = d_rewriter->postRewrite(n10);
 420   ASSERT_TRUE(response10.d_node == A
 421               && response10.d_status == REWRITE_AGAIN_FULL);
 422
 423   // (intersection_min (union_disjoint B A) A) = A
 424   Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A);
 425   RewriteResponse response11 = d_rewriter->postRewrite(n11);
 426   ASSERT_TRUE(response11.d_node == A
 427               && response11.d_status == REWRITE_AGAIN_FULL);
 428 }
 429
 430 TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract)
 431 {
 432   int n = 3;
 433   std::vector<Node> elements = getNStrings(2);
 434   Node emptyBag = d_nodeManager->mkConst(
 435       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 436   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 437                                 elements[0],
 438                                 d_nodeManager->mkConst(Rational(n)));
 439   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 440                                 elements[1],
 441                                 d_nodeManager->mkConst(Rational(n + 1)));
 442   Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
 443   Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
 444   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 445   Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
 446   Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
 447   Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
 448
 449   // (difference_subtract A emptybag) = A
 450   Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag);
 451   RewriteResponse response1 = d_rewriter->postRewrite(n1);
 452   ASSERT_TRUE(response1.d_node == A
 453               && response1.d_status == REWRITE_AGAIN_FULL);
 454
 455   // (difference_subtract emptybag A) = emptyBag
 456   Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A);
 457   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 458   ASSERT_TRUE(response2.d_node == emptyBag
 459               && response2.d_status == REWRITE_AGAIN_FULL);
 460
 461   // (difference_subtract A A) = emptybag
 462   Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A);
 463   RewriteResponse response3 = d_rewriter->postRewrite(n3);
 464   ASSERT_TRUE(response3.d_node == emptyBag
 465               && response3.d_status == REWRITE_AGAIN_FULL);
 466
 467   // (difference_subtract (union_disjoint A B) A) = B
 468   Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A);
 469   RewriteResponse response4 = d_rewriter->postRewrite(n4);
 470   ASSERT_TRUE(response4.d_node == B
 471               && response4.d_status == REWRITE_AGAIN_FULL);
 472
 473   // (difference_subtract (union_disjoint B A) A) = B
 474   Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A);
 475   RewriteResponse response5 = d_rewriter->postRewrite(n5);
 476   ASSERT_TRUE(response5.d_node == B
 477               && response4.d_status == REWRITE_AGAIN_FULL);
 478
 479   // (difference_subtract A (union_disjoint A B)) = emptybag
 480   Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB);
 481   RewriteResponse response6 = d_rewriter->postRewrite(n6);
 482   ASSERT_TRUE(response6.d_node == emptyBag
 483               && response6.d_status == REWRITE_AGAIN_FULL);
 484
 485   // (difference_subtract A (union_disjoint B A)) = emptybag
 486   Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA);
 487   RewriteResponse response7 = d_rewriter->postRewrite(n7);
 488   ASSERT_TRUE(response7.d_node == emptyBag
 489               && response7.d_status == REWRITE_AGAIN_FULL);
 490
 491   // (difference_subtract A (union_max A B)) = emptybag
 492   Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB);
 493   RewriteResponse response8 = d_rewriter->postRewrite(n8);
 494   ASSERT_TRUE(response8.d_node == emptyBag
 495               && response8.d_status == REWRITE_AGAIN_FULL);
 496
 497   // (difference_subtract A (union_max B A)) = emptybag
 498   Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA);
 499   RewriteResponse response9 = d_rewriter->postRewrite(n9);
 500   ASSERT_TRUE(response9.d_node == emptyBag
 501               && response9.d_status == REWRITE_AGAIN_FULL);
 502
 503   // (difference_subtract (intersection_min A B) A) = emptybag
 504   Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A);
 505   RewriteResponse response10 = d_rewriter->postRewrite(n10);
 506   ASSERT_TRUE(response10.d_node == emptyBag
 507               && response10.d_status == REWRITE_AGAIN_FULL);
 508
 509   // (difference_subtract (intersection_min B A) A) = emptybag
 510   Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A);
 511   RewriteResponse response11 = d_rewriter->postRewrite(n11);
 512   ASSERT_TRUE(response11.d_node == emptyBag
 513               && response11.d_status == REWRITE_AGAIN_FULL);
 514 }
 515
 516 TEST_F(TestTheoryWhiteBagsRewriter, difference_remove)
 517 {
 518   int n = 3;
 519   std::vector<Node> elements = getNStrings(2);
 520   Node emptyBag = d_nodeManager->mkConst(
 521       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 522   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 523                                 elements[0],
 524                                 d_nodeManager->mkConst(Rational(n)));
 525   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 526                                 elements[1],
 527                                 d_nodeManager->mkConst(Rational(n + 1)));
 528   Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
 529   Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
 530   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 531   Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
 532   Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
 533   Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
 534
 535   // (difference_remove A emptybag) = A
 536   Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag);
 537   RewriteResponse response1 = d_rewriter->postRewrite(n1);
 538   ASSERT_TRUE(response1.d_node == A
 539               && response1.d_status == REWRITE_AGAIN_FULL);
 540
 541   // (difference_remove emptybag A) = emptyBag
 542   Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A);
 543   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 544   ASSERT_TRUE(response2.d_node == emptyBag
 545               && response2.d_status == REWRITE_AGAIN_FULL);
 546
 547   // (difference_remove A A) = emptybag
 548   Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A);
 549   RewriteResponse response3 = d_rewriter->postRewrite(n3);
 550   ASSERT_TRUE(response3.d_node == emptyBag
 551               && response3.d_status == REWRITE_AGAIN_FULL);
 552
 553   // (difference_remove A (union_disjoint A B)) = emptybag
 554   Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB);
 555   RewriteResponse response6 = d_rewriter->postRewrite(n6);
 556   ASSERT_TRUE(response6.d_node == emptyBag
 557               && response6.d_status == REWRITE_AGAIN_FULL);
 558
 559   // (difference_remove A (union_disjoint B A)) = emptybag
 560   Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA);
 561   RewriteResponse response7 = d_rewriter->postRewrite(n7);
 562   ASSERT_TRUE(response7.d_node == emptyBag
 563               && response7.d_status == REWRITE_AGAIN_FULL);
 564
 565   // (difference_remove A (union_max A B)) = emptybag
 566   Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB);
 567   RewriteResponse response8 = d_rewriter->postRewrite(n8);
 568   ASSERT_TRUE(response8.d_node == emptyBag
 569               && response8.d_status == REWRITE_AGAIN_FULL);
 570
 571   // (difference_remove A (union_max B A)) = emptybag
 572   Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA);
 573   RewriteResponse response9 = d_rewriter->postRewrite(n9);
 574   ASSERT_TRUE(response9.d_node == emptyBag
 575               && response9.d_status == REWRITE_AGAIN_FULL);
 576
 577   // (difference_remove (intersection_min A B) A) = emptybag
 578   Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A);
 579   RewriteResponse response10 = d_rewriter->postRewrite(n10);
 580   ASSERT_TRUE(response10.d_node == emptyBag
 581               && response10.d_status == REWRITE_AGAIN_FULL);
 582
 583   // (difference_remove (intersection_min B A) A) = emptybag
 584   Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A);
 585   RewriteResponse response11 = d_rewriter->postRewrite(n11);
 586   ASSERT_TRUE(response11.d_node == emptyBag
 587               && response11.d_status == REWRITE_AGAIN_FULL);
 588 }
 589
 590 TEST_F(TestTheoryWhiteBagsRewriter, choose)
 591 {
 592   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 593   Node c = d_nodeManager->mkConst(Rational(3));
 594   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 595
 596   // (bag.choose (mkBag x c)) = x where c is a constant > 0
 597   Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag);
 598   RewriteResponse response1 = d_rewriter->postRewrite(n1);
 599   ASSERT_TRUE(response1.d_node == x
 600               && response1.d_status == REWRITE_AGAIN_FULL);
 601 }
 602
 603 TEST_F(TestTheoryWhiteBagsRewriter, bag_card)
 604 {
 605   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 606   Node emptyBag = d_nodeManager->mkConst(
 607       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 608   Node zero = d_nodeManager->mkConst(Rational(0));
 609   Node c = d_nodeManager->mkConst(Rational(3));
 610   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 611   std::vector<Node> elements = getNStrings(2);
 612   Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
 613                                 elements[0],
 614                                 d_nodeManager->mkConst(Rational(4)));
 615   Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
 616                                 elements[1],
 617                                 d_nodeManager->mkConst(Rational(5)));
 618   Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
 619
 620   // TODO(projects#223): enable this test after implementing bags normal form
 621   //    // (bag.card emptybag) = 0
 622   //    Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag);
 623   //    RewriteResponse response1 = d_rewriter->postRewrite(n1);
 624   //    ASSERT_TRUE(response1.d_node == zero && response1.d_status ==
 625   //    REWRITE_AGAIN_FULL);
 626
 627   // (bag.card (mkBag x c)) = c where c is a constant > 0
 628   Node n2 = d_nodeManager->mkNode(BAG_CARD, bag);
 629   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 630   ASSERT_TRUE(response2.d_node == c
 631               && response2.d_status == REWRITE_AGAIN_FULL);
 632
 633   // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B))
 634   Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB);
 635   Node cardA = d_nodeManager->mkNode(BAG_CARD, A);
 636   Node cardB = d_nodeManager->mkNode(BAG_CARD, B);
 637   Node plus = d_nodeManager->mkNode(PLUS, cardA, cardB);
 638   RewriteResponse response3 = d_rewriter->postRewrite(n3);
 639   ASSERT_TRUE(response3.d_node == plus
 640               && response3.d_status == REWRITE_AGAIN_FULL);
 641 }
 642
 643 TEST_F(TestTheoryWhiteBagsRewriter, is_singleton)
 644 {
 645   Node emptybag = d_nodeManager->mkConst(
 646       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 647   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 648   Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
 649   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 650
 651   // TODO(projects#223): complete this function
 652   // (bag.is_singleton emptybag) = false
 653   //    Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag);
 654   //    RewriteResponse response1 = d_rewriter->postRewrite(n1);
 655   //    ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false)
 656   //              && response1.d_status == REWRITE_AGAIN_FULL);
 657
 658   // (bag.is_singleton (mkBag x c) = (c == 1)
 659   Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag);
 660   RewriteResponse response2 = d_rewriter->postRewrite(n2);
 661   Node one = d_nodeManager->mkConst(Rational(1));
 662   Node equal = c.eqNode(one);
 663   ASSERT_TRUE(response2.d_node == equal
 664               && response2.d_status == REWRITE_AGAIN_FULL);
 665 }
 666
 667 TEST_F(TestTheoryWhiteBagsRewriter, from_set)
 668 {
 669   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 670   Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
 671
 672   // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
 673   Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
 674   RewriteResponse response = d_rewriter->postRewrite(n);
 675   Node one = d_nodeManager->mkConst(Rational(1));
 676   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one);
 677   ASSERT_TRUE(response.d_node == bag
 678               && response.d_status == REWRITE_AGAIN_FULL);
 679 }
 680
 681 TEST_F(TestTheoryWhiteBagsRewriter, to_set)
 682 {
 683   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
 684   Node bag = d_nodeManager->mkBag(
 685       d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
 686
 687   // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
 688   Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
 689   RewriteResponse response = d_rewriter->postRewrite(n);
 690   Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
 691   ASSERT_TRUE(response.d_node == singleton
 692               && response.d_status == REWRITE_AGAIN_FULL);
 693 }
 694 }  // namespace test
 695 }  // namespace cvc5