resolutioninferenceengine3.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.*;
import org.mandarax.kernel.*;
import org.mandarax.util.ClauseIterator;

/**
 * Implementation of an inference engine returning many results.
 * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
 * @version 3.4 <7 March 05>
 * @since 2.0
 */
public final class ResolutionInferenceEngine3
	extends AbstractResolutionInferenceEngine {

	/**
	 * Constructor.
	 */
	public ResolutionInferenceEngine3() {
		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
							.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 list of constraints
	 * @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 session the 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());
		}

		// 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 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;
		}

		// check for the next clause to continue. Try resolution.
		try {
			ClauseIterator e = kb.clauses(goal, null);
			boolean useClause = true;
			while (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);
				} 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,
								nextConstraintPool,
								counter,
								renameVariables,
								logOn,
								appliedClauses,
								results,
								session);

						nextNode.setQuery(goal);
						nextNode.setAppliedClause(c);

						// register the subnode
						node.addSubNode(nextNode);

						if (!nextNode.isFailed()) {
							// add renamings and unification
							nextNode.varRenamings = renamed;
							nextNode.setUnification(r.unification);
						}
					}
				} else {
					if (logOn) {
						LOG_IE_STEP.debug("Cannot apply the following rule:");
						LOG_IE_STEP.debug("Clause     : " + c.toString());
						LOG_IE_STEP.debug(
							"Clause (rn): " + workCopy.toString());
					}
				}
			}
			// release resources!
			e.close();
		} catch (ClauseSetException x) {
			String msg = "Exception getting clause iterator for " + goal;
			LOG_IE_STEP.error(msg, x);
			if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
				throw new InferenceException(msg, x);
		}
		if ((nextNode == null) || nextNode.isFailed()) {
			List l = node.getSubNodes();
			int n = l.size();
			boolean result = true;
			for (int i = 0; i < n; i++) {
				result = result && ((DerivationNodeImpl) l.get(i)).isFailed();
				node.setFailed(result);
			}
			// new in 1.9.2 
			node.setFailed(result);
		}
		return node;
	}
	/**
	 * Try to proof prereqs. If the proof succeeds, remove them from the goal.
	 * If the proof fails, return null.
	 * @param goal a goal
	 * @param kb - the knowledge base used
	 * @param logOn - indicates whether we must log this proof step
	 * @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
	 * @return the new goal
	 */
	private Clause proofNAFClauses(
		Clause goal,
		org.mandarax.kernel.KnowledgeBase kb,
		boolean logOn,
		int exceptionHandlingStrategy,
		int cardinalityConstraint)
		throws InferenceException {
		Fact literal = null;
		for (Iterator it = goal.getNegativeLiterals().iterator();
			it.hasNext();
			) {
			literal = (Fact) it.next();
			if (literal.isNegatedAF() && !IEUtils.containsVars(literal)) {
				if (logOn)
					LOG_IE.debug("Evaluate NAF " + literal);
				// build new query
				Query query =
					LogicFactory.getDefaultFactory().createQuery(
						LogicFactory.getDefaultFactory().createFact(
							literal.getPredicate(),
							literal.getTerms()),
						"Query to proof NAF in " + literal);
				// issue query
				boolean proved = false;
				try {
					ResultSet rs =
						this.query(
							query,
							kb,
							cardinalityConstraint,
							exceptionHandlingStrategy);
					proved = !rs.next();
				} catch (InferenceException x) {
					LOG_IE_STEP.error("Error proofing NAF: " + literal, x);
					if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
						throw x;
					else {
						// assume failure proofs NAF !
						LOG_IE_STEP.debug(
							"Assume error means failure and verifies NAF "
								+ literal);
						proved = true;
					}
				}
				// remove if proved
				if (proved) {
					LOG_IE_STEP.debug("Remove from list " + literal);
					it.remove();
				} else {
					LOG_IE_STEP.debug(
						"Cannot prove "
							+ literal
							+ " (unnegated fact is provable)");
					return null;
				}
			}
		}
		return goal;
	}
	/**
	 * Answer a query, retrieve (multiple different) result.
	 * The cardinality contraints describe how many results should be computed. It is either
	 * <ol>
	 * <li> <code>ONE</code> - indicating that only one answer is expected
	 * <li> <code>ALL</code> - indicating that all answers should be computed
	 * <li> <code>an integer value greater than 0 indicating that this number of results expected
	 * </ol>
	 * @see #ONE
	 * @see #ALL
	 * @return the result set of the query
	 * @param query the query clause
	 * @param kb the knowledge base used to answer the query
	 * @param aCardinalityConstraint the number of results expected
	 * @param exceptionHandlingPolicy one of the constants definied in this class (BUBBLE_EXCEPTIONS,TRY_NEXT)
	 * @throws an InferenceException
	 */
	public ResultSet query(
		Query query,
		org.mandarax.kernel.KnowledgeBase kb,
		int aCardinalityConstraint,
		int exceptionHandlingPolicy)
		throws InferenceException {
		Clause firstGoal = getGoal(query);
		VariableRenaming renameVariables = new VariableRenaming();
		List resultNodes = new ArrayList();
		SessionImpl session = new SessionImpl(kb,this,query,exceptionHandlingPolicy,aCardinalityConstraint);
		notifyListenersOnDerivationStart(session,LOG_IE_STEP.isDebugEnabled());
		
		// proof
		DerivationNodeImpl linResult =
			proof(
				firstGoal,
				new ArrayList(),
				new DerivationStepCounter(),
				renameVariables,
				LOG_IE_STEP.isDebugEnabled(),
				new ArrayList(MAXSTEPS),
				resultNodes,
				session);

		for (int i = 0; i < resultNodes.size(); i++)
			((DerivationNodeImpl) resultNodes.get(i))
				.propagateSupportedSolutions();
		linResult.setSemanticEvaluationPolicy(getSemanticEvaluationPolicy());
		return new ResultSetImpl2(linResult, resultNodes, firstGoal);
	}
	/**
	 * Build the next goal, i.e., remove the unified terms, join the remaining clauses,
	 * and apply the unifications.
	 * @return the next goal
	 * @param c1 the first unified clause
	 * @param c2 the second unified clause
	 * @param u a resolution
	 */
	protected Clause getNextGoal(Clause c1, Clause c2, Resolution r) {
		TmpClause nextClause = new TmpClause();
		nextClause.positiveLiterals =
			merge(
				c2.getPositiveLiterals(),
				c1.getPositiveLiterals(),
				r.position2);
		nextClause.negativeLiterals =
			merge2(
				c1.getNegativeLiterals(),
				c2.getNegativeLiterals(),
				r.position1);
		return nextClause;
	}
	/**
	 * Merge lists (of facts), skip the element at the index "skip" in the second list.
	 * This method moves negated facts to the right. This increases the chances that all
	 * terms are "ground".
	 * @return a new list
	 * @param v1 the first list
	 * @param v2 the second list
	 * @param skip the index to be skipped in the second list
	 */
	private List merge2(List v1, List v2, int skip) {
		List merged = new ArrayList(v1.size() + v2.size());
		int posCounter = 0;
		Fact f = null;
		for (int i = 0; i < v1.size(); i++) {
			f = (Fact) v1.get(i);
			if (!f.isNegatedAF()) {
				merged.add(posCounter, f);
				posCounter = posCounter + 1;
			} else
				merged.add(v1.get(i));
		}
		for (int i = 0; i < v2.size(); i++) {
			if (skip != i) {
				merged.add(v2.get(i));
			}
		}
		return merged;
	}

}