1

有什么方法可以禁用 Z3（版本 4.8.8）中断言的简化/重写？

我目前正在 KeyY ( https://www.key-project.org ) 中对 Z3 证明进行证明重放。但是，为了能够重放 Z3 的“断言”规则，我需要在 Z3 的 SMT-LIB 输入中指定的确切断言，而不是它的简化版本。

作为可能发生的情况的一个极端示例，请考虑以下 SMT-LIB 输入：

(set-option :produce-proofs true)

(assert
  (not
    (forall ((y Int))
      (exists ((x Int))
        (= x (+ y 1))
      )
    )
  )
)
(check-sat)
(get-proof)

运行 Z3 4.8.8 会导致以下输出：

unsat
((proof
(asserted false)))

显然，断言已被简化，这使得证明没有真正的帮助。有没有办法完全禁用这种简化（从而从 Z3 获得“真实”证明，我可以在我们的工具中重播）？

4

1 回答 1

0

如果您使用更新版本的 z3，您可能会得到更好的服务。例如，给定您的示例，最近从 github-master 编译的版本会产生：

((proof
(let (($x88 (not true)))
 (let (($x48 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ 1 y)) :qid k!8))
  :qid k!9))
 ))
 (let (($x54 (not $x48)))
 (let ((@x36 (rewrite (= $x54 $x54))))
 (let (($x30 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ y 1)) :qid k!8))
  :qid k!9))
 ))
 (let (($x31 (not $x30)))
 (let ((@x32 (asserted $x31)))
 (let ((@x45 (mp (mp (mp @x32 (rewrite (= $x31 $x54)) $x54) @x36 $x54) @x36 $x54)))
 (let ((@x53 (mp (mp (mp @x45 @x36 $x54) @x36 $x54) (rewrite (= $x54 $x88)) $x88)))
 (mp @x53 (rewrite (= $x88 false)) false))))))))))))

格式仍然没有记录，一般来说，z3 很难在量词存在的情况下产生细粒度的证明。直接引用自：https ://theory.stanford.edu/~nikolaj/programmingz3.html#sec-proofs说：

证明对象的粒度是尽力而为的。SMT 核心的证明相对细粒度，而执行量词消除的过程的证明，例如第 6.4 节中描述的 QSAT，则暴露为大的不透明步骤。

于 2020-10-17T20:45:34.273 回答