content: /**
   * Copyright (c) 2017-2018, the Alpha Team.
   * All rights reserved.
   * 
   * Additional changes made by Siemens.
   * 
   * Redistribution and use in source and binary forms, with or without
   * modification, are permitted provided that the following conditions are met:
   * 
   * 1) Redistributions of source code must retain the above copyright notice, this
   *    list of conditions and the following disclaimer.
   * 
   * 2) Redistributions in binary form must reproduce the above copyright notice,
   *    this list of conditions and the following disclaimer in the documentation
   *    and/or other materials provided with the distribution.
   * 
   * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
   * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
   * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
   * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
   * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
   * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
   * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
   * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
   * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   */
  package at.ac.tuwien.kr.alpha.core.grounder;
  
  import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
  
  import java.util.Set;
  
  import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
  import at.ac.tuwien.kr.alpha.api.programs.terms.ArithmeticTerm;
  import at.ac.tuwien.kr.alpha.api.programs.terms.FunctionTerm;
  import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
  import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;
  import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier;
  
  /**
   * Copyright (c) 2017, the Alpha Team.
   */
  public class Unification {
  
  	/**
  	 * Computes the most-general-unifier of two atoms that share no common variables.
  	 * @param left the one atom to unify with
  	 * @param right to other atom to unify with
  	 * @return the most-general-unifier of the two given atoms if it exists, and null otherwise.
  	 */
  	public static Unifier unifyAtoms(Atom left, Atom right) {
  		return unifyAtoms(left, right, false);
  	}
  
  	/**
  	 * Instantiates the general Atom to match the specific one and returns the corresponding substitution.
  	 * @param general the general Atom to instantiate.
  	 * @param specific the specific Atom.
  	 * @return a Unifier sigma such that specific == general.substitute(sigma), returns null if no such sigma exists.
  	 */
  	public static Unifier instantiate(Atom general, Atom specific) {
  		return unifyAtoms(specific, general, true);
  	}
  
  	private static Unifier unifyAtoms(Atom left, Atom right, boolean keepLeftAsIs) {
  		Set<VariableTerm> leftOccurringVariables = left.getOccurringVariables();
  		Set<VariableTerm> rightOccurringVaribles = right.getOccurringVariables();
  		boolean leftSmaller = leftOccurringVariables.size() < rightOccurringVaribles.size();
  		Set<VariableTerm> smallerSet = leftSmaller ? leftOccurringVariables : rightOccurringVaribles;
  		Set<VariableTerm> largerSet = leftSmaller ? rightOccurringVaribles : leftOccurringVariables;
  		for (VariableTerm variableTerm : smallerSet) {
  			if (largerSet.contains(variableTerm)) {
  				throw oops("Left and right atom share variables.");
  			}
  		}
  		Unifier mgu = new Unifier();
  		if (!left.getPredicate().equals(right.getPredicate())) {
  			return null;
  		}
  		for (int i = 0; i < left.getPredicate().getArity(); i++) {
  			final Term leftTerm = left.getTerms().get(i);
  			final Term rightTerm = right.getTerms().get(i);
  			if (!unifyTerms(leftTerm, rightTerm, mgu, keepLeftAsIs)) {
  				return null;
  			}
  		}
  		return mgu;
  	}
  
  	private static boolean unifyTerms(Term left, Term right, Unifier currentSubstitution, boolean keepLeftAsIs) {
  		final Term leftSubs = left.substitute(currentSubstitution);
  		final Term rightSubs = right.substitute(currentSubstitution);
  		if (leftSubs == rightSubs) {
  			return true;
  		}
  		if (!keepLeftAsIs && leftSubs instanceof VariableTerm && !currentSubstitution.isVariableSet((VariableTerm) leftSubs)) {
  			currentSubstitution.put((VariableTerm) leftSubs, rightSubs);
  			return true;
  		}
  		if (rightSubs instanceof VariableTerm && !currentSubstitution.isVariableSet((VariableTerm) rightSubs)) {
  			currentSubstitution.put((VariableTerm) rightSubs, leftSubs);
  			return true;
  		}
  		if (leftSubs instanceof FunctionTerm && rightSubs instanceof FunctionTerm) {
  			final FunctionTerm leftFunction = (FunctionTerm) leftSubs;
  			final FunctionTerm rightFunction = (FunctionTerm) rightSubs;
  			if (!leftFunction.getSymbol().equals(rightFunction.getSymbol())
  				|| leftFunction.getTerms().size() != rightFunction.getTerms().size()) {
  				return false;
  			}
  			for (int i = 0; i < leftFunction.getTerms().size(); i++) {
  				final Term leftTerm = leftFunction.getTerms().get(i);
  				final Term rightTerm = rightFunction.getTerms().get(i);
  				if (!unifyTerms(leftTerm, rightTerm, currentSubstitution, keepLeftAsIs)) {
  					return false;
  				}
  			}
  			return true;
  		}
  		if (leftSubs instanceof ArithmeticTerm && rightSubs instanceof ArithmeticTerm) {
  			// ArithmeticTerms are similar to FunctionTerms, i.e. if the operator is the same and its subterms unify, the ArithmeticTerms unify.
  			final ArithmeticTerm leftArithmeticTerm = (ArithmeticTerm) leftSubs;
  			final ArithmeticTerm rightArithmeticTerm = (ArithmeticTerm) rightSubs;
  			if (!leftArithmeticTerm.getOperator().equals(rightArithmeticTerm.getOperator())) {
  				return false;
  			}
  			final Term leftTermLeftSubterm = leftArithmeticTerm.getLeftOperand();
  			final Term rightTermLeftSubterm = rightArithmeticTerm.getLeftOperand();
  			if (!unifyTerms(leftTermLeftSubterm, rightTermLeftSubterm, currentSubstitution, keepLeftAsIs)) {
  				return false;
  			}
  			final Term leftTermRightSubterm = leftArithmeticTerm.getRightOperand();
  			final Term rightTermRightSubterm = rightArithmeticTerm.getRightOperand();
  			if (!unifyTerms(leftTermRightSubterm, rightTermRightSubterm, currentSubstitution, keepLeftAsIs)) {
  				return false;
  			}
  			return true;
  		}
  		return false;
  	}
  }
  