从 z3py 获取证据

Question

我一直在浏览 Z3Py 的文档，像我这样的人一直无法弄清楚如何从求解器获得证明（例如，如果我从 De Morgan 定律的一个实例开始，怎么能我从实例的 Z3Py 中提取证明，一步一步）。我看到的唯一参考是 Solver class 中的 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'`

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

Update：实际上，在尝试时，（相信我，我确保我的版本是 Microsoft Research 的最新版本网站，甚至重建它和所有）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)

从 z3py 获取证据

Getting proof from z3py

python

z3

z3py