001: package org.mandarax.reference;
002:
003: /*
004: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
005: *
006: * This library is free software; you can redistribute it and/or
007: * modify it under the terms of the GNU Lesser General Public
008: * License as published by the Free Software Foundation; either
009: * version 2 of the License, or (at your option) any later version.
010: *
011: * This library is distributed in the hope that it will be useful,
012: * but WITHOUT ANY WARRANTY; without even the implied warranty of
013: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
014: * Lesser General Public License for more details.
015: *
016: * You should have received a copy of the GNU Lesser General Public
017: * License along with this library; if not, write to the Free Software
018: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
019: */
020: import java.util.*;
021: import org.mandarax.kernel.*;
022: import org.mandarax.util.logging.LogCategories;
023:
024: /**
025: * Abstract superclass for inference engines based on resolution.
026: * The design is rather modular - a selection rule, the unification
027: * algorithm and a loop checking algorithm used are public properties of the engine and can be configured.
028: * Note that by default we do not use loop checking, the default loop checker is the trivial do nothing
029: * implementation.
030: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
031: * @version 3.4 <7 March 05>
032: * @since 1.7.2
033: */
034: public abstract class AbstractResolutionInferenceEngine implements
035: InferenceEngine, LogCategories {
036:
037: protected SelectionPolicy selectionPolicy = new LeftMostSelectionPolicy();
038: protected UnificationAlgorithm unificationAlgorithm = new RobinsonsUnificationAlgorithm();
039: protected LoopCheckingAlgorithm loopCheckingAlgorithm = new NullLoopCheckingAlgorithm();
040: protected InferenceEngineFeatureDescriptions featureDescriptions = null;
041: protected SemanticEvaluationPolicy semanticEvaluationPolicy = new DefaultSemanticEvaluationPolicy();
042:
043: // maximum number of resolution steps
044: public int MAXSTEPS = 100000;
045:
046: /**
047: * AbstractInferenceEngine constructor comment.
048: */
049: public AbstractResolutionInferenceEngine() {
050: super ();
051: }
052:
053: /**
054: * Get the loop checking algorithm.
055: * @return an algorithm
056: */
057: public LoopCheckingAlgorithm getLoopCheckingAlgorithm() {
058: return loopCheckingAlgorithm;
059: }
060:
061: /**
062: * Get the maximum number of proof steps that should be performed.
063: * If this number is reached without a result, the engine gives up.
064: * @return the max number of proof steps
065: */
066: public int getMaxNumberOfProofSteps() {
067: return MAXSTEPS;
068: }
069:
070: /**
071: * Get the next constraint pool.
072: * @return a list replacements
073: * @param cp the previous constraint pool
074: * @param r a resulution
075: */
076: protected List getNextConstraintPool(List cp, Resolution r) {
077: List nextConstraintPool = new ArrayList(cp.size() + 5);
078: nextConstraintPool.addAll(cp);
079:
080: for (Iterator it = r.unification.replacements.iterator(); it
081: .hasNext();) {
082: nextConstraintPool.add(it.next());
083: }
084: return nextConstraintPool;
085: }
086:
087: /**
088: * Build the next goal, i.e., remove the unified terms, join the remaining clauses,
089: * and apply the unifications.
090: * @return the next goal
091: * @param c1 the first unified clause
092: * @param c2 the second unified clause
093: * @param u a resolution
094: */
095: protected Clause getNextGoal(Clause c1, Clause c2, Resolution r) {
096: TmpClause nextClause = new TmpClause();
097: nextClause.positiveLiterals = merge(c2.getPositiveLiterals(),
098: c1.getPositiveLiterals(), r.position2);
099: nextClause.negativeLiterals = merge(c1.getNegativeLiterals(),
100: c2.getNegativeLiterals(), r.position1);
101: return nextClause;
102: }
103:
104: /**
105: * Build the first goal from the query.
106: * @return a goal
107: * @param query a query
108: */
109: protected Clause getGoal(Query query) {
110: return IEUtils.getGoal(query);
111: }
112:
113: /**
114: * Get the used selection policy.
115: * @return the used policy
116: */
117: public SelectionPolicy getSelectionPolicy() {
118: return selectionPolicy;
119: }
120:
121: /**
122: * Get the used unification algorithm.
123: * @return the used algorithm
124: */
125: public UnificationAlgorithm getUnificationAlgorithm() {
126: return unificationAlgorithm;
127: }
128:
129: /**
130: * Merge both lists, skip the element at the index "skip" in the second list.
131: * @return a new list
132: * @param v1 the first list
133: * @param v2 the second list
134: * @param skip the index to be skipped in the second list
135: */
136: protected List merge(List v1, List v2, int skip) {
137: List merged = new ArrayList(v1.size() + v2.size());
138: for (int i = 0; i < v1.size(); i++) {
139: merged.add(v1.get(i));
140: }
141: for (int i = 0; i < v2.size(); i++) {
142: if (skip != i) {
143: merged.add(v2.get(i));
144: }
145: }
146: return merged;
147: }
148:
149: /**
150: * Try to execute literals in the clause, and remove those literals if the
151: * result ist true. E.g., the result of performing +[]-[L1,L2,2<4,L3]
152: * would be +[]-[L1,L2,2<4,L3]. If the parameter was +[]-[L1,L2,2>4,L3],
153: * null would be returned.
154: * <p>
155: * Check whether we should use the selection policy here, right now we
156: * use a from the left to the right policy.
157: * <p>
158: * A rather sensible question is how to handle exceptions that occur when
159: * evaluating literals. The approach taken here is that an exception will render
160: * the literal as "false".
161: * @param c a clause
162: * @param session a session
163: * @param logOn indicates whether we should log
164: * @return another clause
165: */
166: protected Clause performSemanticalEvaluation(Clause c,
167: Session session, boolean logOn) {
168: return semanticEvaluationPolicy.evaluate(c, session, logOn);
169: }
170:
171: /**
172: * Set a new loop checking algorithm.
173: * @param lp a loop checker
174: */
175: public void setLoopCheckingAlgorithm(
176: LoopCheckingAlgorithm anAlgorithm) {
177: loopCheckingAlgorithm = anAlgorithm;
178: }
179:
180: /**
181: * Set the maximum number of proof steps that should be performed.
182: * If this number is reached without a result, the engine gives up.
183: * @param steps the max number of steps
184: */
185: public void setMaxNumberOfProofSteps(int steps) {
186: MAXSTEPS = steps;
187: }
188:
189: /**
190: * Set a selection policy.
191: * @param aPolicy the new selection policy
192: */
193: public void setSelectionPolicy(SelectionPolicy aPolicy) {
194: selectionPolicy = aPolicy;
195: }
196:
197: /**
198: * Set a unification algorithm.
199: * @param anAlgorithm the new algorithm
200: */
201: public void setUnificationAlgorithm(UnificationAlgorithm anAlgorithm) {
202: unificationAlgorithm = anAlgorithm;
203:
204: if (unificationAlgorithm != null
205: && unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
206: ((ExtendedUnificationAlgorithm) unificationAlgorithm)
207: .setSemanticEvaluationPolicy(semanticEvaluationPolicy);
208: }
209: }
210:
211: /**
212: * Returns the semantic evaluation policy.
213: * @return the current policy
214: */
215: public SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
216: return semanticEvaluationPolicy;
217: }
218:
219: /**
220: * Sets the semantic evaluation policy.
221: * @param policy The policy to set
222: */
223: public void setSemanticEvaluationPolicy(
224: SemanticEvaluationPolicy policy) {
225: semanticEvaluationPolicy = policy;
226:
227: if (unificationAlgorithm != null
228: && unificationAlgorithm instanceof ExtendedUnificationAlgorithm) {
229: ((ExtendedUnificationAlgorithm) unificationAlgorithm)
230: .setSemanticEvaluationPolicy(policy);
231: }
232: }
233:
234: /**
235: * Returns the max number of resolution steps.
236: * @return int
237: */
238: public int getMaxSteps() {
239: return MAXSTEPS;
240: }
241:
242: /**
243: * Sets the max number of resolution steps.
244: * @param value the max number of resolution steps
245: */
246: public void setMaxSteps(int value) {
247: MAXSTEPS = value;
248: }
249:
250: /**
251: * Invoke a procedural attachment.
252: * @param session a session
253: * @param debugOn whether debug is switched on
254: */
255: protected void notifyListenersOnResult(Session session,
256: boolean debugOn) throws InferenceException {
257: DerivationEventListener[] listeners = session.getQuery()
258: .getDerivationEventListeners();
259: if (listeners != null && listeners.length > 0) {
260: Map varReplacements = new Hashtable();
261: for (int i = 0; i < listeners.length; i++) {
262: listeners[i].onResultDo(session);
263: }
264: }
265: }
266:
267: /**
268: * Invoke a procedural attachment.
269: * @param session a session
270: * @param debugOn whether debug is switched on
271: */
272: protected void notifyListenersOnDerivationStart(Session session,
273: boolean debugOn) throws InferenceException {
274: DerivationEventListener[] listeners = session.getQuery()
275: .getDerivationEventListeners();
276: if (listeners != null && listeners.length > 0) {
277: for (int i = 0; i < listeners.length; i++) {
278: listeners[i].beforeDerivationDo(session);
279: }
280: }
281: }
282:
283: }
|