使用Z3py可以計算Kauffman括號嗎？

Question

我正在嘗試使用Z3py來計算三葉草結的Kauffman支架。到現在爲止，我有以下代碼：

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確實不會在運營商的關聯性或交換性下執行替換。因此，替代（x * y * z，（x * z，u））不會簡化爲u * y。

Answer 2

解決方案使用減少：

請讓我知道，如果它是可以做到使用Z3PY同樣的事情。