org.semanticweb.HermiT.tableau
Class Tableau

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

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

This class coordinates the main tableau expansion for a given DLOntology (a normalized and clausified ontology). It represents the state of a run on a set of clauses and coordinates the extension of the ABox and also the retraction of facts when backtracking. Before starting the expansion, the given clauses are (for better performance) preprocessed via the HyperresolutionManager into a compiled and executable form.

See Also:
Serialized Form

Field Summary
protected  DLOntology m_additionalDLOntology
           
protected  HyperresolutionManager m_additionalHyperresolutionManager
           
protected  int m_allocatedNodes
           
protected  BranchingPoint[] m_branchingPoints
           
protected  boolean m_checkDatatypes
           
protected  boolean m_checkUnknownDatatypeRestrictions
           
protected  ClashManager m_clashManager
           
protected  int m_currentBranchingPoint
           
protected  DatatypeManager m_datatypeManager
           
protected  DependencySetFactory m_dependencySetFactory
           
protected  DescriptionGraphManager m_descriptionGraphManager
           
protected  java.util.List<java.util.List<ExistentialConcept>> m_existentialConceptsBuffers
           
protected  ExistentialExpansionStrategy m_existentialExpansionStrategy
           
protected  ExistentialExpansionManager m_existentialExpasionManager
           
protected  ExtensionManager m_extensionManager
           
protected  Node m_firstFreeNode
           
protected  GroundDisjunction m_firstGroundDisjunction
           
protected  Node m_firstTableauNode
           
protected  GroundDisjunction m_firstUnprocessedGroundDisjunction
           
protected  boolean m_hasDescriptionGraphs
           
protected  InterruptFlag m_interruptFlag
           
protected  boolean m_isCurrentModelDeterministic
           
protected  Node m_lastMergedOrPrunedNode
           
protected  Node m_lastTableauNode
           
protected  MergingManager m_mergingManager
           
protected  boolean m_needsNamedExtension
           
protected  boolean m_needsRDFSLiteralExtension
           
protected  boolean m_needsThingExtension
           
protected  NominalIntroductionManager m_nominalIntroductionManager
           
protected  int m_nonbacktrackableBranchingPoint
           
protected  int m_numberOfMergedOrPrunedNodes
           
protected  int m_numberOfNodeCreations
           
protected  int m_numberOfNodesInTableau
           
protected  java.util.Map<java.lang.String,java.lang.Object> m_parameters
           
protected  DLOntology m_permanentDLOntology
           
protected  HyperresolutionManager m_permanentHyperresolutionManager
           
protected  TableauMonitor m_tableauMonitor
           
protected  boolean m_useDisjunctionLearning
           
 
Constructor Summary
Tableau(InterruptFlag interruptFlag, TableauMonitor tableauMonitor, ExistentialExpansionStrategy existentialsExpansionStrategy, boolean useDisjunctionLearning, DLOntology permanentDLOntology, DLOntology additionalDLOntology, java.util.Map<java.lang.String,java.lang.Object> parameters)
           
 
Method Summary
 void addGroundDisjunction(GroundDisjunction groundDisjunction)
           
protected  void backtrackLastMergedOrPrunedNode()
           
protected  void backtrackTo(int newCurrentBrancingPoint)
          Backtrack to a certain branching point in the list of branching points that have been set during the run.
 void checkTableauList()
           
 void clear()
           
 void clearAdditionalDLOntology()
           
 Node createNewConcreteNode(DependencySet dependencySet, Node parent)
          Create a new concrete node for datatypes.
 Node createNewGraphNode(Node parent, DependencySet dependencySet)
          Create a new node graph node for description graphs
 Node createNewNamedNode(DependencySet dependencySet)
          Create a new node that represents an individual named in the input ontology (thus, keys have to be applied to it)
 Node createNewNINode(DependencySet dependencySet)
          Create a new node that represents a nominal, but one that is not named in the input ontology (thus, keys are not applicable)
protected  Node createNewNodeRaw(DependencySet dependencySet, Node parent, NodeType nodeType, int treeDepth)
           
 Node createNewRootConstantNode(DependencySet dependencySet)
          Create a new root constant node for datatypes.
 Node createNewTreeNode(DependencySet dependencySet, Node parent)
          Create a new tree node.
protected  void destroyLastTableauNode()
           
protected  boolean doIteration()
           
 DLOntology getAdditionalDLOntology()
           
 HyperresolutionManager getAdditionalHyperresolutionManager()
           
 BranchingPoint getCurrentBranchingPoint()
           
 int getCurrentBranchingPointLevel()
           
 DependencySetFactory getDependencySetFactory()
           
 DescriptionGraphManager getDescriptionGraphManager()
           
