从 z3py 获取证据 [英] Getting proof from z3py

问题描述

我一直在浏览 Z3Py 的文档，对于我这样的人，我无法弄清楚如何从求解器中获得证明(例如，如果我从德摩根定律的一个实例开始，我如何提取来自实例的 Z3Py 的证明，一步一步).我看到的唯一参考是 proof(self) 在 Solver 类中，如果启用了证明构造，它应该会获得上次检查的证明，但我一直在找回非常模糊的错误:

回溯(最近一次调用最后一次): 中的文件example.py"，第 36 行证明(道具)文件example.py"，第 15 行，证明打印(s.proof())文件src/api/python/z3.py"，第 5851 行，证明Z3_solver_get_proof 中的文件src/api/python/z3core.py"，第 3770 行z3types.Z3Exception: '无效使用'`

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

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

<预><代码>>>>从 z3 导入 *>>>打印 [s for s in dir(z3) if 'set_param' in s]['Z3_fixedpoint_set_params', 'Z3_set_param_value', 'Z3_solver_set_params']>>>设置参数回溯(最近一次调用最后一次):文件<stdin>"，第 1 行，在 <module> 中NameError: name 'set_param' 未定义

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

<预><代码>>>>设置选项(证明=真)设置PROOF"时出错，原因:未知选项.抛出z3_error"实例后调用终止中止(核心转储)

解决方案

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

<预><代码>>>>设置参数(证明=真)>>>ctx = 上下文()>>>s = 求解器(ctx=ctx)>>>x = Int('x', ctx=ctx)>>>s.add(x > 0)>>>s.add(x == 0)>>>s.check()未满足>>>s.proof()mp(mp(断言(x > 0)，重写((x > 0) == Not(x <= 0)),不(x <= 0)),反式(单调性(反式(单调性(断言(x == 0)，(x <= 0) == (0 <= 0)),重写((0 <= 0)==真)，(x <= 0) == 真),不(x <= 0)== 不(真))，重写(不(真)==假)，不(x <= 0) == False),错误的)

在此示例中，我将证明模式全局设置为 true.然后创建一个引用上下文，该上下文在所有创建表达式或求解器的地方都传递.

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

python.exe>>>从 z3 导入 *>>>设置参数(证明=真)>>>x = Int('x')>>>s = 求解器()>>>s.add(x > 0)>>>s.add(x == 0)>>>s.check()未满足>>>s.proof()mp(mp(断言(x > 0)，重写((x > 0) == Not(x <= 0)),不(x <= 0)),反式(单调性(反式(单调性(断言(x == 0)，(x <= 0) == (0 <= 0)),重写((0 <= 0)==真)，(x <= 0) == 真),不(x <= 0)== 不(真))，重写(不(真)==假)，不(x <= 0) == False),错误的)

I've been skimming through the documentation of Z3Py and for the likes of me have not been able to figure out how to get the proof from a Solver (E.g. if I start from an instance of De Morgan's Laws how can I extract the proof from Z3Py of the instance, step by step). The only reference I saw was for proof(self) in the Solver class which supposedly gets the proof of the last check if proof construction is enabled, but I keep getting back the very vague error:

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'`

So I figure proof construction is disabled by default (probably because of an overhead concern). How do I enable it? Or does this not even achieve what I think it should, by showing a derivation of a proof, step-by-step, from axioms as simple as Idempotency, etc?

Update: Actually, upon trying it, (and believe me, I made sure my version was the latest from the Microsoft Research Website, and even rebuilt it and all) set_param is undefined:

>>> 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

I subsequently tried using Z3_set_param_value, Z3_solver_set_params, and then set_option(proof=True) (because it was listed as an alias for set_param` in the reference) to no avail:

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

解决方案

Yes, you have to set proof=True to enable proofs. Moreover, all expressions have to be created in a mode where proofs are enabled. One way to do this is as follows:

>>> 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)

In this example, I set the proof mode globally true. Then create a reference context that is passed everywhere expressions or solvers are created.

If you make sure to set the proof mode to True before any other calls into Z3, then you don't have to carry your own context. In other words, the following also works:

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 获取证据的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！