z3 - Presburger 公式与 z3 的可满足性

Question

我正在使用 z3（Linux 上的 v4.3.2 32 位）来确定 Presburger 算术公式的可满足性，但我对以下公式有疑问：

(assert (forall ((x1 Int) (x2 Int) (x3 Int))
                  (=> (and (= x3 1) (= x1 (- x2))) 
                      (forall ((x4 Int) (x5 Int) (x6 Int)) 
                              (=> (= x6 x2) 
                                  (exists ((y Int)) 
                                          (=> (= x5 (+ x6 (- x4))) 
                                              (and (= (+ x1 x4) y) 
                                                   (= x5 (- y)) 
                                                   (= (+ x1 x4) (- x5))
                                              )
                                          )
                                  )
                              )
                      )
                  )
        )
)

(check-sat)

我很确定这个公式是可以满足的，但是 z3 回答“不满足”。事实上，如果我试着改变一下公式，z3 会回答“sat”，就像下面的公式一样

(assert (forall ((x3 Int) (x1 Int) (x2 Int))
                  (=> (and (= x3 1) (= x1 (- x2))) 
                      (forall ((x4 Int) (x5 Int) (x6 Int)) 
                              (=> (= x6 x2) 
                                  (exists ((y Int)) 
                                          (=> (= x5 (+ x6 (- x4))) 
                                              (and (= (+ x1 x4) y) 
                                                   (= x5 (- y)) 
                                                   (= (+ x1 x4) (- x5))
                                              )
                                          )
                                  )
                              )
                      )
                  )
        )
)

(check-sat)

我刚刚在第一个 forall 量化列表的顶部切换了 x3 上的量化。如果我还删除了实际上没用的 x3 变量，z3 也会回答“sat”。有什么我不明白的还是这是一个错误？

Answer 1

感谢您指出了这一点。这是量词消除模块中的一个错误，会影响嵌套量词的情况。它现在固定在不稳定的分支中。