如何在 Z3py 中检查表达式是否包含条件 (=>)答案

【问题标题】：How to check in Z3py whether the expression contains a conditional (=>)如何在 Z3py 中检查表达式是否包含条件 (=>)
【发布时间】：2017-12-05 21:15:54
【问题描述】：

我正在使用 Z3py 来遍历布尔公式。如何检查公式是否包含条件。我检查了 z3.py 源代码，它包含 is_and()、is_or()、is_not()、.. 但与 is_implies() 没有任何关系。任何想法？谢谢。

【问题讨论】：

我不是z3 的专家，但a -> c 基本上是!a v c... 其中a 和c 可以是任何东西。例如 b v c 是 !b -> c 和 !c -> b，!a v !b v c 是 a -> (!b v c) 和 b -> (!a v c) 以及 !c -> (!a v !b) 和 (a & b) -> c 和 ...。所以is_or() 应该足够了，不是吗？
哦，我正在编写用于消除隐含的代码。所以首先我必须以某种方式解析代码包含含义（准确地说是条件）。然后我将 a => b 转换为 !a 或 b。谢谢。
我想这意味着您很高兴能够仅捕获明确的含义，而不是所有含义，因此我的评论无关紧要。 :)
感谢您的评论 :)

标签： z3 z3py

【解决方案1】：

您可以使用函数“is_app_of”来确定表达式的内置函数。因此，

def is_and(a):
    return is_app_of(a, Z3_OP_AND)

在 z3.py 文件中已经实现，类似

def is_implies(a):
    return is_app_of(a, Z3_OP_IMPLIES)

【讨论】：

谢谢。很高兴知道。