protected  java.util.List<ExistentialConcept> getExistentialConceptsBuffer()
           
 ExistentialExpansionManager getExistentialExpansionManager()
           
 ExistentialExpansionStrategy getExistentialsExpansionStrategy()
           
 ExtensionManager getExtensionManager()
           
 Node getFirstTableauNode()
           
 GroundDisjunction getFirstUnprocessedGroundDisjunction()
           
 InterruptFlag getInterruptFlag()
           
 Node getLastTableauNode()
           
 MergingManager getMergingManager()
           
 Node getNode(int nodeID)
           
protected  Node getNodeForTerm(java.util.Map<Term,Node> termsToNodes, Term term, DependencySet dependencySet)
           
 NominalIntroductionManager getNominalIntroductionManager()
           
 int getNumberOfAllocatedNodes()
           
 int getNumberOfMergedOrPrunedNodes()
           
 int getNumberOfNodeCreations()
           
 int getNumberOfNodesInTableau()
           
 java.util.Map<java.lang.String,java.lang.Object> getParameters()
           
 DLOntology getPermanentDLOntology()
           
 HyperresolutionManager getPermanentHyperresolutionManager()
           
 TableauMonitor getTableauMonitor()
           
 boolean isCurrentModelDeterministic()
           
 boolean isDeterministic()
           
 boolean isSatisfiable(boolean loadPermanentABox, boolean loadAdditionalABox, java.util.Set<Atom> perTestPositiveFactsNoDependency, java.util.Set<Atom> perTestNegativeFactsNoDependency, java.util.Set<Atom> perTestPositiveFactsDummyDependency, java.util.Set<Atom> perTestNegativeFactsDummyDependency, java.util.Map<Individual,Node> nodesForIndividuals, ReasoningTaskDescription reasoningTaskDescription)
           
 boolean isSatisfiable(boolean loadAdditionalABox, java.util.Set<Atom> perTestPositiveFactsNoDependency, java.util.Set<Atom> perTestNegativeFactsNoDependency, java.util.Set<Atom> perTestPositiveFactsDummyDependency, java.util.Set<Atom> perTestNegativeFactsDummyDependency, java.util.Map<Individual,Node> nodesForIndividuals, ReasoningTaskDescription reasoningTaskDescription)
           
protected  void loadNegativeFact(java.util.Map<Term,Node> termsToNodes, Atom atom, DependencySet dependencySet)
           
protected  void loadPositiveFact(java.util.Map<Term,Node> termsToNodes, Atom atom, DependencySet dependencySet)
           
 void mergeNode(Node node, Node mergeInto, DependencySet dependencySet)
          Merges node into mergeInto.
 void pruneNode(Node node)
           
 void pushBranchingPoint(BranchingPoint branchingPoint)
          Add a branching point in case we need to backtrack to this state.
 void putExistentialConceptsBuffer(java.util.List<ExistentialConcept> buffer)
           
protected  boolean runCalculus()
           
 void setAdditionalDLOntology(DLOntology additionalDLOntology)
           
 boolean supportsAdditionalDLOntology(DLOntology additionalDLOntology)
           
protected  void updateFlagsDependentOnAdditionalOntology()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

m_interruptFlag

protected final InterruptFlag m_interruptFlag

m_parameters

protected final java.util.Map<java.lang.String,java.lang.Object> m_parameters

m_tableauMonitor

protected final TableauMonitor m_tableauMonitor

m_existentialExpansionStrategy

protected final ExistentialExpansionStrategy m_existentialExpansionStrategy

m_permanentDLOntology

protected final DLOntology m_permanentDLOntology

m_additionalDLOntology

protected DLOntology m_additionalDLOntology

m_dependencySetFactory

protected final DependencySetFactory m_dependencySetFactory

m_extensionManager

protected final ExtensionManager m_extensionManager

m_clashManager

protected final ClashManager m_clashManager

m_permanentHyperresolutionManager

protected final HyperresolutionManager m_permanentHyperresolutionManager

m_additionalHyperresolutionManager

protected HyperresolutionManager m_additionalHyperresolutionManager

m_mergingManager

protected final MergingManager m_mergingManager

m_existentialExpasionManager

protected final ExistentialExpansionManager m_existentialExpasionManager

m_nominalIntroductionManager

protected final NominalIntroductionManager m_nominalIntroductionManager

m_descriptionGraphManager

protected final DescriptionGraphManager m_descriptionGraphManager

m_datatypeManager

protected final DatatypeManager m_datatypeManager

m_existentialConceptsBuffers

