1

在 Z3Py 中，我需要使用标准语法检查某事是否是一个术语term := const | var | 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
4

2 回答 2

1

功能是否合理，几点评论：

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

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

  3. 还有其他关系操作，例如比较位向量的操作。这取决于您的意图和代码的使用，但您也可以检查表达式的类型是否为布尔值，以及是否确保头函数符号未被解释。

  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, {})
于 2013-01-03T16:10:47.113 回答
1

一阶逻辑中使用的术语、原子和文字的“教科书”定义不能直接应用于 Z3 表达式。在 Z3 中，我们允许诸如f(And(a, b)) > 0and之类的表达式f(ForAll([x], g(x) == 0))，其中f是从 Boolean 到 Integer 的函数。这个扩展并没有增加表现力，但是在写问题的时候非常方便。SMT 2.0 标准还允许“术语”if-then-else表达式。这是另一个允许我们将“公式”嵌套在“术语”中的功能。示例：g(If(And(a, b), 1, 0))。

在实现操作 Z3 表达式的过程时，我们有时需要区分布尔表达式和非布尔表达式。在这种情况下，“术语”只是一个没有布尔排序的表达式。

def is_term(a):
   return not is_bool(a)

在其他情况下，我们希望以特殊方式处理布尔连接词 ( And, Or, ...)。例如，我们正在定义一个 CNF 转换器。在这种情况下，我们将“原子”定义为任何不是量词的布尔表达式，是（自由）变量或不是布尔连接词之一的应用程序。

def is_atom(a):
   return is_bool(a) and (is_var(a) or (is_app(a) and a.decl().kind() not in CONNECTIVE_OPS))

在我们定义了一个原子之后，一个字面量可以定义为：

def is_literal(a):
   return is_atom(a) or (is_not(a) and is_atom(a.arg(0)))

这是一个演示这些功能的示例（也可以在rise4fun在线获得）：

x = Int('x')
p, q = Bools('p q')   
f = Function('f', IntSort(), BoolSort())   
g = Function('g', IntSort(), IntSort())
print is_literal(Not(x > 0))    
print is_literal(f(x))
print is_atom(Not(x > 0))
print is_atom(f(x))
print is_atom(x)
print is_term(f(x))
print is_term(g(x))
print is_term(x)
print is_term(Var(1, IntSort()))
于 2013-01-03T16:22:23.300 回答