From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Mon, 25 Oct 2021 16:36:35 +0000 (-0500)
Subject: Add inference for count map (#7264)
X-Git-Tag: cvc5-1.0.0~985
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e28a3a86f45e012e59751b0091760f5e2baebd6;p=cvc5.git

Add inference for count map (#7264)
---

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index c06f016c4..80626fbc6 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -54,6 +54,8 @@ const char* toString(SkolemFunId id)
     case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
     case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
     case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
+    case SkolemFunId::BAGS_MAP_PREIMAGE: return "BAGS_MAP_PREIMAGE";
+    case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM";
     case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
     default: return "?";
   }
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1d35fa4b5..90e935767 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -51,6 +51,22 @@ enum class SkolemFunId
    * i = 0, ..., n.
    */
   RE_UNFOLD_POS_COMPONENT,
+  /** An uninterpreted function for bag.map operator:
+   * To compute (bag.count y (map f A)), we need to find the distinct
+   * elements in A that are mapped to y by function f (i.e., preimage of {y}).
+   * If n is the cardinality of this preimage, then
+   * the preimage is the set {uf(1), ..., uf(n)}
+   * where uf: Int -> E is a skolem function, and E is the type of elements of A
+   */
+  BAGS_MAP_PREIMAGE,
+  /** An uninterpreted function for bag.map operator:
+   * If the preimage of {y} in A is {uf(1), ..., uf(n)} (see BAGS_MAP_PREIMAGE},
+   * then the multiplicity of an element y in a bag (map f A) is sum(n),
+   * where sum: Int -> Int is a skolem function such that:
+   * sum(0) = 0
+   * sum(i) = sum (i-1) + (bag.count (uf i) A)
+   */
+  BAGS_MAP_SUM,
   /** Higher-order type match predicate, see HoTermDb */
   HO_TYPE_MATCH_PRED,
 };
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7c813cee0..2ea4987ec 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1350,8 +1350,6 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
         Notice() << "Disabling bound finite-model finding since it is "
                     "incompatible with HOL.\n";
       }
-
-      opts.quantifiers.fmfBound = false;
       Trace("smt") << "turning off fmf-bound, since HOL\n";
     }
   }
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 203903d88..341798eb2 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -31,8 +31,16 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-BagSolver::BagSolver(SolverState& s, InferenceManager& im, TermRegistry& tr)
-    : d_state(s), d_ig(&s, &im), d_im(im), d_termReg(tr)
+BagSolver::BagSolver(Env& env,
+                     SolverState& s,
+                     InferenceManager& im,
+                     TermRegistry& tr)
+    : EnvObj(env),
+      d_state(s),
+      d_ig(&s, &im),
+      d_im(im),
+      d_termReg(tr),
+      d_mapCache(userContext())
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -69,6 +77,7 @@ void BagSolver::postCheck()
         case kind::DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break;
         case kind::DIFFERENCE_REMOVE: checkDifferenceRemove(n); break;
         case kind::DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break;
+        case kind::BAG_MAP: checkMap(n); break;
         default: break;
       }
       it++;
@@ -210,6 +219,34 @@ void BagSolver::checkDisequalBagTerms()
   }
 }
 
+void BagSolver::checkMap(Node n)
+{
+  Assert(n.getKind() == BAG_MAP);
+  const set<Node>& downwards = d_state.getElements(n);
+  const set<Node>& upwards = d_state.getElements(n[1]);
+  for (const Node& y : downwards)
+  {
+    if (d_mapCache.count(n) && d_mapCache[n].get()->contains(y))
+    {
+      continue;
+    }
+    auto [downInference, uf, preImageSize] = d_ig.mapDownwards(n, y);
+    d_im.lemmaTheoryInference(&downInference);
+    for (const Node& x : upwards)
+    {
+      InferInfo upInference = d_ig.mapUpwards(n, uf, preImageSize, y, x);
+      d_im.lemmaTheoryInference(&upInference);
+    }
+    if (!d_mapCache.count(n))
+    {
+      std::shared_ptr<context::CDHashSet<Node> > set =
+          std::make_shared<context::CDHashSet<Node> >(userContext());
+      d_mapCache.insert(n, set);
+    }
+    d_mapCache[n].get()->insert(y);
+  }
+}
+
 }  // namespace bags
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index 5fb49fab7..9155c93d0 100644
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -13,7 +13,10 @@
  * Solver for the theory of bags.
  */
 
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "cvc5_private.h"
+#include "smt/env_obj.h"
 
 #ifndef CVC5__THEORY__BAG__SOLVER_H
 #define CVC5__THEORY__BAG__SOLVER_H
