📄 proofanalyzer.java
字号:
/*
* 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
*/
package org.mandarax.util;
import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Vector;
import org.apache.commons.collections.Predicate;
import org.mandarax.kernel.Derivation;
import org.mandarax.kernel.DerivationNode;
/**
* This class implements some useful in order to analyze proofs.
* @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
* @version 3.4 <7 March 05>
* @since 1.2
*/
public class ProofAnalyzer {
/**
* Collect all applied clauses meeting a certain condition.
* @param node a derivation node
* @param condition a condition
* @param coll a collection of clauses
*/
private static void collectClauses(DerivationNode node, org.apache.commons.collections.Predicate condition,Collection coll) {
if(node == null) {
return;
}
if(condition.evaluate(node)) {
coll.add (node.getAppliedClause ());
}
List subNodes = node.getSubNodes ();
DerivationNode nextNode = null;
for(Iterator it = subNodes.iterator (); it.hasNext (); ) {
nextNode = (DerivationNode) it.next ();
collectClauses (nextNode, condition, coll);
}
}
/**
* Collect and return all clauses which have applied used in
* the given proof.
* @return a collection of clauses
* @param proof a derivation
*/
public static Collection getAppliedClauses(Derivation proof) {
org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
public boolean evaluate(Object obj) {
if (obj!=null && obj instanceof DerivationNode) {
DerivationNode node = (DerivationNode)obj;
return !node.isFailed();
}
return false;
}
};
return getClauses (proof.getRoot (), condition);
}
/**
* Collect and return all clauses which have been
* tried in the given proof.
* @return a collection of clauses
* @param proof a derivation
*/
public static Collection getUsedClauses(Derivation proof) {
org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
public boolean evaluate(Object obj) {
return true;
}
};
return getClauses (proof.getRoot (), condition);
}
/**
* Collect and return all clauses which have been
* used in the proof of the result with the given number.
* @return a collection of clauses
* @param proof a derivation
*/
public static Collection getAppliedClauses(Derivation proof,final int resultNumber) {
org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
public boolean evaluate(Object obj) {
if (obj!=null && obj instanceof DerivationNode) {
DerivationNode node = (DerivationNode)obj;
return node.isSupported(resultNumber);
}
return false;
}
};
return getClauses (proof.getRoot (), condition);
}
/**
* Collect and return all clauses which occur in a derivations
* and meet a certain condition.
* @return a collection of clauses
* @param node a derivation node
* @param condition a condition
*/
public static Collection getClauses(DerivationNode node, org.apache.commons.collections.Predicate condition) {
Collection coll = new Vector ();
collectClauses (node, condition, coll);
return coll;
}
}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -