public boolean unifyInternal ( Term left , Term right , List < Variable > leftTrail , List < Variable > rightTrail ) { /*log.fine("public boolean unifyInternal(Term left = " + left + ", Term right = " + right + ", List<Variable> trail = " + leftTrail + "): called");*/ if ( left == right ) { /*log.fine("Terms are identical objects.");*/ return true ; } if ( ! left . isVar ( ) && ! right . isVar ( ) && left . isConstant ( ) && right . isConstant ( ) && left . equals ( right ) ) { /*log.fine("Terms are equal atoms or literals.");*/ return true ; } else if ( left . isVar ( ) ) { /*log.fine("Left is a variable.");*/ return unifyVar ( ( Variable ) left , right , leftTrail , rightTrail ) ; } else if ( right . isVar ( ) ) { /*log.fine("Right is a variable.");*/ return unifyVar ( ( Variable ) right , left , rightTrail , leftTrail ) ; } else if ( left . isFunctor ( ) && right . isFunctor ( ) ) { /*log.fine("Terms are functors, at least one of which is not an atom.");*/ Functor leftFunctor = ( Functor ) left ; Functor rightFunctor = ( Functor ) right ; // Check if the functors may be not be equal (that is, they do not have the same name and arity), in // which case they cannot possibly be unified. if ( ! left . equals ( right ) ) { return false ; } /*log.fine("Terms are functors with same name and arity, both are compound.");*/ // Pairwise unify all of the arguments of the functor. int arity = leftFunctor . getArity ( ) ; for ( int i = 0 ; i < arity ; i ++ ) { Term leftArgument = leftFunctor . getArgument ( i ) ; Term rightArgument = rightFunctor . getArgument ( i ) ; boolean result = unifyInternal ( leftArgument , rightArgument , leftTrail , rightTrail ) ; if ( ! result ) { /*log.fine("Non unifying arguments in functors encountered, left = " + leftArgument + ", right = " + rightArgument);*/ return false ; } } return true ; } else { return false ; } }
Attempts to unify one term with another against a background of already unified variables in both terms . In the case where two terms are being unified from scratch the variable assignments will be empty .