Z3的的Java API手柄量詞變量錯誤

Question

對於下面的公式 (declare-fun i() Int) (declare-fun @I() Int) (declare-fun r2() (Array Int Int)) (assert (= i 4)) (assert (forall ((@I Int)) (! (=> (and (>= @I 0) (< @I i)) (= (select r2 @I) 0)) :weight 10 :skolemid test :qid test))) (check-sat) (get-model)

Java API的回報：

SATISFIABLE (define-fun i() Int 4) (define-fun @I() Int (- 1))

爲什麼產生量詞變量 「@I」 特定的值？該@I聲明兩次

Answer 1

注：

(declare-fun @I() Int) 
... 
(assert (forall ((@I Int)) ... 

因此，這的確是雙方的，存在的和普遍的。我冒昧地將此複製到我們的issue tracker。正如在此討論的那樣，這不是一個錯誤：「在術語名稱空間內，綁定變量可以互相影響以及函數符號名稱......」是SMT2 standard所說的（備註2，第3.3節）。