I use the next unification lib.
from unification import *
x1 = var('x1')
unify((x1, 1), x1) # {~x1: (~x1, 1)}
Can you please suggest how to eliminate such circular solutions (~x1 references to itself)? For my particular task it is not a solution. unify should return False.
How it can be a solution? ((x1, 1), 1) is not eq (x1, 1)
If it is not possible to do in library itself. Can you please suggest an algorithm to track such circular references? Example of another solution to reject:
{~x1: (~s1_1, (~s1_2, ~s1_3)),
~x2: (~s1_1, ~s1_2),
~x3: (~s1_1, ~s1_3),
~s1_1: ~i1,
~i1: (~x3, ~s1_3),
~i2: (~s1_2, ~s1_3),
~s1_2: (~x3, ~s1_3)}
~x3: (~s1_1, ~s1_3) -> ~x3: (~i1, ~s1_3) -> ~x3: ((~x3, ~s1_3), ~s1_3)