public Optional < ImmutableSubstitution < ImmutableTerm > > computeDirectedMGU ( ImmutableTerm sourceTerm , ImmutableTerm targetTerm ) { /* * Variable */ if ( sourceTerm instanceof Variable ) { Variable sourceVariable = ( Variable ) sourceTerm ; // Constraint if ( ( targetTerm instanceof ImmutableFunctionalTerm ) && ( ( ImmutableFunctionalTerm ) targetTerm ) . getVariables ( ) . contains ( sourceVariable ) ) { return Optional . empty ( ) ; } ImmutableSubstitution < ImmutableTerm > substitution = sourceVariable . equals ( targetTerm ) ? substitutionFactory . getSubstitution ( ) : substitutionFactory . getSubstitution ( ImmutableMap . of ( sourceVariable , targetTerm ) ) ; return Optional . of ( substitution ) ; } /* * Functional term */ else if ( sourceTerm instanceof ImmutableFunctionalTerm ) { ImmutableFunctionalTerm sourceFunctionalTerm = ( ImmutableFunctionalTerm ) sourceTerm ; if ( targetTerm instanceof Variable ) { Variable targetVariable = ( Variable ) targetTerm ; // Constraint if ( sourceFunctionalTerm . getVariables ( ) . contains ( targetVariable ) ) { return Optional . empty ( ) ; } else { ImmutableSubstitution < ImmutableTerm > substitution = substitutionFactory . getSubstitution ( ImmutableMap . of ( targetVariable , sourceTerm ) ) ; return Optional . of ( substitution ) ; } } else if ( targetTerm instanceof ImmutableFunctionalTerm ) { return computeDirectedMGUOfTwoFunctionalTerms ( ( ImmutableFunctionalTerm ) sourceTerm , ( ImmutableFunctionalTerm ) targetTerm ) ; } else { return Optional . empty ( ) ; } } /* * Constant */ else if ( sourceTerm instanceof Constant ) { if ( targetTerm instanceof Variable ) { Variable targetVariable = ( Variable ) targetTerm ; ImmutableSubstitution < ImmutableTerm > substitution = substitutionFactory . getSubstitution ( ImmutableMap . of ( targetVariable , sourceTerm ) ) ; return Optional . of ( substitution ) ; } else if ( sourceTerm . equals ( targetTerm ) ) { return Optional . of ( substitutionFactory . getSubstitution ( ) ) ; } else { return Optional . empty ( ) ; } } else { throw new RuntimeException ( "Unexpected term: " + sourceTerm + " (" + sourceTerm . getClass ( ) + ")" ) ; } }
Computes a MGU that reuses as much as possible the variables from the target part .