lojix/prolog/src/main/com/thesett/aima/logic/fol/prolog/builtins/PrologUnifier.java
protected boolean unifyVar(Variable leftVar, Term rightTerm, List<Variable> leftTrail, List<Variable> rightTrail)
    {
        /*log.fine("protected boolean unifyVar(Variable var = " + leftVar + ", Term term = " + rightTerm +
            ", List<Variable> trail = " + leftTrail + "): called");*/

        // Check if the variable is bound (in the trail, but no need to explicitly check the trail as the binding is
        // already held against the variable).
        if (leftVar.isBound())
        {
            /*log.fine("Variable is bound.");*/

            return unifyInternal(leftVar.getValue(), rightTerm, leftTrail, rightTrail);
        }
        else if (rightTerm.isVar() && ((Variable) rightTerm).isBound())
        {
            // The variable is free, but the term itself is a bound variable, in which case unify againt the value
            // of the term.
            /*log.fine("Term is a bound variable.");*/

            return unifyInternal(leftVar, rightTerm.getValue(), leftTrail, rightTrail);
        }
        else
        {
            // Otherwise, unify by binding the variable to the value of the term.
            /*log.fine("Variable is free, substituting in the term for it.");*/
            leftVar.setSubstitution(rightTerm);
            leftTrail.add(leftVar.getStorageCell(leftVar));
            //leftTrail.add(leftVar);

            return true;
        }

        // Occurs can go above if desired.
        /*else if (var occurs anywhere in x)
        {
            return false;
        }*/
    }
protected boolean unifyVar(Variable leftVar, Term rightTerm, List<Variable> leftTrail, List<Variable> rightTrail)
    {
        /*log.fine("protected boolean unifyVar(Variable var = " + leftVar + ", Term term = " + rightTerm +
            ", List<Variable> trail = " + leftTrail + "): called");*/

        // Check if the variable is bound (in the trail, but no need to explicitly check the trail as the binding is
        // already held against the variable).
        if (leftVar.isBound())
        {
            /*log.fine("Variable is bound.");*/

            return unifyInternal(leftVar.getValue(), rightTerm, leftTrail, rightTrail);
        }
        else if (rightTerm.isVar() && ((Variable) rightTerm).isBound())
        {
            // The variable is free, but the term itself is a bound variable, in which case unify againt the value
            // of the term.
            /*log.fine("Term is a bound variable.");*/

            return unifyInternal(leftVar, rightTerm.getValue(), leftTrail, rightTrail);
        }
        else
        {
            // Otherwise, unify by binding the variable to the value of the term.
            /*log.fine("Variable is free, substituting in the term for it.");*/
            leftVar.setSubstitution(rightTerm);
            leftTrail.add(leftVar.getStorageCell(leftVar));
            //leftTrail.add(leftVar);

            return true;
        }

        // Occurs can go above if desired.
        /*else if (var occurs anywhere in x)
        {
            return false;
        }*/
    }
protected boolean unifyVar ( Variable leftVar , Term rightTerm , List < Variable > leftTrail , List < Variable > rightTrail ) { /*log.fine("protected boolean unifyVar(Variable var = " + leftVar + ", Term term = " + rightTerm +
            ", List<Variable> trail = " + leftTrail + "): called");*/ // Check if the variable is bound (in the trail, but no need to explicitly check the trail as the binding is // already held against the variable). if ( leftVar . isBound ( ) ) { /*log.fine("Variable is bound.");*/ return unifyInternal ( leftVar . getValue ( ) , rightTerm , leftTrail , rightTrail ) ; } else if ( rightTerm . isVar ( ) && ( ( Variable ) rightTerm ) . isBound ( ) ) { // The variable is free, but the term itself is a bound variable, in which case unify againt the value // of the term. /*log.fine("Term is a bound variable.");*/ return unifyInternal ( leftVar , rightTerm . getValue ( ) , leftTrail , rightTrail ) ; } else { // Otherwise, unify by binding the variable to the value of the term. /*log.fine("Variable is free, substituting in the term for it.");*/ leftVar . setSubstitution ( rightTerm ) ; leftTrail . add ( leftVar . getStorageCell ( leftVar ) ) ; //leftTrail.add(leftVar); return true ; } // Occurs can go above if desired. /*else if (var occurs anywhere in x)
        {
            return false;
        }*/ }
Unifies a variable with a term. If the variable is bound, then the bound value is unified with the term. If the
term is a bound variable, and the variable is free, then the vairable is unified with the bound value of the
term. Otherwise, the variable is free and is bound to the value of the term.

@param  leftVar    The variable to unify.
@param  rightTerm  The term to unify against.
@param  leftTrail  The built up trail of substitutions in the left hand side.
@param  rightTrail The built up trail of substitutions in the right hand side.

@return <tt>true</tt> if the variable unifies with the term, <tt>false</tt> otherwise.
Unifies a variable with a term . If the variable is bound then the bound value is unified with the term . If the term is a bound variable and the variable is free then the vairable is unified with the bound value of the term . Otherwise the variable is free and is bound to the value of the term .