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.ClauseIterator;
023:
024: /**
025: * Implementation of an inference engine returning many results.
026: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
027: * @version 3.4 <7 March 05>
028: * @since 2.0
029: */
030: public final class ResolutionInferenceEngine3 extends
031: AbstractResolutionInferenceEngine {
032:
033: /**
034: * Constructor.
035: */
036: public ResolutionInferenceEngine3() {
037: super ();
038: }
039:
040: /**
041: * Get the feature descriptions.
042: * @return the feature descriptions
043: */
044: public InferenceEngineFeatureDescriptions getFeatureDescriptions() {
045: if (featureDescriptions == null) {
046: featureDescriptions = new InferenceEngineFeatureDescriptions() {
047: protected void initialize() {
048: super .initialize();
049: this .supported
050: .add(InferenceEngineFeatureDescriptions.LOOP_CHECKS);
051: this .supported
052: .add(InferenceEngineFeatureDescriptions.MULTIPLE_RESULTS);
053: this .supported
054: .add(InferenceEngineFeatureDescriptions.NEGATION_AS_FAILURE);
055: this .supported
056: .add(InferenceEngineFeatureDescriptions.DERIVATION_EVENT_LISTENERS);
057: }
058:
059: };
060: }
061: return featureDescriptions;
062: }
063:
064: /**
065: * Try to proof a goal.
066: * @return a derivation node
067: * @param goal - the goal that has to be proved
068: * @param constraintPool - a list of constraints
069: * @param counter - the proof step counter
070: * @param renameVariables a variable renaming
071: * @param logEnabled - indicates whether we must log this proof step
072: * @param results - the list collecting the results
073: * @param appliedClauses - a list of all clauses applied so far (used to detect loops)
074: * @param session the session object
075: * @throws InferenceException
076: */
077: private DerivationNodeImpl proof(Clause goal, List constraintPool,
078: DerivationStepCounter counter,
079: VariableRenaming renameVariables, boolean logEnabled,
080: List appliedClauses, List results, SessionImpl session)
081: throws InferenceException {
082:
083: int exceptionHandlingStrategy = session
084: .getExceptionHandlingStrategy();
085: int cardinalityConstraint = session.getCardinalityContraint();
086: org.mandarax.kernel.KnowledgeBase kb = session
087: .getKnowledgeBase();
088:
089: // make sure that the session is uptodate
090: session.update(renameVariables.getAllRenamings(),
091: constraintPool);
092:
093: // for performance reasons we want to minimize checks whether log is
094: // enabled. On the other hand, we would like to switch log on / off
095: // during a proof (e.g., to analyse a long proof). This implementation
096: // checks the respective log category every 10 steps
097: boolean logOn = (counter.count % 10 == 0) ? LOG_IE_STEP
098: .isDebugEnabled() : logEnabled;
099: DerivationNodeImpl node = new DerivationNodeImpl();
100: node.setId(counter.next());
101: // node.supportedSolution = results.size();
102: DerivationNodeImpl nextNode = null;
103:
104: if (logOn) {
105: LOG_IE_STEP.debug("PROOF STEP "
106: + String.valueOf(counter.count));
107: LOG_IE_STEP.debug("Goal : " + goal.toString());
108: }
109:
110: // try to remove clauses using the object semantics
111: goal = performSemanticalEvaluation(goal, session, logOn);
112:
113: if (goal == null) {
114: node.setFailed(true);
115: return node;
116: }
117:
118: // check for negation (NAF)
119: goal = proofNAFClauses(goal, kb, logOn,
120: exceptionHandlingStrategy, cardinalityConstraint);
121: if (goal == null) {
122: node.setFailed(true);
123: return node;
124: }
125:
126: if (logOn) {
127: LOG_IE_STEP.debug("Goal (semantic,NAF done): "
128: + goal.toString());
129: }
130:
131: // check whether the max proof length has been reached
132: if (counter.count >= MAXSTEPS) {
133: if (logOn) {
134: LOG_IE_STEP
135: .debug("Maximum number of steps reached, stop here !");
136: }
137: return node;
138: }
139:
140: // if the goal is the empty clause, return success
141: if (goal.isEmpty()) {
142: if (logOn) {
143: LOG_IE_STEP.debug("Derivation successful !");
144: }
145: results.add(node);
146: // new in 3.2: notify listener
147: notifyListenersOnResult(session, logOn);
148:
149: node.setResultNode(true);
150: node.setSupported(results.size() - 1);
151: node.setFailed(false);
152: // check whether we have enough results
153: if (cardinalityConstraint != ALL) {
154: node
155: .setLastNode((results.size() >= cardinalityConstraint));
156: }
157: return node;
158: }
159:
160: // check for the next clause to continue. Try resolution.
161: try {
162: ClauseIterator e = kb.clauses(goal, null);
163: boolean useClause = true;
164: while (e.hasMoreClauses()
165: && (cardinalityConstraint == ALL || results.size() < cardinalityConstraint)) {
166: useClause = true;
167: Resolution r = null;
168: Clause c = null;
169: Clause workCopy = null;
170: try {
171: c = e.nextClause();
172: workCopy = renameVariables.cloneAndRenameVars(c);
173: } catch (ClauseSetException x) {
174: String msg = "Exception fetching clause from iterator for "
175: + goal;
176: LOG_IE_STEP.error(msg, x);
177: // depending on the exception handling strategy we forward the exception or carry on
178: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
179: throw new InferenceException(msg, x);
180: useClause = false;
181: }
182: if (useClause
183: && (r = Resolution.resolve(workCopy, goal,
184: unificationAlgorithm, selectionPolicy,
185: session)) != null) {
186: appliedClauses.add(c);
187:
188: if (loopCheckingAlgorithm
189: .isInfiniteLoop(appliedClauses)) {
190: if (logOn) {
191: LOG_IE_STEP
192: .debug("LoopChecking Algorithm "
193: + loopCheckingAlgorithm
194: + " has detected a loop! Try to continue with next clause");
195: }
196: } else {
197: // log
198: if (logOn) {
199: LOG_IE_STEP
200: .debug("Can apply the following rule:");
201: LOG_IE_STEP.debug("Clause : "
202: + c.toString());
203: LOG_IE_STEP.debug("Clause (rn): "
204: + workCopy.toString());
205:
206: // log unification
207: Replacement nextReplacement = null;
208:
209: for (Iterator er = r.unification.replacements
210: .iterator(); er.hasNext();) {
211: nextReplacement = (Replacement) er
212: .next();
213: LOG_IE_STEP.debug("unify : "
214: + nextReplacement.original
215: .toString()
216: + " -> "
217: + nextReplacement.replacement
218: .toString());
219: }
220: }
221:
222: // build a new subgoal
223: Clause nextGoal = getNextGoal(workCopy, goal, r);
224:
225: // build a new constraint pool for the next step
226: List nextConstraintPool = getNextConstraintPool(
227: constraintPool, r);
228:
229: // apply constraints
230: nextGoal = nextGoal.apply(nextConstraintPool);
231:
232: // rename variables in the subgoal
233: nextGoal = renameVariables
234: .cloneAndRenameVars(nextGoal);
235:
236: // keep the renamed var here, otherwise they get overridden in the recursion
237: Hashtable renamed = renameVariables
238: .getRecentRenamings();
239:
240: // log renamings
241: if (logOn) {
242: Object nextRenaming = null;
243:
244: for (Enumeration er = renamed.keys(); er
245: .hasMoreElements();) {
246: nextRenaming = er.nextElement();
247: LOG_IE_STEP.debug("rename : "
248: + nextRenaming.toString()
249: + " -> "
250: + renamed.get(nextRenaming)
251: .toString());
252: }
253: }
254:
255: // proof the new subgoal
256: nextNode = proof(nextGoal, nextConstraintPool,
257: counter, renameVariables, logOn,
258: appliedClauses, results, session);
259:
260: nextNode.setQuery(goal);
261: nextNode.setAppliedClause(c);
262:
263: // register the subnode
264: node.addSubNode(nextNode);
265:
266: if (!nextNode.isFailed()) {
267: // add renamings and unification
268: nextNode.varRenamings = renamed;
269: nextNode.setUnification(r.unification);
270: }
271: }
272: } else {
273: if (logOn) {
274: LOG_IE_STEP
275: .debug("Cannot apply the following rule:");
276: LOG_IE_STEP.debug("Clause : "
277: + c.toString());
278: LOG_IE_STEP.debug("Clause (rn): "
279: + workCopy.toString());
280: }
281: }
282: }
283: // release resources!
284: e.close();
285: } catch (ClauseSetException x) {
286: String msg = "Exception getting clause iterator for "
287: + goal;
288: LOG_IE_STEP.error(msg, x);
289: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
290: throw new InferenceException(msg, x);
291: }
292: if ((nextNode == null) || nextNode.isFailed()) {
293: List l = node.getSubNodes();
294: int n = l.size();
295: boolean result = true;
296: for (int i = 0; i < n; i++) {
297: result = result
298: && ((DerivationNodeImpl) l.get(i)).isFailed();
299: node.setFailed(result);
300: }
301: // new in 1.9.2
302: node.setFailed(result);
303: }
304: return node;
305: }
306:
307: /**
308: * Try to proof prereqs. If the proof succeeds, remove them from the goal.
309: * If the proof fails, return null.
310: * @param goal a goal
311: * @param kb - the knowledge base used
312: * @param logOn - indicates whether we must log this proof step
313: * @param exceptionHandlingStrategy - an integer decoding the exception handling strategy when fetching and resolving
314: * ClauseSetExceptions
315: * @param cardinalityConstraint - the cardinality constraint specifying the number of results we are looking for
316: * @return the new goal
317: */
318: private Clause proofNAFClauses(Clause goal,
319: org.mandarax.kernel.KnowledgeBase kb, boolean logOn,
320: int exceptionHandlingStrategy, int cardinalityConstraint)
321: throws InferenceException {
322: Fact literal = null;
323: for (Iterator it = goal.getNegativeLiterals().iterator(); it
324: .hasNext();) {
325: literal = (Fact) it.next();
326: if (literal.isNegatedAF() && !IEUtils.containsVars(literal)) {
327: if (logOn)
328: LOG_IE.debug("Evaluate NAF " + literal);
329: // build new query
330: Query query = LogicFactory.getDefaultFactory()
331: .createQuery(
332: LogicFactory.getDefaultFactory()
333: .createFact(
334: literal.getPredicate(),
335: literal.getTerms()),
336: "Query to proof NAF in " + literal);
337: // issue query
338: boolean proved = false;
339: try {
340: ResultSet rs = this .query(query, kb,
341: cardinalityConstraint,
342: exceptionHandlingStrategy);
343: proved = !rs.next();
344: } catch (InferenceException x) {
345: LOG_IE_STEP.error("Error proofing NAF: " + literal,
346: x);
347: if (exceptionHandlingStrategy == BUBBLE_EXCEPTIONS)
348: throw x;
349: else {
350: // assume failure proofs NAF !
351: LOG_IE_STEP
352: .debug("Assume error means failure and verifies NAF "
353: + literal);
354: proved = true;
355: }
356: }
357: // remove if proved
358: if (proved) {
359: LOG_IE_STEP.debug("Remove from list " + literal);
360: it.remove();
361: } else {
362: LOG_IE_STEP.debug("Cannot prove " + literal
363: + " (unnegated fact is provable)");
364: return null;
365: }
366: }
367: }
368: return goal;
369: }
370:
371: /**
372: * Answer a query, retrieve (multiple different) result.
373: * The cardinality contraints describe how many results should be computed. It is either
374: * <ol>
375: * <li> <code>ONE</code> - indicating that only one answer is expected
376: * <li> <code>ALL</code> - indicating that all answers should be computed
377: * <li> <code>an integer value greater than 0 indicating that this number of results expected
378: * </ol>
379: * @see #ONE
380: * @see #ALL
381: * @return the result set of the query
382: * @param query the query clause
383: * @param kb the knowledge base used to answer the query
384: * @param aCardinalityConstraint the number of results expected
385: * @param exceptionHandlingPolicy one of the constants definied in this class (BUBBLE_EXCEPTIONS,TRY_NEXT)
386: * @throws an InferenceException
387: */
388: public ResultSet query(Query query,
389: org.mandarax.kernel.KnowledgeBase kb,
390: int aCardinalityConstraint, int exceptionHandlingPolicy)
391: throws InferenceException {
392: Clause firstGoal = getGoal(query);
393: VariableRenaming renameVariables = new VariableRenaming();
394: List resultNodes = new ArrayList();
395: SessionImpl session = new SessionImpl(kb, this , query,
396: exceptionHandlingPolicy, aCardinalityConstraint);
397: notifyListenersOnDerivationStart(session, LOG_IE_STEP
398: .isDebugEnabled());
399:
400: // proof
401: DerivationNodeImpl linResult = proof(firstGoal,
402: new ArrayList(), new DerivationStepCounter(),
403: renameVariables, LOG_IE_STEP.isDebugEnabled(),
404: new ArrayList(MAXSTEPS), resultNodes, session);
405:
406: for (int i = 0; i < resultNodes.size(); i++)
407: ((DerivationNodeImpl) resultNodes.get(i))
408: .propagateSupportedSolutions();
409: linResult
410: .setSemanticEvaluationPolicy(getSemanticEvaluationPolicy());
411: return new ResultSetImpl2(linResult, resultNodes, firstGoal);
412: }
413:
414: /**
415: * Build the next goal, i.e., remove the unified terms, join the remaining clauses,
416: * and apply the unifications.
417: * @return the next goal
418: * @param c1 the first unified clause
419: * @param c2 the second unified clause
420: * @param u a resolution
421: */
422: protected Clause getNextGoal(Clause c1, Clause c2, Resolution r) {
423: TmpClause nextClause = new TmpClause();
424: nextClause.positiveLiterals = merge(c2.getPositiveLiterals(),
425: c1.getPositiveLiterals(), r.position2);
426: nextClause.negativeLiterals = merge2(c1.getNegativeLiterals(),
427: c2.getNegativeLiterals(), r.position1);
428: return nextClause;
429: }
430:
431: /**
432: * Merge lists (of facts), skip the element at the index "skip" in the second list.
433: * This method moves negated facts to the right. This increases the chances that all
434: * terms are "ground".
435: * @return a new list
436: * @param v1 the first list
437: * @param v2 the second list
438: * @param skip the index to be skipped in the second list
439: */
440: private List merge2(List v1, List v2, int skip) {
441: List merged = new ArrayList(v1.size() + v2.size());
442: int posCounter = 0;
443: Fact f = null;
444: for (int i = 0; i < v1.size(); i++) {
445: f = (Fact) v1.get(i);
446: if (!f.isNegatedAF()) {
447: merged.add(posCounter, f);
448: posCounter = posCounter + 1;
449: } else
450: merged.add(v1.get(i));
451: }
452: for (int i = 0; i < v2.size(); i++) {
453: if (skip != i) {
454: merged.add(v2.get(i));
455: }
456: }
457: return merged;
458: }
459:
460: }
|