python - 如何在 z3 python API 中使用 Implies 和 if 布尔命令

Question

如何if-then-else使用 Z3 python API 作为一阶公式结合的一部分来实现？例如

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

一个相关的问题是：如何为此目的使用 Z3 python 在线指南中给出的布尔“暗示”或“如果”命令？

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, If(A, B, C))
print s

这是另一个使用“暗示”的例子

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

上述示例的链接是：http : //rise4fun.com/Z3Py/4BF，http: //rise4fun.com/Z3Py/JEU