在Z3Py中,我需要使用标准语法term := const | var | f(t1,...,tn)
)检查某个词是否是一个术语。我已经编写了下面的函数来确定这一点,但是我的方法来检查n元函数是否看起来不是很理想。在
有更好的方法吗?这些函数是有用的。我会把它们放在贡献区
CONNECTIVE_OPS = [Z3_OP_NOT,Z3_OP_AND,Z3_OP_OR,Z3_OP_IMPLIES,Z3_OP_IFF,Z3_OP_ITE]
REL_OPS = [Z3_OP_EQ,Z3_OP_LE,Z3_OP_LT,Z3_OP_GE,Z3_OP_GT]
def is_term(a):
"""
term := const | var | f(t1,...,tn)
"""
if is_const(a):
return True
else:
r = (is_app(a) and \
a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \
all(is_term(c) for c in a.children()))
return r
一阶逻辑中使用的术语、原子和文字的“教科书”定义不能直接应用于Z3表达式。在Z3中,我们允许像
f(And(a, b)) > 0
和f(ForAll([x], g(x) == 0))
这样的表达式,其中f
是一个从布尔到整数的函数。这种扩展并没有增加表现力,但在编写问题时它们非常方便。SMT2.0标准还允许“term”if-then-else
表达式。这是另一个允许我们在“术语”中嵌套“公式”的功能。示例:g(If(And(a, b), 1, 0))
。在在实现操作Z3表达式的过程时,我们有时需要区分布尔表达式和非布尔表达式。在本例中,“term”只是一个没有布尔排序的表达式。在
在其他实例中,我们希望以一种特殊的方式处理布尔连接词(
^{pr2}$And
,Or
,…)。例如,我们定义了一个CNF转换器。在本例中,我们将“atom”定义为任何不是量词的布尔表达式、一个(自由)变量或一个不是布尔连接词的应用程序。在在我们定义原子之后,字面量可以定义为:
^{3}$下面是一个示例,演示了这些函数(也可以在rise4fun上在线获得):
功能合理,有几点意见:
这取决于您在规范中所说的“var”是什么意思。Z3的变量为de Brujin指数。“如果函数中有一个变量,则检查变量”。
还有另一个布尔连接词Z3\u-OP-XOR。
还有其他的关系操作,例如比较位向量的操作。 这取决于您的意图和代码的用法,但是您也可以检查 表达式的排序是布尔型的,如果是,请确保头函数符号是 没想到。
is_const(a)定义为返回is_app(a)和a.num_args()==0。所以is_const实际上是由默认情况处理的。
作为简化、解析或其他转换的结果,Z3创建的表达式可能有许多共享子表达式。因此,一个直接的递归下降可能需要指数时间的DAG大小的表达式。您可以通过维护已访问节点的哈希表来处理此问题。在Python中,可以使用Z3_get_ast_id来检索表达式的唯一编号,并将其保存在一个集合中。只要术语不是垃圾收集的,标识符是唯一的,因此 你应该把这样一个集合作为局部变量来维护。
所以,大致如下:
相关问题 更多 >
编程相关推荐