Z3中的量词和数组

Question

z3在使用数组上使用量词给出此代码时，用"未知"答案：

(declare-const ia Int)
(declare-const ib Int)
(declare-const la Int)
(declare-const lb Int)
(declare-const A (Array Int Int))
(declare-const a (Array Int Int))
(declare-const b (Array Int Int))
(assert 
    (exists 
        ((ia_1 Int) (ia_2 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int)))
        (and (= ia ia_2) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ia_1 0) (= ib_1 0) (< ia_1 la_0) (< ib_1 lb_0) (< (select a_0 ia_1) (select b_0 ib_1)) (= ia_2 (+ ia_1 1)))))
(assert 
    (not 
        (exists 
            ((ia_1 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int)))
            (and (= ia ia_1) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ib_1 0)))))
(check-sat)

在这种情况下，有没有办法获得正确的答案（" unsat"）？

编辑：z3用" sat"正确地回答，例如，将约束 (= ia_1 0)添加到第二个连词中。

Answer 1

在这里，"未知"是一个"正确"答案。通常，对数组的量词不是可决定的（至少不是在进一步的假设下）。Z3在此示例上放弃了，因为其默认量词实例化启发式方法不会拾取正确的实例化模式。有关更多信息，请参见Z3教程中的量词部分。

我们可以指定自己的实例化模式来帮助Z3，或者我们至少可以重述问题，以便启发式方法自动找到正确的模式。在这种情况下，我成功地重写了第二个量词：

(assert 
    (forall ((la_0 Int) (lb_0 Int) (A_0 (Array Int Int)))
            (and 
                (= A A_0) 
                (= la la_0) 
                (= lb lb_0)
                (forall ((b_0 (Array Int Int)) (ib_1 Int))
                    (and 
                        (= b b_0)
                        (= ib ib_1)
                        (= ib_1 0)
                        (forall ((a_0 (Array Int Int)) (ia_1 Int))
                            (not (and (= ia ia_1) (= a a_0))))                       
                        )))))

对每个子定量器的争论较少，很可能会选择有用的东西（我认为），但这当然并不总是足够的。