z3 - 可以使用 Z3py 计算 Kauffman 括号吗？

Question

我正在尝试使用 Z3py 计算三叶结的考夫曼括号。到目前为止，我有以下代码：

a, b, c, d, e, f, A, B = Ints('a b c d e f A B')

delta = Function('delta', IntSort(), IntSort(), IntSort())
def X(a,b,c,d):
    return A*delta(a,d)*delta(b,c)+B*delta(a,b)*delta(c,d)
Trefoil = X(a,d,b,e)*X(e,b,f,c)*X(c,f,d,a)  
print simplify(simplify(Trefoil, som= True),mul_to_power=True)

使用此代码，我获得以下输出：

A**3·
delta(a, e)·
delta(b, f)·
delta(c, a)·
delta(d, b)·
delta(e, c)·
delta(f, d) +
A**2·
B·
delta(a, d)·
delta(b, e)·
delta(b, f)·
delta(c, a)·
delta(e, c)·
delta(f, d) +
A**2·
B·
delta(a, e)·
delta(c, a)·
delta(d, b)·
delta(e, b)·
delta(f, c)·
delta(f, d) +
A·
B**2·
delta(a, d)·
delta(b, e)·
delta(c, a)·
delta(e, b)·
delta(f, c)·
delta(f, d) +
A**2·
B·
delta(a, e)·
delta(b, f)·
delta(c, f)·
delta(d, a)·
delta(d, b)·
delta(e, c) +
A·
B**2·
delta(a, d)·
delta(b, e)·
delta(b, f)·
delta(c, f)·
delta(d, a)·
delta(e, c) +
A·
B**2·
delta(a, e)·
delta(c, f)·
delta(d, a)·
delta(d, b)·
delta(e, b)·
delta(f, c) +
B**3·
delta(a, d)·
delta(b, e)·
delta(c, f)·
delta(d, a)·
delta(e, b)·
delta(f, c)

现在我需要应用规则：

delta(a,b)*delta(b,c) = delta(a,c)

并使用此类规则简化输出。拜托，你能告诉我怎么做吗？非常感谢。

Answer 1

您可以使用“替换”功能将子术语替换为其他术语。但是，在您的示例中，没有子项 delta(a,b) 或 delta(a,c) 因此替换将无效。请记住，Z3 在运算符的关联性或交换性下不执行替换。因此，substitute(x*y*z, (x*z, u)) 不会简化为 u*y。

Answer 2

使用 Reduce 的解决方案：

请让我知道是否可以使用 Z3PY 做同样的事情。