Z3 禁用证明的断言简化

Question

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

我目前正致力于在 Key (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 获得“真实”证明，我可以在我们的工具中重播）？

Answer 1

如果您使用更新版本的 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 核心，是相对细粒度的，而证明 执行量词消除的程序，例如 QSAT 第 6.4 节中描述的，暴露为大的不透明步骤。