سؤال

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.

هل كانت مفيدة؟

المحلول

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.

نصائح أخرى

Solution using Reduce:

enter image description here

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

مرخصة بموجب: CC-BY-SA مع الإسناد
لا تنتمي إلى StackOverflow
scroll top