1 files changed, 53 insertions, 0 deletions
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