📄 derivationnodeimpl.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;
/**
* Derivation nodes represent application of a single rule.
* @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
* @version 3.4 <7 March 05>
* @since 1.0
* Prova re-integration modifications
* @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
* @version 3.4 <7 March 05>
*/
public class DerivationNodeImpl implements org.mandarax.kernel.DerivationNode, LogCategories {
private List subNodes = new java.util.Vector ();
private boolean failed = false;
private Unification unification = null;
private Clause appliedClause = null;
private Clause query = null;
private DerivationNodeImpl parent = null;
private SemanticEvaluationPolicy semanticEvaluationPolicy = null;
private static LogicFactory lfactory = LogicFactory.getDefaultFactory();
Map varRenamings = new HashMap();
private int id = 0;
private boolean isLastNode = false;
private boolean isResultNode = false;
private boolean isCut = false;
// 2.2
// Further corrections 28/04/03
private Object cutPredicate = null;
private BitSet supportedSolutions = null;
/** Cache the string representation for optimized debugging. */
private transient String cachedToString = null;
/**
* Constructor.
*/
public DerivationNodeImpl() {
super ();
}
/**
* Add a subnode.
* @param dn a child node
*/
public void addSubNode(DerivationNodeImpl dn) {
subNodes.add (dn);
dn.parent = this;
}
/**
* Get the applied clause.
* @return the applied clause
*/
public Clause getAppliedClause() {
return appliedClause;
}
/**
* Get the parent derivation node.
* @return the parent node
*/
public DerivationNodeImpl getParent() {
return parent;
}
/**
* Get the query.
* @return the query
*/
public Clause getQuery() {
return query;
}
/**
* Get the state of this node.
* @see org.mandarax.kernel.DerivationNodeImpl
* @return the state, the value is one of the constants defined in org.mandarax.kernel.DerivationNodeImpl
*/
public int getState() {
return isFailed()
? org.mandarax.kernel.DerivationNode.FAILED
: org.mandarax.kernel.DerivationNode.SUCCESS;
}
/**
* Indicates whether the result at the given index is supported by this node.
* @param int resultNumber - the number of the result in the result set indexing starts with 0
* @return boolean
*/
public boolean isSupported(int resultNumber) {
return supportedSolutions!=null && supportedSolutions.get(resultNumber);
}
/**
* Set the result number as supported.
* @param int resultNumber - the number of the result in the result set indexing starts with 0
*/
public void setSupported(int resultNumber) {
if (supportedSolutions==null) supportedSolutions= new BitSet();
supportedSolutions.set(resultNumber);
}
/**
* Get the sub nodes.
* @return a list containing the child nodes
*/
public List getSubNodes() {
return subNodes;
}
/**
* Get the unification.
* @return the unification applied
*/
public Unification getUnification() {
return unification;
}
/**
* Indicates whether this derivation step has failed.
* @return true if this proof step has failed, false otherwise
*/
public boolean isFailed() {
return failed;
}
/**
* Remove a subnode.
* @return boolean
* @param dn a child node
*/
public boolean removeSubNode(DerivationNodeImpl dn) {
dn.parent = null;
return subNodes.remove (dn);
}
/**
* Replace a term. Check unification and renamings - do not traverse children.
* Method has been changed in 1.9.2 to support complex terms!
* @return a term that is the result of applying the unification or a renaming to the original term
* @param original a term
*/
private Term replaceByUnificationOrRenaming(Term original) {
boolean debug = LOG_IE_RESULT.isDebugEnabled();
Term replacedHere = original;
if (debug) LOG_IE_RESULT.debug("Replace " + original + " in node " + this);
Replacement r = null;
// first check the unification
if(getUnification () != null) {
Collection uni = getUnification ().replacements;
for(Iterator it = uni.iterator (); it.hasNext (); ) {
r = (Replacement) it.next ();
replacedHere = replacedHere.apply(r);
if (debug) LOG_IE_RESULT.debug("Replaced by unification " + original + " -> " + replacedHere);
}
}
// apply renamings
if (replacedHere instanceof VariableTerm) {
// more effective for variable terms
Object rp = varRenamings.get (replacedHere);
if(rp != null) {
replacedHere = (Term) rp;
if (debug) LOG_IE_RESULT.debug("Replaced by var renaming " + original + " -> " + replacedHere);
}
}
else {
// general, in particular for complex terms
for (Iterator iter = varRenamings.keySet().iterator();iter.hasNext();) {
Term nextKey = (Term)iter.next();
r = new Replacement();
r.original = nextKey;
r.replacement = (Term)varRenamings.get(nextKey);
replacedHere = replacedHere.apply(r);
if (debug) LOG_IE_RESULT.debug("Replaced by var renaming " + original + " -> " + replacedHere);
}
}
// try to simplify terms - only necessary for complex terms
if (replacedHere instanceof ComplexTerm) {
// TODO pass session !
replacedHere = getSemanticEvaluationPolicy().evaluate((ComplexTerm)replacedHere,appliedClause,null,debug);
}
return replacedHere;
}
/**
* Replace a term.
* @return a term
* @param original a term
*/
Term replace(Term original) {
Term replacedHere = replaceByUnificationOrRenaming(original);
// the following code has been replace as from version 1.8 !!
// now we check whether there are more subnodes. In this case we must continue replacing !!
/*
if(getSubNodes ().isEmpty ()) return replacedHere;
else {
List sn = getSubNodes ();
DerivationNodeImpl nextNode = (DerivationNodeImpl) sn.get(sn.size () - 1);
return nextNode.replace (replacedHere);
}
*/
// new code: look for the first successful node
for (Iterator iter = getSubNodes().iterator();iter.hasNext();) {
DerivationNodeImpl nextNode = (DerivationNodeImpl)iter.next();
if (!nextNode.isFailed()) return nextNode.replace (replacedHere);
}
return replacedHere;
}
/**
* Replace a term and add any replacements found to the list,
* @return an array of lists, each containing a list of terms representing the
* solution for the variable at the respective position
* [Prova] Made public to be callable from ws.prova.reference.ProvaResultSetImpl2
* @param originals an array of terms
*/
public void replace(List[] replacements,Term[] originals) {
boolean logOn = LOG_IE_RESULT.isDebugEnabled();
Term[] replacedHere = new Term[originals.length];
for (int i=0;i<originals.length;i++) {
replacedHere[i] = replaceByUnificationOrRenaming(originals[i]);
}
if (logOn) {
LOG_IE_RESULT.debug("Replaced in derivation node " + this);
boolean somethingReplaced = false;
for (int i=0;i<originals.length;i++) {
if (originals[i]!=replacedHere[i]) {
LOG_IE_RESULT.debug(originals[i] + " -> " + replacedHere[i]);
somethingReplaced = true;
}
if (!somethingReplaced) LOG_IE_RESULT.debug("<nothing replaced>");
}
}
//boolean finalNode = true;
for (Iterator iter = getSubNodes().iterator();iter.hasNext();) {
DerivationNodeImpl nextNode = (DerivationNodeImpl)iter.next();
//finalNode = false;
if (!nextNode.isFailed()) nextNode.replace(replacements,replacedHere);
}
if (isResultNode) {
if (logOn) LOG_IE_RESULT.debug("Add solution in node " + this);
for (int i=0;i<originals.length;i++) {
replacements[i].add(replacedHere[i]);
}
}
}
/**
* Set the applied clause.
* @param c the applied clause
*/
public void setAppliedClause(Clause c) {
cachedToString = null;
appliedClause = c;
}
/**
* Set the failed flag.
* @param f true if this node has failed, false otherwise
*/
public void setFailed(boolean f) {
cachedToString = null;
failed = f;
}
/**
* Set the query.
* @param f a query
*/
public void setQuery(Clause f) {
query = f;
}
/**
* Set the subnodes.
* @param sn a list of subnodes
*/
public void setSubNodes(List sn) {
subNodes = sn;
for(Iterator it = sn.iterator (); it.hasNext (); ) {
((DerivationNodeImpl) it.next ()).parent = this;
}
}
/**
* Set the unification.
* @param u a unification
*/
public void setUnification(Unification u) {
unification = u;
}
/**
* Convert the derivation node to a string.
* @return the string representation of this object
*/
public String toString() {
if (cachedToString == null) {
StringBuffer buf = new StringBuffer();
buf.append("NODE ");
buf.append(id);
buf.append(" : CLAUSE: \"");
if(getAppliedClause () == null) {
buf.append("<NONE>");
}
else buf.append(getAppliedClause ().toString ());
buf.append("\" FAILED: ");
buf.append(isFailed ());
buf.append(" IS_LAST_NODE: ");
buf.append(this.isLastNode);
cachedToString = buf.toString();
}
return cachedToString;
}
/**
* Dump the derivation node and the subtree having this node as a root to the print writer.
* This method is for developer support only.
* @param out a print stream
*/
public void dump(java.io.PrintStream out) {
dump(out,0);
}
/**
* Dump the derivation node and the subtree having this node as a root to the print writer.
* This method is for developer support only.
* @param out a print stream
* @param childLevel the child level (visualized by an indent)
*/
private void dump(java.io.PrintStream out,int childLevel) {
startLine(out,childLevel);
out.println(this);
// recursion
List subNodes = getSubNodes();
for (Iterator iter = subNodes.iterator();iter.hasNext();) {
((DerivationNodeImpl)iter.next()).dump(out,childLevel+1);
}
}
/**
* Start a line. Support method for dump.
* out a print stream
* @param childLevel the child level
*/
private void startLine(java.io.PrintStream out,int childLevel) {
out.print(childLevel);
int maxIndent = 10;
int indent = 1+ Math.min(childLevel,maxIndent);
char indentChar = '.';
for (int i=0;i<indent;i++) out.print(indentChar);
}
/**
* Returns the semantic evaluation policy.
* @return the policy
*/
SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
return semanticEvaluationPolicy==null?this.parent.getSemanticEvaluationPolicy():semanticEvaluationPolicy;
}
/**
* Propagate supported solutions to the parent node.
* [Prova] Changed to public to allow out of package inference engines.
*/
public void propagateSupportedSolutions() {
if (supportedSolutions!=null && parent!=null) {
for (int i=0;i<supportedSolutions.length();i++) {
if (supportedSolutions.get(i)) {
parent.setSupported(i);
if (LOG_IE_STEP.isDebugEnabled()) LOG_IE_STEP.debug("propagate supported result index " + i + " in " + this);
}
}
parent.propagateSupportedSolutions();
}
}
/**
* Sets the semantic evaluation policy.
* [Prova] Changed to public to allow out of package inference engines.
* @param policy The semantic evaluation policy to set
*/
public void setSemanticEvaluationPolicy(SemanticEvaluationPolicy policy) {
this.semanticEvaluationPolicy = policy;
}
/**
* Get an array of integers containing the indexes of all solutions supported.
* @return an array of integer
*/
public int[] getSupportedResults() {
if (supportedSolutions==null) return new int[]{};
int[] resultIndexes = new int[supportedSolutions.length()];
int i,j=0;
for (i=0;i<supportedSolutions.length();i++) {
if (supportedSolutions.get(i)) {
resultIndexes[j]=i;
j=j+1;
}
}
int[] array = new int[j];
for (i=0;i<j;i++) array[i]=resultIndexes[i];
return array;
}
public boolean isCut() {
return isCut;
}
public void setCut(boolean cut) {
isCut = cut;
}
public int getId() {
return id;
}
public void setId(int id) {
this.id = id;
}
public Object getCutPredicate() {
return cutPredicate;
}
public void setCutPredicate(Object cutPredicate) {
this.cutPredicate = cutPredicate;
}
public boolean isLastNode() {
return isLastNode;
}
public void setLastNode(boolean lastNode) {
isLastNode = lastNode;
}
public boolean isResultNode() {
return isResultNode;
}
public void setResultNode(boolean resultNode) {
isResultNode = resultNode;
}
}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -