量词和数组在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) 

有没有一种方法，以获得正确的答案在这种情况下（“不饱和度”）？

编辑：如果向第二个连接添加例如约束(= ia_1 0)，则Z3正确回答“sat”。

Answer 1

这里，“未知”是一个“正确的”答案。一般来说，数组上的量词不是可确定的（至少不是在进一步的假设下）。 Z3放弃了这个例子，因为它的默认量词实例化试探法没有选择正确的实例化模式。欲了解更多信息，请参阅有关quantifiers in the Z3 tutorial的部分。

我们可以指定自己的实例化模式来帮助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))))      
         ))))) 

用较少的参数每个子量词，很可能是更好的，它会拿起一些有用的东西（我认为），但当然是意志并不总是够用的。