Improve the quantified formula for bag map (cvc5#10713)

This PR forces the range [1,n] to only include elements in the bag A for
map terms (bag.map f A).

src/theory/bags/inference_generator.cpp

@@ -461,7 +461,6 @@ std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDown(Node n, Node e)
   Node f_iEqualE = d_nm->mkNode(Kind::EQUAL, f_uf_i, e);
   Node distinct = d_nm->mkNode(Kind::DISTINCT, f_uf_i, e);
   Node geqOne = d_nm->mkNode(Kind::GEQ, count_uf_i, d_one);
-  Node eqZero = d_nm->mkNode(Kind::EQUAL, count_uf_i, d_zero);
 
   // i < j <= size
   Node interval_j = d_nm->mkNode(Kind::AND,
@@ -472,12 +471,10 @@ std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDown(Node n, Node e)
   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 disjunct1 =
-      d_nm->mkNode(Kind::AND, {f_iEqualE, geqOne, addMultiplicity});
-  Node disjunct2 =
-      d_nm->mkNode(Kind::AND, {distinct, eqZero, previousValue});
+  Node disjunct1 = d_nm->mkNode(Kind::AND, {f_iEqualE, addMultiplicity});
+  Node disjunct2 = d_nm->mkNode(Kind::AND, {distinct, previousValue});
   Node orNode = disjunct1.orNode(disjunct2);
-  Node andNode = forAll_j.andNode(orNode);
+  Node andNode = d_nm->mkNode(Kind::AND, {forAll_j, geqOne, orNode});
   Node body_i = d_nm->mkNode(Kind::OR, interval_i.negate(), andNode);
   Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
   Node sizeGTE_zero = d_nm->mkNode(Kind::GEQ, size, d_zero);

src/theory/bags/inference_generator.h

@@ -243,18 +243,17 @@ class InferenceGenerator
    *                  (or
    *                   (not (and (< i j) (<= j size)))
    *                   (not (= (u i) (u j)))))
+   *          (>= count_u_i 1)
    *          (or
    *           (and
-   *            (= (f u_i) e)
-   *            (>= count_u_i 1)
+   *            (= (f u_i) e)            
    *            (= (sum i) (+ (sum (- i 1)) count_u_i))
    *            (forall ((j Int))
    *                    (or
    *                     (not (and (< i j) (<= j size)))
    *                     (not (= (u i) (u j))))))
    *           (and
-   *            (distinct (f u_i) e)
-   *            (= count_u_i 0)
+   *            (distinct (f u_i) e)   
    *            (= (sum i) (sum (- i 1)))))))))))
    * where uf: Int -> E is an uninterpreted function from integers to the
    * type of the elements of A,

test/regress/cli/CMakeLists.txt