@@ -31,10 +34,10 @@ class TermRegistry;
 /** The solver for the theory of bags
  *
  */
-class BagSolver
+class BagSolver : protected EnvObj
 {
  public:
-  BagSolver(SolverState& s, InferenceManager& im, TermRegistry& tr);
+  BagSolver(Env& env, SolverState& s, InferenceManager& im, TermRegistry& tr);
   ~BagSolver();
 
   void postCheck();
@@ -73,6 +76,8 @@ class BagSolver
   void checkNonNegativeCountTerms(const Node& bag, const Node& element);
   /** apply inference rules for disequal bag terms */
   void checkDisequalBagTerms();
+  /** apply inference rules for map operator */
+  void checkMap(Node n);
 
   /** The solver state object */
   SolverState& d_state;
@@ -82,6 +87,14 @@ class BagSolver
   InferenceManager& d_im;
   /** Reference to the term registry of theory of bags */
   TermRegistry& d_termReg;
+
+  /** a cache that stores bags of kind BAG_MAP and those element representatives
+   * which we generated their inferences.
+   */
+  using BagElementsMap =
+      context::CDHashMap<Node, std::shared_ptr<context::CDHashSet<Node> > >;
+  BagElementsMap d_mapCache;
+
   /** Commonly used constants */
   Node d_true;
   Node d_false;
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 646bb28cf..0be83fb13 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -532,7 +532,8 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const
     case MK_BAG:
     {
       Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]);
-      Node ret = d_nm->mkNode(MK_BAG, mappedElement, n[1][0]);
+      Node ret =
+          d_nm->mkBag(n[0].getType().getRangeType(), mappedElement, n[1][1]);
       return BagsRewriteResponse(ret, Rewrite::MAP_MK_BAG);
     }
 
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 556dc76d6..734572f7c 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -20,6 +20,7 @@
 #include "expr/skolem_manager.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/uf/equality_engine.h"
 #include "util/rational.h"
 
@@ -42,7 +43,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
   Assert(n.getType().isBag());
   Assert(e.getType() == n.getType().getBagElementType());
 
-  InferInfo inferInfo(d_im, InferenceId::BAG_NON_NEGATIVE_COUNT);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
   Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);
 
   Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
@@ -59,7 +60,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
   {
     // TODO issue #78: refactor this with BagRewriter
     // (=> true (= (bag.count e (bag e c)) c))
-    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG_SAME_ELEMENT);
+    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
     Node skolem = getSkolem(n, inferInfo);
     Node count = getMultiplicityTerm(e, skolem);
     inferInfo.d_conclusion = count.eqNode(n[1]);
@@ -70,7 +71,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
     // (=>
     //   true
     //   (= (bag.count e (bag x c)) (ite (= e x) c 0)))
-    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG);
+    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG);
     Node skolem = getSkolem(n, inferInfo);
     Node count = getMultiplicityTerm(e, skolem);
     Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
@@ -81,6 +82,27 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
   }
 }
 
+/**
+ * A bound variable corresponding to the universally quantified integer
+ * variable used to range over the distinct elements in a bag, used
+ * for axiomatizing the behavior of some term.
+ */
+struct FirstIndexVarAttributeId
+{
+};
+typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute;
+
+/**
+ * A bound variable corresponding to the universally quantified integer
+ * variable used to range over the distinct elements in a bag, used
+ * for axiomatizing the behavior of some term.
+ */
+struct SecondIndexVarAttributeId
+{
+};
+typedef expr::Attribute<SecondIndexVarAttributeId, Node>
+    SecondIndexVarAttribute;
+
 struct BagsDeqAttributeId
 {
 };
@@ -93,7 +115,7 @@ InferInfo InferenceGenerator::bagDisequality(Node n)
   Node A = n[0];
   Node B = n[1];
 
-  InferInfo inferInfo(d_im, InferenceId::BAG_DISEQUALITY);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_DISEQUALITY);
 
   TypeNode elementType = A.getType().getBagElementType();
   BoundVarManager* bvm = d_nm->getBoundVarManager();
@@ -126,7 +148,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e)
   Assert(n.getKind() == kind::EMPTYBAG);
   Assert(e.getType() == n.getType().getBagElementType());
 
