1

我正在尝试使用Why3 的​​ Z3 后端来检索模型，然后这些模型可用于派生显示程序错误的测试用例。然而，Z3 版本 4.3.2 似乎无法回答sat任何 Why3 目标。看起来Why3 使用的一些公理化定义以某种方式混淆了 Z3。例如，下面的例子（这是 Why3 生成的一小部分）

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)

结果timeout如下命令行：

z3 -smt2 model.partial=true file.smt2 -T:10

另一方面，将定义更改为

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

会给我一个模型（看起来很合理）

(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)

但是如果我尝试添加原始Why3文件中存在的下一个公理，即

;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))

Z3 再次回答timeout。

Z3的配置中是否缺少我的东西？此外，在以前的Why3 版本中，有一个选项MODEL_ON_TIMEOUT，允许在这种情况下检索模型。尽管不能保证这是一个真实的模型，因为 Z3 无法完成检查，但实际上这些模型通常包含我需要的所有信息。但是，我在 4.3.2 中没有找到类似的选项。它还存在吗？

更新最后一个公理Abs_pos是错误的（我在此处发布之前对Why3 的​​输出进行了一些玩弄，最终粘贴了该问题的错误版本）。现在已修复。

4

1 回答 1

0

附加公理

(assert (not (forall ((x Int)) (<= 0 (abs1 x))))))

使问题无法解决，因为 abs1 总是返回一个非负整数，并且使用附加公理，您需要某些 x 的 abs1 存在负结果。Z3 的网页版按预期返回 unsat，请参见此处。

于 2015-02-24T09:43:20.500 回答