z3 - 对 Z3 表达式的集合操作

Question

是否有定义集合操作的函数，例如 set, intersection, union, members等，超过 Z3 表达式？此外，是否有功能可以检查公式是 acnf还是dnf？

如果没有，我可以尝试在 z3utils 文件中实现它们。

Answer 1

我们可以使用 Python 集来编码表达式集。唯一的问题是__eq__Z3Py 表达式的运算符将构建一个新表达式，而不是比较表达式是否相等。为了解决这个问题，我们可以使用调用正确的比较 Z3 表达式的包装器。这是一个示例（可在rise4fun在线获得）。

class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)
    def __repr__(self):
        return str(self.n)

def askey(n):
    assert isinstance(n, AstRef)
    return AstRefKey(n)

x = Int('x')
s = set()
s.add(askey(x+1))
s.add(askey(x))
print s
print askey(x + 1) in s
s2 = set()
s2.add(askey(x+2))
s2.add(askey(x))
print s2
print s.union(s2)

唯一的不便是我们必须继续使用askey. 我们可以通过定义一个ASTSet包装 Python对象并为我们set调用的类来避免这种不便。askey

关于dnf和cnf识别器。此功能未在外部 API 中公开。