时间戳

首页 > 解决方案 > seq.nth 在存在表达式中的奇怪行为

z3 - seq.nth 在存在表达式中的奇怪行为

问题描述

在此运行 z3

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

结果有UNSAT

但是跑步

(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 被视为函数上的变量？它不应该是一个常量函数（总是返回 seq 的索引值）吗？

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

帮助表示赞赏...

标签： z3smt

解决方案

该函数seq.nth未指定。也就是说，如果您查询超出范围的元素（即，在负索引处或在大于上一个的索引处），则可以自由地返回求解器想要的任何值。（并且求解器将始终选择一个值以使您的查询可满足。）

这是 SMTLib 的典型特征，当给定的参数不在其参数域中时，未指定的函数可以简单地取任何值。因此，z3 通过使用序列索引越界来告诉您存在这样的模型(seq.unit 0)。即，我们可以在某个负值或某个大于 的索引处对其进行索引0。

请注意，seq.nth_u模型中给出的值（注意_u后缀！）表示如何对下溢/上溢行为进行建模。它不应与函数的值混淆seq.nth。

x如果您将其设为顶级存在，您实际上可以让 z3 显示索引的值：

(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了预期。并且在使用序列时，您应该添加这些类型的约束（如果可能的话！）以避免越界访问。

推荐阅读