如何使用 Z3 python API 实现 if-then-else 作为一阶公式合取的一部分？例如
s.add( F, H, (if then else)).
一个相关的问题是:如何使用 Z3 python 在线指南中给出的 bool “Implies”或“if”命令来实现此目的？
最佳答案
使用 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
这是使用“implies”的另一个示例
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
关于python - 如何在 z3 python API 中使用 Implies 和 if bool 命令，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/11817007/