src/theory/bags/inference_generator.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed, Andrew Reynolds, Gereon Kremer
   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  * Inference generator utility.
  14  */
  15
  16 #include "inference_generator.h"
  17
  18 #include "expr/attribute.h"
  19 #include "expr/bound_var_manager.h"
  20 #include "expr/dtype_cons.h"
  21 #include "expr/emptybag.h"
  22 #include "expr/skolem_manager.h"
  23 #include "theory/bags/bags_utils.h"
  24 #include "theory/bags/inference_manager.h"
  25 #include "theory/bags/solver_state.h"
  26 #include "theory/datatypes/tuple_utils.h"
  27 #include "theory/quantifiers/fmf/bounded_integers.h"
  28 #include "theory/uf/equality_engine.h"
  29 #include "util/rational.h"
  30
  31 using namespace cvc5::kind;
  32 using namespace cvc5::theory::datatypes;
  33
  34 namespace cvc5 {
  35 namespace theory {
  36 namespace bags {
  37
  38 InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
  39     : d_state(state), d_im(im)
  40 {
  41   d_nm = NodeManager::currentNM();
  42   d_sm = d_nm->getSkolemManager();
  43   d_true = d_nm->mkConst(true);
  44   d_zero = d_nm->mkConstInt(Rational(0));
  45   d_one = d_nm->mkConstInt(Rational(1));
  46 }
  47
  48 InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
  49 {
  50   Assert(n.getType().isBag());
  51   Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
  52
  53   InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
  54   Node count = d_nm->mkNode(BAG_COUNT, e, n);
  55   Node gte = d_nm->mkNode(GEQ, count, d_zero);
  56   inferInfo.d_conclusion = gte;
  57   return inferInfo;
  58 }
  59
  60 InferInfo InferenceGenerator::nonNegativeCardinality(Node n)
  61 {
  62   InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
  63   Node gte = d_nm->mkNode(GEQ, n, d_zero);
  64   inferInfo.d_conclusion = gte;
  65   return inferInfo;
  66 }
  67
  68 InferInfo InferenceGenerator::bagMake(Node n)
  69 {
  70   Assert(n.getKind() == BAG_MAKE);
  71   /*
  72    * (or
  73    *   (and (<  c 1) (= (bag x c) (as bag.empty (Bag E))))
  74    *   (and (>= c 1) (not (= (bag x c) (as bag.empty (Bag E))))
  75    */
  76   Node x = n[0];
  77   Node c = n[1];
  78   InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE_SPLIT);
  79   Node empty = d_nm->mkConst(EmptyBag(n.getType()));
  80   Node equal = d_nm->mkNode(EQUAL, n, empty);
  81   Node geq = d_nm->mkNode(GEQ, c, d_one);
  82   Node isEmpty = geq.notNode().andNode(equal);
  83   Node isNotEmpty = geq.andNode(equal.notNode());
  84   Node orNode = isEmpty.orNode(isNotEmpty);
  85   inferInfo.d_conclusion = orNode;
  86   return inferInfo;
  87 }
  88
  89 InferInfo InferenceGenerator::bagMake(Node n, Node e)
  90 {
  91   Assert(n.getKind() == BAG_MAKE);
  92   Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
  93
  94   /*
  95    * (ite (and (= e x) (>= c 1))
  96    *   (= (bag.count e skolem) c)
  97    *   (= (bag.count e skolem) 0))
  98    */
  99   Node x = n[0];
 100   Node c = n[1];
 101   InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE);
 102   Node same = d_nm->mkNode(EQUAL, e, x);
 103   Node geq = d_nm->mkNode(GEQ, c, d_one);
 104   Node andNode = same.andNode(geq);
 105   Node skolem = getSkolem(n, inferInfo);
 106   Node count = getMultiplicityTerm(e, skolem);
 107   Node equalC = d_nm->mkNode(EQUAL, count, c);
 108   Node equalZero = d_nm->mkNode(EQUAL, count, d_zero);
 109   Node ite = d_nm->mkNode(ITE, andNode, equalC, equalZero);
 110   inferInfo.d_conclusion = ite;
 111   return inferInfo;
 112 }
 113
 114 /**
 115  * A bound variable corresponding to the universally quantified integer
 116  * variable used to range over the distinct elements in a bag, used
 117  * for axiomatizing the behavior of some term.
 118  */
 119 struct FirstIndexVarAttributeId
 120 {
 121 };
 122 typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute;
 123
 124 /**
 125  * A bound variable corresponding to the universally quantified integer
 126  * variable used to range over the distinct elements in a bag, used
 127  * for axiomatizing the behavior of some term.
 128  */
 129 struct SecondIndexVarAttributeId
 130 {
 131 };
 132 typedef expr::Attribute<SecondIndexVarAttributeId, Node>
 133     SecondIndexVarAttribute;
 134
 135 struct BagsDeqAttributeId
 136 {
 137 };
 138 typedef expr::Attribute<BagsDeqAttributeId, Node> BagsDeqAttribute;
 139
 140 InferInfo InferenceGenerator::bagDisequality(Node n)
 141 {
 142   Assert(n.getKind() == EQUAL && n[0].getType().isBag());
 143
 144   Node A = n[0];
 145   Node B = n[1];
 146
 147   InferInfo inferInfo(d_im, InferenceId::BAGS_DISEQUALITY);
 148
 149   TypeNode elementType = A.getType().getBagElementType();
 150   BoundVarManager* bvm = d_nm->getBoundVarManager();
 151   Node element = bvm->mkBoundVar<BagsDeqAttribute>(n, elementType);
 152   Node skolem =
 153       d_sm->mkSkolem(element,
 154                      n,
 155                      "bag_disequal",
 156                      "an extensional lemma for disequality of two bags");
 157
 158   Node countA = getMultiplicityTerm(skolem, A);
 159   Node countB = getMultiplicityTerm(skolem, B);
 160
 161   Node disEqual = countA.eqNode(countB).notNode();
 162
 163   inferInfo.d_premises.push_back(n.notNode());
 164   inferInfo.d_conclusion = disEqual;
 165   return inferInfo;
 166 }
 167
 168 Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
 169 {
 170   Node skolem = d_sm->mkPurifySkolem(n, "skolem_bag", "skolem bag");
 171   inferInfo.d_skolems[n] = skolem;
 172   return skolem;
 173 }
 174
 175 InferInfo InferenceGenerator::empty(Node n, Node e)
 176 {
 177   Assert(n.getKind() == BAG_EMPTY);
 178   Assert(e.getType() == n.getType().getBagElementType());
 179
 180   InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
 181   Node skolem = getSkolem(n, inferInfo);
 182   Node count = getMultiplicityTerm(e, skolem);
 183
 184   Node equal = count.eqNode(d_zero);
 185   inferInfo.d_conclusion = equal;
 186   return inferInfo;
 187 }
 188
 189 InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
 190 {
 191   Assert(n.getKind() == BAG_UNION_DISJOINT && n[0].getType().isBag());
 192   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 193
 194   Node A = n[0];
 195   Node B = n[1];
 196   InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_DISJOINT);
 197
 198   Node countA = getMultiplicityTerm(e, A);
 199   Node countB = getMultiplicityTerm(e, B);
 200
 201   Node skolem = getSkolem(n, inferInfo);
 202   Node count = getMultiplicityTerm(e, skolem);
 203
 204   Node sum = d_nm->mkNode(ADD, countA, countB);
 205   Node equal = count.eqNode(sum);
 206
 207   inferInfo.d_conclusion = equal;
 208   return inferInfo;
 209 }
 210
 211 InferInfo InferenceGenerator::unionMax(Node n, Node e)
 212 {
 213   Assert(n.getKind() == BAG_UNION_MAX && n[0].getType().isBag());
 214   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 215
 216   Node A = n[0];
 217   Node B = n[1];
 218   InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_MAX);
 219
 220   Node countA = getMultiplicityTerm(e, A);
 221   Node countB = getMultiplicityTerm(e, B);
 222
 223   Node skolem = getSkolem(n, inferInfo);
 224   Node count = getMultiplicityTerm(e, skolem);
 225
 226   Node gt = d_nm->mkNode(GT, countA, countB);
 227   Node max = d_nm->mkNode(ITE, gt, countA, countB);
 228   Node equal = count.eqNode(max);
 229
 230   inferInfo.d_conclusion = equal;
 231   return inferInfo;
 232 }
 233
 234 InferInfo InferenceGenerator::intersection(Node n, Node e)
 235 {
 236   Assert(n.getKind() == BAG_INTER_MIN && n[0].getType().isBag());
 237   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 238
 239   Node A = n[0];
 240   Node B = n[1];
 241   InferInfo inferInfo(d_im, InferenceId::BAGS_INTERSECTION_MIN);
 242
 243   Node countA = getMultiplicityTerm(e, A);
 244   Node countB = getMultiplicityTerm(e, B);
 245   Node skolem = getSkolem(n, inferInfo);
 246   Node count = getMultiplicityTerm(e, skolem);
 247
 248   Node lt = d_nm->mkNode(LT, countA, countB);
 249   Node min = d_nm->mkNode(ITE, lt, countA, countB);
 250   Node equal = count.eqNode(min);
 251   inferInfo.d_conclusion = equal;
 252   return inferInfo;
 253 }
 254
 255 InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
 256 {
 257   Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT && n[0].getType().isBag());
 258   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 259
 260   Node A = n[0];
 261   Node B = n[1];
 262   InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_SUBTRACT);
 263
 264   Node countA = getMultiplicityTerm(e, A);
 265   Node countB = getMultiplicityTerm(e, B);
 266   Node skolem = getSkolem(n, inferInfo);
 267   Node count = getMultiplicityTerm(e, skolem);
 268
 269   Node subtract = d_nm->mkNode(SUB, countA, countB);
 270   Node gte = d_nm->mkNode(GEQ, countA, countB);
 271   Node difference = d_nm->mkNode(ITE, gte, subtract, d_zero);
 272   Node equal = count.eqNode(difference);
 273   inferInfo.d_conclusion = equal;
 274   return inferInfo;
 275 }
 276
 277 InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
 278 {
 279   Assert(n.getKind() == BAG_DIFFERENCE_REMOVE && n[0].getType().isBag());
 280   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 281
 282   Node A = n[0];
 283   Node B = n[1];
 284   InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_REMOVE);
 285
 286   Node countA = getMultiplicityTerm(e, A);
 287   Node countB = getMultiplicityTerm(e, B);
 288
 289   Node skolem = getSkolem(n, inferInfo);
 290   Node count = getMultiplicityTerm(e, skolem);
 291
 292   Node notInB = d_nm->mkNode(LEQ, countB, d_zero);
 293   Node difference = d_nm->mkNode(ITE, notInB, countA, d_zero);
 294   Node equal = count.eqNode(difference);
 295   inferInfo.d_conclusion = equal;
 296   return inferInfo;
 297 }
 298
 299 InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
 300 {
 301   Assert(n.getKind() == BAG_DUPLICATE_REMOVAL && n[0].getType().isBag());
 302   Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 303
 304   Node A = n[0];
 305   InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL);
 306
 307   Node countA = getMultiplicityTerm(e, A);
 308   Node skolem = getSkolem(n, inferInfo);
 309   Node count = getMultiplicityTerm(e, skolem);
 310
 311   Node gte = d_nm->mkNode(GEQ, countA, d_one);
 312   Node ite = d_nm->mkNode(ITE, gte, d_one, d_zero);
 313   Node equal = count.eqNode(ite);
 314   inferInfo.d_conclusion = equal;
 315   return inferInfo;
 316 }
 317
 318 InferInfo InferenceGenerator::cardEmpty(const std::pair<Node, Node>& pair,
 319                                         Node n)
 320 {
 321   Assert(pair.first.getKind() == BAG_CARD);
 322   Assert(n.getKind() == BAG_EMPTY && n.getType() == pair.first[0].getType());
 323   InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
 324   Node premise = pair.first[0].eqNode(n);
 325   Node conclusion = pair.second.eqNode(d_zero);
 326   inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
 327   return inferInfo;
 328 }
 329
 330 InferInfo InferenceGenerator::cardBagMake(const std::pair<Node, Node>& pair,
 331                                           Node n)
 332 {
 333   Assert(pair.first.getKind() == BAG_CARD);
 334   Assert(n.getKind() == BAG_MAKE && n.getType() == pair.first[0].getType());
 335   //(=>
 336   //  (and (= A (bag x c)) (>= 0 c))
 337   //  (= (bag.card A) c))
 338   Node c = n[1];
 339   InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
 340   Node nonNegative = d_nm->mkNode(GEQ, c, d_zero);
 341   Node premise = pair.first[0].eqNode(n).andNode(nonNegative);
 342   Node conclusion = pair.second.eqNode(c);
 343   inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
 344   return inferInfo;
 345 }
 346
 347 InferInfo InferenceGenerator::cardUnionDisjoint(Node premise,
 348                                                 Node parent,
 349                                                 const std::set<Node>& children)
 350 {
 351   Assert(premise.getType().isBoolean());
 352   Assert(!children.empty());
 353   InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
 354
 355   std::set<Node>::iterator it = children.begin();
 356   Node child = *it;
 357   d_state->registerBag(child);
 358   Node unionDisjoints = child;
 359   Node card = d_nm->mkNode(BAG_CARD, child);
 360   std::vector<Node> lemmas;
 361   lemmas.push_back(d_state->registerCardinalityTerm(card));
 362   Node sum = d_state->getCardinalitySkolem(card);
 363   ++it;
 364   while (it != children.end())
 365   {
 366     child = *it;
 367     d_state->registerBag(child);
 368     unionDisjoints =
 369         d_nm->mkNode(kind::BAG_UNION_DISJOINT, unionDisjoints, child);
 370     card = d_nm->mkNode(BAG_CARD, child);
 371     lemmas.push_back(d_state->registerCardinalityTerm(card));
 372     d_state->getCardinalitySkolem(card);
 373     Node skolem = d_state->getCardinalitySkolem(card);
 374     sum = d_nm->mkNode(ADD, sum, skolem);
 375     ++it;
 376   }
 377   Node parentCard = d_nm->mkNode(BAG_CARD, parent);
 378   lemmas.push_back(d_state->registerCardinalityTerm(parentCard));
 379   Node parentSkolem = d_state->getCardinalitySkolem(parentCard);
 380
 381   Node bags = parent.eqNode(unionDisjoints);
 382   lemmas.push_back(bags);
 383   Node cards = parentSkolem.eqNode(sum);
 384   lemmas.push_back(cards);
 385   Node conclusion = d_nm->mkNode(AND, lemmas);
 386   inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
 387   return inferInfo;
 388 }
 389
 390 Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
 391 {
 392   Node count = d_nm->mkNode(BAG_COUNT, element, bag);
 393   return count;
 394 }
 395
 396 std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
 397                                                                    Node e)
 398 {
 399   Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
 400   Assert(n[0].getType().isFunction()
 401          && n[0].getType().getArgTypes().size() == 1);
 402   Assert(e.getType() == n[0].getType().getRangeType());
 403
 404   InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
 405
 406   Node f = n[0];
 407   Node A = n[1];
 408   // declare an uninterpreted function uf: Int -> T
 409   TypeNode domainType = f.getType().getArgTypes()[0];
 410   TypeNode ufType = d_nm->mkFunctionType(d_nm->integerType(), domainType);
 411   Node uf =
 412       d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE, ufType, {n, e});
 413
 414   // declare uninterpreted function sum: Int -> Int
 415   TypeNode sumType =
 416       d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType());
 417   Node sum = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_SUM, sumType, {n, e});
 418
 419   // (= (sum 0) 0)
 420   Node sum_zero = d_nm->mkNode(APPLY_UF, sum, d_zero);
 421   Node baseCase = d_nm->mkNode(EQUAL, sum_zero, d_zero);
 422
 423   // guess the size of the preimage of e
 424   Node preImageSize = d_sm->mkDummySkolem("preImageSize", d_nm->integerType());
 425
 426   // (= (sum preImageSize) (bag.count e skolem))
 427   Node mapSkolem = getSkolem(n, inferInfo);
 428   Node countE = getMultiplicityTerm(e, mapSkolem);
 429   Node totalSum = d_nm->mkNode(APPLY_UF, sum, preImageSize);
 430   Node totalSumEqualCountE = d_nm->mkNode(EQUAL, totalSum, countE);
 431
 432   // (forall ((i Int))
 433   //        (let ((uf_i (uf i)))
 434   //          (let ((count_uf_i (bag.count uf_i A)))
 435   //            (=>
 436   //             (and (>= i 1) (<= i preImageSize))
 437   //             (and
 438   //               (= (f uf_i) e)
 439   //               (>= count_uf_i 1)
 440   //               (= (sum i) (+ (sum (- i 1)) count_uf_i))
 441   //               (forall ((j Int))
 442   //                 (=>
 443   //                  (and (< i j) (<= j preImageSize))
 444   //                  (not (= (uf i) (uf j))))))
 445   //               )))))
 446
 447   BoundVarManager* bvm = d_nm->getBoundVarManager();
 448   Node i = bvm->mkBoundVar<FirstIndexVarAttribute>(n, "i", d_nm->integerType());
 449   Node j =
 450       bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType());
 451   Node iList = d_nm->mkNode(BOUND_VAR_LIST, i);
 452   Node jList = d_nm->mkNode(BOUND_VAR_LIST, j);
 453   Node iPlusOne = d_nm->mkNode(ADD, i, d_one);
 454   Node iMinusOne = d_nm->mkNode(SUB, i, d_one);
 455   Node uf_i = d_nm->mkNode(APPLY_UF, uf, i);
 456   Node uf_j = d_nm->mkNode(APPLY_UF, uf, j);
 457   Node f_uf_i = d_nm->mkNode(APPLY_UF, f, uf_i);
 458   Node uf_iPlusOne = d_nm->mkNode(APPLY_UF, uf, iPlusOne);
 459   Node uf_iMinusOne = d_nm->mkNode(APPLY_UF, uf, iMinusOne);
 460   Node interval_i = d_nm->mkNode(
 461       AND, d_nm->mkNode(GEQ, i, d_one), d_nm->mkNode(LEQ, i, preImageSize));
 462   Node sum_i = d_nm->mkNode(APPLY_UF, sum, i);
 463   Node sum_iPlusOne = d_nm->mkNode(APPLY_UF, sum, iPlusOne);
 464   Node sum_iMinusOne = d_nm->mkNode(APPLY_UF, sum, iMinusOne);
 465   Node count_iMinusOne = d_nm->mkNode(BAG_COUNT, uf_iMinusOne, A);
 466   Node count_uf_i = d_nm->mkNode(BAG_COUNT, uf_i, A);
 467   Node inductiveCase =
 468       d_nm->mkNode(EQUAL, sum_i, d_nm->mkNode(ADD, sum_iMinusOne, count_uf_i));
 469   Node f_iEqualE = d_nm->mkNode(EQUAL, f_uf_i, e);
 470   Node geqOne = d_nm->mkNode(GEQ, count_uf_i, d_one);
 471
 472   // i < j <= preImageSize
 473   Node interval_j = d_nm->mkNode(
 474       AND, d_nm->mkNode(LT, i, j), d_nm->mkNode(LEQ, j, preImageSize));
 475   // uf(i) != uf(j)
 476   Node uf_i_equals_uf_j = d_nm->mkNode(EQUAL, uf_i, uf_j);
 477   Node notEqual = d_nm->mkNode(EQUAL, uf_i, uf_j).negate();
 478   Node body_j = d_nm->mkNode(OR, interval_j.negate(), notEqual);
 479   Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j);
 480   Node andNode =
 481       d_nm->mkNode(AND, {f_iEqualE, geqOne, inductiveCase, forAll_j});
 482   Node body_i = d_nm->mkNode(OR, interval_i.negate(), andNode);
 483   Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
 484   Node preImageGTE_zero = d_nm->mkNode(GEQ, preImageSize, d_zero);
 485   Node conclusion = d_nm->mkNode(
 486       AND, {baseCase, totalSumEqualCountE, forAll_i, preImageGTE_zero});
 487   inferInfo.d_conclusion = conclusion;
 488
 489   std::map<Node, Node> m;
 490   m[e] = conclusion;
 491   Trace("bags::InferenceGenerator::mapDownwards")
 492       << "conclusion: " << inferInfo.d_conclusion << std::endl;
 493   return std::tuple(inferInfo, uf, preImageSize);
 494 }
 495
 496 InferInfo InferenceGenerator::mapUpwards(
 497     Node n, Node uf, Node preImageSize, Node y, Node x)
 498 {
 499   Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
 500   Assert(n[0].getType().isFunction()
 501          && n[0].getType().getArgTypes().size() == 1);
 502
 503   InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
 504   Node f = n[0];
 505   Node A = n[1];
 506
 507   Node countA = getMultiplicityTerm(x, A);
 508   Node xInA = d_nm->mkNode(GEQ, countA, d_one);
 509   Node notEqual = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, f, x), y).negate();
 510
 511   Node k = d_sm->mkDummySkolem("k", d_nm->integerType());
 512   Node inRange = d_nm->mkNode(
 513       AND, d_nm->mkNode(GEQ, k, d_one), d_nm->mkNode(LEQ, k, preImageSize));
 514   Node equal = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, uf, k), x);
 515   Node andNode = d_nm->mkNode(AND, inRange, equal);
 516   Node orNode = d_nm->mkNode(OR, notEqual, andNode);
 517   Node implies = d_nm->mkNode(IMPLIES, xInA, orNode);
 518   inferInfo.d_conclusion = implies;
 519   Trace("bags::InferenceGenerator::mapUpwards")
 520       << "conclusion: " << inferInfo.d_conclusion << std::endl;
 521   return inferInfo;
 522 }
 523
 524 InferInfo InferenceGenerator::filterDownwards(Node n, Node e)
 525 {
 526   Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
 527   Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType()));
 528
 529   Node P = n[0];
 530   Node A = n[1];
 531   InferInfo inferInfo(d_im, InferenceId::BAGS_FILTER_DOWN);
 532
 533   Node countA = getMultiplicityTerm(e, A);
 534   Node skolem = getSkolem(n, inferInfo);
 535   Node count = getMultiplicityTerm(e, skolem);
 536
 537   Node member = d_nm->mkNode(GEQ, count, d_one);
 538   Node pOfe = d_nm->mkNode(APPLY_UF, P, e);
 539   Node equal = count.eqNode(countA);
 540
 541   inferInfo.d_conclusion = pOfe.andNode(equal);
 542   inferInfo.d_premises.push_back(member);
 543   return inferInfo;
 544 }
 545
 546 InferInfo InferenceGenerator::filterUpwards(Node n, Node e)
 547 {
 548   Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
 549   Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType()));
 550
 551   Node P = n[0];
 552   Node A = n[1];
 553   InferInfo inferInfo(d_im, InferenceId::BAGS_FILTER_UP);
 554
 555   Node countA = getMultiplicityTerm(e, A);
 556   Node skolem = getSkolem(n, inferInfo);
 557   Node count = getMultiplicityTerm(e, skolem);
 558
 559   Node member = d_nm->mkNode(GEQ, countA, d_one);
 560   Node pOfe = d_nm->mkNode(APPLY_UF, P, e);
 561   Node equal = count.eqNode(countA);
 562   Node included = pOfe.andNode(equal);
 563   Node equalZero = count.eqNode(d_zero);
 564   Node excluded = pOfe.notNode().andNode(equalZero);
 565   inferInfo.d_conclusion = included.orNode(excluded);
 566   inferInfo.d_premises.push_back(member);
 567   return inferInfo;
 568 }
 569
 570 InferInfo InferenceGenerator::productUp(Node n, Node e1, Node e2)
 571 {
 572   Assert(n.getKind() == TABLE_PRODUCT);
 573   Node A = n[0];
 574   Node B = n[1];
 575   Node tuple = BagsUtils::constructProductTuple(n, e1, e2);
 576
 577   InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP);
 578
 579   Node countA = getMultiplicityTerm(e1, A);
 580   Node countB = getMultiplicityTerm(e2, B);
 581
 582   Node skolem = getSkolem(n, inferInfo);
 583   Node count = getMultiplicityTerm(tuple, skolem);
 584
 585   Node multiply = d_nm->mkNode(MULT, countA, countB);
 586   inferInfo.d_conclusion = count.eqNode(multiply);
 587
 588   return inferInfo;
 589 }
 590
 591 InferInfo InferenceGenerator::productDown(Node n, Node e)
 592 {
 593   Assert(n.getKind() == TABLE_PRODUCT);
 594   Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
 595
 596   Node A = n[0];
 597   Node B = n[1];
 598
 599   TypeNode tupleBType = B.getType().getBagElementType();
 600   TypeNode tupleAType = A.getType().getBagElementType();
 601   size_t tupleALength = tupleAType.getTupleLength();
 602   size_t productTupleLength = n.getType().getBagElementType().getTupleLength();
 603
 604   std::vector<Node> elements = TupleUtils::getTupleElements(e);
 605   Node a = TupleUtils::constructTupleFromElements(
 606       tupleAType, elements, 0, tupleALength - 1);
 607   Node b = TupleUtils::constructTupleFromElements(
 608       tupleBType, elements, tupleALength, productTupleLength - 1);
 609
 610   InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_DOWN);
 611
 612   Node countA = getMultiplicityTerm(a, A);
 613   Node countB = getMultiplicityTerm(b, B);
 614
 615   Node skolem = getSkolem(n, inferInfo);
 616   Node count = getMultiplicityTerm(e, skolem);
 617
 618   Node multiply = d_nm->mkNode(MULT, countA, countB);
 619   inferInfo.d_conclusion = count.eqNode(multiply);
 620
 621   return inferInfo;
 622 }
 623
 624 }  // namespace bags
 625 }  // namespace theory
 626 }  // namespace cvc5