从 z3py 获取证据

Question

我一直在浏览 Z3Py 的文档，但对于我这样的人来说，我无法弄清楚如何从 Solver 获得证明（例如，如果我从 De Morgan 定律的一个实例开始，我该如何提取来自实例的 Z3Py 的证明，一步一步）。我看到的唯一参考是Solver 类中的proof(self)，如果启用了证明构造，它应该得到最后一次检查的证明，但我不断收到非常模糊的错误：

Traceback (most recent call last):
  File "example.py", line 36, in <module>
    prove(prop)
  File "example.py", line 15, in prove
    print(s.proof())
  File "src/api/python/z3.py", line 5851, in proof
  File "src/api/python/z3core.py", line 3770, in Z3_solver_get_proof
z3types.Z3Exception: 'invalid usage'`

所以我认为默认情况下禁用证明构造（可能是因为开销问题）。如何启用它？或者这甚至没有达到我认为应该的，通过逐步展示证明的推导，从像幂等这样简单的公理等？

更新：实际上，在尝试过之后，（相信我，我确保我的版本是 Microsoft 研究网站上的最新版本，甚至重建了它和所有) set_param 未定义：

>>> from z3 import *
>>> print [s for s in dir(z3) if 'set_param' in s]
['Z3_fixedpoint_set_params', 'Z3_set_param_value', 'Z3_solver_set_params']
>>> set_param
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'set_param' is not defined

我随后尝试使用Z3_set_param_value、Z3_solver_set_params，然后使用set_option(proof=True)（因为它在参考文献中被列为 set_param` 的别名）无济于事：

>>> set_option(proof=True)
Error setting 'PROOF', reason: unknown option.
terminate called after throwing an instance of 'z3_error'
Aborted (core dumped)

Answer 1

是的，您必须设置 proof=True 才能启用证明。此外，所有表达式都必须在启用证明的模式下创建。一种方法如下：

>>> set_param(proof=True)
>>> ctx = Context()
>>> s = Solver(ctx=ctx)
>>> x = Int('x', ctx=ctx)
>>> s.add(x > 0)
>>> s.add(x == 0)
>>> s.check()
unsat
>>> s.proof()
mp(mp(asserted(x > 0),
      rewrite((x > 0) == Not(x <= 0)),
      Not(x <= 0)),
   trans(monotonicity(trans(monotonicity(asserted(x == 0),
                                        (x <= 0) == (0 <= 0)),
                            rewrite((0 <= 0) == True),
                            (x <= 0) == True),
                      Not(x <= 0) == Not(True)),
         rewrite(Not(True) == False),
         Not(x <= 0) == False),
   False)

在这个例子中，我将证明模式设置为全局真。然后创建一个在创建表达式或求解器的任何地方传递的引用上下文。

如果您确保在任何其他调用 Z3 之前将证明模式设置为 True，那么您不必携带自己的上下文。换句话说，以下内容也有效：

python.exe
>>> from z3 import *
>>> set_param(proof=True)
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x == 0)
>>> s.check()
unsat
>>> s.proof() 
mp(mp(asserted(x > 0),
      rewrite((x > 0) == Not(x <= 0)),
      Not(x <= 0)),
   trans(monotonicity(trans(monotonicity(asserted(x == 0),
                                        (x <= 0) == (0 <= 0)),
                          rewrite((0 <= 0) == True),
                        (x <= 0) == True),
                  Not(x <= 0) == Not(True)),
     rewrite(Not(True) == False),
     Not(x <= 0) == False),
  False)