2 files changed, 18 insertions, 0 deletions
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,
 };