resolutioninferenceengine.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 only one result.
 * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
 * @version 3.4 <7 March 05>
 * @since 1.0
 */
public final class ResolutionInferenceEngine extends AbstractResolutionInferenceEngine {

	private static final DerivationTreeBuilder derivationTreeBuilder = new DerivationTreeBuilder();
	/**
	 * Constructor.
	 */
	public ResolutionInferenceEngine() {
		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);
				}
			
			};            
		}

		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 count - the proof step count
	 * @param renameVariables  a variable renaming
	 * @param logEnabled - indicates whether we must log this proof step
	 * @param appliedClauses - a list of all clauses applied so far (used to detect loops)
	 * @param session a session
	 * @throws InferenceException
	 */
	private DerivationNodeImpl proof(Clause goal, List constraintPool,
								 DerivationStepCounter counter, VariableRenaming renameVariables,
								 boolean logEnabled, List appliedClauses,SessionImpl session) throws InferenceException {

		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());
		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, null,logOn);

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

		// 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 !");
			}

			node.setFailed (false);
			node.setResultNode(true);

			return node;
		}

		// check for the next clause to continue. Try resolution.
		
		try {
			ClauseIterator e = kb.clauses (goal, null);
			boolean useClause = true;
	        while(e.hasMoreClauses () && ((nextNode == null) || nextNode.isFailed ())) {	            
	            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 (session.getExceptionHandlingStrategy()==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,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 ());
	                }
	            }
	        }
	        // new in 2.0 - release resources!
	        e.close();