resolutioninferenceengine4.java

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

package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:[e-mail]">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.*;
import org.mandarax.kernel.*;
import org.mandarax.lib.Cut;
import org.mandarax.util.ClauseIterator;

/**
 * Implementation of an inference engine returning many results.
 * Negation and cut are supported.
 * @author <A HREF="mailto:[e-mail]">Jens Dietrich</A>, <A HREF="mailto:[e-mail]">Alexander Kozlenkov</A>
 * @version 3.4 <7 March 05>
 * @since 2.1
 * Prova re-integration modifications
 * @author <A HREF="mailto:[e-mail]">Alex Kozlenkov</A>
 * @version 3.4 <7 March 05>
 */
public final class ResolutionInferenceEngine4
	extends AbstractResolutionInferenceEngine {

	/**
	 * Constructor.
	 */
	public ResolutionInferenceEngine4() {
		super();
	}
	/**
	 * Get the feature descriptions.
	 * @return the feature descriptions
	 */
	public InferenceEngineFeatureDescriptions getFeatureDescriptions() {
		if (featureDescriptions == null) {
			featureDescriptions = new InferenceEngineFeatureDescriptions() {
				protected void initialize() {
					super.initialize();
					this.supported.add(
						InferenceEngineFeatureDescriptions.LOOP_CHECKS);
					this.supported.add(
						InferenceEngineFeatureDescriptions.MULTIPLE_RESULTS);
					this.supported.add(
						InferenceEngineFeatureDescriptions.NEGATION_AS_FAILURE);
					this.supported.add(InferenceEngineFeatureDescriptions.CUT);
					this.supported.add(
						InferenceEngineFeatureDescriptions
							.DERIVATION_EVENT_LISTENERS);
				}

			};
		}
		return featureDescriptions;
	}
	/**
	 * Try to proof a goal.
	 * @return a derivation node
	 * @param goal - the goal that has to be proved
	 * @param constraintPool - a vector of constraints
	 * @param queryVariables - a list of query variables
	 * @param kb - the knowledge base used
	 * @param counter - the proof step counter
	 * @param renameVariables  a variable renaming
	 * @param logEnabled - indicates whether we must log this proof step
	 * @param results - the list collecting the results
	 * @param appliedClauses - a list of all clauses applied so far (used to detect loops)
	 * @param exceptionHandlingStrategy - an integer decoding the exception handling strategy when fetching and resolving
	 * 			ClauseSetExceptions
	 * @param cardinalityConstraint - the cardinality constraint specifying the number of results we are looking for
	 * @param listeners the derivation listeners
	 * @param session a session object
	 * @throws InferenceException
	 */
	private DerivationNodeImpl proof(
		Clause goal,
		List constraintPool,
		DerivationStepCounter counter,
		VariableRenaming renameVariables,
		boolean logEnabled,
		List appliedClauses,
		List results,
		SessionImpl session)
		throws InferenceException {

		int exceptionHandlingStrategy = session.getExceptionHandlingStrategy();
		int cardinalityConstraint = session.getCardinalityContraint();
		org.mandarax.kernel.KnowledgeBase kb = session.getKnowledgeBase();


		// make sure that the session is uptodate
		session.update(renameVariables.getAllRenamings(),constraintPool);

		// for performance reasons we want to minimize checks whether log is
		// enabled. On the other hand, we would like to switch log on / off
		// during a proof (e.g., to analyse a long proof). This implementation
		// checks the respective log category every 10 steps
		boolean logOn =
			(counter.count % 10 == 0)
				? LOG_IE_STEP.isDebugEnabled()
				: logEnabled;
		DerivationNodeImpl node = new DerivationNodeImpl();
		node.setId(counter.next());
		// node.supportedSolution = results.size();
		DerivationNodeImpl nextNode = null;

		if (logOn) {
			LOG_IE_STEP.debug("PROOF STEP " + String.valueOf(counter.count));
			LOG_IE_STEP.debug("Goal       : " + goal.toString());
		}

		// check for cut
		// System.out.println("Goal before: " + goal.toString());
		checkCut(node, goal);
		// System.out.println("Goal after : " + goal.toString());

		// try to remove clauses using the object semantics
		goal = performSemanticalEvaluation(goal, session,logOn);

		if (goal == null) {
			node.setFailed(true);
			return node;
		}

		// check for negation (NAF)
		goal =
			proofNAFClauses(
				goal,
				kb,
				logOn,
				exceptionHandlingStrategy,
				cardinalityConstraint);
		if (goal == null) {
			node.setFailed(true);
			return node;
		}

		if (logOn) {
			LOG_IE_STEP.debug(
				"Goal (semantic,NAF,CUT check done): " + goal.toString());
		}

		// check whether the max proof length has been reached
		if (counter.count >= MAXSTEPS) {
			if (logOn) {
				LOG_IE_STEP.debug(
					"Maximum number of steps reached, stop here !");
			}
			return node;
		}

		// if the goal is the empty clause, return success
		if (goal.isEmpty()) {
			if (logOn) {
				LOG_IE_STEP.debug("Derivation successful !");
			}
			results.add(node);
			// new in 3.2: notify listener
			notifyListenersOnResult(session,logOn);

			node.setResultNode(true);
			node.setSupported(results.size() - 1);
			node.setFailed(false);
			// check whether we have enough results
			if (cardinalityConstraint != ALL) {
				node.setLastNode((results.size() >= cardinalityConstraint));
			}
			return node;
		}
		String goalPredicateName =
			((Fact) goal.getNegativeLiterals().get(0)).getPredicate().getName();

		// check for the next clause to continue. Try resolution.
		try {

			ClauseIterator e = kb.clauses(goal, null);
			boolean useClause = true;
			while ((nextNode == null || !nextNode.isCut())
				&& e.hasMoreClauses()
				&& (cardinalityConstraint == ALL
					|| results.size() < cardinalityConstraint)) {
				useClause = true;
				Resolution r = null;
				Clause c = null;
				Clause workCopy = null;
				try {
					c = e.nextClause();
					workCopy = renameVariables.cloneAndRenameVars(c);
					recordCut(node.getId(), workCopy);
				} catch (ClauseSetException x) {
					String msg =
						"Exception fetching clause from iterator for " + goal;
					LOG_IE_STEP.error(msg, x);
					// depending on the exception handling strategy we forward the exception or carry on
					if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
						throw new InferenceException(msg, x);
					useClause = false;
				}
				if (useClause
					&& (r =
						Resolution.resolve(
							workCopy,
							goal,
							unificationAlgorithm,
							selectionPolicy,
							session))
						!= null) {
					appliedClauses.add(c);

					if (loopCheckingAlgorithm.isInfiniteLoop(appliedClauses)) {
						if (logOn) {
							LOG_IE_STEP.debug(
								"LoopChecking Algorithm "
									+ loopCheckingAlgorithm
									+ " has detected a loop! Try to continue with next clause");
						}
					} else {
						// log
						if (logOn) {
							LOG_IE_STEP.debug("Can apply the following rule:");
							LOG_IE_STEP.debug("Clause     : " + c.toString());
							LOG_IE_STEP.debug(
								"Clause (rn): " + workCopy.toString());

							// log unification
							Replacement nextReplacement = null;

							for (Iterator er =
								r.unification.replacements.iterator();
								er.hasNext();
								) {
								nextReplacement = (Replacement) er.next();
								LOG_IE_STEP.debug(
									"unify      : "
										+ nextReplacement.original.toString()
										+ " -> "
										+ nextReplacement.replacement.toString());
							}
						}

						// build a new subgoal
						Clause nextGoal = getNextGoal(workCopy, goal, r);

						// build a new constraint pool for the next step
						List nextConstraintPool =
							getNextConstraintPool(constraintPool, r);

						// apply constraints
						nextGoal = nextGoal.apply(nextConstraintPool);

						// rename variables in the subgoal
						nextGoal = renameVariables.cloneAndRenameVars(nextGoal);

						// keep the renamed var here, otherwise they get overridden in the recursion
						Hashtable renamed = renameVariables.getRecentRenamings();

						// log renamings
						if (logOn) {
							Object nextRenaming = null;

							for (Enumeration er = renamed.keys();
								er.hasMoreElements();
								) {
								nextRenaming = er.nextElement();
								LOG_IE_STEP.debug(
									"rename     : "
										+ nextRenaming.toString()
										+ " -> "
										+ renamed.get(nextRenaming).toString());
							}
						}

						// proof the new subgoal
						nextNode =
							proof(
								nextGoal,