exist-expression中seq.nth的奇怪行为。

Question

在这上面运行z3

(assert (< (seq.nth (seq.unit 0) 0) 0))
(check-sat)

有联合国卫星图像作为结果

但是运行

(assert (exists ((x Int))
  (< (seq.nth (seq.unit 0) x) 0)))

(check-sat)
(get-model)

是SAT。从模型上看

(model 
  (define-fun seq.nth_u ((x!0 Seq) (x!1 Int)) Int
    (- 1))
)

那么，这是不是意味着seq.nth被当作一个Function上的变量？它是不是应该是一个常量函数（总是返回seq的索引值）？

我希望第二种情况也是UNSAT。为了实现这一点，我如何使seq.nth成为一个非变量函数？

感谢帮助...

Answer 1

函数 seq.nth 是欠规格的。也就是说，如果你查询的元素是越界的（也就是说，要么是负索引，要么是比上一个索引大的索引），那么它可以自由地返回解算器想要的任何值。而且解算器总是会选取一个值来使你的查询可以满足）。

这就是典型的SMTLib，在SMTLib中，当给定的参数不在其参数域内时，欠指定的函数可以简单地取任何值。所以，z3是通过使用序列索引出界来告诉你有这样一个模型。(seq.unit 0).也就是说，我们可以把它的指数定为某个负值，或者是某个指数大于 0.

请注意 seq.nth_u 模型中给出的（注意 _u 后缀!)表示如何对下溢流行为进行建模。它不应该与函数 seq.nth.

实际上，你可以让z3显示索引的值。x 如果你把它作为一个顶层的存在。

(declare-fun x () Int)

(assert (< (seq.nth (seq.unit 0) x) 0))

(check-sat)
(get-value (x))

对于这个，z3说：

sat
((x (- 1)))

就是说，索引的位置 -1. 但不要把它与 -1 你在解释中看到的 seq.nth_u. 事实上，如果我们还加上。

(assert (> x 0))

那么z3说：

sat
((x 1))

但是，如果我们加上：

(assert (>= x 0))
(assert (<  x 1))

那么我们得到 unsat 的访问。而在处理序列时，你应该添加这类约束（如果可能的话！）以避免越界访问。