resolutioninferenceengine4.java

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

								nextConstraintPool,
								counter,
								renameVariables,
								logOn,
								appliedClauses,
								results,
								session);

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

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

						if (nextNode.isCut() && logOn) {
							LOG_IE_STEP.debug(
								"Cut encountered - prune derivation tree here!");
						}

						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);
		}
		if (node != null) {
			boolean nextCut =
				(nextNode != null)
					&& nextNode.isCut()
					&& !(nextNode.getCutPredicate().equals(goalPredicateName));
			node.setCut(node.isCut() || nextCut);
			if (nextCut && node.isCut()) {
				// The cut level that survived up to here from deeper calls takes precedence
				node.setCutPredicate(nextNode.getCutPredicate());
			}
		}
		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;
	}
	/**
	 * Indicates whether a clause set is a cut.
	 * @param cs a clause set
	 * @return a boolean
	 */
	private boolean isCut(ClauseSet cs) {
		return cs.getKey() instanceof Cut;
	}
	/**
	 * Check whether a goal has a cut.
	 */
	private void checkCut(DerivationNodeImpl node, Clause goal) {
		// the assumption is that cuts are only occuring in instances of TmpClause
		// in the first proof step, goal is an instance of Fact (originating from the query),
		// but then the predicate cannot be a cut anyway
		// @todo check selection policies
		if (goal instanceof TmpClause) {
			List negLiterals = ( (TmpClause) goal).getNegativeLiterals();
			// There may be several cut(s) so use while below
			while (negLiterals.size() > 0 &&
					 ( (Clause) negLiterals.get(0)).getKey() instanceof Cut) {
				// Now the node knows where this cut came from
				node.setCutPredicate(( (Prerequisite) negLiterals.get(0)).getExtra());
				node.setCut(true);
				negLiterals.remove(0);
			}
		}
	}

	/**
	 * Check whether a goal generates a cut and record the node id
	 * in the prerequisite corresponding to this cut.
	 * @param id the id of the current node
	 * @param workCopy the clause about to be resolved that is checked here
	 * for the presence of cuts.
	 */
	private boolean recordCut(int id, Clause workCopy) {
		// Further corrections 28/04/03
		boolean cut_found = false;
		List negLiterals = workCopy.getNegativeLiterals();
		for (ListIterator li = negLiterals.listIterator(); li.hasNext(); ) {
			Fact clause = (Fact) li.next();
			Object pred = clause.getKey();
			if (pred instanceof Cut) {
				// Record in the cut predicate itself what LHS it was opened from.
				// Used in checkOut() when the cut is finally reached
				((Prerequisite)clause).setExtra(new Integer(id));
				cut_found = true;
				// There may be more than one cut in one rule, so continue
			}
		}
		return cut_found;
	}

}