z3 - z3 を使用した Presburger Formulas の充足可能性

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 は "unsat" と答えます。実際、数式を少し変更しようとすると、次の数式のように、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

ご指摘ありがとうございます。これは、ネストされた量指定子のケースに影響する量指定子削除モジュールのバグです。現在、不安定版ブランチで修正されています。