如何使用意味着，如果在Z3的Python API

Question

布爾命令如何使用Z3 Python API中一階公式結合的部分實施if-then-else？例如

s.add(F, H, (if then else)). 

一個相關的問題是：如何使用布爾「暗示」或「如果」，在Z3蟒蛇在線指南給出了此目的的命令？

Answer 1

在編碼使用If(A, B, C)的Z3的Python API中的表達式if(A, B, C)。 下面是一個例子：在另一個實例中使用 「隱含」

F, H, A, B, C = Bools('F H A B C') 
s = Solver() 
s.add(F, H, Implies(A, B)) 
print s 

對於上面的實施例中的鏈接是

F, H, A, B, C = Bools('F H A B C') 
s = Solver() 
s.add(F, H, If(A, B, C)) 
print s 

這裏：http://rise4fun.com/Z3Py/4BF，http://rise4fun.com/Z3Py/JEU