如何使用s.proof（）在z3中獲得完整的證明？

如果證明過長，s.proof（）只能打印部分。有沒有其他可用的功能，我們可以得到完整的證據。如何使用s.proof（）在z3中獲得完整的證明？

我使用下面的代碼

from z3 import * 
set_param(proof=True) 
. 
. 

. 
. 
if unsat==s.check(): 
    s.proof()

請指引我。

2016-07-05 Tom

's.proof（）''返回ExprRef'，這顯然有一些允許通過其元素（在樹組織）行走方法的一個實例。因此，您可以爲此對象編寫自己的打印功能。 –

非常感謝......正在工作 – Tom

如果您已經編寫了代碼，您應該添加一個包含它的答案並將其作爲正確答案接受，以便將來可以幫助其他人。 ;） –

from z3 import * 
set_param(proof=True) 
. 
. 

. 
. 
if unsat==s.check(): 
    print s.proof().children()

可打印完整的證明

2016-07-05 23:21:56 Tom

回答