#NEWLINE# def _unify_terms( a , b , bindings = None , used = None ) : #NEWLINE# #INDENT# '\n    This method attempts to unify two terms.  Two expressions are unifiable\n    if there exists a substitution function S such that S(a) == S(-b).\n\n    :param a: ``Expression``\n    :param b: ``Expression``\n    :param bindings: ``BindingDict`` a starting set of bindings with which\n    the unification must be consistent\n    :return: ``BindingDict`` A dictionary of the bindings required to unify\n    :raise ``BindingException``: If the terms cannot be unified\n    ' #NEWLINE# assert isinstance ( a , Expression ) #NEWLINE# assert isinstance ( b , Expression ) #NEWLINE# if ( bindings is None ) : #NEWLINE# #INDENT# bindings = BindingDict ( ) #NEWLINE# #UNINDENT# if ( used is None ) : #NEWLINE# #INDENT# used = ( [ ] , [ ] ) #NEWLINE# #UNINDENT# if ( isinstance ( a , NegatedExpression ) and isinstance ( b , ApplicationExpression ) ) : #NEWLINE# #INDENT# newbindings = most_general_unification ( a . term , b , bindings ) #NEWLINE# newused = ( ( used [ 0 ] + [ a ] ) , ( used [ 1 ] + [ b ] ) ) #NEWLINE# unused = ( [ ] , [ ] ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if ( isinstance ( a , ApplicationExpression ) and isinstance ( b , NegatedExpression ) ) : #NEWLINE# #INDENT# newbindings = most_general_unification ( a , b . term , bindings ) #NEWLINE# newused = ( ( used [ 0 ] + [ a ] ) , ( used [ 1 ] + [ b ] ) ) #NEWLINE# unused = ( [ ] , [ ] ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( a , EqualityExpression ) : #NEWLINE# #INDENT# newbindings = BindingDict ( [ ( a . first . variable , a . second ) ] ) #NEWLINE# newused = ( ( used [ 0 ] + [ a ] ) , used [ 1 ] ) #NEWLINE# unused = ( [ ] , [ b ] ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( b , EqualityExpression ) : #NEWLINE# #INDENT# newbindings = BindingDict ( [ ( b . first . variable , b . second ) ] ) #NEWLINE# newused = ( used [ 0 ] , ( used [ 1 ] + [ b ] ) ) #NEWLINE# unused = ( [ a ] , [ ] ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# raise BindingException ( ( a , b ) ) #NEWLINE# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# return ( newbindings , newused , unused )