protected final java.util.List<java.util.List<ExistentialConcept>> m_existentialConceptsBuffers

m_useDisjunctionLearning

protected final boolean m_useDisjunctionLearning

m_hasDescriptionGraphs

protected final boolean m_hasDescriptionGraphs

m_branchingPoints

protected BranchingPoint[] m_branchingPoints

m_currentBranchingPoint

protected int m_currentBranchingPoint

m_nonbacktrackableBranchingPoint

protected int m_nonbacktrackableBranchingPoint

m_isCurrentModelDeterministic

protected boolean m_isCurrentModelDeterministic

m_needsThingExtension

protected boolean m_needsThingExtension

m_needsNamedExtension

protected boolean m_needsNamedExtension

m_needsRDFSLiteralExtension

protected boolean m_needsRDFSLiteralExtension

m_checkDatatypes

protected boolean m_checkDatatypes

m_checkUnknownDatatypeRestrictions

protected boolean m_checkUnknownDatatypeRestrictions

m_allocatedNodes

protected int m_allocatedNodes

m_numberOfNodesInTableau

protected int m_numberOfNodesInTableau

m_numberOfMergedOrPrunedNodes

protected int m_numberOfMergedOrPrunedNodes

m_numberOfNodeCreations

protected int m_numberOfNodeCreations

m_firstFreeNode

protected Node m_firstFreeNode

m_firstTableauNode

protected Node m_firstTableauNode

m_lastTableauNode

protected Node m_lastTableauNode

m_lastMergedOrPrunedNode

protected Node m_lastMergedOrPrunedNode

m_firstGroundDisjunction

protected GroundDisjunction m_firstGroundDisjunction

m_firstUnprocessedGroundDisjunction

protected GroundDisjunction m_firstUnprocessedGroundDisjunction
Constructor Detail

Tableau

public Tableau(InterruptFlag interruptFlag,
               TableauMonitor tableauMonitor,
               ExistentialExpansionStrategy existentialsExpansionStrategy,
               boolean useDisjunctionLearning,
               DLOntology permanentDLOntology,
               DLOntology additionalDLOntology,
               java.util.Map<java.lang.String,java.lang.Object> parameters)
Method Detail

getInterruptFlag

public InterruptFlag getInterruptFlag()

getPermanentDLOntology

public DLOntology getPermanentDLOntology()

getAdditionalDLOntology

public DLOntology getAdditionalDLOntology()

getParameters

public java.util.Map<java.lang.String,java.lang.Object> getParameters()

getTableauMonitor

public TableauMonitor getTableauMonitor()

getExistentialsExpansionStrategy

public ExistentialExpansionStrategy getExistentialsExpansionStrategy()

isDeterministic

public boolean isDeterministic()

getDependencySetFactory

public DependencySetFactory getDependencySetFactory()

getExtensionManager

public ExtensionManager getExtensionManager()

getPermanentHyperresolutionManager

public HyperresolutionManager getPermanentHyperresolutionManager()

getAdditionalHyperresolutionManager

public HyperresolutionManager getAdditionalHyperresolutionManager()

getMergingManager

public MergingManager getMergingManager()

getExistentialExpansionManager

public ExistentialExpansionManager getExistentialExpansionManager()

getNominalIntroductionManager

public NominalIntroductionManager getNominalIntroductionManager()

getDescriptionGraphManager

public DescriptionGraphManager getDescriptionGraphManager()

clear

public void clear()

supportsAdditionalDLOntology

public boolean supportsAdditionalDLOntology(DLOntology additionalDLOntology)

setAdditionalDLOntology

public void setAdditionalDLOntology(DLOntology additionalDLOntology)

clearAdditionalDLOntology

public void clearAdditionalDLOntology()

updateFlagsDependentOnAdditionalOntology

protected void updateFlagsDependentOnAdditionalOntology()

isSatisfiable

public boolean isSatisfiable(boolean loadAdditionalABox,
                             java.util.Set<Atom> perTestPositiveFactsNoDependency,
                             java.util.Set<Atom> perTestNegativeFactsNoDependency,
                             java.util.Set<Atom> perTestPositiveFactsDummyDependency,
                             java.util.Set<Atom> perTestNegativeFactsDummyDependency,
                             java.util.Map<Individual,Node> nodesForIndividuals,
                             ReasoningTaskDescription reasoningTaskDescription)

isSatisfiable

public boolean isSatisfiable(boolean loadPermanentABox,
                             boolean loadAdditionalABox,
                             java.util.Set<Atom> perTestPositiveFactsNoDependency,
                             java.util.Set<Atom> perTestNegativeFactsNoDependency,
                             java.util.Set<Atom> perTestPositiveFactsDummyDependency,
                             java.util.Set<Atom> perTestNegativeFactsDummyDependency,
                             java.util.Map<Individual,Node> nodesForIndividuals,
                             ReasoningTaskDescription reasoningTaskDescription)

