📄 abstractresolutioninferenceengine.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.logging.LogCategories;
/**
* Abstract superclass for inference engines based on resolution.
* The design is rather modular - a selection rule, the unification
* algorithm and a loop checking algorithm used are public properties of the engine and can be configured.
* Note that by default we do not use loop checking, the default loop checker is the trivial do nothing
* implementation.
* @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
* @version 3.4 <7 March 05>
* @since 1.7.2
*/
public abstract class AbstractResolutionInferenceEngine implements InferenceEngine, LogCategories {
protected SelectionPolicy selectionPolicy = new LeftMostSelectionPolicy();
protected UnificationAlgorithm unificationAlgorithm = new RobinsonsUnificationAlgorithm();
protected LoopCheckingAlgorithm loopCheckingAlgorithm = new NullLoopCheckingAlgorithm();
protected InferenceEngineFeatureDescriptions featureDescriptions = null;
protected SemanticEvaluationPolicy semanticEvaluationPolicy = new DefaultSemanticEvaluationPolicy();
// maximum number of resolution steps
public int MAXSTEPS = 100000;
/**
* AbstractInferenceEngine constructor comment.
*/
public AbstractResolutionInferenceEngine() {
super();
}
/**
* Get the loop checking algorithm.
* @return an algorithm
*/
public LoopCheckingAlgorithm getLoopCheckingAlgorithm() {
return loopCheckingAlgorithm;
}
/**
* Get the maximum number of proof steps that should be performed.
* If this number is reached without a result, the engine gives up.
* @return the max number of proof steps
*/
public int getMaxNumberOfProofSteps() {
return MAXSTEPS;
}
/**
* Get the next constraint pool.
* @return a list replacements
* @param cp the previous constraint pool
* @param r a resulution
*/
protected List getNextConstraintPool(List cp, Resolution r) {
List nextConstraintPool = new ArrayList(cp.size() + 5);
nextConstraintPool.addAll(cp);
for (Iterator it = r.unification.replacements.iterator();
it.hasNext();
) {
nextConstraintPool.add(it.next());
}
return nextConstraintPool;
}
/**
* 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 =
merge(
c1.getNegativeLiterals(),
c2.getNegativeLiterals(),
r.position1);
return nextClause;
}
/**
* Build the first goal from the query.
* @return a goal
* @param query a query
*/
protected Clause getGoal(Query query) {
return IEUtils.getGoal(query);
}
/**
* Get the used selection policy.
* @return the used policy
*/
public SelectionPolicy getSelectionPolicy() {
return selectionPolicy;
}
/**
* Get the used unification algorithm.
* @return the used algorithm
*/
public UnificationAlgorithm getUnificationAlgorithm() {
return unificationAlgorithm;
}
/**
* Merge both lists, skip the element at the index "skip" in the second list.
* @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
*/
protected List merge(List v1, List v2, int skip) {
List merged = new ArrayList(v1.size() + v2.size());
for (int i = 0; i < v1.size(); i++) {
merged.add(v1.get(i));
}
for (int i = 0; i < v2.size(); i++) {
if (skip != i) {
merged.add(v2.get(i));
}
}
return merged;
}
/**
* Try to execute literals in the clause, and remove those literals if the
* result ist true. E.g., the result of performing +[]-[L1,L2,2<4,L3]
* would be +[]-[L1,L2,2<4,L3]. If the parameter was +[]-[L1,L2,2>4,L3],
* null would be returned.
* <p>
* Check whether we should use the selection policy here, right now we
* use a from the left to the right policy.
* <p>
* A rather sensible question is how to handle exceptions that occur when
* evaluating literals. The approach taken here is that an exception will render
* the literal as "false".
* @param c a clause
* @param session a session
* @param logOn indicates whether we should log
* @return another clause
*/
protected Clause performSemanticalEvaluation(Clause c, Session session,boolean logOn) {
return semanticEvaluationPolicy.evaluate(c,session, logOn);
}
/**
* Set a new loop checking algorithm.
* @param lp a loop checker
*/
public void setLoopCheckingAlgorithm(LoopCheckingAlgorithm anAlgorithm) {
loopCheckingAlgorithm = anAlgorithm;
}
/**
* Set the maximum number of proof steps that should be performed.
* If this number is reached without a result, the engine gives up.
* @param steps the max number of steps
*/
public void setMaxNumberOfProofSteps(int steps) {
MAXSTEPS = steps;
}
/**
* Set a selection policy.
* @param aPolicy the new selection policy
*/
public void setSelectionPolicy(SelectionPolicy aPolicy) {
selectionPolicy = aPolicy;
}
/**
* Set a unification algorithm.
* @param anAlgorithm the new algorithm
*/
public void setUnificationAlgorithm(UnificationAlgorithm anAlgorithm) {
unificationAlgorithm = anAlgorithm;
if (unificationAlgorithm != null
&& unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
(
(
ExtendedUnificationAlgorithm) unificationAlgorithm)
.setSemanticEvaluationPolicy(
semanticEvaluationPolicy);
}
}
/**
* Returns the semantic evaluation policy.
* @return the current policy
*/
public SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
return semanticEvaluationPolicy;
}
/**
* Sets the semantic evaluation policy.
* @param policy The policy to set
*/
public void setSemanticEvaluationPolicy(SemanticEvaluationPolicy policy) {
semanticEvaluationPolicy = policy;
if (unificationAlgorithm != null
&& unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
(
(
ExtendedUnificationAlgorithm) unificationAlgorithm)
.setSemanticEvaluationPolicy(
policy);
}
}
/**
* Returns the max number of resolution steps.
* @return int
*/
public int getMaxSteps() {
return MAXSTEPS;
}
/**
* Sets the max number of resolution steps.
* @param value the max number of resolution steps
*/
public void setMaxSteps(int value) {
MAXSTEPS = value;
}
/**
* Invoke a procedural attachment.
* @param session a session
* @param debugOn whether debug is switched on
*/
protected void notifyListenersOnResult(Session session,boolean debugOn) throws InferenceException {
DerivationEventListener[] listeners = session.getQuery().getDerivationEventListeners();
if (listeners != null && listeners.length>0) {
Map varReplacements = new Hashtable();
for (int i=0;i<listeners.length;i++) {
listeners[i].onResultDo(session);
}
}
}
/**
* Invoke a procedural attachment.
* @param session a session
* @param debugOn whether debug is switched on
*/
protected void notifyListenersOnDerivationStart(Session session,boolean debugOn) throws InferenceException {
DerivationEventListener[] listeners = session.getQuery().getDerivationEventListeners();
if (listeners != null && listeners.length>0) {
for (int i=0;i<listeners.length;i++) {
listeners[i].beforeDerivationDo(session);
}
}
}
}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -