1 files changed, 42 insertions, 12 deletions
diff --git a/src/theory/bags/bag_reduction.h b/src/theory/bags/bag_reduction.h
index 11f091f94..694379dfc 100644
--- a/src/theory/bags/bag_reduction.h
+++ b/src/theory/bags/bag_reduction.h
@@ -41,9 +41,8 @@ class BagReduction : EnvObj
    *        t: T2 is the initial value
    *        A: (Bag T1) is a bag
    * @param asserts a list of assertions generated by this reduction
-   * @return the reduction term (combine n) such that
-   * (and
-   *  (forall ((i Int))
+   * @return the reduction term (combine n) with asserts:
+   * - (forall ((i Int))
    *    (let ((iMinusOne (- i 1)))
    *      (let ((uf_i (uf i)))
    *        (=>
@@ -55,18 +54,49 @@ class BagReduction : EnvObj
    *              (bag.union_disjoint
    *                (bag uf_i 1)
    *                (unionDisjoint iMinusOne))))))))
-   *   (= (combine 0) t)
-   *   (= (unionDisjoint 0) (as bag.empty (Bag T1)))
-   *   (= A (unionDisjoint n))
-   *   (>= n 0))
-   *   where
-   *   n: Int is the cardinality of bag A
-   *   uf:Int -> T1 is an uninterpreted function that represents elements of A
-   *   combine: Int -> T2 is an uninterpreted function
-   *   unionDisjoint: Int -> (Bag T1) is an uninterpreted function
+   * - (= (combine 0) t)
+   * - (= (unionDisjoint 0) (as bag.empty (Bag T1)))
+   * - (= A (unionDisjoint n))
+   * - (>= n 0))
+   * where
+   * n: Int is the cardinality of bag A
+   * uf:Int -> T1 is an uninterpreted function that represents elements of A
+   * combine: Int -> T2 is an uninterpreted function
+   * unionDisjoint: Int -> (Bag T1) is an uninterpreted function
    */
   Node reduceFoldOperator(Node node, std::vector<Node>& asserts);
 
+  /**
+   * @param node a term of the form (bag.card A) where A: (Bag T) is a bag
+   * @param asserts a list of assertions generated by this reduction
+   * @return the reduction term (cardinality n) with asserts:
+   * - (forall ((i Int))
+   *    (let ((uf_i (uf i)))
+   *     (let ((count_uf_i (bag.count uf_i A)))
+   *      (=>
+   *       (and (>= i 1) (<= i n))
+   *       (and
+   *        (= (cardinality i) (+ count_uf_i (cardinality (- i 1))))
+   *        (=
+   *         (unionDisjoint i)
+   *         (bag.union_disjoint (bag uf_i count_uf_i) (unionDisjoint (- i 1))))
+   *        (forall ((j Int))
+   *                (or (not (and (< i j) (<= j n)))
+   *                    (not (= (uf i) (uf j))))))))))
+   * - (= (cardinality 0) 0)
+   * - (= (unionDisjoint 0) (as bag.empty (Bag String)))
+   * - (= A (unionDisjoint n))
+   * - (>= n 0)
+   *
+   * where
+   *   n: number of distinct elements in A
+   *   uf:Int -> T is an uninterpreted function that represents distinct
+   *             elements of A
+   *   cardinality: Int -> Int is an uninterpreted function
+   *   unionDisjoint: Int -> (Bag T1) is an uninterpreted function
+   */
+  Node reduceCardOperator(Node node, std::vector<Node>& asserts);
+
  private:
 };