resolution.java

Mandarax是一个规则引擎的纯Java实现。它支持多类型的事实和基于反映的规则

package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">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 java.util.List;
import org.mandarax.kernel.*;

/**
 * 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="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
 * @version 3.4 <7 March 05>
 * @since 1.0
 * Prova re-integration modifications
 * @author <A HREF="mailto:[e-mail]">Alex Kozlenkov</A>
 * @version 3.4 <7 March 05>
 */
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.
	 * @return the resolution
	 * @param c the clause
	 * @param goal the goal
	 * @param ua the unification algorithm used
	 * @param sp the selection policy used
	 * @param session a session
	 */
	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 ([e-mail])
				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.
	 * @return the resolution
	 * @param c the clause
	 * @param goal the goal
	 * @param ua the unification algorithm used
	 * @param sp the selection policy used
	 */
	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;
	}
}