Z3py?를 사용하여 Kauffman 브래킷을 계산할 수 있습니까?

Question

나는 Z3py를 사용하여 trefoil 매듭의 Kauffman 브래킷을 계산하려고합니다.

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

및 단순화 :

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) 

지금 내가 규칙을 적용 할 필요가 : 나는 다음과 같은 출력을 취득하고이 코드

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) 

: 지금까지 나는 다음과 같은 코드가 있습니다 그러한 규칙을 사용하는 출력. 제발, 어떻게하는지 말해 줄 수 있어요. 많은 감사합니다.

Answer 1

"대체"기능을 사용하여 하위 용어를 다른 것으로 대체 할 수 있습니다. 그러나 귀하의 예에서는 하위 용어 델타 (a, b) 또는 델타 (a, c) 이 없으므로 대체 할 수 없습니다. Z3은 연산자의 결합 또는 commutativity에서 대체를 수행하지 않는다는 것을 명심하십시오. 그래서 substitute (x * y * z, (x * z, u))는 u * y로 단순화되지 않습니다. 감소하여

Answer 2

솔루션 :

Z3PY를 사용하여 같은 일을 할 수있는 경우 알려 주시기 바랍니다.