001: /*
002: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
003: *
004: * This library is free software; you can redistribute it and/or
005: * modify it under the terms of the GNU Lesser General Public
006: * License as published by the Free Software Foundation; either
007: * version 2 of the License, or (at your option) any later version.
008: *
009: * This library is distributed in the hope that it will be useful,
010: * but WITHOUT ANY WARRANTY; without even the implied warranty of
011: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
012: * Lesser General Public License for more details.
013: *
014: * You should have received a copy of the GNU Lesser General Public
015: * License along with this library; if not, write to the Free Software
016: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
017: */
018: package org.mandarax.util;
019:
020: import java.util.Collection;
021: import java.util.Iterator;
022: import java.util.List;
023: import java.util.Vector;
024: import org.apache.commons.collections.Predicate;
025: import org.mandarax.kernel.Derivation;
026: import org.mandarax.kernel.DerivationNode;
027:
028: /**
029: * This class implements some useful in order to analyze proofs.
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.2
033: */
034: public class ProofAnalyzer {
035:
036: /**
037: * Collect all applied clauses meeting a certain condition.
038: * @param node a derivation node
039: * @param condition a condition
040: * @param coll a collection of clauses
041: */
042: private static void collectClauses(DerivationNode node,
043: org.apache.commons.collections.Predicate condition,
044: Collection coll) {
045: if (node == null) {
046: return;
047: }
048: if (condition.evaluate(node)) {
049: coll.add(node.getAppliedClause());
050: }
051: List subNodes = node.getSubNodes();
052: DerivationNode nextNode = null;
053: for (Iterator it = subNodes.iterator(); it.hasNext();) {
054: nextNode = (DerivationNode) it.next();
055: collectClauses(nextNode, condition, coll);
056: }
057: }
058:
059: /**
060: * Collect and return all clauses which have applied used in
061: * the given proof.
062: * @return a collection of clauses
063: * @param proof a derivation
064: */
065: public static Collection getAppliedClauses(Derivation proof) {
066: org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
067: public boolean evaluate(Object obj) {
068: if (obj != null && obj instanceof DerivationNode) {
069: DerivationNode node = (DerivationNode) obj;
070: return !node.isFailed();
071: }
072: return false;
073: }
074: };
075: return getClauses(proof.getRoot(), condition);
076: }
077:
078: /**
079: * Collect and return all clauses which have been
080: * tried in the given proof.
081: * @return a collection of clauses
082: * @param proof a derivation
083: */
084: public static Collection getUsedClauses(Derivation proof) {
085: org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
086: public boolean evaluate(Object obj) {
087: return true;
088: }
089: };
090: return getClauses(proof.getRoot(), condition);
091: }
092:
093: /**
094: * Collect and return all clauses which have been
095: * used in the proof of the result with the given number.
096: * @return a collection of clauses
097: * @param proof a derivation
098: */
099: public static Collection getAppliedClauses(Derivation proof,
100: final int resultNumber) {
101: org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
102: public boolean evaluate(Object obj) {
103: if (obj != null && obj instanceof DerivationNode) {
104: DerivationNode node = (DerivationNode) obj;
105: return node.isSupported(resultNumber);
106: }
107: return false;
108: }
109: };
110: return getClauses(proof.getRoot(), condition);
111: }
112:
113: /**
114: * Collect and return all clauses which occur in a derivations
115: * and meet a certain condition.
116: * @return a collection of clauses
117: * @param node a derivation node
118: * @param condition a condition
119: */
120: public static Collection getClauses(DerivationNode node,
121: org.apache.commons.collections.Predicate condition) {
122: Collection coll = new Vector();
123: collectClauses(node, condition, coll);
124: return coll;
125: }
126: }
|