It is possible to compute the Kauffman bracket using Z3py?

Question

I am trying to compute the Kauffman bracket of the trefoil knot using Z3py. Until now I have the following code:

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)

with this code I am obtaining the following output:

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)

Now I need to apply the rule:

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

and to simplify the output using such rule. Please, could you tell me how to do it. Many thanks.

Answer 1

You can use the function "substitute" to replace sub-terms by others. However, on your example, there is no sub-term delta(a,b) or delta(a,c) so substitution will have no effect. Bear in mind that Z3 does not perform substitution under associativity or commutativity of operators. So substitute(x*y*z, (x*z, u)) does not simplify to u*y.

Answer 2

Solution using Reduce:

Please let me know if it is possible to do the same thing using Z3PY.