-  InferInfo inferInfo(d_im, InferenceId::BAG_EMPTY);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
   Node skolem = getSkolem(n, inferInfo);
   Node count = getMultiplicityTerm(e, skolem);
 
@@ -142,7 +164,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_DISJOINT);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_DISJOINT);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -164,7 +186,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_MAX);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_MAX);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -187,7 +209,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo(d_im, InferenceId::BAG_INTERSECTION_MIN);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_INTERSECTION_MIN);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -208,7 +230,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_SUBTRACT);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_SUBTRACT);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -230,7 +252,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
 
   Node A = n[0];
   Node B = n[1];
-  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_REMOVE);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_REMOVE);
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -251,7 +273,7 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
   Assert(e.getType() == n[0].getType().getBagElementType());
 
   Node A = n[0];
-  InferInfo inferInfo(d_im, InferenceId::BAG_DUPLICATE_REMOVAL);
+  InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL);
 
   Node countA = getMultiplicityTerm(e, A);
   Node skolem = getSkolem(n, inferInfo);
@@ -270,6 +292,137 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
   return count;
 }
 
+std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
+                                                                   Node e)
+{
+  Assert(n.getKind() == kind::BAG_MAP && n[1].getType().isBag());
+  Assert(n[0].getType().isFunction()
+         && n[0].getType().getArgTypes().size() == 1);
+  Assert(e.getType() == n[0].getType().getRangeType());
+
+  InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
+
+  Node f = n[0];
+  Node A = n[1];
+  // declare an uninterpreted function uf: Int -> T
+  TypeNode domainType = f.getType().getArgTypes()[0];
+  TypeNode ufType = d_nm->mkFunctionType(d_nm->integerType(), domainType);
+  Node uf =
+      d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE, ufType, {n, e});
+
+  // declare uninterpreted function sum: Int -> Int
+  TypeNode sumType =
+      d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType());
+  Node sum = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_SUM, sumType, {n, e});
+
+  // (= (sum 0) 0)
+  Node sum_zero = d_nm->mkNode(kind::APPLY_UF, sum, d_zero);
+  Node baseCase = d_nm->mkNode(Kind::EQUAL, sum_zero, d_zero);
+
+  // guess the size of the preimage of e
+  Node preImageSize = d_sm->mkDummySkolem("preImageSize", d_nm->integerType());
+
+  // (= (sum preImageSize) (bag.count e skolem))
+  Node mapSkolem = getSkolem(n, inferInfo);
+  Node countE = getMultiplicityTerm(e, mapSkolem);
+  Node totalSum = d_nm->mkNode(kind::APPLY_UF, sum, preImageSize);
+  Node totalSumEqualCountE = d_nm->mkNode(kind::EQUAL, totalSum, countE);
+
+  // (forall ((i Int))
+  //        (let ((uf_i (uf i)))
+  //          (let ((count_uf_i (bag.count uf_i A)))
+  //            (=>
+  //             (and (>= i 1) (<= i preImageSize))
+  //             (and
+  //               (= (f uf_i) e)
+  //               (>= count_uf_i 1)
+  //               (= (sum i) (+ (sum (- i 1)) count_uf_i))
+  //               (forall ((j Int))
+  //                 (=>
+  //                  (and (< i j) (<= j preImageSize))
+  //                  (not (= (uf i) (uf j))))))
+  //               )))))
+
+  BoundVarManager* bvm = d_nm->getBoundVarManager();
+  Node i = bvm->mkBoundVar<FirstIndexVarAttribute>(n, "i", d_nm->integerType());
+  Node j =
+      bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType());
+  Node iList = d_nm->mkNode(kind::BOUND_VAR_LIST, i);
+  Node jList = d_nm->mkNode(kind::BOUND_VAR_LIST, j);
+  Node iPlusOne = d_nm->mkNode(kind::PLUS, i, d_one);
+  Node iMinusOne = d_nm->mkNode(kind::MINUS, i, d_one);
+  Node uf_i = d_nm->mkNode(kind::APPLY_UF, uf, i);
+  Node uf_j = d_nm->mkNode(kind::APPLY_UF, uf, j);
+  Node f_uf_i = d_nm->mkNode(kind::APPLY_UF, f, uf_i);
+  Node uf_iPlusOne = d_nm->mkNode(kind::APPLY_UF, uf, iPlusOne);
+  Node uf_iMinusOne = d_nm->mkNode(kind::APPLY_UF, uf, iMinusOne);
+  Node interval_i = d_nm->mkNode(kind::AND,
+                                 d_nm->mkNode(kind::GEQ, i, d_one),
+                                 d_nm->mkNode(kind::LEQ, i, preImageSize));
+  Node sum_i = d_nm->mkNode(kind::APPLY_UF, sum, i);
+  Node sum_iPlusOne = d_nm->mkNode(kind::APPLY_UF, sum, iPlusOne);
+  Node sum_iMinusOne = d_nm->mkNode(kind::APPLY_UF, sum, iMinusOne);
+  Node count_iMinusOne = d_nm->mkNode(kind::BAG_COUNT, uf_iMinusOne, A);
+  Node count_uf_i = d_nm->mkNode(kind::BAG_COUNT, uf_i, A);
+  Node inductiveCase = d_nm->mkNode(
+      Kind::EQUAL, sum_i, d_nm->mkNode(kind::PLUS, sum_iMinusOne, count_uf_i));
+  Node f_iEqualE = d_nm->mkNode(kind::EQUAL, f_uf_i, e);
+  Node geqOne = d_nm->mkNode(kind::GEQ, count_uf_i, d_one);
+
+  // i < j <= preImageSize
+  Node interval_j = d_nm->mkNode(kind::AND,
+                                 d_nm->mkNode(kind::LT, i, j),
+                                 d_nm->mkNode(kind::LEQ, j, preImageSize));
+  // uf(i) != uf(j)
+  Node uf_i_equals_uf_j = d_nm->mkNode(kind::EQUAL, uf_i, uf_j);
+  Node notEqual = d_nm->mkNode(kind::EQUAL, uf_i, uf_j).negate();
+  Node body_j = d_nm->mkNode(kind::OR, interval_j.negate(), notEqual);
+  Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j);
+  Node andNode =
+      d_nm->mkNode(kind::AND, {f_iEqualE, geqOne, inductiveCase, forAll_j});
+  Node body_i = d_nm->mkNode(kind::OR, interval_i.negate(), andNode);
+  Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
+  Node preImageGTE_zero = d_nm->mkNode(kind::GEQ, preImageSize, d_zero);
+  Node conclusion = d_nm->mkNode(
+      kind::AND, {baseCase, totalSumEqualCountE, forAll_i, preImageGTE_zero});
+  inferInfo.d_conclusion = conclusion;
+
+  std::map<Node, Node> m;
+  m[e] = conclusion;
+  return std::tuple(inferInfo, uf, preImageSize);
+}
+
+InferInfo InferenceGenerator::mapUpwards(
+    Node n, Node uf, Node preImageSize, Node y, Node x)
+{
+  Assert(n.getKind() == kind::BAG_MAP && n[1].getType().isBag());
+  Assert(n[0].getType().isFunction()
+         && n[0].getType().getArgTypes().size() == 1);
+
+  InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
+  Node f = n[0];
+  Node A = n[1];
+
+  Node countA = getMultiplicityTerm(x, A);
+  Node xInA = d_nm->mkNode(kind::GEQ, countA, d_one);
+  Node notEqual =
+      d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f, x), y).negate();
+
+  Node k = d_sm->mkDummySkolem("k", d_nm->integerType());
+  Node inRange = d_nm->mkNode(kind::AND,
+                              d_nm->mkNode(kind::GEQ, k, d_one),
+                              d_nm->mkNode(kind::LEQ, k, preImageSize));
+  Node equal =
+      d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, uf, k), x);
+  Node andNode = d_nm->mkNode(kind::AND, inRange, equal);
+  Node orNode = d_nm->mkNode(kind::OR, notEqual, andNode);
+  Node implies = d_nm->mkNode(kind::IMPLIES, xInA, orNode);
+  inferInfo.d_conclusion = implies;
+  std::cout << "Upwards conclusion: " << inferInfo.d_conclusion << std::endl
+            << std::endl;
+  return inferInfo;
+}
+
 }  // namespace bags
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index 252b9641e..ab3a84b29 100644
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -164,6 +164,59 @@ class InferenceGenerator
    * where skolem is a fresh variable equals (duplicate_removal A)
    */
   InferInfo duplicateRemoval(Node n, Node e);
