package aima.core.logic.fol.inference;

import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import aima.core.logic.fol.inference.proof.ProofStepClauseDemodulation;
import aima.core.logic.fol.kb.data.Clause;
import aima.core.logic.fol.kb.data.Literal;
import aima.core.logic.fol.parsing.ast.AtomicSentence;
import aima.core.logic.fol.parsing.ast.Term;
import aima.core.logic.fol.parsing.ast.TermEquality;
import aima.core.logic.fol.parsing.ast.Variable;

/**
 * Artificial Intelligence A Modern Approach (3rd Edition): page 354.<br>
 * <br>
 * Demodulation: For any terms x, y, and z, where z appears somewhere in literal
 * m<sub>i</sub> and where UNIFY(x,z) = &theta;:<br>
 * 
 * <pre>
 *                 x=y,    m<sub>1</sub> OR ... OR m<sub>n</sub>[z]
 *     ------------------------------------------------------------
 *     SUB(SUBST(&theta;,x), SUBST(&theta;,y), m<sub>1</sub> OR ... OR m<sub>n</sub>)
 * </pre>
 * 
 * where SUBST is the usual substitution of a binding list, and SUB(x,y,m) means
 * to replace x with y everywhere that x occurs within m.<br>
 * <br>
 * Some additional restrictions/clarifications highlighted in:<br>
 * <a href="http://logic.stanford.edu/classes/cs157/2008/lectures/lecture15.pdf"
 * >Demodulation Restrictions</a> <br>
 * 1. Unit Equations Only.<br>
 * 2. Variables substituted in Equation Only.<br>
 * 
 * @author Ciaran O'Reilly
 * 
 */
public class Demodulation extends AbstractModulation {
	public Demodulation() {
	}

	public Clause apply(TermEquality assertion, Clause clExpression) {
		Clause altClExpression = null;

		for (Literal l1 : clExpression.getLiterals()) {
			AtomicSentence altExpression = apply(assertion,
					l1.getAtomicSentence());
			if (null != altExpression) {
				// I have an alternative, create a new clause
				// with the alternative and return
				List<Literal> newLits = new ArrayList<Literal>();
				for (Literal l2 : clExpression.getLiterals()) {
					if (l1.equals(l2)) {
						newLits.add(l1.newInstance(altExpression));
					} else {
						newLits.add(l2);
					}
				}
				// Only apply demodulation at most once on
				// each call.
				altClExpression = new Clause(newLits);
				altClExpression.setProofStep(new ProofStepClauseDemodulation(
						altClExpression, clExpression, assertion));
				if (clExpression.isImmutable()) {
					altClExpression.setImmutable();
				}
				if (!clExpression.isStandardizedApartCheckRequired()) {
					altClExpression.setStandardizedApartCheckNotRequired();
				}
				break;
			}
		}

		return altClExpression;
	}

	public AtomicSentence apply(TermEquality assertion,
			AtomicSentence expression) {
		AtomicSentence altExpression = null;

		IdentifyCandidateMatchingTerm icm = getMatchingSubstitution(
				assertion.getTerm1(), expression);

		if (null != icm) {
			Term replaceWith = substVisitor.subst(
					icm.getMatchingSubstitution(), assertion.getTerm2());
			// Want to ignore reflexivity axiom situation, i.e. x = x
			if (!icm.getMatchingTerm().equals(replaceWith)) {
				ReplaceMatchingTerm rmt = new ReplaceMatchingTerm();

				// Only apply demodulation at most once on each call.
				altExpression = rmt.replace(expression, icm.getMatchingTerm(),
						replaceWith);
			}
		}

		return altExpression;
	}

	//
	// PROTECTED METHODS
	//
	@Override
	protected boolean isValidMatch(Term toMatch,
			Set<Variable> toMatchVariables, Term possibleMatch,
			Map<Variable, Term> substitution) {
		// Demodulation only allows substitution in the equation only,
		// if the substitution contains variables not in the toMatch
		// side of the equation (i.e. left hand side), then
		// it is not a legal demodulation match.
		// Note: see:
		// http://logic.stanford.edu/classes/cs157/2008/lectures/lecture15.pdf
		// slide 23 for an example.
		if (toMatchVariables.containsAll(substitution.keySet())) {
			return true;
		}

		return false;
	}
}