Z3给序列指定的错误模型

Question

我在https://rise4fun.com/Z3/中放置了以下代码

(declare-const s (Seq Int))
(declare-const t1 (Seq Int))
(declare-const t2 (Seq Int))
(declare-const n Int)

(assert (= (seq.len s) n))
(assert (>= n 3))
(assert (= (seq.extract s 0 (- n 1)) t1))
(assert (= (seq.extract s 1 (- n 1)) t2))
(assert (= t1 t2))
;;(assert (not (= (seq.at s 0) (seq.at s (- n 1)))))

(check-sat)
(get-model)

结果是

sat
(model 
  (define-fun s () (Seq Int)
    (seq.++ (seq.unit 14) (seq.++ (seq.unit 16) (seq.unit 18))))
  (define-fun t2 () (Seq Int)
    (seq.++ (seq.unit 16) (seq.unit 18)))
  (define-fun n () Int
    3)
  (define-fun t1 () (Seq Int)
    (seq.++ (seq.unit 16) (seq.unit 18)))
)

此模型是错误的。 (seq.extract s 0 (- n 1))应该是[14; 16]而不是[16; 18]。

我误解了什么还是Z3的错误？

Answer 1

自z3的rise4fun版本发布以来，顺序逻辑在z3中发生了很多变化，修复了许多错误。使用最新版本，我得到：

sat
(model
  (define-fun s () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4) (seq.unit 4)))
  (define-fun t2 () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4)))
  (define-fun t1 () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4)))
  (define-fun n () Int
    3)
)

对我来说看起来正确。

长话短说：rise4fun的z3版本对于这个问题来说太旧了，而且有很多错误。查看您是否可以从https://github.com/Z3Prover/z3/releases

下载较新的版本（甚至每晚构建）