是否有定义集合操作的函数,例如 set, intersection, union, members
等,超过 Z3 表达式?此外,是否有功能可以检查公式是 acnf
还是dnf
?
如果没有,我可以尝试在 z3utils 文件中实现它们。
是否有定义集合操作的函数,例如 set, intersection, union, members
等,超过 Z3 表达式?此外,是否有功能可以检查公式是 acnf
还是dnf
?
如果没有,我可以尝试在 z3utils 文件中实现它们。
我们可以使用 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 中公开。