org.semanticweb.HermiT.tableau
Class ExistentialExpansionManager

java.lang.Object
  extended by org.semanticweb.HermiT.tableau.ExistentialExpansionManager
All Implemented Interfaces:
java.io.Serializable

public final class ExistentialExpansionManager
extends java.lang.Object
implements java.io.Serializable

Manages the expansion of at least restrictions in a tableau.

See Also:
Serialized Form

Field Summary
protected  java.util.List<Node> m_auxiliaryNodes
           
protected  java.lang.Object[] m_auxiliaryTuple
           
protected  UnionDependencySet m_binaryUnionDependencySet
           
protected  TupleTable m_expandedExistentials
           
protected  ExtensionManager m_extensionManager
           
protected  java.util.Map<Role,Role[]> m_functionalRoles
           
protected  int[] m_indicesByBranchingPoint
           
protected  Tableau m_tableau
           
protected  ExtensionTable.Retrieval m_ternaryExtensionTableSearch01Bound
           
protected  ExtensionTable.Retrieval m_ternaryExtensionTableSearch02Bound
           
 
Constructor Summary
ExistentialExpansionManager(Tableau tableau)
           
 
Method Summary
 void backtrack()
           
 void branchingPointPushed()
           
 void clear()
           
 void doNormalExpansion(AtLeastConcept atLeastConcept, Node forNode)
           
 void doNormalExpansion(AtLeastDataRange atLeastDataRange, Node forNode)
           
 void expand(AtLeast atLeast, Node forNode)
           
protected  boolean getFunctionalExpansionNode(Role role, Node forNode, java.lang.Object[] result)
           
protected  void loadDLClausesIntoGraph(java.util.Set<DLClause> dlClauses, Graph<Role> superRoleGraph, java.util.Set<Role> functionalRoles)
           
 void markExistentialProcessed(ExistentialConcept existentialConcept, Node forNode)
           
 boolean tryFunctionalExpansion(AtLeast atLeast, Node forNode)
          Creates a new node in the tableau if the at least concept that caused the expansion is for cardinality 1.
protected  void updateFunctionalRoles()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

m_tableau

protected final Tableau m_tableau

m_extensionManager

protected final ExtensionManager m_extensionManager

m_expandedExistentials

protected final TupleTable m_expandedExistentials

m_auxiliaryTuple

protected final java.lang.Object[] m_auxiliaryTuple

m_auxiliaryNodes

protected final java.util.List<Node> m_auxiliaryNodes

m_ternaryExtensionTableSearch01Bound

protected final ExtensionTable.Retrieval m_ternaryExtensionTableSearch01Bound

m_ternaryExtensionTableSearch02Bound

protected final ExtensionTable.Retrieval m_ternaryExtensionTableSearch02Bound

m_functionalRoles

protected final java.util.Map<Role,Role[]> m_functionalRoles

m_binaryUnionDependencySet

protected final UnionDependencySet m_binaryUnionDependencySet

m_indicesByBranchingPoint

protected int[] m_indicesByBranchingPoint
Constructor Detail

ExistentialExpansionManager

public ExistentialExpansionManager(Tableau tableau)
Method Detail

updateFunctionalRoles

protected void updateFunctionalRoles()

loadDLClausesIntoGraph

protected void loadDLClausesIntoGraph(java.util.Set<DLClause> dlClauses,
                                      Graph<Role> superRoleGraph,
                                      java.util.Set<Role> functionalRoles)

markExistentialProcessed

public void markExistentialProcessed(ExistentialConcept existentialConcept,
                                     Node forNode)

branchingPointPushed

public void branchingPointPushed()

backtrack

public void backtrack()

clear

public void clear()

tryFunctionalExpansion

public boolean tryFunctionalExpansion(AtLeast atLeast,
                                      Node forNode)
Creates a new node in the tableau if the at least concept that caused the expansion is for cardinality 1. If it is not of cardinality 1 and the role in the at least concept is a functional role, it sets a clash in the extension manager.

Returns:
true if the at least cardinality is 1 (causes an expansion) or it is greater than one but the role is functional (causes a clash) and false otherwise.

getFunctionalExpansionNode

protected boolean getFunctionalExpansionNode(Role role,
                                             Node forNode,
                                             java.lang.Object[] result)

doNormalExpansion

public void doNormalExpansion(AtLeastConcept atLeastConcept,
                              Node forNode)

doNormalExpansion

public void doNormalExpansion(AtLeastDataRange atLeastDataRange,
                              Node forNode)

expand

public void expand(AtLeast atLeast,
                   Node forNode)