private void nestedEQSubstitutions ( Function atom , Substitution mgu ) { List < Term > terms = atom . getTerms ( ) ; for ( int i = 0 ; i < terms . size ( ) ; i ++ ) { Term t = terms . get ( i ) ; if ( t instanceof Function ) { Function t2 = ( Function ) t ; substitutionUtilities . applySubstitution ( t2 , mgu ) ; //in case of equalities do the substitution and remove the term if ( t2 . getFunctionSymbol ( ) == ExpressionOperation . EQ && ! ( ( atom . getTerm ( 0 ) instanceof Function ) && ( atom . getTerm ( 1 ) instanceof Function ) ) ) { if ( ! mgu . composeTerms ( t2 . getTerm ( 0 ) , t2 . getTerm ( 1 ) ) ) continue ; terms . remove ( i ) ; i -= 1 ; } //consider the case of AND function. Calls recursive method to consider nested equalities else { if ( t2 . getFunctionSymbol ( ) == ExpressionOperation . AND ) { nestedEQSubstitutions ( t2 , mgu ) ; //we remove the function if empty because all its terms were equalities if ( t2 . getTerms ( ) . isEmpty ( ) ) { terms . remove ( i ) ; i -- ; } else { //if there is only a term left we remove the conjunction //we remove and function and we set atom equals to the term that remained if ( t2 . getTerms ( ) . size ( ) == 1 ) { atom . setTerm ( i , t2 . getTerm ( 0 ) ) ; } } } } } } }
We search for equalities in conjunctions . This recursive methods explore AND functions and removes EQ functions substituting the values using the class