+  /**
+   * @param n is (bag.map f A) where f is a function (-> E T), A a bag of type
+   * (Bag E)
+   * @param e is a node of Type E
+   * @return an inference that represents the following implication
+   * (and
+   *   (= (sum 0) 0)
+   *   (= (sum preImageSize) (bag.count e skolem))
+   *   (>= preImageSize 0)
+   *   (forall ((i Int))
+   *          (let ((uf_i (uf i)))
+   *            (let ((count_uf_i (bag.count uf_i A)))
+   *              (=>
+   *               (and (>= i 1) (<= i preImageSize))
+   *               (and
+   *                 (= (f uf_i) e)
+   *                 (>= count_uf_i 1)
+   *                 (= (sum i) (+ (sum (- i 1)) count_uf_i))
+   *                 (forall ((j Int))
+   *                   (or
+   *                     (not (and (< i j) (<= j preImageSize)))
+   *                     (not (= (uf i) (uf j)))) )
+   *                 ))))))
+   * where uf: Int -> E is an uninterpreted function from integers to the
+   * type of the elements of A
+   * preImageSize is the cardinality of the distinct elements in A that are
+   * mapped to e by function f (i.e., preimage of {e})
+   * sum: Int -> Int is a function that aggregates the multiplicities of the
+   * preimage of e,
+   * and skolem is a fresh variable equals (bag.map f A))
+   */
+  std::tuple<InferInfo, Node, Node> mapDownwards(Node n, Node e);
+
+  /**
+   * @param n is (bag.map f A) where f is a function (-> E T), A a bag of type
+   * (Bag E)
+   * @param uf is an uninterpreted function Int -> E
+   * @param preImageSize is the cardinality of the distinct elements in A that
+   * are mapped to y by function f (i.e., preimage of {y})
+   * @param y is an element of type T
+   * @param e is an element of type E
+   * @return an inference that represents the following implication
+   * (=>
+   *   (>= (bag.count x A) 1)
+   *   (or
+   *     (not (= (f x) y)
+   *     (and
+   *       (>= skolem 1)
+   *       (<= skolem preImageSize)
+   *       (= (uf skolem) x)))))
+   * where skolem is a fresh variable
+   */
+  InferInfo mapUpwards(Node n, Node uf, Node preImageSize, Node y, Node x);
 
   /**
    * @param element of type T
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 58445de59..69401b3fa 100644
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -159,7 +159,7 @@ Node NormalForm::evaluateBinaryOperation(const TNode& n,
   // handle the remaining elements from A
   remainderOfA(elements, elementsA, itA);
   // handle the remaining elements from B
-  remainderOfA(elements, elementsB, itB);
+  remainderOfB(elements, elementsB, itB);
 
   Trace("bags-evaluate") << "elements: " << elements << std::endl;
   Node bag = constructConstantBagFromElements(n.getType(), elements);
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 4a6d345e9..f10144255 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -36,7 +36,7 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
       d_statistics(),
       d_rewriter(&d_statistics.d_rewrites),
       d_termReg(env, d_state, d_im),
-      d_solver(d_state, d_im, d_termReg)
+      d_solver(env, d_state, d_im, d_termReg)
 {
   // use the official theory state and inference manager objects
   d_theoryState = &d_state;
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index af753dd26..5439e7549 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -103,18 +103,19 @@ const char* toString(InferenceId i)
       return "ARRAYS_CONST_ARRAY_DEFAULT";
     case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY";
 
-    case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
-    case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
-    case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG";
-    case InferenceId::BAG_EQUALITY: return "BAG_EQUALITY";
-    case InferenceId::BAG_DISEQUALITY: return "BAG_DISEQUALITY";
-    case InferenceId::BAG_EMPTY: return "BAG_EMPTY";
-    case InferenceId::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT";
-    case InferenceId::BAG_UNION_MAX: return "BAG_UNION_MAX";
-    case InferenceId::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN";
-    case InferenceId::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT";
-    case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
-    case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
+    case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT";
+    case InferenceId::BAGS_MK_BAG_SAME_ELEMENT: return "BAGS_MK_BAG_SAME_ELEMENT";
+    case InferenceId::BAGS_MK_BAG: return "BAGS_MK_BAG";
+    case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY";
+    case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY";
+    case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY";
+    case InferenceId::BAGS_UNION_DISJOINT: return "BAGS_UNION_DISJOINT";
+    case InferenceId::BAGS_UNION_MAX: return "BAGS_UNION_MAX";
+    case InferenceId::BAGS_INTERSECTION_MIN: return "BAGS_INTERSECTION_MIN";
+    case InferenceId::BAGS_DIFFERENCE_SUBTRACT: return "BAGS_DIFFERENCE_SUBTRACT";
+    case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE";
+    case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL";
+    case InferenceId::BAGS_MAP: return "BAGS_MAP";
 
     case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
     case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA:
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 70f70e717..f6a689cf6 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -168,18 +168,19 @@ enum class InferenceId
   // ---------------------------------- end arrays theory
 
   // ---------------------------------- bags theory
-  BAG_NON_NEGATIVE_COUNT,
-  BAG_MK_BAG_SAME_ELEMENT,
-  BAG_MK_BAG,
-  BAG_EQUALITY,
-  BAG_DISEQUALITY,
-  BAG_EMPTY,
-  BAG_UNION_DISJOINT,
-  BAG_UNION_MAX,
-  BAG_INTERSECTION_MIN,
-  BAG_DIFFERENCE_SUBTRACT,
-  BAG_DIFFERENCE_REMOVE,
-  BAG_DUPLICATE_REMOVAL,
+  BAGS_NON_NEGATIVE_COUNT,
+  BAGS_MK_BAG_SAME_ELEMENT,
+  BAGS_MK_BAG,
+  BAGS_EQUALITY,
+  BAGS_DISEQUALITY,
+  BAGS_EMPTY,
+  BAGS_UNION_DISJOINT,
+  BAGS_UNION_MAX,
+  BAGS_INTERSECTION_MIN,
+  BAGS_DIFFERENCE_SUBTRACT,
+  BAGS_DIFFERENCE_REMOVE,
+  BAGS_DUPLICATE_REMOVAL,
+  BAGS_MAP,
   // ---------------------------------- end bags theory
 
   // ---------------------------------- bitvector theory
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5b3f3b729..c248d2231 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1569,9 +1569,14 @@ set(regress_1_tests
   regress1/bags/duplicate_removal1.smt2
   regress1/bags/duplicate_removal2.smt2
   regress1/bags/emptybag1.smt2
+  regress1/bags/fuzzy1.smt2
+  regress1/bags/fuzzy2.smt2
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
+  regress1/bags/map1.smt2
+  regress1/bags/map2.smt2
+  regress1/bags/map3.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
   regress1/bags/union_disjoint.smt2
diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2
new file mode 100644
index 000000000..f9fee0ec4
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int) ; c here is zero
+(assert
+  (and
+    (= b (difference_subtract b a)) ; b is empty
+    (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|}
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2
new file mode 100644
index 000000000..31da47f53
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy2.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+  (let ((D (bag d c))) ; when c = zero, then D is empty
+    (and
+      (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty
+      (= a (union_max a D))
+      (= a (difference_subtract a (bag d 1)))
+      (= a (union_disjoint a D))
+      (= a (intersection_min a D)))))
+(check-sat)
diff --git a/test/regress/regress1/bags/map.smt2 b/test/regress/regress1/bags/map.smt2
deleted file mode 100644
index 54d671415..000000000
--- a/test/regress/regress1/bags/map.smt2
+++ /dev/null
@@ -1,12 +0,0 @@
-(set-logic ALL)
-(set-info :status sat)
-(declare-fun A () (Bag Int))
-(declare-fun B () (Bag Int))
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun f (Int) Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= B (bag.map f A)))
-(assert (distinct (f x) (f y) x y))
-(check-sat)
diff --git a/test/regress/regress1/bags/map1.smt2 b/test/regress/regress1/bags/map1.smt2
new file mode 100644
index 000000000..54d671415
--- /dev/null
+++ b/test/regress/regress1/bags/map1.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun f (Int) Int)
+(assert (= A (union_max (bag x 1) (bag y 2))))
+(assert (= A (union_max (bag x 1) (bag y 2))))
+(assert (= B (bag.map f A)))
+(assert (distinct (f x) (f y) x y))
+(check-sat)
diff --git a/test/regress/regress1/bags/map2.smt2 b/test/regress/regress1/bags/map2.smt2
new file mode 100644
index 000000000..faed04caa
--- /dev/null
+++ b/test/regress/regress1/bags/map2.smt2
@@ -0,0 +1,9 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(declare-fun f (Int) Int)
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(check-sat)
diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2
new file mode 100644
index 000000000..637815fa5
--- /dev/null
+++ b/test/regress/regress1/bags/map3.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(define-fun f ((x Int)) Int (+ x 1))
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(assert (= A (as emptybag (Bag Int)) ))
+(check-sat)