python - 检查公式是否为 Z3Py 中的项

Question

在 Z3Py 中，我需要使用标准语法检查某项是否是术语 term := const |变量 | f(t1,...,tn))。我已经编写了以下函数来确定这一点，但我检查 n 元函数是否的方法似乎不是很理想。

有更好的方法吗？这些实用函数 is_term、is_atom、is_literal 等如果包含在 Z3 中将会很有用。我会将它们放在贡献部分

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

Answer 1

功能合理，几点评论:

1. 这取决于您的规范中“var”的含义。 Z3 具有作为 de-Brujin 指数的变量。 z3py中有一个函数“is_var(a)”来检查“a”是否是变量索引。

2. 还有另一个 bool 连接词 Z3_OP_XOR。

3. 还有其他关系运算，例如比较位向量的运算。这取决于您的意图和代码的使用，但您也可以检查是否表达式的排序是 bool 型，如果是则保证头函数符号是未解释。

4. is_const(a) 定义为 return is_app(a) 且 a.num_args() == 0。因此 is_const 确实由默认情况处理。

5. Z3 由于简化、解析或其他转换而创建的表达式可能有许多共享子表达式。因此，直接递归下降可能会花费表达式 DAG 大小的指数时间。您可以通过维护已访问节点的哈希表来处理此问题。在 Python 中，您可以使用 Z3_get_ast_id 检索表达式的唯一编号并将其维护在集合中。只要术语不被垃圾收集，标识符就是唯一的，因此您应该将这样的集合维护为局部变量。

所以，大致如下:

 def get_expr_id(e):
     return Z3_get_ast_id(e.ctx.ref(), e.ast)

 def is_term_aux(a, seen):
    if get_expr_id(a) in seen:
        return True
    else:
        seen[get_expr_id(a)] = True
        r = (is_app(a) and \
             a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \
             all(is_term_aux(c, seen) for c in a.children()))
        return r

 def is_term(a):
     return is_term_aux(a, {})