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

【问题标题】：How to use Implies and if boolean commands in z3 python API如何在 z3 python API 中使用 Implies 和 if 布尔命令
【发布时间】：2012-08-05 13:55:24
【问题描述】：

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

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

一个相关的问题是：如何使用 Z3 python 在线指南中给出的布尔“Implies”或“if”命令来实现此目的？

【问题讨论】：

标签： python python-2.7 z3

【解决方案1】：

在 Z3 Python API 中使用 If(A, B, C) 编码的表达式 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

【讨论】：