loadPositiveFact

protected void loadPositiveFact(java.util.Map<Term,Node> termsToNodes,
                                Atom atom,
                                DependencySet dependencySet)

loadNegativeFact

protected void loadNegativeFact(java.util.Map<Term,Node> termsToNodes,
                                Atom atom,
                                DependencySet dependencySet)

getNodeForTerm

protected Node getNodeForTerm(java.util.Map<Term,Node> termsToNodes,
                              Term term,
                              DependencySet dependencySet)

runCalculus

protected boolean runCalculus()

doIteration

protected boolean doIteration()

isCurrentModelDeterministic

public boolean isCurrentModelDeterministic()

getCurrentBranchingPointLevel

public int getCurrentBranchingPointLevel()

getCurrentBranchingPoint

public BranchingPoint getCurrentBranchingPoint()

addGroundDisjunction

public void addGroundDisjunction(GroundDisjunction groundDisjunction)

getFirstUnprocessedGroundDisjunction

public GroundDisjunction getFirstUnprocessedGroundDisjunction()

pushBranchingPoint

public void pushBranchingPoint(BranchingPoint branchingPoint)
Add a branching point in case we need to backtrack to this state.

Parameters:
branchingPoint -

backtrackTo

protected void backtrackTo(int newCurrentBrancingPoint)
Backtrack to a certain branching point in the list of branching points that have been set during the run.

Parameters:
newCurrentBrancingPoint -

createNewNamedNode

public Node createNewNamedNode(DependencySet dependencySet)
Create a new node that represents an individual named in the input ontology (thus, keys have to be applied to it)

Parameters:
dependencySet - the dependency set for the node
Returns:
the created node

createNewNINode

public Node createNewNINode(DependencySet dependencySet)
Create a new node that represents a nominal, but one that is not named in the input ontology (thus, keys are not applicable)

Parameters:
dependencySet - the dependency set for the node
Returns:
the created node

createNewTreeNode

public Node createNewTreeNode(DependencySet dependencySet,
                              Node parent)
Create a new tree node.

Parameters:
dependencySet - the dependency set for the node
parent - the parent of the node that is to be created
Returns:
the created node

createNewConcreteNode

public Node createNewConcreteNode(DependencySet dependencySet,
                                  Node parent)
Create a new concrete node for datatypes.

Parameters:
dependencySet - the dependency set for the node
parent - the parent of the node that is to be created
Returns:
the created node

createNewRootConstantNode

public Node createNewRootConstantNode(DependencySet dependencySet)
Create a new root constant node for datatypes.

Parameters:
dependencySet - the dependency set for the node
Returns:
the created node

createNewGraphNode

public Node createNewGraphNode(Node parent,
                               DependencySet dependencySet)
Create a new node graph node for description graphs

Parameters:
parent - the parent of the node that is to be created (may be null)
dependencySet - the dependency set for the node
Returns:
the created node

createNewNodeRaw

protected Node createNewNodeRaw(DependencySet dependencySet,
                                Node parent,
                                NodeType nodeType,
                                int treeDepth)

mergeNode

public void mergeNode(Node node,
                      Node mergeInto,
                      DependencySet dependencySet)
Merges node into mergeInto. We assume that concepts and roles have already been copied from node to mergeInto. After the merge node has state NodeState.MERGED.

Parameters:
node - the node that is to be merged
mergeInto - the node we merge into
dependencySet -

pruneNode

public void pruneNode(Node node)

backtrackLastMergedOrPrunedNode

protected void backtrackLastMergedOrPrunedNode()

destroyLastTableauNode

protected void destroyLastTableauNode()

getNumberOfNodeCreations

public int getNumberOfNodeCreations()

getFirstTableauNode

public Node getFirstTableauNode()

getLastTableauNode

public Node getLastTableauNode()

getNumberOfAllocatedNodes

public int getNumberOfAllocatedNodes()

getNumberOfNodesInTableau

public int getNumberOfNodesInTableau()

getNumberOfMergedOrPrunedNodes

public int getNumberOfMergedOrPrunedNodes()

getNode

public Node getNode(int nodeID)

getExistentialConceptsBuffer

protected java.util.List<ExistentialConcept> getExistentialConceptsBuffer()

putExistentialConceptsBuffer

public void putExistentialConceptsBuffer(java.util.List<ExistentialConcept> buffer)

checkTableauList

public void checkTableauList()