package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:mandarax@jbdietrich.com">Jens Dietrich</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

import org.mandarax.kernel.*;

import java.util.List;

/**
 * Helper class to retrieve resolution steps. Instances are created
 * using the static method <code>resolver(..)</code>.
 * The created resolution has the following structure:
 * <ul>
 * <li> position1 is the position of the resolved fact in clause 1
 * <li> position1 is the position of the resolved fact in clause 2
 * <li> unification is the unification computed
 * <li> order is true if a negative literal from clause 1 has been unified with a positive
 * literal from clause 2 and false if it is the other way around.
 * </ul>
 *
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.0
 *        Prova re-integration modifications
 */
public class Resolution extends org.mandarax.kernel.LObject {

	public int position1;
	public int position2;
	public Unification unification = null;

	/**
	 * Constructor.
	 *
	 * @param p1 position 1
	 * @param p2 position 2
	 * @param u  the unification
	 */
	private Resolution( int p1, int p2, Unification u ) {
		super();

		position1 = p1;
		position2 = p2;
		unification = u;
	}

	/**
	 * Indicate whether this resolution has failed.
	 *
	 * @return true if the resolution has failed, false otherwise
	 */
	public boolean hasFailed() {
		return (unification == null) || unification.hasFailed();
	}

	/**
	 * Resolve the two clauses.
	 *
	 * @param c       the clause
	 * @param goal    the goal
	 * @param ua      the unification algorithm used
	 * @param sp      the selection policy used
	 * @param session a session
	 * @return the resolution
	 */
	public static Resolution resolve( Clause c,
	                                  Clause goal,
	                                  UnificationAlgorithm ua,
	                                  SelectionPolicy sp,
	                                  Session session ) {
		int i, j = 0;
		Fact f1, f2 = null;
		Unification u = null;
		List negLitFromGoal = goal.getNegativeLiterals();
		List posLit = c.getPositiveLiterals();
		int[] selection = sp.getOrderedPositions(goal, c);

		for( i = 0; i < selection.length; i++ ) {
			f1 = (Fact) negLitFromGoal.get(selection[i]);

			for( j = 0; j < posLit.size(); j++ ) {
				f2 = (Fact) posLit.get(j);

				// Corrected in 2.2.1 - take NAF into account
				// by Hans-Henning Wiesner (Hans-Henning.Wiesner@bauer-partner.com)
				String p1 = f1.getPredicate().getName();
				String p2 = f2.getPredicate().getName();

				if( !p1.equals(p2) || f1.isNegatedAF() != f2.isNegatedAF() ) {
					u = Unification.noUnificationPossible;
				} else {
					u = ua.unify(f1.getTerms(), f2.getTerms(), session);
				}
				if( !u.hasFailed() ) {
					// in this case, build and return a resolution
					return new Resolution(selection[i], j, u);
				}
			}
		}

		return null;
	}

	/**
	 * Prova version.
	 * Resolve the two clauses.
	 *
	 * @param c    the clause
	 * @param goal the goal
	 * @param ua   the unification algorithm used
	 * @param sp   the selection policy used
	 * @return the resolution
	 */
	public static Resolution resolve( Clause c, Clause goal,
	                                  UnificationAlgorithm ua,
	                                  SelectionPolicy sp, boolean isRule ) {
		int i,
		        j = 0;
		Fact f1,
		        f2 = null;
		Unification u = null;
		List negLitFromGoal = goal.getNegativeLiterals();
		List posLit = c.getPositiveLiterals();
		int[] selection = sp.getOrderedPositions(goal, c);

		for( i = 0; i < selection.length; i++ ) {
			f1 = (Fact) negLitFromGoal.get(selection[i]);

			for( j = 0; j < posLit.size(); j++ ) {
				f2 = (Fact) posLit.get(j);

				// Corrected in 2.2
				String p1 = f1.getPredicate().getName();
				String p2 = f2.getPredicate().getName();
				if( !p1.equals(p2) ) {
					u = Unification.noUnificationPossible;
				} else {
					u = ua.unify(f1.getTerms(), f2.getTerms(), isRule);
				}
				if( !u.hasFailed() ) {
					// in this case, build and return a resolution
					return new Resolution(selection[i], j, u);
				}
			}
		}

		return null;
	}

	/**
	 * Optimised Prova version.
	 * Resolve two facts.
	 *
	 * @param f2     the clause fact
	 * @param f1     the goal fact
	 * @param ua     the unification algorithm used
	 * @param isRule whether we are unifying with a rule
	 * @return the resolution
	 */
	public static Resolution resolve2( Fact f2, Fact f1,
	                                   UnificationAlgorithm ua, boolean isRule ) {
		Unification u = null;
		String p1 = f1.getPredicate().getName();
		String p2 = f2.getPredicate().getName();
		if( !p1.equals(p2) ) {
			u = Unification.noUnificationPossible;
		} else {
			u = ua.unify2(f1.getTerms(), f2.getTerms(), isRule);
		}
		if( !u.hasFailed() ) {
			// in this case, build and return a resolution
			return new Resolution(0, 0, u);
		}


		return null;
	}

    /**
     * Check if one fact subsumes another
     * @param f1 The first fact
     * @param f2 The second fact
     * @param ua UnificationAlgorithm used
     * @return <code>true</code> if <code>f1</code> subsumes <code>f2</code>  
     */
    public static boolean subsumes( Fact f1, Fact f2, UnificationAlgorithm ua ) {
        Resolution r = null;
        if ((r = Resolution.resolve2(f1, f2, ua,
                true)) != null) {
            // The supplied fact subsumes a KB fact if:
            // (1) EITHER the substitutions are to a variable of a more specific type
            // (2) OR the substitutions are to a constant
            if ( r.unification.replacements.size()==0 ) {
                return true;
            }
        }
        return false;
    }
}