@@ -3528,7 +3528,7 @@ set(regress_2_tests
   regress2/arith/uart-8.base.cvc.smtv1.smt2
   regress2/bags/injective_functions.smt2
   regress2/bags/map_bug.smt2
-  regress2/bags/pull_null.smt2
+  regress2/bags/reduce_constants_dup.smt2
   regress2/bug136.smtv1.smt2
   regress2/bug148.smtv1.smt2
   regress2/bug349.smtv1.smt2
@@ -3837,6 +3837,8 @@ set(regression_disabled_tests
   # previously sygus inference did not apply, now (correctly) times out
   regress1/sygus/issue3498.smt2
   regress2/arith/miplib-opt1217--27.smt2
+  # unknown answer after optimizing map formulas
+  regress2/bags/pull_null.smt2
   # times out after #7345
   regress2/bv_to_int_mask_array_1.smt2
   regress2/nl/dumortier-050317.smt2

test/regress/cli/regress2/bags/reduce_constants_dup.smt2

@@ -0,0 +1,31 @@
+; DISABLE-TESTER: alf
+; DISABLE-TESTER: lfsc
+; test name: testReduceConstantsDup2
+;Translating sql query: SELECT * FROM EMP AS EMP WHERE EMP.DEPTNO = 7 AND EMP.DEPTNO = 8 AND EMP.EMPNO = 10 AND EMP.MGR IS NULL AND EMP.EMPNO = 10
+;Translating sql query: SELECT 10 AS EMPNO, t0.ENAME, t0.JOB, CAST(NULL AS INT) AS MGR, t0.HIREDATE, t0.SAL, t0.COMM, t0.DEPTNO, t0.SLACKER FROM (SELECT * FROM EMP WHERE FALSE) AS t0
+(set-logic HO_ALL)
+(set-info :status unsat)
+(set-option :dag-thresh 0)
+(set-option :uf-lazy-ll true)
+(set-option :fmf-bound true)
+(set-option :tlimit-per 10000)
+(set-option :strings-exp true)
+
+(declare-const EMP (Bag (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int))))
+(declare-const q1 (Bag (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int))))
+(declare-const q2 (Bag (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int))))
+(declare-const p2 (-> (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)) Bool))
+(declare-const p3 (-> (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)) Bool))
+(declare-const nullableOr (-> (Nullable Bool) (Nullable Bool) (Nullable Bool)))
+(declare-const nullableAnd (-> (Nullable Bool) (Nullable Bool) (Nullable Bool)))
+(declare-const f4 (-> (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)) (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int))))
+(assert (= nullableAnd (lambda ((x (Nullable Bool)) (y (Nullable Bool))) (ite (and (nullable.is_null x) (= y (nullable.some false))) (nullable.some false) (ite (and (= x (nullable.some false)) (nullable.is_null y)) (nullable.some false) (ite (and (nullable.is_null x) (= y (nullable.some true))) (as nullable.null (Nullable Bool)) (ite (and (= x (nullable.some true)) (nullable.is_null y)) (as nullable.null (Nullable Bool)) (nullable.some (and (nullable.val x) (nullable.val y))))))))))
+(assert (= nullableOr (lambda ((x (Nullable Bool)) (y (Nullable Bool))) (ite (and (nullable.is_null x) (= y (nullable.some true))) (nullable.some true) (ite (and (= x (nullable.some true)) (nullable.is_null y)) (nullable.some true) (ite (and (nullable.is_null x) (= y (nullable.some false))) (as nullable.null (Nullable Bool)) (ite (and (= x (nullable.some false)) (nullable.is_null y)) (as nullable.null (Nullable Bool)) (nullable.some (or (nullable.val x) (nullable.val y))))))))))
+(assert (= p2 (lambda ((t (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)))) (and (nullable.is_some (nullableAnd (nullableAnd (nullableAnd (nullableAnd (nullable.lift (lambda ((BOUND_VARIABLE_549341 Int) (BOUND_VARIABLE_549342 Int)) (= BOUND_VARIABLE_549341 BOUND_VARIABLE_549342)) ((_ tuple.select 7) t) (nullable.some 7)) (nullable.lift (lambda ((BOUND_VARIABLE_549347 Int) (BOUND_VARIABLE_549348 Int)) (= BOUND_VARIABLE_549347 BOUND_VARIABLE_549348)) ((_ tuple.select 7) t) (nullable.some 8))) (nullable.lift (lambda ((BOUND_VARIABLE_549354 Int) (BOUND_VARIABLE_549355 Int)) (= BOUND_VARIABLE_549354 BOUND_VARIABLE_549355)) ((_ tuple.select 0) t) (nullable.some 10))) (nullable.some (nullable.is_null ((_ tuple.select 3) t)))) (nullable.lift (lambda ((BOUND_VARIABLE_549363 Int) (BOUND_VARIABLE_549364 Int)) (= BOUND_VARIABLE_549363 BOUND_VARIABLE_549364)) ((_ tuple.select 0) t) (nullable.some 10)))) (nullable.val (nullableAnd (nullableAnd (nullableAnd (nullableAnd (nullable.lift (lambda ((BOUND_VARIABLE_549341 Int) (BOUND_VARIABLE_549342 Int)) (= BOUND_VARIABLE_549341 BOUND_VARIABLE_549342)) ((_ tuple.select 7) t) (nullable.some 7)) (nullable.lift (lambda ((BOUND_VARIABLE_549347 Int) (BOUND_VARIABLE_549348 Int)) (= BOUND_VARIABLE_549347 BOUND_VARIABLE_549348)) ((_ tuple.select 7) t) (nullable.some 8))) (nullable.lift (lambda ((BOUND_VARIABLE_549354 Int) (BOUND_VARIABLE_549355 Int)) (= BOUND_VARIABLE_549354 BOUND_VARIABLE_549355)) ((_ tuple.select 0) t) (nullable.some 10))) (nullable.some (nullable.is_null ((_ tuple.select 3) t)))) (nullable.lift (lambda ((BOUND_VARIABLE_549363 Int) (BOUND_VARIABLE_549364 Int)) (= BOUND_VARIABLE_549363 BOUND_VARIABLE_549364)) ((_ tuple.select 0) t) (nullable.some 10))))))))
+(assert (= p3 (lambda ((t (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)))) (and (nullable.is_some (nullable.some false)) (nullable.val (nullable.some false))))))
+(assert (not (= q1 q2)))
+(assert (= (nullable.val (as nullable.null (Nullable Bool))) false))
+(assert (= f4 (lambda ((t (Tuple (Nullable Int) (Nullable String) (Nullable String) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int) (Nullable Int)))) (tuple (nullable.some 10) ((_ tuple.select 1) t) ((_ tuple.select 2) t) (as nullable.null (Nullable Int)) ((_ tuple.select 4) t) ((_ tuple.select 6) t) ((_ tuple.select 5) t) ((_ tuple.select 7) t) ((_ tuple.select 8) t)))))
+(assert (= q1 ((_ table.project 0 1 2 3 4 5 6 7 8) (bag.filter p2 EMP))))
+(assert (= q2 (bag.map f4 (bag.filter p3 EMP))))
+(check-sat)